Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
For an actual table an inverse exists exactly when N=0 or F(1) is signed +1 or -1. At a positive window this is the unit-at-one criterion; the empty window imposes no condition at one. Every inverse has actual delta and two-sided convolution witnesses. Its zeroth value is arbitrary, so uniqueness is positive-value equality, not equality of codes or of zeroth values. Multiplicative-function closure and full finite signed G009 are admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ F. ArithTable(N,F) → ((∃ x. DirichletInverse(N,F,x)) → N = 0 ∨ DirichletUnitAtOne(F)) ∧ (N = 0 ∨ DirichletUnitAtOne(F) → ∃ x. DirichletInverse(N,F,x))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N F. (exists dst_positive_code_criterion_input dst_positive_scale_criterion_input dst_negative_code_criterion_input dst_negative_scale_criterion_input. (((F) = (((((dst_positive_code_criterion_input) + (dst_positive_scale_criterion_input)) * S ((dst_positive_code_criterion_input) + (dst_positive_scale_criterion_input)) + ((dst_positive_scale_criterion_input) + (dst_positive_scale_criterion_input))) + (((dst_negative_code_criterion_input) + (dst_negative_scale_criterion_input)) * S ((dst_negative_code_criterion_input) + (dst_negative_scale_criterion_input)) + ((dst_negative_scale_criterion_input) + (dst_negative_scale_criterion_input)))) * S ((((dst_positive_code_criterion_input) + (dst_positive_scale_criterion_input)) * S ((dst_positive_code_criterion_input) + (dst_positive_scale_criterion_input)) + ((dst_positive_scale_criterion_input) + (dst_positive_scale_criterion_input))) + (((dst_negative_code_criterion_input) + (dst_negative_scale_criterion_input)) * S ((dst_negative_code_criterion_input) + (dst_negative_scale_criterion_input)) + ((dst_negative_scale_criterion_input) + (dst_negative_scale_criterion_input)))) + ((((dst_negative_code_criterion_input) + (dst_negative_scale_criterion_input)) * S ((dst_negative_code_criterion_input) + (dst_negative_scale_criterion_input)) + ((dst_negative_scale_criterion_input) + (dst_negative_scale_criterion_input))) + (((dst_negative_code_criterion_input) + (dst_negative_scale_criterion_input)) * S ((dst_negative_code_criterion_input) + (dst_negative_scale_criterion_input)) + ((dst_negative_scale_criterion_input) + (dst_negative_scale_criterion_input)))))) /\ (forall dst_index_criterion_input. (exists pvs_le_gap_criterion_inputdomain. pvs_le_gap_criterion_inputdomain + (dst_index_criterion_input) = (N)) -> exists dst_positive_criterion_input dst_negative_criterion_input dst_value_criterion_input. ((((exists ff_h_pvs_criterion_inputentrypositive. ff_h_pvs_criterion_inputentrypositive + S (dst_positive_criterion_input) = S ((S (dst_index_criterion_input)) * dst_positive_scale_criterion_input)) /\ exists ff_q_pvs_criterion_inputentrypositive. dst_positive_code_criterion_input = ff_q_pvs_criterion_inputentrypositive * S ((S (dst_index_criterion_input)) * dst_positive_scale_criterion_input) + (dst_positive_criterion_input))) /\ (((((exists ff_h_pvs_criterion_inputentrynegative. ff_h_pvs_criterion_inputentrynegative + S (dst_negative_criterion_input) = S ((S (dst_index_criterion_input)) * dst_negative_scale_criterion_input)) /\ exists ff_q_pvs_criterion_inputentrynegative. dst_negative_code_criterion_input = ff_q_pvs_criterion_inputentrynegative * S ((S (dst_index_criterion_input)) * dst_negative_scale_criterion_input) + (dst_negative_criterion_input))) /\ (exists ge_balance_positive_criterion_inputentryvalue ge_balance_negative_criterion_inputentryvalue. (((((dst_value_criterion_input) = 2 * (ge_balance_positive_criterion_inputentryvalue) /\ (ge_balance_negative_criterion_inputentryvalue) = 0) \/ exists ge_signed_half_criterion_inputentryvaluedecode. (((dst_value_criterion_input) = 2 * ge_signed_half_criterion_inputentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inputentryvalue) = 0) /\ (ge_balance_negative_criterion_inputentryvalue) = S ge_signed_half_criterion_inputentryvaluedecode))) /\ ((dst_positive_criterion_input) + ge_balance_negative_criterion_inputentryvalue = (dst_negative_criterion_input) + ge_balance_positive_criterion_inputentryvalue))))))))) -> (((exists G. (exists di_delta_criterion_inverse. ((((exists dst_positive_code_criterion_inversedeltatable dst_positive_scale_criterion_inversedeltatable dst_negative_code_criterion_inversedeltatable dst_negative_scale_criterion_inversedeltatable. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable)) * S ((dst_positive_code_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable)) + ((dst_positive_scale_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable))) + (((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) * S ((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) + ((dst_negative_scale_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)))) * S ((((dst_positive_code_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable)) * S ((dst_positive_code_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable)) + ((dst_positive_scale_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable))) + (((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) * S ((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) + ((dst_negative_scale_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)))) + ((((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) * S ((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) + ((dst_negative_scale_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable))) + (((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) * S ((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) + ((dst_negative_scale_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)))))) /\ (forall dst_index_criterion_inversedeltatable. (exists pvs_le_gap_criterion_inversedeltatabledomain. pvs_le_gap_criterion_inversedeltatabledomain + (dst_index_criterion_inversedeltatable) = (N)) -> exists dst_positive_criterion_inversedeltatable dst_negative_criterion_inversedeltatable dst_value_criterion_inversedeltatable. ((((exists ff_h_pvs_criterion_inversedeltatableentrypositive. ff_h_pvs_criterion_inversedeltatableentrypositive + S (dst_positive_criterion_inversedeltatable) = S ((S (dst_index_criterion_inversedeltatable)) * dst_positive_scale_criterion_inversedeltatable)) /\ exists ff_q_pvs_criterion_inversedeltatableentrypositive. dst_positive_code_criterion_inversedeltatable = ff_q_pvs_criterion_inversedeltatableentrypositive * S ((S (dst_index_criterion_inversedeltatable)) * dst_positive_scale_criterion_inversedeltatable) + (dst_positive_criterion_inversedeltatable))) /\ (((((exists ff_h_pvs_criterion_inversedeltatableentrynegative. ff_h_pvs_criterion_inversedeltatableentrynegative + S (dst_negative_criterion_inversedeltatable) = S ((S (dst_index_criterion_inversedeltatable)) * dst_negative_scale_criterion_inversedeltatable)) /\ exists ff_q_pvs_criterion_inversedeltatableentrynegative. dst_negative_code_criterion_inversedeltatable = ff_q_pvs_criterion_inversedeltatableentrynegative * S ((S (dst_index_criterion_inversedeltatable)) * dst_negative_scale_criterion_inversedeltatable) + (dst_negative_criterion_inversedeltatable))) /\ (exists ge_balance_positive_criterion_inversedeltatableentryvalue ge_balance_negative_criterion_inversedeltatableentryvalue. (((((dst_value_criterion_inversedeltatable) = 2 * (ge_balance_positive_criterion_inversedeltatableentryvalue) /\ (ge_balance_negative_criterion_inversedeltatableentryvalue) = 0) \/ exists ge_signed_half_criterion_inversedeltatableentryvaluedecode. (((dst_value_criterion_inversedeltatable) = 2 * ge_signed_half_criterion_inversedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inversedeltatableentryvalue) = 0) /\ (ge_balance_negative_criterion_inversedeltatableentryvalue) = S ge_signed_half_criterion_inversedeltatableentryvaluedecode))) /\ ((dst_positive_criterion_inversedeltatable) + ge_balance_negative_criterion_inversedeltatableentryvalue = (dst_negative_criterion_inversedeltatable) + ge_balance_positive_criterion_inversedeltatableentryvalue))))))))) /\ (forall du_index_criterion_inversedelta du_value_criterion_inversedelta. ~(du_index_criterion_inversedelta=0) -> (exists pvs_le_gap_criterion_inversedeltabound. pvs_le_gap_criterion_inversedeltabound + (du_index_criterion_inversedelta) = (N)) -> (exists dst_positive_code_criterion_inversedeltaentry dst_positive_scale_criterion_inversedeltaentry dst_negative_code_criterion_inversedeltaentry dst_negative_scale_criterion_inversedeltaentry dst_positive_criterion_inversedeltaentry dst_negative_criterion_inversedeltaentry. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry)) * S ((dst_positive_code_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry)) + ((dst_positive_scale_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry))) + (((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) * S ((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) + ((dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)))) * S ((((dst_positive_code_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry)) * S ((dst_positive_code_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry)) + ((dst_positive_scale_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry))) + (((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) * S ((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) + ((dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)))) + ((((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) * S ((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) + ((dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry))) + (((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) * S ((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) + ((dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)))))) /\ (((((exists ff_h_pvs_criterion_inversedeltaentrypositive. ff_h_pvs_criterion_inversedeltaentrypositive + S (dst_positive_criterion_inversedeltaentry) = S ((S (du_index_criterion_inversedelta)) * dst_positive_scale_criterion_inversedeltaentry)) /\ exists ff_q_pvs_criterion_inversedeltaentrypositive. dst_positive_code_criterion_inversedeltaentry = ff_q_pvs_criterion_inversedeltaentrypositive * S ((S (du_index_criterion_inversedelta)) * dst_positive_scale_criterion_inversedeltaentry) + (dst_positive_criterion_inversedeltaentry))) /\ (((((exists ff_h_pvs_criterion_inversedeltaentrynegative. ff_h_pvs_criterion_inversedeltaentrynegative + S (dst_negative_criterion_inversedeltaentry) = S ((S (du_index_criterion_inversedelta)) * dst_negative_scale_criterion_inversedeltaentry)) /\ exists ff_q_pvs_criterion_inversedeltaentrynegative. dst_negative_code_criterion_inversedeltaentry = ff_q_pvs_criterion_inversedeltaentrynegative * S ((S (du_index_criterion_inversedelta)) * dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_criterion_inversedeltaentry))) /\ (exists ge_balance_positive_criterion_inversedeltaentryvalue ge_balance_negative_criterion_inversedeltaentryvalue. (((((du_value_criterion_inversedelta) = 2 * (ge_balance_positive_criterion_inversedeltaentryvalue) /\ (ge_balance_negative_criterion_inversedeltaentryvalue) = 0) \/ exists ge_signed_half_criterion_inversedeltaentryvaluedecode. (((du_value_criterion_inversedelta) = 2 * ge_signed_half_criterion_inversedeltaentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inversedeltaentryvalue) = 0) /\ (ge_balance_negative_criterion_inversedeltaentryvalue) = S ge_signed_half_criterion_inversedeltaentryvaluedecode))) /\ ((dst_positive_criterion_inversedeltaentry) + ge_balance_negative_criterion_inversedeltaentryvalue = (dst_negative_criterion_inversedeltaentry) + ge_balance_positive_criterion_inversedeltaentryvalue))))))))) -> ((((du_index_criterion_inversedelta)=1 -> (du_value_criterion_inversedelta)=2) /\ (~((du_index_criterion_inversedelta)=1) -> (du_value_criterion_inversedelta)=0)))))) /\ (((((exists dst_positive_code_criterion_inverseleftleft dst_positive_scale_criterion_inverseleftleft dst_negative_code_criterion_inverseleftleft dst_negative_scale_criterion_inverseleftleft. (((F) = (((((dst_positive_code_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft)) * S ((dst_positive_code_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft)) + ((dst_positive_scale_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft))) + (((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) * S ((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) + ((dst_negative_scale_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)))) * S ((((dst_positive_code_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft)) * S ((dst_positive_code_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft)) + ((dst_positive_scale_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft))) + (((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) * S ((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) + ((dst_negative_scale_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)))) + ((((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) * S ((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) + ((dst_negative_scale_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft))) + (((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) * S ((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) + ((dst_negative_scale_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)))))) /\ (forall dst_index_criterion_inverseleftleft. (exists pvs_le_gap_criterion_inverseleftleftdomain. pvs_le_gap_criterion_inverseleftleftdomain + (dst_index_criterion_inverseleftleft) = (N)) -> exists dst_positive_criterion_inverseleftleft dst_negative_criterion_inverseleftleft dst_value_criterion_inverseleftleft. ((((exists ff_h_pvs_criterion_inverseleftleftentrypositive. ff_h_pvs_criterion_inverseleftleftentrypositive + S (dst_positive_criterion_inverseleftleft) = S ((S (dst_index_criterion_inverseleftleft)) * dst_positive_scale_criterion_inverseleftleft)) /\ exists ff_q_pvs_criterion_inverseleftleftentrypositive. dst_positive_code_criterion_inverseleftleft = ff_q_pvs_criterion_inverseleftleftentrypositive * S ((S (dst_index_criterion_inverseleftleft)) * dst_positive_scale_criterion_inverseleftleft) + (dst_positive_criterion_inverseleftleft))) /\ (((((exists ff_h_pvs_criterion_inverseleftleftentrynegative. ff_h_pvs_criterion_inverseleftleftentrynegative + S (dst_negative_criterion_inverseleftleft) = S ((S (dst_index_criterion_inverseleftleft)) * dst_negative_scale_criterion_inverseleftleft)) /\ exists ff_q_pvs_criterion_inverseleftleftentrynegative. dst_negative_code_criterion_inverseleftleft = ff_q_pvs_criterion_inverseleftleftentrynegative * S ((S (dst_index_criterion_inverseleftleft)) * dst_negative_scale_criterion_inverseleftleft) + (dst_negative_criterion_inverseleftleft))) /\ (exists ge_balance_positive_criterion_inverseleftleftentryvalue ge_balance_negative_criterion_inverseleftleftentryvalue. (((((dst_value_criterion_inverseleftleft) = 2 * (ge_balance_positive_criterion_inverseleftleftentryvalue) /\ (ge_balance_negative_criterion_inverseleftleftentryvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftleftentryvaluedecode. (((dst_value_criterion_inverseleftleft) = 2 * ge_signed_half_criterion_inverseleftleftentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftleftentryvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftleftentryvalue) = S ge_signed_half_criterion_inverseleftleftentryvaluedecode))) /\ ((dst_positive_criterion_inverseleftleft) + ge_balance_negative_criterion_inverseleftleftentryvalue = (dst_negative_criterion_inverseleftleft) + ge_balance_positive_criterion_inverseleftleftentryvalue))))))))) /\ (((exists dst_positive_code_criterion_inverseleftright dst_positive_scale_criterion_inverseleftright dst_negative_code_criterion_inverseleftright dst_negative_scale_criterion_inverseleftright. (((G) = (((((dst_positive_code_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright)) * S ((dst_positive_code_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright)) + ((dst_positive_scale_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright))) + (((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) * S ((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) + ((dst_negative_scale_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)))) * S ((((dst_positive_code_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright)) * S ((dst_positive_code_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright)) + ((dst_positive_scale_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright))) + (((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) * S ((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) + ((dst_negative_scale_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)))) + ((((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) * S ((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) + ((dst_negative_scale_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright))) + (((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) * S ((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) + ((dst_negative_scale_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)))))) /\ (forall dst_index_criterion_inverseleftright. (exists pvs_le_gap_criterion_inverseleftrightdomain. pvs_le_gap_criterion_inverseleftrightdomain + (dst_index_criterion_inverseleftright) = (N)) -> exists dst_positive_criterion_inverseleftright dst_negative_criterion_inverseleftright dst_value_criterion_inverseleftright. ((((exists ff_h_pvs_criterion_inverseleftrightentrypositive. ff_h_pvs_criterion_inverseleftrightentrypositive + S (dst_positive_criterion_inverseleftright) = S ((S (dst_index_criterion_inverseleftright)) * dst_positive_scale_criterion_inverseleftright)) /\ exists ff_q_pvs_criterion_inverseleftrightentrypositive. dst_positive_code_criterion_inverseleftright = ff_q_pvs_criterion_inverseleftrightentrypositive * S ((S (dst_index_criterion_inverseleftright)) * dst_positive_scale_criterion_inverseleftright) + (dst_positive_criterion_inverseleftright))) /\ (((((exists ff_h_pvs_criterion_inverseleftrightentrynegative. ff_h_pvs_criterion_inverseleftrightentrynegative + S (dst_negative_criterion_inverseleftright) = S ((S (dst_index_criterion_inverseleftright)) * dst_negative_scale_criterion_inverseleftright)) /\ exists ff_q_pvs_criterion_inverseleftrightentrynegative. dst_negative_code_criterion_inverseleftright = ff_q_pvs_criterion_inverseleftrightentrynegative * S ((S (dst_index_criterion_inverseleftright)) * dst_negative_scale_criterion_inverseleftright) + (dst_negative_criterion_inverseleftright))) /\ (exists ge_balance_positive_criterion_inverseleftrightentryvalue ge_balance_negative_criterion_inverseleftrightentryvalue. (((((dst_value_criterion_inverseleftright) = 2 * (ge_balance_positive_criterion_inverseleftrightentryvalue) /\ (ge_balance_negative_criterion_inverseleftrightentryvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftrightentryvaluedecode. (((dst_value_criterion_inverseleftright) = 2 * ge_signed_half_criterion_inverseleftrightentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftrightentryvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftrightentryvalue) = S ge_signed_half_criterion_inverseleftrightentryvaluedecode))) /\ ((dst_positive_criterion_inverseleftright) + ge_balance_negative_criterion_inverseleftrightentryvalue = (dst_negative_criterion_inverseleftright) + ge_balance_positive_criterion_inverseleftrightentryvalue))))))))) /\ (((exists dst_positive_code_criterion_inverselefttable dst_positive_scale_criterion_inverselefttable dst_negative_code_criterion_inverselefttable dst_negative_scale_criterion_inverselefttable. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable)) * S ((dst_positive_code_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable)) + ((dst_positive_scale_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable))) + (((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) * S ((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) + ((dst_negative_scale_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)))) * S ((((dst_positive_code_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable)) * S ((dst_positive_code_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable)) + ((dst_positive_scale_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable))) + (((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) * S ((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) + ((dst_negative_scale_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)))) + ((((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) * S ((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) + ((dst_negative_scale_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable))) + (((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) * S ((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) + ((dst_negative_scale_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)))))) /\ (forall dst_index_criterion_inverselefttable. (exists pvs_le_gap_criterion_inverselefttabledomain. pvs_le_gap_criterion_inverselefttabledomain + (dst_index_criterion_inverselefttable) = (N)) -> exists dst_positive_criterion_inverselefttable dst_negative_criterion_inverselefttable dst_value_criterion_inverselefttable. ((((exists ff_h_pvs_criterion_inverselefttableentrypositive. ff_h_pvs_criterion_inverselefttableentrypositive + S (dst_positive_criterion_inverselefttable) = S ((S (dst_index_criterion_inverselefttable)) * dst_positive_scale_criterion_inverselefttable)) /\ exists ff_q_pvs_criterion_inverselefttableentrypositive. dst_positive_code_criterion_inverselefttable = ff_q_pvs_criterion_inverselefttableentrypositive * S ((S (dst_index_criterion_inverselefttable)) * dst_positive_scale_criterion_inverselefttable) + (dst_positive_criterion_inverselefttable))) /\ (((((exists ff_h_pvs_criterion_inverselefttableentrynegative. ff_h_pvs_criterion_inverselefttableentrynegative + S (dst_negative_criterion_inverselefttable) = S ((S (dst_index_criterion_inverselefttable)) * dst_negative_scale_criterion_inverselefttable)) /\ exists ff_q_pvs_criterion_inverselefttableentrynegative. dst_negative_code_criterion_inverselefttable = ff_q_pvs_criterion_inverselefttableentrynegative * S ((S (dst_index_criterion_inverselefttable)) * dst_negative_scale_criterion_inverselefttable) + (dst_negative_criterion_inverselefttable))) /\ (exists ge_balance_positive_criterion_inverselefttableentryvalue ge_balance_negative_criterion_inverselefttableentryvalue. (((((dst_value_criterion_inverselefttable) = 2 * (ge_balance_positive_criterion_inverselefttableentryvalue) /\ (ge_balance_negative_criterion_inverselefttableentryvalue) = 0) \/ exists ge_signed_half_criterion_inverselefttableentryvaluedecode. (((dst_value_criterion_inverselefttable) = 2 * ge_signed_half_criterion_inverselefttableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverselefttableentryvalue) = 0) /\ (ge_balance_negative_criterion_inverselefttableentryvalue) = S ge_signed_half_criterion_inverselefttableentryvaluedecode))) /\ ((dst_positive_criterion_inverselefttable) + ge_balance_negative_criterion_inverselefttableentryvalue = (dst_negative_criterion_inverselefttable) + ge_balance_positive_criterion_inverselefttableentryvalue))))))))) /\ (forall dc_input_criterion_inverseleft dc_output_criterion_inverseleft. ~(dc_input_criterion_inverseleft=0) -> (exists pvs_le_gap_criterion_inverseleftdomain. pvs_le_gap_criterion_inverseleftdomain + (dc_input_criterion_inverseleft) = (N)) -> (exists dst_positive_code_criterion_inverseleftlookup dst_positive_scale_criterion_inverseleftlookup dst_negative_code_criterion_inverseleftlookup dst_negative_scale_criterion_inverseleftlookup dst_positive_criterion_inverseleftlookup dst_negative_criterion_inverseleftlookup. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup)) * S ((dst_positive_code_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup)) + ((dst_positive_scale_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup))) + (((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) * S ((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) + ((dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)))) * S ((((dst_positive_code_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup)) * S ((dst_positive_code_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup)) + ((dst_positive_scale_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup))) + (((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) * S ((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) + ((dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)))) + ((((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) * S ((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) + ((dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup))) + (((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) * S ((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) + ((dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)))))) /\ (((((exists ff_h_pvs_criterion_inverseleftlookuppositive. ff_h_pvs_criterion_inverseleftlookuppositive + S (dst_positive_criterion_inverseleftlookup) = S ((S (dc_input_criterion_inverseleft)) * dst_positive_scale_criterion_inverseleftlookup)) /\ exists ff_q_pvs_criterion_inverseleftlookuppositive. dst_positive_code_criterion_inverseleftlookup = ff_q_pvs_criterion_inverseleftlookuppositive * S ((S (dc_input_criterion_inverseleft)) * dst_positive_scale_criterion_inverseleftlookup) + (dst_positive_criterion_inverseleftlookup))) /\ (((((exists ff_h_pvs_criterion_inverseleftlookupnegative. ff_h_pvs_criterion_inverseleftlookupnegative + S (dst_negative_criterion_inverseleftlookup) = S ((S (dc_input_criterion_inverseleft)) * dst_negative_scale_criterion_inverseleftlookup)) /\ exists ff_q_pvs_criterion_inverseleftlookupnegative. dst_negative_code_criterion_inverseleftlookup = ff_q_pvs_criterion_inverseleftlookupnegative * S ((S (dc_input_criterion_inverseleft)) * dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_criterion_inverseleftlookup))) /\ (exists ge_balance_positive_criterion_inverseleftlookupvalue ge_balance_negative_criterion_inverseleftlookupvalue. (((((dc_output_criterion_inverseleft) = 2 * (ge_balance_positive_criterion_inverseleftlookupvalue) /\ (ge_balance_negative_criterion_inverseleftlookupvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftlookupvaluedecode. (((dc_output_criterion_inverseleft) = 2 * ge_signed_half_criterion_inverseleftlookupvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftlookupvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftlookupvalue) = S ge_signed_half_criterion_inverseleftlookupvaluedecode))) /\ ((dst_positive_criterion_inverseleftlookup) + ge_balance_negative_criterion_inverseleftlookupvalue = (dst_negative_criterion_inverseleftlookup) + ge_balance_positive_criterion_inverseleftlookupvalue))))))))) -> (((~((dc_input_criterion_inverseleft)=0)) /\ (exists dc_mask_criterion_inverseleftvalue. ((((exists dst_positive_code_criterion_inverseleftvaluemasktable dst_positive_scale_criterion_inverseleftvaluemasktable dst_negative_code_criterion_inverseleftvaluemasktable dst_negative_scale_criterion_inverseleftvaluemasktable. (((dc_mask_criterion_inverseleftvalue) = (((((dst_positive_code_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)))) * S ((((dst_positive_code_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)))) + ((((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)))))) /\ (forall dst_index_criterion_inverseleftvaluemasktable. (exists pvs_le_gap_criterion_inverseleftvaluemasktabledomain. pvs_le_gap_criterion_inverseleftvaluemasktabledomain + (dst_index_criterion_inverseleftvaluemasktable) = (dc_input_criterion_inverseleft)) -> exists dst_positive_criterion_inverseleftvaluemasktable dst_negative_criterion_inverseleftvaluemasktable dst_value_criterion_inverseleftvaluemasktable. ((((exists ff_h_pvs_criterion_inverseleftvaluemasktableentrypositive. ff_h_pvs_criterion_inverseleftvaluemasktableentrypositive + S (dst_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_criterion_inverseleftvaluemasktable)) * dst_positive_scale_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_criterion_inverseleftvaluemasktableentrypositive. dst_positive_code_criterion_inverseleftvaluemasktable = ff_q_pvs_criterion_inverseleftvaluemasktableentrypositive * S ((S (dst_index_criterion_inverseleftvaluemasktable)) * dst_positive_scale_criterion_inverseleftvaluemasktable) + (dst_positive_criterion_inverseleftvaluemasktable))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemasktableentrynegative. ff_h_pvs_criterion_inverseleftvaluemasktableentrynegative + S (dst_negative_criterion_inverseleftvaluemasktable) = S ((S (dst_index_criterion_inverseleftvaluemasktable)) * dst_negative_scale_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_criterion_inverseleftvaluemasktableentrynegative. dst_negative_code_criterion_inverseleftvaluemasktable = ff_q_pvs_criterion_inverseleftvaluemasktableentrynegative * S ((S (dst_index_criterion_inverseleftvaluemasktable)) * dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_criterion_inverseleftvaluemasktable))) /\ (exists ge_balance_positive_criterion_inverseleftvaluemasktableentryvalue ge_balance_negative_criterion_inverseleftvaluemasktableentryvalue. (((((dst_value_criterion_inverseleftvaluemasktable) = 2 * (ge_balance_positive_criterion_inverseleftvaluemasktableentryvalue) /\ (ge_balance_negative_criterion_inverseleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemasktableentryvaluedecode. (((dst_value_criterion_inverseleftvaluemasktable) = 2 * ge_signed_half_criterion_inverseleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluemasktableentryvalue) = S ge_signed_half_criterion_inverseleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_criterion_inverseleftvaluemasktable) + ge_balance_negative_criterion_inverseleftvaluemasktableentryvalue = (dst_negative_criterion_inverseleftvaluemasktable) + ge_balance_positive_criterion_inverseleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_criterion_inverseleftvaluemask dc_value_criterion_inverseleftvaluemask. (exists pvs_le_gap_criterion_inverseleftvaluemaskdomain. pvs_le_gap_criterion_inverseleftvaluemaskdomain + (dc_index_criterion_inverseleftvaluemask) = (dc_input_criterion_inverseleft)) -> (exists dst_positive_code_criterion_inverseleftvaluemasklookup dst_positive_scale_criterion_inverseleftvaluemasklookup dst_negative_code_criterion_inverseleftvaluemasklookup dst_negative_scale_criterion_inverseleftvaluemasklookup dst_positive_criterion_inverseleftvaluemasklookup dst_negative_criterion_inverseleftvaluemasklookup. (((dc_mask_criterion_inverseleftvalue) = (((((dst_positive_code_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)))) * S ((((dst_positive_code_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)))) + ((((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemasklookuppositive. ff_h_pvs_criterion_inverseleftvaluemasklookuppositive + S (dst_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_positive_scale_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_criterion_inverseleftvaluemasklookuppositive. dst_positive_code_criterion_inverseleftvaluemasklookup = ff_q_pvs_criterion_inverseleftvaluemasklookuppositive * S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_positive_scale_criterion_inverseleftvaluemasklookup) + (dst_positive_criterion_inverseleftvaluemasklookup))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemasklookupnegative. ff_h_pvs_criterion_inverseleftvaluemasklookupnegative + S (dst_negative_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_negative_scale_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_criterion_inverseleftvaluemasklookupnegative. dst_negative_code_criterion_inverseleftvaluemasklookup = ff_q_pvs_criterion_inverseleftvaluemasklookupnegative * S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_criterion_inverseleftvaluemasklookup))) /\ (exists ge_balance_positive_criterion_inverseleftvaluemasklookupvalue ge_balance_negative_criterion_inverseleftvaluemasklookupvalue. (((((dc_value_criterion_inverseleftvaluemask) = 2 * (ge_balance_positive_criterion_inverseleftvaluemasklookupvalue) /\ (ge_balance_negative_criterion_inverseleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemasklookupvaluedecode. (((dc_value_criterion_inverseleftvaluemask) = 2 * ge_signed_half_criterion_inverseleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluemasklookupvalue) = S ge_signed_half_criterion_inverseleftvaluemasklookupvaluedecode))) /\ ((dst_positive_criterion_inverseleftvaluemasklookup) + ge_balance_negative_criterion_inverseleftvaluemasklookupvalue = (dst_negative_criterion_inverseleftvaluemasklookup) + ge_balance_positive_criterion_inverseleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_criterion_inverseleftvaluemask)=0)) /\ (exists dc_quotient_criterion_inverseleftvaluemaskentry dc_left_criterion_inverseleftvaluemaskentry dc_right_criterion_inverseleftvaluemaskentry. (((dc_input_criterion_inverseleft)=(dc_index_criterion_inverseleftvaluemask)*dc_quotient_criterion_inverseleftvaluemaskentry) /\ (((exists dst_positive_code_criterion_inverseleftvaluemaskentryleft dst_positive_scale_criterion_inverseleftvaluemaskentryleft dst_negative_code_criterion_inverseleftvaluemaskentryleft dst_negative_scale_criterion_inverseleftvaluemaskentryleft dst_positive_criterion_inverseleftvaluemaskentryleft dst_negative_criterion_inverseleftvaluemaskentryleft. (((F) = (((((dst_positive_code_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)))) * S ((((dst_positive_code_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)))) + ((((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemaskentryleftpositive. ff_h_pvs_criterion_inverseleftvaluemaskentryleftpositive + S (dst_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_criterion_inverseleftvaluemaskentryleftpositive. dst_positive_code_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_criterion_inverseleftvaluemaskentryleftpositive * S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_positive_scale_criterion_inverseleftvaluemaskentryleft) + (dst_positive_criterion_inverseleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemaskentryleftnegative. ff_h_pvs_criterion_inverseleftvaluemaskentryleftnegative + S (dst_negative_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_criterion_inverseleftvaluemaskentryleftnegative. dst_negative_code_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_criterion_inverseleftvaluemaskentryleftnegative * S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_criterion_inverseleftvaluemaskentryleft))) /\ (exists ge_balance_positive_criterion_inverseleftvaluemaskentryleftvalue ge_balance_negative_criterion_inverseleftvaluemaskentryleftvalue. (((((dc_left_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_criterion_inverseleftvaluemaskentryleftvalue) /\ (ge_balance_negative_criterion_inverseleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryleftvaluedecode. (((dc_left_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluemaskentryleftvalue) = S ge_signed_half_criterion_inverseleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_negative_criterion_inverseleftvaluemaskentryleftvalue = (dst_negative_criterion_inverseleftvaluemaskentryleft) + ge_balance_positive_criterion_inverseleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_criterion_inverseleftvaluemaskentryright dst_positive_scale_criterion_inverseleftvaluemaskentryright dst_negative_code_criterion_inverseleftvaluemaskentryright dst_negative_scale_criterion_inverseleftvaluemaskentryright dst_positive_criterion_inverseleftvaluemaskentryright dst_negative_criterion_inverseleftvaluemaskentryright. (((G) = (((((dst_positive_code_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)))) * S ((((dst_positive_code_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)))) + ((((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemaskentryrightpositive. ff_h_pvs_criterion_inverseleftvaluemaskentryrightpositive + S (dst_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_criterion_inverseleftvaluemaskentryrightpositive. dst_positive_code_criterion_inverseleftvaluemaskentryright = ff_q_pvs_criterion_inverseleftvaluemaskentryrightpositive * S ((S (dc_quotient_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_criterion_inverseleftvaluemaskentryright) + (dst_positive_criterion_inverseleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemaskentryrightnegative. ff_h_pvs_criterion_inverseleftvaluemaskentryrightnegative + S (dst_negative_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_criterion_inverseleftvaluemaskentryrightnegative. dst_negative_code_criterion_inverseleftvaluemaskentryright = ff_q_pvs_criterion_inverseleftvaluemaskentryrightnegative * S ((S (dc_quotient_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_criterion_inverseleftvaluemaskentryright))) /\ (exists ge_balance_positive_criterion_inverseleftvaluemaskentryrightvalue ge_balance_negative_criterion_inverseleftvaluemaskentryrightvalue. (((((dc_right_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_criterion_inverseleftvaluemaskentryrightvalue) /\ (ge_balance_negative_criterion_inverseleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryrightvaluedecode. (((dc_right_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluemaskentryrightvalue) = S ge_signed_half_criterion_inverseleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_negative_criterion_inverseleftvaluemaskentryrightvalue = (dst_negative_criterion_inverseleftvaluemaskentryright) + ge_balance_positive_criterion_inverseleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_criterion_inverseleftvaluemaskentryproduct sto_an_criterion_inverseleftvaluemaskentryproduct sto_bp_criterion_inverseleftvaluemaskentryproduct sto_bn_criterion_inverseleftvaluemaskentryproduct sto_cp_criterion_inverseleftvaluemaskentryproduct sto_cn_criterion_inverseleftvaluemaskentryproduct. (((((dc_left_criterion_inverseleftvaluemaskentry) = 2 * (sto_ap_criterion_inverseleftvaluemaskentryproduct) /\ (sto_an_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryproductleft. (((dc_left_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryproductleft + 1 /\ (sto_ap_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_an_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_criterion_inverseleftvaluemaskentryproductleft))) /\ ((((((dc_right_criterion_inverseleftvaluemaskentry) = 2 * (sto_bp_criterion_inverseleftvaluemaskentryproduct) /\ (sto_bn_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryproductright. (((dc_right_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryproductright + 1 /\ (sto_bp_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_bn_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_criterion_inverseleftvaluemaskentryproductright))) /\ ((((((dc_value_criterion_inverseleftvaluemask) = 2 * (sto_cp_criterion_inverseleftvaluemaskentryproduct) /\ (sto_cn_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryproductoutput. (((dc_value_criterion_inverseleftvaluemask) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryproductoutput + 1 /\ (sto_cp_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_cn_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_criterion_inverseleftvaluemaskentryproductoutput))) /\ ((sto_ap_criterion_inverseleftvaluemaskentryproduct * sto_bp_criterion_inverseleftvaluemaskentryproduct + sto_an_criterion_inverseleftvaluemaskentryproduct * sto_bn_criterion_inverseleftvaluemaskentryproduct) + sto_cn_criterion_inverseleftvaluemaskentryproduct = (sto_ap_criterion_inverseleftvaluemaskentryproduct * sto_bn_criterion_inverseleftvaluemaskentryproduct + sto_an_criterion_inverseleftvaluemaskentryproduct * sto_bp_criterion_inverseleftvaluemaskentryproduct) + sto_cp_criterion_inverseleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_criterion_inverseleftvaluemask)=0 \/ ~(exists pvs_factor_criterion_inverseleftvaluemaskentrynondivisor. (dc_input_criterion_inverseleft) = (dc_index_criterion_inverseleftvaluemask) * pvs_factor_criterion_inverseleftvaluemaskentrynondivisor)) /\ ((dc_value_criterion_inverseleftvaluemask)=0))))))) /\ (exists dst_positive_code_criterion_inverseleftvaluefold dst_positive_scale_criterion_inverseleftvaluefold dst_negative_code_criterion_inverseleftvaluefold dst_negative_scale_criterion_inverseleftvaluefold dst_positive_sum_criterion_inverseleftvaluefold dst_negative_sum_criterion_inverseleftvaluefold. (((dc_mask_criterion_inverseleftvalue) = (((((dst_positive_code_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold)) * S ((dst_positive_code_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold)) + ((dst_positive_scale_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold))) + (((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) * S ((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) + ((dst_negative_scale_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)))) * S ((((dst_positive_code_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold)) * S ((dst_positive_code_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold)) + ((dst_positive_scale_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold))) + (((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) * S ((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) + ((dst_negative_scale_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)))) + ((((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) * S ((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) + ((dst_negative_scale_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold))) + (((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) * S ((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) + ((dst_negative_scale_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)))))) /\ (((exists fs_u_dst_criterion_inverseleftvaluefoldpositive fs_v_dst_criterion_inverseleftvaluefoldpositive. ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_start. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_start. fs_u_dst_criterion_inverseleftvaluefoldpositive = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_criterion_inverseleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_terminal. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_terminal + S (dst_positive_sum_criterion_inverseleftvaluefold) = S ((S (S (dc_input_criterion_inverseleft))) * fs_v_dst_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_terminal. fs_u_dst_criterion_inverseleftvaluefoldpositive = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_criterion_inverseleft))) * fs_v_dst_criterion_inverseleftvaluefoldpositive) + (dst_positive_sum_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps. (exists fs_lt_dst_criterion_inverseleftvaluefoldpositive_body_steps_bound. fs_lt_dst_criterion_inverseleftvaluefoldpositive_body_steps_bound + S fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps = S (dc_input_criterion_inverseleft)) -> exists fs_a_dst_criterion_inverseleftvaluefoldpositive_body_steps fs_r_dst_criterion_inverseleftvaluefoldpositive_body_steps fs_s_dst_criterion_inverseleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_summand. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_summand. dst_positive_code_criterion_inverseleftvaluefold = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_criterion_inverseleftvaluefold) + (fs_a_dst_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_u_dst_criterion_inverseleftvaluefoldpositive = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldpositive) + (fs_r_dst_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_u_dst_criterion_inverseleftvaluefoldpositive = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldpositive) + (fs_s_dst_criterion_inverseleftvaluefoldpositive_body_steps))) /\ fs_s_dst_criterion_inverseleftvaluefoldpositive_body_steps = fs_r_dst_criterion_inverseleftvaluefoldpositive_body_steps + fs_a_dst_criterion_inverseleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_criterion_inverseleftvaluefoldnegative fs_v_dst_criterion_inverseleftvaluefoldnegative. ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_start. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_start. fs_u_dst_criterion_inverseleftvaluefoldnegative = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_criterion_inverseleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_terminal. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_terminal + S (dst_negative_sum_criterion_inverseleftvaluefold) = S ((S (S (dc_input_criterion_inverseleft))) * fs_v_dst_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_terminal. fs_u_dst_criterion_inverseleftvaluefoldnegative = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_criterion_inverseleft))) * fs_v_dst_criterion_inverseleftvaluefoldnegative) + (dst_negative_sum_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps. (exists fs_lt_dst_criterion_inverseleftvaluefoldnegative_body_steps_bound. fs_lt_dst_criterion_inverseleftvaluefoldnegative_body_steps_bound + S fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps = S (dc_input_criterion_inverseleft)) -> exists fs_a_dst_criterion_inverseleftvaluefoldnegative_body_steps fs_r_dst_criterion_inverseleftvaluefoldnegative_body_steps fs_s_dst_criterion_inverseleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_summand. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_summand. dst_negative_code_criterion_inverseleftvaluefold = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_criterion_inverseleftvaluefold) + (fs_a_dst_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_u_dst_criterion_inverseleftvaluefoldnegative = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldnegative) + (fs_r_dst_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_u_dst_criterion_inverseleftvaluefoldnegative = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldnegative) + (fs_s_dst_criterion_inverseleftvaluefoldnegative_body_steps))) /\ fs_s_dst_criterion_inverseleftvaluefoldnegative_body_steps = fs_r_dst_criterion_inverseleftvaluefoldnegative_body_steps + fs_a_dst_criterion_inverseleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_criterion_inverseleftvaluefoldresult ge_balance_negative_criterion_inverseleftvaluefoldresult. (((((dc_output_criterion_inverseleft) = 2 * (ge_balance_positive_criterion_inverseleftvaluefoldresult) /\ (ge_balance_negative_criterion_inverseleftvaluefoldresult) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluefoldresultdecode. (((dc_output_criterion_inverseleft) = 2 * ge_signed_half_criterion_inverseleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluefoldresult) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluefoldresult) = S ge_signed_half_criterion_inverseleftvaluefoldresultdecode))) /\ ((dst_positive_sum_criterion_inverseleftvaluefold) + ge_balance_negative_criterion_inverseleftvaluefoldresult = (dst_negative_sum_criterion_inverseleftvaluefold) + ge_balance_positive_criterion_inverseleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_criterion_inverserightleft dst_positive_scale_criterion_inverserightleft dst_negative_code_criterion_inverserightleft dst_negative_scale_criterion_inverserightleft. (((G) = (((((dst_positive_code_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft)) * S ((dst_positive_code_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft)) + ((dst_positive_scale_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft))) + (((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) * S ((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) + ((dst_negative_scale_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)))) * S ((((dst_positive_code_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft)) * S ((dst_positive_code_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft)) + ((dst_positive_scale_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft))) + (((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) * S ((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) + ((dst_negative_scale_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)))) + ((((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) * S ((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) + ((dst_negative_scale_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft))) + (((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) * S ((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) + ((dst_negative_scale_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)))))) /\ (forall dst_index_criterion_inverserightleft. (exists pvs_le_gap_criterion_inverserightleftdomain. pvs_le_gap_criterion_inverserightleftdomain + (dst_index_criterion_inverserightleft) = (N)) -> exists dst_positive_criterion_inverserightleft dst_negative_criterion_inverserightleft dst_value_criterion_inverserightleft. ((((exists ff_h_pvs_criterion_inverserightleftentrypositive. ff_h_pvs_criterion_inverserightleftentrypositive + S (dst_positive_criterion_inverserightleft) = S ((S (dst_index_criterion_inverserightleft)) * dst_positive_scale_criterion_inverserightleft)) /\ exists ff_q_pvs_criterion_inverserightleftentrypositive. dst_positive_code_criterion_inverserightleft = ff_q_pvs_criterion_inverserightleftentrypositive * S ((S (dst_index_criterion_inverserightleft)) * dst_positive_scale_criterion_inverserightleft) + (dst_positive_criterion_inverserightleft))) /\ (((((exists ff_h_pvs_criterion_inverserightleftentrynegative. ff_h_pvs_criterion_inverserightleftentrynegative + S (dst_negative_criterion_inverserightleft) = S ((S (dst_index_criterion_inverserightleft)) * dst_negative_scale_criterion_inverserightleft)) /\ exists ff_q_pvs_criterion_inverserightleftentrynegative. dst_negative_code_criterion_inverserightleft = ff_q_pvs_criterion_inverserightleftentrynegative * S ((S (dst_index_criterion_inverserightleft)) * dst_negative_scale_criterion_inverserightleft) + (dst_negative_criterion_inverserightleft))) /\ (exists ge_balance_positive_criterion_inverserightleftentryvalue ge_balance_negative_criterion_inverserightleftentryvalue. (((((dst_value_criterion_inverserightleft) = 2 * (ge_balance_positive_criterion_inverserightleftentryvalue) /\ (ge_balance_negative_criterion_inverserightleftentryvalue) = 0) \/ exists ge_signed_half_criterion_inverserightleftentryvaluedecode. (((dst_value_criterion_inverserightleft) = 2 * ge_signed_half_criterion_inverserightleftentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightleftentryvalue) = 0) /\ (ge_balance_negative_criterion_inverserightleftentryvalue) = S ge_signed_half_criterion_inverserightleftentryvaluedecode))) /\ ((dst_positive_criterion_inverserightleft) + ge_balance_negative_criterion_inverserightleftentryvalue = (dst_negative_criterion_inverserightleft) + ge_balance_positive_criterion_inverserightleftentryvalue))))))))) /\ (((exists dst_positive_code_criterion_inverserightright dst_positive_scale_criterion_inverserightright dst_negative_code_criterion_inverserightright dst_negative_scale_criterion_inverserightright. (((F) = (((((dst_positive_code_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright)) * S ((dst_positive_code_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright)) + ((dst_positive_scale_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright))) + (((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) * S ((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) + ((dst_negative_scale_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)))) * S ((((dst_positive_code_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright)) * S ((dst_positive_code_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright)) + ((dst_positive_scale_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright))) + (((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) * S ((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) + ((dst_negative_scale_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)))) + ((((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) * S ((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) + ((dst_negative_scale_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright))) + (((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) * S ((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) + ((dst_negative_scale_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)))))) /\ (forall dst_index_criterion_inverserightright. (exists pvs_le_gap_criterion_inverserightrightdomain. pvs_le_gap_criterion_inverserightrightdomain + (dst_index_criterion_inverserightright) = (N)) -> exists dst_positive_criterion_inverserightright dst_negative_criterion_inverserightright dst_value_criterion_inverserightright. ((((exists ff_h_pvs_criterion_inverserightrightentrypositive. ff_h_pvs_criterion_inverserightrightentrypositive + S (dst_positive_criterion_inverserightright) = S ((S (dst_index_criterion_inverserightright)) * dst_positive_scale_criterion_inverserightright)) /\ exists ff_q_pvs_criterion_inverserightrightentrypositive. dst_positive_code_criterion_inverserightright = ff_q_pvs_criterion_inverserightrightentrypositive * S ((S (dst_index_criterion_inverserightright)) * dst_positive_scale_criterion_inverserightright) + (dst_positive_criterion_inverserightright))) /\ (((((exists ff_h_pvs_criterion_inverserightrightentrynegative. ff_h_pvs_criterion_inverserightrightentrynegative + S (dst_negative_criterion_inverserightright) = S ((S (dst_index_criterion_inverserightright)) * dst_negative_scale_criterion_inverserightright)) /\ exists ff_q_pvs_criterion_inverserightrightentrynegative. dst_negative_code_criterion_inverserightright = ff_q_pvs_criterion_inverserightrightentrynegative * S ((S (dst_index_criterion_inverserightright)) * dst_negative_scale_criterion_inverserightright) + (dst_negative_criterion_inverserightright))) /\ (exists ge_balance_positive_criterion_inverserightrightentryvalue ge_balance_negative_criterion_inverserightrightentryvalue. (((((dst_value_criterion_inverserightright) = 2 * (ge_balance_positive_criterion_inverserightrightentryvalue) /\ (ge_balance_negative_criterion_inverserightrightentryvalue) = 0) \/ exists ge_signed_half_criterion_inverserightrightentryvaluedecode. (((dst_value_criterion_inverserightright) = 2 * ge_signed_half_criterion_inverserightrightentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightrightentryvalue) = 0) /\ (ge_balance_negative_criterion_inverserightrightentryvalue) = S ge_signed_half_criterion_inverserightrightentryvaluedecode))) /\ ((dst_positive_criterion_inverserightright) + ge_balance_negative_criterion_inverserightrightentryvalue = (dst_negative_criterion_inverserightright) + ge_balance_positive_criterion_inverserightrightentryvalue))))))))) /\ (((exists dst_positive_code_criterion_inverserighttable dst_positive_scale_criterion_inverserighttable dst_negative_code_criterion_inverserighttable dst_negative_scale_criterion_inverserighttable. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable)) * S ((dst_positive_code_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable)) + ((dst_positive_scale_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable))) + (((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) * S ((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) + ((dst_negative_scale_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)))) * S ((((dst_positive_code_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable)) * S ((dst_positive_code_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable)) + ((dst_positive_scale_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable))) + (((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) * S ((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) + ((dst_negative_scale_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)))) + ((((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) * S ((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) + ((dst_negative_scale_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable))) + (((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) * S ((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) + ((dst_negative_scale_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)))))) /\ (forall dst_index_criterion_inverserighttable. (exists pvs_le_gap_criterion_inverserighttabledomain. pvs_le_gap_criterion_inverserighttabledomain + (dst_index_criterion_inverserighttable) = (N)) -> exists dst_positive_criterion_inverserighttable dst_negative_criterion_inverserighttable dst_value_criterion_inverserighttable. ((((exists ff_h_pvs_criterion_inverserighttableentrypositive. ff_h_pvs_criterion_inverserighttableentrypositive + S (dst_positive_criterion_inverserighttable) = S ((S (dst_index_criterion_inverserighttable)) * dst_positive_scale_criterion_inverserighttable)) /\ exists ff_q_pvs_criterion_inverserighttableentrypositive. dst_positive_code_criterion_inverserighttable = ff_q_pvs_criterion_inverserighttableentrypositive * S ((S (dst_index_criterion_inverserighttable)) * dst_positive_scale_criterion_inverserighttable) + (dst_positive_criterion_inverserighttable))) /\ (((((exists ff_h_pvs_criterion_inverserighttableentrynegative. ff_h_pvs_criterion_inverserighttableentrynegative + S (dst_negative_criterion_inverserighttable) = S ((S (dst_index_criterion_inverserighttable)) * dst_negative_scale_criterion_inverserighttable)) /\ exists ff_q_pvs_criterion_inverserighttableentrynegative. dst_negative_code_criterion_inverserighttable = ff_q_pvs_criterion_inverserighttableentrynegative * S ((S (dst_index_criterion_inverserighttable)) * dst_negative_scale_criterion_inverserighttable) + (dst_negative_criterion_inverserighttable))) /\ (exists ge_balance_positive_criterion_inverserighttableentryvalue ge_balance_negative_criterion_inverserighttableentryvalue. (((((dst_value_criterion_inverserighttable) = 2 * (ge_balance_positive_criterion_inverserighttableentryvalue) /\ (ge_balance_negative_criterion_inverserighttableentryvalue) = 0) \/ exists ge_signed_half_criterion_inverserighttableentryvaluedecode. (((dst_value_criterion_inverserighttable) = 2 * ge_signed_half_criterion_inverserighttableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserighttableentryvalue) = 0) /\ (ge_balance_negative_criterion_inverserighttableentryvalue) = S ge_signed_half_criterion_inverserighttableentryvaluedecode))) /\ ((dst_positive_criterion_inverserighttable) + ge_balance_negative_criterion_inverserighttableentryvalue = (dst_negative_criterion_inverserighttable) + ge_balance_positive_criterion_inverserighttableentryvalue))))))))) /\ (forall dc_input_criterion_inverseright dc_output_criterion_inverseright. ~(dc_input_criterion_inverseright=0) -> (exists pvs_le_gap_criterion_inverserightdomain. pvs_le_gap_criterion_inverserightdomain + (dc_input_criterion_inverseright) = (N)) -> (exists dst_positive_code_criterion_inverserightlookup dst_positive_scale_criterion_inverserightlookup dst_negative_code_criterion_inverserightlookup dst_negative_scale_criterion_inverserightlookup dst_positive_criterion_inverserightlookup dst_negative_criterion_inverserightlookup. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup)) * S ((dst_positive_code_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup)) + ((dst_positive_scale_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup))) + (((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) * S ((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) + ((dst_negative_scale_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)))) * S ((((dst_positive_code_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup)) * S ((dst_positive_code_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup)) + ((dst_positive_scale_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup))) + (((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) * S ((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) + ((dst_negative_scale_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)))) + ((((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) * S ((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) + ((dst_negative_scale_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup))) + (((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) * S ((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) + ((dst_negative_scale_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)))))) /\ (((((exists ff_h_pvs_criterion_inverserightlookuppositive. ff_h_pvs_criterion_inverserightlookuppositive + S (dst_positive_criterion_inverserightlookup) = S ((S (dc_input_criterion_inverseright)) * dst_positive_scale_criterion_inverserightlookup)) /\ exists ff_q_pvs_criterion_inverserightlookuppositive. dst_positive_code_criterion_inverserightlookup = ff_q_pvs_criterion_inverserightlookuppositive * S ((S (dc_input_criterion_inverseright)) * dst_positive_scale_criterion_inverserightlookup) + (dst_positive_criterion_inverserightlookup))) /\ (((((exists ff_h_pvs_criterion_inverserightlookupnegative. ff_h_pvs_criterion_inverserightlookupnegative + S (dst_negative_criterion_inverserightlookup) = S ((S (dc_input_criterion_inverseright)) * dst_negative_scale_criterion_inverserightlookup)) /\ exists ff_q_pvs_criterion_inverserightlookupnegative. dst_negative_code_criterion_inverserightlookup = ff_q_pvs_criterion_inverserightlookupnegative * S ((S (dc_input_criterion_inverseright)) * dst_negative_scale_criterion_inverserightlookup) + (dst_negative_criterion_inverserightlookup))) /\ (exists ge_balance_positive_criterion_inverserightlookupvalue ge_balance_negative_criterion_inverserightlookupvalue. (((((dc_output_criterion_inverseright) = 2 * (ge_balance_positive_criterion_inverserightlookupvalue) /\ (ge_balance_negative_criterion_inverserightlookupvalue) = 0) \/ exists ge_signed_half_criterion_inverserightlookupvaluedecode. (((dc_output_criterion_inverseright) = 2 * ge_signed_half_criterion_inverserightlookupvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightlookupvalue) = 0) /\ (ge_balance_negative_criterion_inverserightlookupvalue) = S ge_signed_half_criterion_inverserightlookupvaluedecode))) /\ ((dst_positive_criterion_inverserightlookup) + ge_balance_negative_criterion_inverserightlookupvalue = (dst_negative_criterion_inverserightlookup) + ge_balance_positive_criterion_inverserightlookupvalue))))))))) -> (((~((dc_input_criterion_inverseright)=0)) /\ (exists dc_mask_criterion_inverserightvalue. ((((exists dst_positive_code_criterion_inverserightvaluemasktable dst_positive_scale_criterion_inverserightvaluemasktable dst_negative_code_criterion_inverserightvaluemasktable dst_negative_scale_criterion_inverserightvaluemasktable. (((dc_mask_criterion_inverserightvalue) = (((((dst_positive_code_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable))) + (((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)))) * S ((((dst_positive_code_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable))) + (((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)))) + ((((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable))) + (((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)))))) /\ (forall dst_index_criterion_inverserightvaluemasktable. (exists pvs_le_gap_criterion_inverserightvaluemasktabledomain. pvs_le_gap_criterion_inverserightvaluemasktabledomain + (dst_index_criterion_inverserightvaluemasktable) = (dc_input_criterion_inverseright)) -> exists dst_positive_criterion_inverserightvaluemasktable dst_negative_criterion_inverserightvaluemasktable dst_value_criterion_inverserightvaluemasktable. ((((exists ff_h_pvs_criterion_inverserightvaluemasktableentrypositive. ff_h_pvs_criterion_inverserightvaluemasktableentrypositive + S (dst_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_criterion_inverserightvaluemasktable)) * dst_positive_scale_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_criterion_inverserightvaluemasktableentrypositive. dst_positive_code_criterion_inverserightvaluemasktable = ff_q_pvs_criterion_inverserightvaluemasktableentrypositive * S ((S (dst_index_criterion_inverserightvaluemasktable)) * dst_positive_scale_criterion_inverserightvaluemasktable) + (dst_positive_criterion_inverserightvaluemasktable))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemasktableentrynegative. ff_h_pvs_criterion_inverserightvaluemasktableentrynegative + S (dst_negative_criterion_inverserightvaluemasktable) = S ((S (dst_index_criterion_inverserightvaluemasktable)) * dst_negative_scale_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_criterion_inverserightvaluemasktableentrynegative. dst_negative_code_criterion_inverserightvaluemasktable = ff_q_pvs_criterion_inverserightvaluemasktableentrynegative * S ((S (dst_index_criterion_inverserightvaluemasktable)) * dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_criterion_inverserightvaluemasktable))) /\ (exists ge_balance_positive_criterion_inverserightvaluemasktableentryvalue ge_balance_negative_criterion_inverserightvaluemasktableentryvalue. (((((dst_value_criterion_inverserightvaluemasktable) = 2 * (ge_balance_positive_criterion_inverserightvaluemasktableentryvalue) /\ (ge_balance_negative_criterion_inverserightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemasktableentryvaluedecode. (((dst_value_criterion_inverserightvaluemasktable) = 2 * ge_signed_half_criterion_inverserightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_criterion_inverserightvaluemasktableentryvalue) = S ge_signed_half_criterion_inverserightvaluemasktableentryvaluedecode))) /\ ((dst_positive_criterion_inverserightvaluemasktable) + ge_balance_negative_criterion_inverserightvaluemasktableentryvalue = (dst_negative_criterion_inverserightvaluemasktable) + ge_balance_positive_criterion_inverserightvaluemasktableentryvalue))))))))) /\ (forall dc_index_criterion_inverserightvaluemask dc_value_criterion_inverserightvaluemask. (exists pvs_le_gap_criterion_inverserightvaluemaskdomain. pvs_le_gap_criterion_inverserightvaluemaskdomain + (dc_index_criterion_inverserightvaluemask) = (dc_input_criterion_inverseright)) -> (exists dst_positive_code_criterion_inverserightvaluemasklookup dst_positive_scale_criterion_inverserightvaluemasklookup dst_negative_code_criterion_inverserightvaluemasklookup dst_negative_scale_criterion_inverserightvaluemasklookup dst_positive_criterion_inverserightvaluemasklookup dst_negative_criterion_inverserightvaluemasklookup. (((dc_mask_criterion_inverserightvalue) = (((((dst_positive_code_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)))) * S ((((dst_positive_code_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)))) + ((((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemasklookuppositive. ff_h_pvs_criterion_inverserightvaluemasklookuppositive + S (dst_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_criterion_inverserightvaluemask)) * dst_positive_scale_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_criterion_inverserightvaluemasklookuppositive. dst_positive_code_criterion_inverserightvaluemasklookup = ff_q_pvs_criterion_inverserightvaluemasklookuppositive * S ((S (dc_index_criterion_inverserightvaluemask)) * dst_positive_scale_criterion_inverserightvaluemasklookup) + (dst_positive_criterion_inverserightvaluemasklookup))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemasklookupnegative. ff_h_pvs_criterion_inverserightvaluemasklookupnegative + S (dst_negative_criterion_inverserightvaluemasklookup) = S ((S (dc_index_criterion_inverserightvaluemask)) * dst_negative_scale_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_criterion_inverserightvaluemasklookupnegative. dst_negative_code_criterion_inverserightvaluemasklookup = ff_q_pvs_criterion_inverserightvaluemasklookupnegative * S ((S (dc_index_criterion_inverserightvaluemask)) * dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_criterion_inverserightvaluemasklookup))) /\ (exists ge_balance_positive_criterion_inverserightvaluemasklookupvalue ge_balance_negative_criterion_inverserightvaluemasklookupvalue. (((((dc_value_criterion_inverserightvaluemask) = 2 * (ge_balance_positive_criterion_inverserightvaluemasklookupvalue) /\ (ge_balance_negative_criterion_inverserightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemasklookupvaluedecode. (((dc_value_criterion_inverserightvaluemask) = 2 * ge_signed_half_criterion_inverserightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_criterion_inverserightvaluemasklookupvalue) = S ge_signed_half_criterion_inverserightvaluemasklookupvaluedecode))) /\ ((dst_positive_criterion_inverserightvaluemasklookup) + ge_balance_negative_criterion_inverserightvaluemasklookupvalue = (dst_negative_criterion_inverserightvaluemasklookup) + ge_balance_positive_criterion_inverserightvaluemasklookupvalue))))))))) -> ((((~((dc_index_criterion_inverserightvaluemask)=0)) /\ (exists dc_quotient_criterion_inverserightvaluemaskentry dc_left_criterion_inverserightvaluemaskentry dc_right_criterion_inverserightvaluemaskentry. (((dc_input_criterion_inverseright)=(dc_index_criterion_inverserightvaluemask)*dc_quotient_criterion_inverserightvaluemaskentry) /\ (((exists dst_positive_code_criterion_inverserightvaluemaskentryleft dst_positive_scale_criterion_inverserightvaluemaskentryleft dst_negative_code_criterion_inverserightvaluemaskentryleft dst_negative_scale_criterion_inverserightvaluemaskentryleft dst_positive_criterion_inverserightvaluemaskentryleft dst_negative_criterion_inverserightvaluemaskentryleft. (((G) = (((((dst_positive_code_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)))) * S ((((dst_positive_code_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)))) + ((((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemaskentryleftpositive. ff_h_pvs_criterion_inverserightvaluemaskentryleftpositive + S (dst_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_criterion_inverserightvaluemask)) * dst_positive_scale_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_criterion_inverserightvaluemaskentryleftpositive. dst_positive_code_criterion_inverserightvaluemaskentryleft = ff_q_pvs_criterion_inverserightvaluemaskentryleftpositive * S ((S (dc_index_criterion_inverserightvaluemask)) * dst_positive_scale_criterion_inverserightvaluemaskentryleft) + (dst_positive_criterion_inverserightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemaskentryleftnegative. ff_h_pvs_criterion_inverserightvaluemaskentryleftnegative + S (dst_negative_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_criterion_inverserightvaluemask)) * dst_negative_scale_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_criterion_inverserightvaluemaskentryleftnegative. dst_negative_code_criterion_inverserightvaluemaskentryleft = ff_q_pvs_criterion_inverserightvaluemaskentryleftnegative * S ((S (dc_index_criterion_inverserightvaluemask)) * dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_criterion_inverserightvaluemaskentryleft))) /\ (exists ge_balance_positive_criterion_inverserightvaluemaskentryleftvalue ge_balance_negative_criterion_inverserightvaluemaskentryleftvalue. (((((dc_left_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_criterion_inverserightvaluemaskentryleftvalue) /\ (ge_balance_negative_criterion_inverserightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryleftvaluedecode. (((dc_left_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_criterion_inverserightvaluemaskentryleftvalue) = S ge_signed_half_criterion_inverserightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_negative_criterion_inverserightvaluemaskentryleftvalue = (dst_negative_criterion_inverserightvaluemaskentryleft) + ge_balance_positive_criterion_inverserightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_criterion_inverserightvaluemaskentryright dst_positive_scale_criterion_inverserightvaluemaskentryright dst_negative_code_criterion_inverserightvaluemaskentryright dst_negative_scale_criterion_inverserightvaluemaskentryright dst_positive_criterion_inverserightvaluemaskentryright dst_negative_criterion_inverserightvaluemaskentryright. (((F) = (((((dst_positive_code_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)))) * S ((((dst_positive_code_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)))) + ((((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemaskentryrightpositive. ff_h_pvs_criterion_inverserightvaluemaskentryrightpositive + S (dst_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_criterion_inverserightvaluemaskentry)) * dst_positive_scale_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_criterion_inverserightvaluemaskentryrightpositive. dst_positive_code_criterion_inverserightvaluemaskentryright = ff_q_pvs_criterion_inverserightvaluemaskentryrightpositive * S ((S (dc_quotient_criterion_inverserightvaluemaskentry)) * dst_positive_scale_criterion_inverserightvaluemaskentryright) + (dst_positive_criterion_inverserightvaluemaskentryright))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemaskentryrightnegative. ff_h_pvs_criterion_inverserightvaluemaskentryrightnegative + S (dst_negative_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_criterion_inverserightvaluemaskentry)) * dst_negative_scale_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_criterion_inverserightvaluemaskentryrightnegative. dst_negative_code_criterion_inverserightvaluemaskentryright = ff_q_pvs_criterion_inverserightvaluemaskentryrightnegative * S ((S (dc_quotient_criterion_inverserightvaluemaskentry)) * dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_criterion_inverserightvaluemaskentryright))) /\ (exists ge_balance_positive_criterion_inverserightvaluemaskentryrightvalue ge_balance_negative_criterion_inverserightvaluemaskentryrightvalue. (((((dc_right_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_criterion_inverserightvaluemaskentryrightvalue) /\ (ge_balance_negative_criterion_inverserightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryrightvaluedecode. (((dc_right_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_criterion_inverserightvaluemaskentryrightvalue) = S ge_signed_half_criterion_inverserightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_criterion_inverserightvaluemaskentryright) + ge_balance_negative_criterion_inverserightvaluemaskentryrightvalue = (dst_negative_criterion_inverserightvaluemaskentryright) + ge_balance_positive_criterion_inverserightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_criterion_inverserightvaluemaskentryproduct sto_an_criterion_inverserightvaluemaskentryproduct sto_bp_criterion_inverserightvaluemaskentryproduct sto_bn_criterion_inverserightvaluemaskentryproduct sto_cp_criterion_inverserightvaluemaskentryproduct sto_cn_criterion_inverserightvaluemaskentryproduct. (((((dc_left_criterion_inverserightvaluemaskentry) = 2 * (sto_ap_criterion_inverserightvaluemaskentryproduct) /\ (sto_an_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryproductleft. (((dc_left_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryproductleft + 1 /\ (sto_ap_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_an_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_criterion_inverserightvaluemaskentryproductleft))) /\ ((((((dc_right_criterion_inverserightvaluemaskentry) = 2 * (sto_bp_criterion_inverserightvaluemaskentryproduct) /\ (sto_bn_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryproductright. (((dc_right_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryproductright + 1 /\ (sto_bp_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_bn_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_criterion_inverserightvaluemaskentryproductright))) /\ ((((((dc_value_criterion_inverserightvaluemask) = 2 * (sto_cp_criterion_inverserightvaluemaskentryproduct) /\ (sto_cn_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryproductoutput. (((dc_value_criterion_inverserightvaluemask) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryproductoutput + 1 /\ (sto_cp_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_cn_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_criterion_inverserightvaluemaskentryproductoutput))) /\ ((sto_ap_criterion_inverserightvaluemaskentryproduct * sto_bp_criterion_inverserightvaluemaskentryproduct + sto_an_criterion_inverserightvaluemaskentryproduct * sto_bn_criterion_inverserightvaluemaskentryproduct) + sto_cn_criterion_inverserightvaluemaskentryproduct = (sto_ap_criterion_inverserightvaluemaskentryproduct * sto_bn_criterion_inverserightvaluemaskentryproduct + sto_an_criterion_inverserightvaluemaskentryproduct * sto_bp_criterion_inverserightvaluemaskentryproduct) + sto_cp_criterion_inverserightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_criterion_inverserightvaluemask)=0 \/ ~(exists pvs_factor_criterion_inverserightvaluemaskentrynondivisor. (dc_input_criterion_inverseright) = (dc_index_criterion_inverserightvaluemask) * pvs_factor_criterion_inverserightvaluemaskentrynondivisor)) /\ ((dc_value_criterion_inverserightvaluemask)=0))))))) /\ (exists dst_positive_code_criterion_inverserightvaluefold dst_positive_scale_criterion_inverserightvaluefold dst_negative_code_criterion_inverserightvaluefold dst_negative_scale_criterion_inverserightvaluefold dst_positive_sum_criterion_inverserightvaluefold dst_negative_sum_criterion_inverserightvaluefold. (((dc_mask_criterion_inverserightvalue) = (((((dst_positive_code_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold)) * S ((dst_positive_code_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold)) + ((dst_positive_scale_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold))) + (((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) * S ((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) + ((dst_negative_scale_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)))) * S ((((dst_positive_code_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold)) * S ((dst_positive_code_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold)) + ((dst_positive_scale_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold))) + (((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) * S ((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) + ((dst_negative_scale_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)))) + ((((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) * S ((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) + ((dst_negative_scale_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold))) + (((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) * S ((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) + ((dst_negative_scale_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)))))) /\ (((exists fs_u_dst_criterion_inverserightvaluefoldpositive fs_v_dst_criterion_inverserightvaluefoldpositive. ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_start. fs_h_dst_criterion_inverserightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_start. fs_u_dst_criterion_inverserightvaluefoldpositive = fs_q_dst_criterion_inverserightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_criterion_inverserightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_terminal. fs_h_dst_criterion_inverserightvaluefoldpositive_body_terminal + S (dst_positive_sum_criterion_inverserightvaluefold) = S ((S (S (dc_input_criterion_inverseright))) * fs_v_dst_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_terminal. fs_u_dst_criterion_inverserightvaluefoldpositive = fs_q_dst_criterion_inverserightvaluefoldpositive_body_terminal * S ((S (S (dc_input_criterion_inverseright))) * fs_v_dst_criterion_inverserightvaluefoldpositive) + (dst_positive_sum_criterion_inverserightvaluefold))) /\ forall fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps. (exists fs_lt_dst_criterion_inverserightvaluefoldpositive_body_steps_bound. fs_lt_dst_criterion_inverserightvaluefoldpositive_body_steps_bound + S fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps = S (dc_input_criterion_inverseright)) -> exists fs_a_dst_criterion_inverserightvaluefoldpositive_body_steps fs_r_dst_criterion_inverserightvaluefoldpositive_body_steps fs_s_dst_criterion_inverserightvaluefoldpositive_body_steps. ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_summand. fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_summand + S (fs_a_dst_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_criterion_inverserightvaluefold)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_summand. dst_positive_code_criterion_inverserightvaluefold = fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_criterion_inverserightvaluefold) + (fs_a_dst_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_partial + S (fs_r_dst_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_u_dst_criterion_inverserightvaluefoldpositive = fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldpositive) + (fs_r_dst_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_successor + S (fs_s_dst_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_u_dst_criterion_inverserightvaluefoldpositive = fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldpositive) + (fs_s_dst_criterion_inverserightvaluefoldpositive_body_steps))) /\ fs_s_dst_criterion_inverserightvaluefoldpositive_body_steps = fs_r_dst_criterion_inverserightvaluefoldpositive_body_steps + fs_a_dst_criterion_inverserightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_criterion_inverserightvaluefoldnegative fs_v_dst_criterion_inverserightvaluefoldnegative. ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_start. fs_h_dst_criterion_inverserightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_start. fs_u_dst_criterion_inverserightvaluefoldnegative = fs_q_dst_criterion_inverserightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_criterion_inverserightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_terminal. fs_h_dst_criterion_inverserightvaluefoldnegative_body_terminal + S (dst_negative_sum_criterion_inverserightvaluefold) = S ((S (S (dc_input_criterion_inverseright))) * fs_v_dst_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_terminal. fs_u_dst_criterion_inverserightvaluefoldnegative = fs_q_dst_criterion_inverserightvaluefoldnegative_body_terminal * S ((S (S (dc_input_criterion_inverseright))) * fs_v_dst_criterion_inverserightvaluefoldnegative) + (dst_negative_sum_criterion_inverserightvaluefold))) /\ forall fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps. (exists fs_lt_dst_criterion_inverserightvaluefoldnegative_body_steps_bound. fs_lt_dst_criterion_inverserightvaluefoldnegative_body_steps_bound + S fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps = S (dc_input_criterion_inverseright)) -> exists fs_a_dst_criterion_inverserightvaluefoldnegative_body_steps fs_r_dst_criterion_inverserightvaluefoldnegative_body_steps fs_s_dst_criterion_inverserightvaluefoldnegative_body_steps. ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_summand. fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_summand + S (fs_a_dst_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_criterion_inverserightvaluefold)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_summand. dst_negative_code_criterion_inverserightvaluefold = fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_criterion_inverserightvaluefold) + (fs_a_dst_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_partial + S (fs_r_dst_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_u_dst_criterion_inverserightvaluefoldnegative = fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldnegative) + (fs_r_dst_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_successor + S (fs_s_dst_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_u_dst_criterion_inverserightvaluefoldnegative = fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldnegative) + (fs_s_dst_criterion_inverserightvaluefoldnegative_body_steps))) /\ fs_s_dst_criterion_inverserightvaluefoldnegative_body_steps = fs_r_dst_criterion_inverserightvaluefoldnegative_body_steps + fs_a_dst_criterion_inverserightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_criterion_inverserightvaluefoldresult ge_balance_negative_criterion_inverserightvaluefoldresult. (((((dc_output_criterion_inverseright) = 2 * (ge_balance_positive_criterion_inverserightvaluefoldresult) /\ (ge_balance_negative_criterion_inverserightvaluefoldresult) = 0) \/ exists ge_signed_half_criterion_inverserightvaluefoldresultdecode. (((dc_output_criterion_inverseright) = 2 * ge_signed_half_criterion_inverserightvaluefoldresultdecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluefoldresult) = 0) /\ (ge_balance_negative_criterion_inverserightvaluefoldresult) = S ge_signed_half_criterion_inverserightvaluefoldresultdecode))) /\ ((dst_positive_sum_criterion_inverserightvaluefold) + ge_balance_negative_criterion_inverserightvaluefoldresult = (dst_negative_sum_criterion_inverserightvaluefold) + ge_balance_positive_criterion_inverserightvaluefoldresult))))))))))))))))))))))))) -> (N=0 \/ ((exists dst_positive_code_criterion_unitpositive dst_positive_scale_criterion_unitpositive dst_negative_code_criterion_unitpositive dst_negative_scale_criterion_unitpositive dst_positive_criterion_unitpositive dst_negative_criterion_unitpositive. (((F) = (((((dst_positive_code_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive)) * S ((dst_positive_code_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive)) + ((dst_positive_scale_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive))) + (((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) * S ((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) + ((dst_negative_scale_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)))) * S ((((dst_positive_code_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive)) * S ((dst_positive_code_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive)) + ((dst_positive_scale_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive))) + (((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) * S ((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) + ((dst_negative_scale_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)))) + ((((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) * S ((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) + ((dst_negative_scale_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive))) + (((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) * S ((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) + ((dst_negative_scale_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)))))) /\ (((((exists ff_h_pvs_criterion_unitpositivepositive. ff_h_pvs_criterion_unitpositivepositive + S (dst_positive_criterion_unitpositive) = S ((S (1)) * dst_positive_scale_criterion_unitpositive)) /\ exists ff_q_pvs_criterion_unitpositivepositive. dst_positive_code_criterion_unitpositive = ff_q_pvs_criterion_unitpositivepositive * S ((S (1)) * dst_positive_scale_criterion_unitpositive) + (dst_positive_criterion_unitpositive))) /\ (((((exists ff_h_pvs_criterion_unitpositivenegative. ff_h_pvs_criterion_unitpositivenegative + S (dst_negative_criterion_unitpositive) = S ((S (1)) * dst_negative_scale_criterion_unitpositive)) /\ exists ff_q_pvs_criterion_unitpositivenegative. dst_negative_code_criterion_unitpositive = ff_q_pvs_criterion_unitpositivenegative * S ((S (1)) * dst_negative_scale_criterion_unitpositive) + (dst_negative_criterion_unitpositive))) /\ (exists ge_balance_positive_criterion_unitpositivevalue ge_balance_negative_criterion_unitpositivevalue. (((((2) = 2 * (ge_balance_positive_criterion_unitpositivevalue) /\ (ge_balance_negative_criterion_unitpositivevalue) = 0) \/ exists ge_signed_half_criterion_unitpositivevaluedecode. (((2) = 2 * ge_signed_half_criterion_unitpositivevaluedecode + 1 /\ (ge_balance_positive_criterion_unitpositivevalue) = 0) /\ (ge_balance_negative_criterion_unitpositivevalue) = S ge_signed_half_criterion_unitpositivevaluedecode))) /\ ((dst_positive_criterion_unitpositive) + ge_balance_negative_criterion_unitpositivevalue = (dst_negative_criterion_unitpositive) + ge_balance_positive_criterion_unitpositivevalue))))))))) \/ (exists dst_positive_code_criterion_unitnegative dst_positive_scale_criterion_unitnegative dst_negative_code_criterion_unitnegative dst_negative_scale_criterion_unitnegative dst_positive_criterion_unitnegative dst_negative_criterion_unitnegative. (((F) = (((((dst_positive_code_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative)) * S ((dst_positive_code_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative)) + ((dst_positive_scale_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative))) + (((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) * S ((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) + ((dst_negative_scale_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)))) * S ((((dst_positive_code_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative)) * S ((dst_positive_code_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative)) + ((dst_positive_scale_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative))) + (((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) * S ((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) + ((dst_negative_scale_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)))) + ((((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) * S ((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) + ((dst_negative_scale_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative))) + (((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) * S ((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) + ((dst_negative_scale_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)))))) /\ (((((exists ff_h_pvs_criterion_unitnegativepositive. ff_h_pvs_criterion_unitnegativepositive + S (dst_positive_criterion_unitnegative) = S ((S (1)) * dst_positive_scale_criterion_unitnegative)) /\ exists ff_q_pvs_criterion_unitnegativepositive. dst_positive_code_criterion_unitnegative = ff_q_pvs_criterion_unitnegativepositive * S ((S (1)) * dst_positive_scale_criterion_unitnegative) + (dst_positive_criterion_unitnegative))) /\ (((((exists ff_h_pvs_criterion_unitnegativenegative. ff_h_pvs_criterion_unitnegativenegative + S (dst_negative_criterion_unitnegative) = S ((S (1)) * dst_negative_scale_criterion_unitnegative)) /\ exists ff_q_pvs_criterion_unitnegativenegative. dst_negative_code_criterion_unitnegative = ff_q_pvs_criterion_unitnegativenegative * S ((S (1)) * dst_negative_scale_criterion_unitnegative) + (dst_negative_criterion_unitnegative))) /\ (exists ge_balance_positive_criterion_unitnegativevalue ge_balance_negative_criterion_unitnegativevalue. (((((1) = 2 * (ge_balance_positive_criterion_unitnegativevalue) /\ (ge_balance_negative_criterion_unitnegativevalue) = 0) \/ exists ge_signed_half_criterion_unitnegativevaluedecode. (((1) = 2 * ge_signed_half_criterion_unitnegativevaluedecode + 1 /\ (ge_balance_positive_criterion_unitnegativevalue) = 0) /\ (ge_balance_negative_criterion_unitnegativevalue) = S ge_signed_half_criterion_unitnegativevaluedecode))) /\ ((dst_positive_criterion_unitnegative) + ge_balance_negative_criterion_unitnegativevalue = (dst_negative_criterion_unitnegative) + ge_balance_positive_criterion_unitnegativevalue)))))))))))) /\ ((N=0 \/ ((exists dst_positive_code_criterion_unitpositive dst_positive_scale_criterion_unitpositive dst_negative_code_criterion_unitpositive dst_negative_scale_criterion_unitpositive dst_positive_criterion_unitpositive dst_negative_criterion_unitpositive. (((F) = (((((dst_positive_code_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive)) * S ((dst_positive_code_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive)) + ((dst_positive_scale_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive))) + (((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) * S ((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) + ((dst_negative_scale_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)))) * S ((((dst_positive_code_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive)) * S ((dst_positive_code_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive)) + ((dst_positive_scale_criterion_unitpositive) + (dst_positive_scale_criterion_unitpositive))) + (((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) * S ((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) + ((dst_negative_scale_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)))) + ((((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) * S ((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) + ((dst_negative_scale_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive))) + (((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) * S ((dst_negative_code_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)) + ((dst_negative_scale_criterion_unitpositive) + (dst_negative_scale_criterion_unitpositive)))))) /\ (((((exists ff_h_pvs_criterion_unitpositivepositive. ff_h_pvs_criterion_unitpositivepositive + S (dst_positive_criterion_unitpositive) = S ((S (1)) * dst_positive_scale_criterion_unitpositive)) /\ exists ff_q_pvs_criterion_unitpositivepositive. dst_positive_code_criterion_unitpositive = ff_q_pvs_criterion_unitpositivepositive * S ((S (1)) * dst_positive_scale_criterion_unitpositive) + (dst_positive_criterion_unitpositive))) /\ (((((exists ff_h_pvs_criterion_unitpositivenegative. ff_h_pvs_criterion_unitpositivenegative + S (dst_negative_criterion_unitpositive) = S ((S (1)) * dst_negative_scale_criterion_unitpositive)) /\ exists ff_q_pvs_criterion_unitpositivenegative. dst_negative_code_criterion_unitpositive = ff_q_pvs_criterion_unitpositivenegative * S ((S (1)) * dst_negative_scale_criterion_unitpositive) + (dst_negative_criterion_unitpositive))) /\ (exists ge_balance_positive_criterion_unitpositivevalue ge_balance_negative_criterion_unitpositivevalue. (((((2) = 2 * (ge_balance_positive_criterion_unitpositivevalue) /\ (ge_balance_negative_criterion_unitpositivevalue) = 0) \/ exists ge_signed_half_criterion_unitpositivevaluedecode. (((2) = 2 * ge_signed_half_criterion_unitpositivevaluedecode + 1 /\ (ge_balance_positive_criterion_unitpositivevalue) = 0) /\ (ge_balance_negative_criterion_unitpositivevalue) = S ge_signed_half_criterion_unitpositivevaluedecode))) /\ ((dst_positive_criterion_unitpositive) + ge_balance_negative_criterion_unitpositivevalue = (dst_negative_criterion_unitpositive) + ge_balance_positive_criterion_unitpositivevalue))))))))) \/ (exists dst_positive_code_criterion_unitnegative dst_positive_scale_criterion_unitnegative dst_negative_code_criterion_unitnegative dst_negative_scale_criterion_unitnegative dst_positive_criterion_unitnegative dst_negative_criterion_unitnegative. (((F) = (((((dst_positive_code_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative)) * S ((dst_positive_code_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative)) + ((dst_positive_scale_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative))) + (((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) * S ((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) + ((dst_negative_scale_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)))) * S ((((dst_positive_code_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative)) * S ((dst_positive_code_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative)) + ((dst_positive_scale_criterion_unitnegative) + (dst_positive_scale_criterion_unitnegative))) + (((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) * S ((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) + ((dst_negative_scale_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)))) + ((((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) * S ((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) + ((dst_negative_scale_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative))) + (((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) * S ((dst_negative_code_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)) + ((dst_negative_scale_criterion_unitnegative) + (dst_negative_scale_criterion_unitnegative)))))) /\ (((((exists ff_h_pvs_criterion_unitnegativepositive. ff_h_pvs_criterion_unitnegativepositive + S (dst_positive_criterion_unitnegative) = S ((S (1)) * dst_positive_scale_criterion_unitnegative)) /\ exists ff_q_pvs_criterion_unitnegativepositive. dst_positive_code_criterion_unitnegative = ff_q_pvs_criterion_unitnegativepositive * S ((S (1)) * dst_positive_scale_criterion_unitnegative) + (dst_positive_criterion_unitnegative))) /\ (((((exists ff_h_pvs_criterion_unitnegativenegative. ff_h_pvs_criterion_unitnegativenegative + S (dst_negative_criterion_unitnegative) = S ((S (1)) * dst_negative_scale_criterion_unitnegative)) /\ exists ff_q_pvs_criterion_unitnegativenegative. dst_negative_code_criterion_unitnegative = ff_q_pvs_criterion_unitnegativenegative * S ((S (1)) * dst_negative_scale_criterion_unitnegative) + (dst_negative_criterion_unitnegative))) /\ (exists ge_balance_positive_criterion_unitnegativevalue ge_balance_negative_criterion_unitnegativevalue. (((((1) = 2 * (ge_balance_positive_criterion_unitnegativevalue) /\ (ge_balance_negative_criterion_unitnegativevalue) = 0) \/ exists ge_signed_half_criterion_unitnegativevaluedecode. (((1) = 2 * ge_signed_half_criterion_unitnegativevaluedecode + 1 /\ (ge_balance_positive_criterion_unitnegativevalue) = 0) /\ (ge_balance_negative_criterion_unitnegativevalue) = S ge_signed_half_criterion_unitnegativevaluedecode))) /\ ((dst_positive_criterion_unitnegative) + ge_balance_negative_criterion_unitnegativevalue = (dst_negative_criterion_unitnegative) + ge_balance_positive_criterion_unitnegativevalue))))))))))) -> exists G. (exists di_delta_criterion_inverse. ((((exists dst_positive_code_criterion_inversedeltatable dst_positive_scale_criterion_inversedeltatable dst_negative_code_criterion_inversedeltatable dst_negative_scale_criterion_inversedeltatable. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable)) * S ((dst_positive_code_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable)) + ((dst_positive_scale_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable))) + (((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) * S ((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) + ((dst_negative_scale_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)))) * S ((((dst_positive_code_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable)) * S ((dst_positive_code_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable)) + ((dst_positive_scale_criterion_inversedeltatable) + (dst_positive_scale_criterion_inversedeltatable))) + (((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) * S ((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) + ((dst_negative_scale_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)))) + ((((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) * S ((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) + ((dst_negative_scale_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable))) + (((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) * S ((dst_negative_code_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)) + ((dst_negative_scale_criterion_inversedeltatable) + (dst_negative_scale_criterion_inversedeltatable)))))) /\ (forall dst_index_criterion_inversedeltatable. (exists pvs_le_gap_criterion_inversedeltatabledomain. pvs_le_gap_criterion_inversedeltatabledomain + (dst_index_criterion_inversedeltatable) = (N)) -> exists dst_positive_criterion_inversedeltatable dst_negative_criterion_inversedeltatable dst_value_criterion_inversedeltatable. ((((exists ff_h_pvs_criterion_inversedeltatableentrypositive. ff_h_pvs_criterion_inversedeltatableentrypositive + S (dst_positive_criterion_inversedeltatable) = S ((S (dst_index_criterion_inversedeltatable)) * dst_positive_scale_criterion_inversedeltatable)) /\ exists ff_q_pvs_criterion_inversedeltatableentrypositive. dst_positive_code_criterion_inversedeltatable = ff_q_pvs_criterion_inversedeltatableentrypositive * S ((S (dst_index_criterion_inversedeltatable)) * dst_positive_scale_criterion_inversedeltatable) + (dst_positive_criterion_inversedeltatable))) /\ (((((exists ff_h_pvs_criterion_inversedeltatableentrynegative. ff_h_pvs_criterion_inversedeltatableentrynegative + S (dst_negative_criterion_inversedeltatable) = S ((S (dst_index_criterion_inversedeltatable)) * dst_negative_scale_criterion_inversedeltatable)) /\ exists ff_q_pvs_criterion_inversedeltatableentrynegative. dst_negative_code_criterion_inversedeltatable = ff_q_pvs_criterion_inversedeltatableentrynegative * S ((S (dst_index_criterion_inversedeltatable)) * dst_negative_scale_criterion_inversedeltatable) + (dst_negative_criterion_inversedeltatable))) /\ (exists ge_balance_positive_criterion_inversedeltatableentryvalue ge_balance_negative_criterion_inversedeltatableentryvalue. (((((dst_value_criterion_inversedeltatable) = 2 * (ge_balance_positive_criterion_inversedeltatableentryvalue) /\ (ge_balance_negative_criterion_inversedeltatableentryvalue) = 0) \/ exists ge_signed_half_criterion_inversedeltatableentryvaluedecode. (((dst_value_criterion_inversedeltatable) = 2 * ge_signed_half_criterion_inversedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inversedeltatableentryvalue) = 0) /\ (ge_balance_negative_criterion_inversedeltatableentryvalue) = S ge_signed_half_criterion_inversedeltatableentryvaluedecode))) /\ ((dst_positive_criterion_inversedeltatable) + ge_balance_negative_criterion_inversedeltatableentryvalue = (dst_negative_criterion_inversedeltatable) + ge_balance_positive_criterion_inversedeltatableentryvalue))))))))) /\ (forall du_index_criterion_inversedelta du_value_criterion_inversedelta. ~(du_index_criterion_inversedelta=0) -> (exists pvs_le_gap_criterion_inversedeltabound. pvs_le_gap_criterion_inversedeltabound + (du_index_criterion_inversedelta) = (N)) -> (exists dst_positive_code_criterion_inversedeltaentry dst_positive_scale_criterion_inversedeltaentry dst_negative_code_criterion_inversedeltaentry dst_negative_scale_criterion_inversedeltaentry dst_positive_criterion_inversedeltaentry dst_negative_criterion_inversedeltaentry. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry)) * S ((dst_positive_code_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry)) + ((dst_positive_scale_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry))) + (((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) * S ((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) + ((dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)))) * S ((((dst_positive_code_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry)) * S ((dst_positive_code_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry)) + ((dst_positive_scale_criterion_inversedeltaentry) + (dst_positive_scale_criterion_inversedeltaentry))) + (((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) * S ((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) + ((dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)))) + ((((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) * S ((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) + ((dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry))) + (((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) * S ((dst_negative_code_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)) + ((dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_scale_criterion_inversedeltaentry)))))) /\ (((((exists ff_h_pvs_criterion_inversedeltaentrypositive. ff_h_pvs_criterion_inversedeltaentrypositive + S (dst_positive_criterion_inversedeltaentry) = S ((S (du_index_criterion_inversedelta)) * dst_positive_scale_criterion_inversedeltaentry)) /\ exists ff_q_pvs_criterion_inversedeltaentrypositive. dst_positive_code_criterion_inversedeltaentry = ff_q_pvs_criterion_inversedeltaentrypositive * S ((S (du_index_criterion_inversedelta)) * dst_positive_scale_criterion_inversedeltaentry) + (dst_positive_criterion_inversedeltaentry))) /\ (((((exists ff_h_pvs_criterion_inversedeltaentrynegative. ff_h_pvs_criterion_inversedeltaentrynegative + S (dst_negative_criterion_inversedeltaentry) = S ((S (du_index_criterion_inversedelta)) * dst_negative_scale_criterion_inversedeltaentry)) /\ exists ff_q_pvs_criterion_inversedeltaentrynegative. dst_negative_code_criterion_inversedeltaentry = ff_q_pvs_criterion_inversedeltaentrynegative * S ((S (du_index_criterion_inversedelta)) * dst_negative_scale_criterion_inversedeltaentry) + (dst_negative_criterion_inversedeltaentry))) /\ (exists ge_balance_positive_criterion_inversedeltaentryvalue ge_balance_negative_criterion_inversedeltaentryvalue. (((((du_value_criterion_inversedelta) = 2 * (ge_balance_positive_criterion_inversedeltaentryvalue) /\ (ge_balance_negative_criterion_inversedeltaentryvalue) = 0) \/ exists ge_signed_half_criterion_inversedeltaentryvaluedecode. (((du_value_criterion_inversedelta) = 2 * ge_signed_half_criterion_inversedeltaentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inversedeltaentryvalue) = 0) /\ (ge_balance_negative_criterion_inversedeltaentryvalue) = S ge_signed_half_criterion_inversedeltaentryvaluedecode))) /\ ((dst_positive_criterion_inversedeltaentry) + ge_balance_negative_criterion_inversedeltaentryvalue = (dst_negative_criterion_inversedeltaentry) + ge_balance_positive_criterion_inversedeltaentryvalue))))))))) -> ((((du_index_criterion_inversedelta)=1 -> (du_value_criterion_inversedelta)=2) /\ (~((du_index_criterion_inversedelta)=1) -> (du_value_criterion_inversedelta)=0)))))) /\ (((((exists dst_positive_code_criterion_inverseleftleft dst_positive_scale_criterion_inverseleftleft dst_negative_code_criterion_inverseleftleft dst_negative_scale_criterion_inverseleftleft. (((F) = (((((dst_positive_code_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft)) * S ((dst_positive_code_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft)) + ((dst_positive_scale_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft))) + (((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) * S ((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) + ((dst_negative_scale_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)))) * S ((((dst_positive_code_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft)) * S ((dst_positive_code_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft)) + ((dst_positive_scale_criterion_inverseleftleft) + (dst_positive_scale_criterion_inverseleftleft))) + (((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) * S ((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) + ((dst_negative_scale_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)))) + ((((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) * S ((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) + ((dst_negative_scale_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft))) + (((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) * S ((dst_negative_code_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)) + ((dst_negative_scale_criterion_inverseleftleft) + (dst_negative_scale_criterion_inverseleftleft)))))) /\ (forall dst_index_criterion_inverseleftleft. (exists pvs_le_gap_criterion_inverseleftleftdomain. pvs_le_gap_criterion_inverseleftleftdomain + (dst_index_criterion_inverseleftleft) = (N)) -> exists dst_positive_criterion_inverseleftleft dst_negative_criterion_inverseleftleft dst_value_criterion_inverseleftleft. ((((exists ff_h_pvs_criterion_inverseleftleftentrypositive. ff_h_pvs_criterion_inverseleftleftentrypositive + S (dst_positive_criterion_inverseleftleft) = S ((S (dst_index_criterion_inverseleftleft)) * dst_positive_scale_criterion_inverseleftleft)) /\ exists ff_q_pvs_criterion_inverseleftleftentrypositive. dst_positive_code_criterion_inverseleftleft = ff_q_pvs_criterion_inverseleftleftentrypositive * S ((S (dst_index_criterion_inverseleftleft)) * dst_positive_scale_criterion_inverseleftleft) + (dst_positive_criterion_inverseleftleft))) /\ (((((exists ff_h_pvs_criterion_inverseleftleftentrynegative. ff_h_pvs_criterion_inverseleftleftentrynegative + S (dst_negative_criterion_inverseleftleft) = S ((S (dst_index_criterion_inverseleftleft)) * dst_negative_scale_criterion_inverseleftleft)) /\ exists ff_q_pvs_criterion_inverseleftleftentrynegative. dst_negative_code_criterion_inverseleftleft = ff_q_pvs_criterion_inverseleftleftentrynegative * S ((S (dst_index_criterion_inverseleftleft)) * dst_negative_scale_criterion_inverseleftleft) + (dst_negative_criterion_inverseleftleft))) /\ (exists ge_balance_positive_criterion_inverseleftleftentryvalue ge_balance_negative_criterion_inverseleftleftentryvalue. (((((dst_value_criterion_inverseleftleft) = 2 * (ge_balance_positive_criterion_inverseleftleftentryvalue) /\ (ge_balance_negative_criterion_inverseleftleftentryvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftleftentryvaluedecode. (((dst_value_criterion_inverseleftleft) = 2 * ge_signed_half_criterion_inverseleftleftentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftleftentryvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftleftentryvalue) = S ge_signed_half_criterion_inverseleftleftentryvaluedecode))) /\ ((dst_positive_criterion_inverseleftleft) + ge_balance_negative_criterion_inverseleftleftentryvalue = (dst_negative_criterion_inverseleftleft) + ge_balance_positive_criterion_inverseleftleftentryvalue))))))))) /\ (((exists dst_positive_code_criterion_inverseleftright dst_positive_scale_criterion_inverseleftright dst_negative_code_criterion_inverseleftright dst_negative_scale_criterion_inverseleftright. (((G) = (((((dst_positive_code_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright)) * S ((dst_positive_code_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright)) + ((dst_positive_scale_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright))) + (((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) * S ((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) + ((dst_negative_scale_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)))) * S ((((dst_positive_code_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright)) * S ((dst_positive_code_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright)) + ((dst_positive_scale_criterion_inverseleftright) + (dst_positive_scale_criterion_inverseleftright))) + (((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) * S ((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) + ((dst_negative_scale_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)))) + ((((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) * S ((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) + ((dst_negative_scale_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright))) + (((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) * S ((dst_negative_code_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)) + ((dst_negative_scale_criterion_inverseleftright) + (dst_negative_scale_criterion_inverseleftright)))))) /\ (forall dst_index_criterion_inverseleftright. (exists pvs_le_gap_criterion_inverseleftrightdomain. pvs_le_gap_criterion_inverseleftrightdomain + (dst_index_criterion_inverseleftright) = (N)) -> exists dst_positive_criterion_inverseleftright dst_negative_criterion_inverseleftright dst_value_criterion_inverseleftright. ((((exists ff_h_pvs_criterion_inverseleftrightentrypositive. ff_h_pvs_criterion_inverseleftrightentrypositive + S (dst_positive_criterion_inverseleftright) = S ((S (dst_index_criterion_inverseleftright)) * dst_positive_scale_criterion_inverseleftright)) /\ exists ff_q_pvs_criterion_inverseleftrightentrypositive. dst_positive_code_criterion_inverseleftright = ff_q_pvs_criterion_inverseleftrightentrypositive * S ((S (dst_index_criterion_inverseleftright)) * dst_positive_scale_criterion_inverseleftright) + (dst_positive_criterion_inverseleftright))) /\ (((((exists ff_h_pvs_criterion_inverseleftrightentrynegative. ff_h_pvs_criterion_inverseleftrightentrynegative + S (dst_negative_criterion_inverseleftright) = S ((S (dst_index_criterion_inverseleftright)) * dst_negative_scale_criterion_inverseleftright)) /\ exists ff_q_pvs_criterion_inverseleftrightentrynegative. dst_negative_code_criterion_inverseleftright = ff_q_pvs_criterion_inverseleftrightentrynegative * S ((S (dst_index_criterion_inverseleftright)) * dst_negative_scale_criterion_inverseleftright) + (dst_negative_criterion_inverseleftright))) /\ (exists ge_balance_positive_criterion_inverseleftrightentryvalue ge_balance_negative_criterion_inverseleftrightentryvalue. (((((dst_value_criterion_inverseleftright) = 2 * (ge_balance_positive_criterion_inverseleftrightentryvalue) /\ (ge_balance_negative_criterion_inverseleftrightentryvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftrightentryvaluedecode. (((dst_value_criterion_inverseleftright) = 2 * ge_signed_half_criterion_inverseleftrightentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftrightentryvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftrightentryvalue) = S ge_signed_half_criterion_inverseleftrightentryvaluedecode))) /\ ((dst_positive_criterion_inverseleftright) + ge_balance_negative_criterion_inverseleftrightentryvalue = (dst_negative_criterion_inverseleftright) + ge_balance_positive_criterion_inverseleftrightentryvalue))))))))) /\ (((exists dst_positive_code_criterion_inverselefttable dst_positive_scale_criterion_inverselefttable dst_negative_code_criterion_inverselefttable dst_negative_scale_criterion_inverselefttable. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable)) * S ((dst_positive_code_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable)) + ((dst_positive_scale_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable))) + (((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) * S ((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) + ((dst_negative_scale_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)))) * S ((((dst_positive_code_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable)) * S ((dst_positive_code_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable)) + ((dst_positive_scale_criterion_inverselefttable) + (dst_positive_scale_criterion_inverselefttable))) + (((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) * S ((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) + ((dst_negative_scale_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)))) + ((((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) * S ((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) + ((dst_negative_scale_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable))) + (((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) * S ((dst_negative_code_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)) + ((dst_negative_scale_criterion_inverselefttable) + (dst_negative_scale_criterion_inverselefttable)))))) /\ (forall dst_index_criterion_inverselefttable. (exists pvs_le_gap_criterion_inverselefttabledomain. pvs_le_gap_criterion_inverselefttabledomain + (dst_index_criterion_inverselefttable) = (N)) -> exists dst_positive_criterion_inverselefttable dst_negative_criterion_inverselefttable dst_value_criterion_inverselefttable. ((((exists ff_h_pvs_criterion_inverselefttableentrypositive. ff_h_pvs_criterion_inverselefttableentrypositive + S (dst_positive_criterion_inverselefttable) = S ((S (dst_index_criterion_inverselefttable)) * dst_positive_scale_criterion_inverselefttable)) /\ exists ff_q_pvs_criterion_inverselefttableentrypositive. dst_positive_code_criterion_inverselefttable = ff_q_pvs_criterion_inverselefttableentrypositive * S ((S (dst_index_criterion_inverselefttable)) * dst_positive_scale_criterion_inverselefttable) + (dst_positive_criterion_inverselefttable))) /\ (((((exists ff_h_pvs_criterion_inverselefttableentrynegative. ff_h_pvs_criterion_inverselefttableentrynegative + S (dst_negative_criterion_inverselefttable) = S ((S (dst_index_criterion_inverselefttable)) * dst_negative_scale_criterion_inverselefttable)) /\ exists ff_q_pvs_criterion_inverselefttableentrynegative. dst_negative_code_criterion_inverselefttable = ff_q_pvs_criterion_inverselefttableentrynegative * S ((S (dst_index_criterion_inverselefttable)) * dst_negative_scale_criterion_inverselefttable) + (dst_negative_criterion_inverselefttable))) /\ (exists ge_balance_positive_criterion_inverselefttableentryvalue ge_balance_negative_criterion_inverselefttableentryvalue. (((((dst_value_criterion_inverselefttable) = 2 * (ge_balance_positive_criterion_inverselefttableentryvalue) /\ (ge_balance_negative_criterion_inverselefttableentryvalue) = 0) \/ exists ge_signed_half_criterion_inverselefttableentryvaluedecode. (((dst_value_criterion_inverselefttable) = 2 * ge_signed_half_criterion_inverselefttableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverselefttableentryvalue) = 0) /\ (ge_balance_negative_criterion_inverselefttableentryvalue) = S ge_signed_half_criterion_inverselefttableentryvaluedecode))) /\ ((dst_positive_criterion_inverselefttable) + ge_balance_negative_criterion_inverselefttableentryvalue = (dst_negative_criterion_inverselefttable) + ge_balance_positive_criterion_inverselefttableentryvalue))))))))) /\ (forall dc_input_criterion_inverseleft dc_output_criterion_inverseleft. ~(dc_input_criterion_inverseleft=0) -> (exists pvs_le_gap_criterion_inverseleftdomain. pvs_le_gap_criterion_inverseleftdomain + (dc_input_criterion_inverseleft) = (N)) -> (exists dst_positive_code_criterion_inverseleftlookup dst_positive_scale_criterion_inverseleftlookup dst_negative_code_criterion_inverseleftlookup dst_negative_scale_criterion_inverseleftlookup dst_positive_criterion_inverseleftlookup dst_negative_criterion_inverseleftlookup. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup)) * S ((dst_positive_code_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup)) + ((dst_positive_scale_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup))) + (((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) * S ((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) + ((dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)))) * S ((((dst_positive_code_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup)) * S ((dst_positive_code_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup)) + ((dst_positive_scale_criterion_inverseleftlookup) + (dst_positive_scale_criterion_inverseleftlookup))) + (((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) * S ((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) + ((dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)))) + ((((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) * S ((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) + ((dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup))) + (((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) * S ((dst_negative_code_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)) + ((dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_scale_criterion_inverseleftlookup)))))) /\ (((((exists ff_h_pvs_criterion_inverseleftlookuppositive. ff_h_pvs_criterion_inverseleftlookuppositive + S (dst_positive_criterion_inverseleftlookup) = S ((S (dc_input_criterion_inverseleft)) * dst_positive_scale_criterion_inverseleftlookup)) /\ exists ff_q_pvs_criterion_inverseleftlookuppositive. dst_positive_code_criterion_inverseleftlookup = ff_q_pvs_criterion_inverseleftlookuppositive * S ((S (dc_input_criterion_inverseleft)) * dst_positive_scale_criterion_inverseleftlookup) + (dst_positive_criterion_inverseleftlookup))) /\ (((((exists ff_h_pvs_criterion_inverseleftlookupnegative. ff_h_pvs_criterion_inverseleftlookupnegative + S (dst_negative_criterion_inverseleftlookup) = S ((S (dc_input_criterion_inverseleft)) * dst_negative_scale_criterion_inverseleftlookup)) /\ exists ff_q_pvs_criterion_inverseleftlookupnegative. dst_negative_code_criterion_inverseleftlookup = ff_q_pvs_criterion_inverseleftlookupnegative * S ((S (dc_input_criterion_inverseleft)) * dst_negative_scale_criterion_inverseleftlookup) + (dst_negative_criterion_inverseleftlookup))) /\ (exists ge_balance_positive_criterion_inverseleftlookupvalue ge_balance_negative_criterion_inverseleftlookupvalue. (((((dc_output_criterion_inverseleft) = 2 * (ge_balance_positive_criterion_inverseleftlookupvalue) /\ (ge_balance_negative_criterion_inverseleftlookupvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftlookupvaluedecode. (((dc_output_criterion_inverseleft) = 2 * ge_signed_half_criterion_inverseleftlookupvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftlookupvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftlookupvalue) = S ge_signed_half_criterion_inverseleftlookupvaluedecode))) /\ ((dst_positive_criterion_inverseleftlookup) + ge_balance_negative_criterion_inverseleftlookupvalue = (dst_negative_criterion_inverseleftlookup) + ge_balance_positive_criterion_inverseleftlookupvalue))))))))) -> (((~((dc_input_criterion_inverseleft)=0)) /\ (exists dc_mask_criterion_inverseleftvalue. ((((exists dst_positive_code_criterion_inverseleftvaluemasktable dst_positive_scale_criterion_inverseleftvaluemasktable dst_negative_code_criterion_inverseleftvaluemasktable dst_negative_scale_criterion_inverseleftvaluemasktable. (((dc_mask_criterion_inverseleftvalue) = (((((dst_positive_code_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)))) * S ((((dst_positive_code_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_criterion_inverseleftvaluemasktable) + (dst_positive_scale_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)))) + ((((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_scale_criterion_inverseleftvaluemasktable)))))) /\ (forall dst_index_criterion_inverseleftvaluemasktable. (exists pvs_le_gap_criterion_inverseleftvaluemasktabledomain. pvs_le_gap_criterion_inverseleftvaluemasktabledomain + (dst_index_criterion_inverseleftvaluemasktable) = (dc_input_criterion_inverseleft)) -> exists dst_positive_criterion_inverseleftvaluemasktable dst_negative_criterion_inverseleftvaluemasktable dst_value_criterion_inverseleftvaluemasktable. ((((exists ff_h_pvs_criterion_inverseleftvaluemasktableentrypositive. ff_h_pvs_criterion_inverseleftvaluemasktableentrypositive + S (dst_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_criterion_inverseleftvaluemasktable)) * dst_positive_scale_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_criterion_inverseleftvaluemasktableentrypositive. dst_positive_code_criterion_inverseleftvaluemasktable = ff_q_pvs_criterion_inverseleftvaluemasktableentrypositive * S ((S (dst_index_criterion_inverseleftvaluemasktable)) * dst_positive_scale_criterion_inverseleftvaluemasktable) + (dst_positive_criterion_inverseleftvaluemasktable))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemasktableentrynegative. ff_h_pvs_criterion_inverseleftvaluemasktableentrynegative + S (dst_negative_criterion_inverseleftvaluemasktable) = S ((S (dst_index_criterion_inverseleftvaluemasktable)) * dst_negative_scale_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_criterion_inverseleftvaluemasktableentrynegative. dst_negative_code_criterion_inverseleftvaluemasktable = ff_q_pvs_criterion_inverseleftvaluemasktableentrynegative * S ((S (dst_index_criterion_inverseleftvaluemasktable)) * dst_negative_scale_criterion_inverseleftvaluemasktable) + (dst_negative_criterion_inverseleftvaluemasktable))) /\ (exists ge_balance_positive_criterion_inverseleftvaluemasktableentryvalue ge_balance_negative_criterion_inverseleftvaluemasktableentryvalue. (((((dst_value_criterion_inverseleftvaluemasktable) = 2 * (ge_balance_positive_criterion_inverseleftvaluemasktableentryvalue) /\ (ge_balance_negative_criterion_inverseleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemasktableentryvaluedecode. (((dst_value_criterion_inverseleftvaluemasktable) = 2 * ge_signed_half_criterion_inverseleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluemasktableentryvalue) = S ge_signed_half_criterion_inverseleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_criterion_inverseleftvaluemasktable) + ge_balance_negative_criterion_inverseleftvaluemasktableentryvalue = (dst_negative_criterion_inverseleftvaluemasktable) + ge_balance_positive_criterion_inverseleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_criterion_inverseleftvaluemask dc_value_criterion_inverseleftvaluemask. (exists pvs_le_gap_criterion_inverseleftvaluemaskdomain. pvs_le_gap_criterion_inverseleftvaluemaskdomain + (dc_index_criterion_inverseleftvaluemask) = (dc_input_criterion_inverseleft)) -> (exists dst_positive_code_criterion_inverseleftvaluemasklookup dst_positive_scale_criterion_inverseleftvaluemasklookup dst_negative_code_criterion_inverseleftvaluemasklookup dst_negative_scale_criterion_inverseleftvaluemasklookup dst_positive_criterion_inverseleftvaluemasklookup dst_negative_criterion_inverseleftvaluemasklookup. (((dc_mask_criterion_inverseleftvalue) = (((((dst_positive_code_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)))) * S ((((dst_positive_code_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)))) + ((((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_criterion_inverseleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemasklookuppositive. ff_h_pvs_criterion_inverseleftvaluemasklookuppositive + S (dst_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_positive_scale_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_criterion_inverseleftvaluemasklookuppositive. dst_positive_code_criterion_inverseleftvaluemasklookup = ff_q_pvs_criterion_inverseleftvaluemasklookuppositive * S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_positive_scale_criterion_inverseleftvaluemasklookup) + (dst_positive_criterion_inverseleftvaluemasklookup))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemasklookupnegative. ff_h_pvs_criterion_inverseleftvaluemasklookupnegative + S (dst_negative_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_negative_scale_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_criterion_inverseleftvaluemasklookupnegative. dst_negative_code_criterion_inverseleftvaluemasklookup = ff_q_pvs_criterion_inverseleftvaluemasklookupnegative * S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_negative_scale_criterion_inverseleftvaluemasklookup) + (dst_negative_criterion_inverseleftvaluemasklookup))) /\ (exists ge_balance_positive_criterion_inverseleftvaluemasklookupvalue ge_balance_negative_criterion_inverseleftvaluemasklookupvalue. (((((dc_value_criterion_inverseleftvaluemask) = 2 * (ge_balance_positive_criterion_inverseleftvaluemasklookupvalue) /\ (ge_balance_negative_criterion_inverseleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemasklookupvaluedecode. (((dc_value_criterion_inverseleftvaluemask) = 2 * ge_signed_half_criterion_inverseleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluemasklookupvalue) = S ge_signed_half_criterion_inverseleftvaluemasklookupvaluedecode))) /\ ((dst_positive_criterion_inverseleftvaluemasklookup) + ge_balance_negative_criterion_inverseleftvaluemasklookupvalue = (dst_negative_criterion_inverseleftvaluemasklookup) + ge_balance_positive_criterion_inverseleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_criterion_inverseleftvaluemask)=0)) /\ (exists dc_quotient_criterion_inverseleftvaluemaskentry dc_left_criterion_inverseleftvaluemaskentry dc_right_criterion_inverseleftvaluemaskentry. (((dc_input_criterion_inverseleft)=(dc_index_criterion_inverseleftvaluemask)*dc_quotient_criterion_inverseleftvaluemaskentry) /\ (((exists dst_positive_code_criterion_inverseleftvaluemaskentryleft dst_positive_scale_criterion_inverseleftvaluemaskentryleft dst_negative_code_criterion_inverseleftvaluemaskentryleft dst_negative_scale_criterion_inverseleftvaluemaskentryleft dst_positive_criterion_inverseleftvaluemaskentryleft dst_negative_criterion_inverseleftvaluemaskentryleft. (((F) = (((((dst_positive_code_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)))) * S ((((dst_positive_code_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)))) + ((((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_criterion_inverseleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemaskentryleftpositive. ff_h_pvs_criterion_inverseleftvaluemaskentryleftpositive + S (dst_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_positive_scale_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_criterion_inverseleftvaluemaskentryleftpositive. dst_positive_code_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_criterion_inverseleftvaluemaskentryleftpositive * S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_positive_scale_criterion_inverseleftvaluemaskentryleft) + (dst_positive_criterion_inverseleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemaskentryleftnegative. ff_h_pvs_criterion_inverseleftvaluemaskentryleftnegative + S (dst_negative_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_negative_scale_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_criterion_inverseleftvaluemaskentryleftnegative. dst_negative_code_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_criterion_inverseleftvaluemaskentryleftnegative * S ((S (dc_index_criterion_inverseleftvaluemask)) * dst_negative_scale_criterion_inverseleftvaluemaskentryleft) + (dst_negative_criterion_inverseleftvaluemaskentryleft))) /\ (exists ge_balance_positive_criterion_inverseleftvaluemaskentryleftvalue ge_balance_negative_criterion_inverseleftvaluemaskentryleftvalue. (((((dc_left_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_criterion_inverseleftvaluemaskentryleftvalue) /\ (ge_balance_negative_criterion_inverseleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryleftvaluedecode. (((dc_left_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluemaskentryleftvalue) = S ge_signed_half_criterion_inverseleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_negative_criterion_inverseleftvaluemaskentryleftvalue = (dst_negative_criterion_inverseleftvaluemaskentryleft) + ge_balance_positive_criterion_inverseleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_criterion_inverseleftvaluemaskentryright dst_positive_scale_criterion_inverseleftvaluemaskentryright dst_negative_code_criterion_inverseleftvaluemaskentryright dst_negative_scale_criterion_inverseleftvaluemaskentryright dst_positive_criterion_inverseleftvaluemaskentryright dst_negative_criterion_inverseleftvaluemaskentryright. (((G) = (((((dst_positive_code_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)))) * S ((((dst_positive_code_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)))) + ((((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_criterion_inverseleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemaskentryrightpositive. ff_h_pvs_criterion_inverseleftvaluemaskentryrightpositive + S (dst_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_criterion_inverseleftvaluemaskentryrightpositive. dst_positive_code_criterion_inverseleftvaluemaskentryright = ff_q_pvs_criterion_inverseleftvaluemaskentryrightpositive * S ((S (dc_quotient_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_criterion_inverseleftvaluemaskentryright) + (dst_positive_criterion_inverseleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_criterion_inverseleftvaluemaskentryrightnegative. ff_h_pvs_criterion_inverseleftvaluemaskentryrightnegative + S (dst_negative_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_criterion_inverseleftvaluemaskentryrightnegative. dst_negative_code_criterion_inverseleftvaluemaskentryright = ff_q_pvs_criterion_inverseleftvaluemaskentryrightnegative * S ((S (dc_quotient_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_criterion_inverseleftvaluemaskentryright) + (dst_negative_criterion_inverseleftvaluemaskentryright))) /\ (exists ge_balance_positive_criterion_inverseleftvaluemaskentryrightvalue ge_balance_negative_criterion_inverseleftvaluemaskentryrightvalue. (((((dc_right_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_criterion_inverseleftvaluemaskentryrightvalue) /\ (ge_balance_negative_criterion_inverseleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryrightvaluedecode. (((dc_right_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluemaskentryrightvalue) = S ge_signed_half_criterion_inverseleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_negative_criterion_inverseleftvaluemaskentryrightvalue = (dst_negative_criterion_inverseleftvaluemaskentryright) + ge_balance_positive_criterion_inverseleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_criterion_inverseleftvaluemaskentryproduct sto_an_criterion_inverseleftvaluemaskentryproduct sto_bp_criterion_inverseleftvaluemaskentryproduct sto_bn_criterion_inverseleftvaluemaskentryproduct sto_cp_criterion_inverseleftvaluemaskentryproduct sto_cn_criterion_inverseleftvaluemaskentryproduct. (((((dc_left_criterion_inverseleftvaluemaskentry) = 2 * (sto_ap_criterion_inverseleftvaluemaskentryproduct) /\ (sto_an_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryproductleft. (((dc_left_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryproductleft + 1 /\ (sto_ap_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_an_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_criterion_inverseleftvaluemaskentryproductleft))) /\ ((((((dc_right_criterion_inverseleftvaluemaskentry) = 2 * (sto_bp_criterion_inverseleftvaluemaskentryproduct) /\ (sto_bn_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryproductright. (((dc_right_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryproductright + 1 /\ (sto_bp_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_bn_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_criterion_inverseleftvaluemaskentryproductright))) /\ ((((((dc_value_criterion_inverseleftvaluemask) = 2 * (sto_cp_criterion_inverseleftvaluemaskentryproduct) /\ (sto_cn_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluemaskentryproductoutput. (((dc_value_criterion_inverseleftvaluemask) = 2 * ge_signed_half_criterion_inverseleftvaluemaskentryproductoutput + 1 /\ (sto_cp_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_cn_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_criterion_inverseleftvaluemaskentryproductoutput))) /\ ((sto_ap_criterion_inverseleftvaluemaskentryproduct * sto_bp_criterion_inverseleftvaluemaskentryproduct + sto_an_criterion_inverseleftvaluemaskentryproduct * sto_bn_criterion_inverseleftvaluemaskentryproduct) + sto_cn_criterion_inverseleftvaluemaskentryproduct = (sto_ap_criterion_inverseleftvaluemaskentryproduct * sto_bn_criterion_inverseleftvaluemaskentryproduct + sto_an_criterion_inverseleftvaluemaskentryproduct * sto_bp_criterion_inverseleftvaluemaskentryproduct) + sto_cp_criterion_inverseleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_criterion_inverseleftvaluemask)=0 \/ ~(exists pvs_factor_criterion_inverseleftvaluemaskentrynondivisor. (dc_input_criterion_inverseleft) = (dc_index_criterion_inverseleftvaluemask) * pvs_factor_criterion_inverseleftvaluemaskentrynondivisor)) /\ ((dc_value_criterion_inverseleftvaluemask)=0))))))) /\ (exists dst_positive_code_criterion_inverseleftvaluefold dst_positive_scale_criterion_inverseleftvaluefold dst_negative_code_criterion_inverseleftvaluefold dst_negative_scale_criterion_inverseleftvaluefold dst_positive_sum_criterion_inverseleftvaluefold dst_negative_sum_criterion_inverseleftvaluefold. (((dc_mask_criterion_inverseleftvalue) = (((((dst_positive_code_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold)) * S ((dst_positive_code_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold)) + ((dst_positive_scale_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold))) + (((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) * S ((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) + ((dst_negative_scale_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)))) * S ((((dst_positive_code_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold)) * S ((dst_positive_code_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold)) + ((dst_positive_scale_criterion_inverseleftvaluefold) + (dst_positive_scale_criterion_inverseleftvaluefold))) + (((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) * S ((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) + ((dst_negative_scale_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)))) + ((((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) * S ((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) + ((dst_negative_scale_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold))) + (((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) * S ((dst_negative_code_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)) + ((dst_negative_scale_criterion_inverseleftvaluefold) + (dst_negative_scale_criterion_inverseleftvaluefold)))))) /\ (((exists fs_u_dst_criterion_inverseleftvaluefoldpositive fs_v_dst_criterion_inverseleftvaluefoldpositive. ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_start. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_start. fs_u_dst_criterion_inverseleftvaluefoldpositive = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_criterion_inverseleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_terminal. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_terminal + S (dst_positive_sum_criterion_inverseleftvaluefold) = S ((S (S (dc_input_criterion_inverseleft))) * fs_v_dst_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_terminal. fs_u_dst_criterion_inverseleftvaluefoldpositive = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_criterion_inverseleft))) * fs_v_dst_criterion_inverseleftvaluefoldpositive) + (dst_positive_sum_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps. (exists fs_lt_dst_criterion_inverseleftvaluefoldpositive_body_steps_bound. fs_lt_dst_criterion_inverseleftvaluefoldpositive_body_steps_bound + S fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps = S (dc_input_criterion_inverseleft)) -> exists fs_a_dst_criterion_inverseleftvaluefoldpositive_body_steps fs_r_dst_criterion_inverseleftvaluefoldpositive_body_steps fs_s_dst_criterion_inverseleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_summand. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_summand. dst_positive_code_criterion_inverseleftvaluefold = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_criterion_inverseleftvaluefold) + (fs_a_dst_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_u_dst_criterion_inverseleftvaluefoldpositive = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldpositive) + (fs_r_dst_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_h_dst_criterion_inverseleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_u_dst_criterion_inverseleftvaluefoldpositive = fs_q_dst_criterion_inverseleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldpositive) + (fs_s_dst_criterion_inverseleftvaluefoldpositive_body_steps))) /\ fs_s_dst_criterion_inverseleftvaluefoldpositive_body_steps = fs_r_dst_criterion_inverseleftvaluefoldpositive_body_steps + fs_a_dst_criterion_inverseleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_criterion_inverseleftvaluefoldnegative fs_v_dst_criterion_inverseleftvaluefoldnegative. ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_start. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_start. fs_u_dst_criterion_inverseleftvaluefoldnegative = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_criterion_inverseleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_terminal. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_terminal + S (dst_negative_sum_criterion_inverseleftvaluefold) = S ((S (S (dc_input_criterion_inverseleft))) * fs_v_dst_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_terminal. fs_u_dst_criterion_inverseleftvaluefoldnegative = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_criterion_inverseleft))) * fs_v_dst_criterion_inverseleftvaluefoldnegative) + (dst_negative_sum_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps. (exists fs_lt_dst_criterion_inverseleftvaluefoldnegative_body_steps_bound. fs_lt_dst_criterion_inverseleftvaluefoldnegative_body_steps_bound + S fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps = S (dc_input_criterion_inverseleft)) -> exists fs_a_dst_criterion_inverseleftvaluefoldnegative_body_steps fs_r_dst_criterion_inverseleftvaluefoldnegative_body_steps fs_s_dst_criterion_inverseleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_summand. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_summand. dst_negative_code_criterion_inverseleftvaluefold = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_criterion_inverseleftvaluefold) + (fs_a_dst_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_u_dst_criterion_inverseleftvaluefoldnegative = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldnegative) + (fs_r_dst_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_h_dst_criterion_inverseleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_u_dst_criterion_inverseleftvaluefoldnegative = fs_q_dst_criterion_inverseleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverseleftvaluefoldnegative) + (fs_s_dst_criterion_inverseleftvaluefoldnegative_body_steps))) /\ fs_s_dst_criterion_inverseleftvaluefoldnegative_body_steps = fs_r_dst_criterion_inverseleftvaluefoldnegative_body_steps + fs_a_dst_criterion_inverseleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_criterion_inverseleftvaluefoldresult ge_balance_negative_criterion_inverseleftvaluefoldresult. (((((dc_output_criterion_inverseleft) = 2 * (ge_balance_positive_criterion_inverseleftvaluefoldresult) /\ (ge_balance_negative_criterion_inverseleftvaluefoldresult) = 0) \/ exists ge_signed_half_criterion_inverseleftvaluefoldresultdecode. (((dc_output_criterion_inverseleft) = 2 * ge_signed_half_criterion_inverseleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_criterion_inverseleftvaluefoldresult) = 0) /\ (ge_balance_negative_criterion_inverseleftvaluefoldresult) = S ge_signed_half_criterion_inverseleftvaluefoldresultdecode))) /\ ((dst_positive_sum_criterion_inverseleftvaluefold) + ge_balance_negative_criterion_inverseleftvaluefoldresult = (dst_negative_sum_criterion_inverseleftvaluefold) + ge_balance_positive_criterion_inverseleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_criterion_inverserightleft dst_positive_scale_criterion_inverserightleft dst_negative_code_criterion_inverserightleft dst_negative_scale_criterion_inverserightleft. (((G) = (((((dst_positive_code_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft)) * S ((dst_positive_code_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft)) + ((dst_positive_scale_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft))) + (((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) * S ((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) + ((dst_negative_scale_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)))) * S ((((dst_positive_code_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft)) * S ((dst_positive_code_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft)) + ((dst_positive_scale_criterion_inverserightleft) + (dst_positive_scale_criterion_inverserightleft))) + (((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) * S ((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) + ((dst_negative_scale_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)))) + ((((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) * S ((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) + ((dst_negative_scale_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft))) + (((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) * S ((dst_negative_code_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)) + ((dst_negative_scale_criterion_inverserightleft) + (dst_negative_scale_criterion_inverserightleft)))))) /\ (forall dst_index_criterion_inverserightleft. (exists pvs_le_gap_criterion_inverserightleftdomain. pvs_le_gap_criterion_inverserightleftdomain + (dst_index_criterion_inverserightleft) = (N)) -> exists dst_positive_criterion_inverserightleft dst_negative_criterion_inverserightleft dst_value_criterion_inverserightleft. ((((exists ff_h_pvs_criterion_inverserightleftentrypositive. ff_h_pvs_criterion_inverserightleftentrypositive + S (dst_positive_criterion_inverserightleft) = S ((S (dst_index_criterion_inverserightleft)) * dst_positive_scale_criterion_inverserightleft)) /\ exists ff_q_pvs_criterion_inverserightleftentrypositive. dst_positive_code_criterion_inverserightleft = ff_q_pvs_criterion_inverserightleftentrypositive * S ((S (dst_index_criterion_inverserightleft)) * dst_positive_scale_criterion_inverserightleft) + (dst_positive_criterion_inverserightleft))) /\ (((((exists ff_h_pvs_criterion_inverserightleftentrynegative. ff_h_pvs_criterion_inverserightleftentrynegative + S (dst_negative_criterion_inverserightleft) = S ((S (dst_index_criterion_inverserightleft)) * dst_negative_scale_criterion_inverserightleft)) /\ exists ff_q_pvs_criterion_inverserightleftentrynegative. dst_negative_code_criterion_inverserightleft = ff_q_pvs_criterion_inverserightleftentrynegative * S ((S (dst_index_criterion_inverserightleft)) * dst_negative_scale_criterion_inverserightleft) + (dst_negative_criterion_inverserightleft))) /\ (exists ge_balance_positive_criterion_inverserightleftentryvalue ge_balance_negative_criterion_inverserightleftentryvalue. (((((dst_value_criterion_inverserightleft) = 2 * (ge_balance_positive_criterion_inverserightleftentryvalue) /\ (ge_balance_negative_criterion_inverserightleftentryvalue) = 0) \/ exists ge_signed_half_criterion_inverserightleftentryvaluedecode. (((dst_value_criterion_inverserightleft) = 2 * ge_signed_half_criterion_inverserightleftentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightleftentryvalue) = 0) /\ (ge_balance_negative_criterion_inverserightleftentryvalue) = S ge_signed_half_criterion_inverserightleftentryvaluedecode))) /\ ((dst_positive_criterion_inverserightleft) + ge_balance_negative_criterion_inverserightleftentryvalue = (dst_negative_criterion_inverserightleft) + ge_balance_positive_criterion_inverserightleftentryvalue))))))))) /\ (((exists dst_positive_code_criterion_inverserightright dst_positive_scale_criterion_inverserightright dst_negative_code_criterion_inverserightright dst_negative_scale_criterion_inverserightright. (((F) = (((((dst_positive_code_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright)) * S ((dst_positive_code_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright)) + ((dst_positive_scale_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright))) + (((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) * S ((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) + ((dst_negative_scale_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)))) * S ((((dst_positive_code_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright)) * S ((dst_positive_code_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright)) + ((dst_positive_scale_criterion_inverserightright) + (dst_positive_scale_criterion_inverserightright))) + (((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) * S ((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) + ((dst_negative_scale_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)))) + ((((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) * S ((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) + ((dst_negative_scale_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright))) + (((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) * S ((dst_negative_code_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)) + ((dst_negative_scale_criterion_inverserightright) + (dst_negative_scale_criterion_inverserightright)))))) /\ (forall dst_index_criterion_inverserightright. (exists pvs_le_gap_criterion_inverserightrightdomain. pvs_le_gap_criterion_inverserightrightdomain + (dst_index_criterion_inverserightright) = (N)) -> exists dst_positive_criterion_inverserightright dst_negative_criterion_inverserightright dst_value_criterion_inverserightright. ((((exists ff_h_pvs_criterion_inverserightrightentrypositive. ff_h_pvs_criterion_inverserightrightentrypositive + S (dst_positive_criterion_inverserightright) = S ((S (dst_index_criterion_inverserightright)) * dst_positive_scale_criterion_inverserightright)) /\ exists ff_q_pvs_criterion_inverserightrightentrypositive. dst_positive_code_criterion_inverserightright = ff_q_pvs_criterion_inverserightrightentrypositive * S ((S (dst_index_criterion_inverserightright)) * dst_positive_scale_criterion_inverserightright) + (dst_positive_criterion_inverserightright))) /\ (((((exists ff_h_pvs_criterion_inverserightrightentrynegative. ff_h_pvs_criterion_inverserightrightentrynegative + S (dst_negative_criterion_inverserightright) = S ((S (dst_index_criterion_inverserightright)) * dst_negative_scale_criterion_inverserightright)) /\ exists ff_q_pvs_criterion_inverserightrightentrynegative. dst_negative_code_criterion_inverserightright = ff_q_pvs_criterion_inverserightrightentrynegative * S ((S (dst_index_criterion_inverserightright)) * dst_negative_scale_criterion_inverserightright) + (dst_negative_criterion_inverserightright))) /\ (exists ge_balance_positive_criterion_inverserightrightentryvalue ge_balance_negative_criterion_inverserightrightentryvalue. (((((dst_value_criterion_inverserightright) = 2 * (ge_balance_positive_criterion_inverserightrightentryvalue) /\ (ge_balance_negative_criterion_inverserightrightentryvalue) = 0) \/ exists ge_signed_half_criterion_inverserightrightentryvaluedecode. (((dst_value_criterion_inverserightright) = 2 * ge_signed_half_criterion_inverserightrightentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightrightentryvalue) = 0) /\ (ge_balance_negative_criterion_inverserightrightentryvalue) = S ge_signed_half_criterion_inverserightrightentryvaluedecode))) /\ ((dst_positive_criterion_inverserightright) + ge_balance_negative_criterion_inverserightrightentryvalue = (dst_negative_criterion_inverserightright) + ge_balance_positive_criterion_inverserightrightentryvalue))))))))) /\ (((exists dst_positive_code_criterion_inverserighttable dst_positive_scale_criterion_inverserighttable dst_negative_code_criterion_inverserighttable dst_negative_scale_criterion_inverserighttable. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable)) * S ((dst_positive_code_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable)) + ((dst_positive_scale_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable))) + (((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) * S ((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) + ((dst_negative_scale_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)))) * S ((((dst_positive_code_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable)) * S ((dst_positive_code_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable)) + ((dst_positive_scale_criterion_inverserighttable) + (dst_positive_scale_criterion_inverserighttable))) + (((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) * S ((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) + ((dst_negative_scale_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)))) + ((((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) * S ((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) + ((dst_negative_scale_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable))) + (((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) * S ((dst_negative_code_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)) + ((dst_negative_scale_criterion_inverserighttable) + (dst_negative_scale_criterion_inverserighttable)))))) /\ (forall dst_index_criterion_inverserighttable. (exists pvs_le_gap_criterion_inverserighttabledomain. pvs_le_gap_criterion_inverserighttabledomain + (dst_index_criterion_inverserighttable) = (N)) -> exists dst_positive_criterion_inverserighttable dst_negative_criterion_inverserighttable dst_value_criterion_inverserighttable. ((((exists ff_h_pvs_criterion_inverserighttableentrypositive. ff_h_pvs_criterion_inverserighttableentrypositive + S (dst_positive_criterion_inverserighttable) = S ((S (dst_index_criterion_inverserighttable)) * dst_positive_scale_criterion_inverserighttable)) /\ exists ff_q_pvs_criterion_inverserighttableentrypositive. dst_positive_code_criterion_inverserighttable = ff_q_pvs_criterion_inverserighttableentrypositive * S ((S (dst_index_criterion_inverserighttable)) * dst_positive_scale_criterion_inverserighttable) + (dst_positive_criterion_inverserighttable))) /\ (((((exists ff_h_pvs_criterion_inverserighttableentrynegative. ff_h_pvs_criterion_inverserighttableentrynegative + S (dst_negative_criterion_inverserighttable) = S ((S (dst_index_criterion_inverserighttable)) * dst_negative_scale_criterion_inverserighttable)) /\ exists ff_q_pvs_criterion_inverserighttableentrynegative. dst_negative_code_criterion_inverserighttable = ff_q_pvs_criterion_inverserighttableentrynegative * S ((S (dst_index_criterion_inverserighttable)) * dst_negative_scale_criterion_inverserighttable) + (dst_negative_criterion_inverserighttable))) /\ (exists ge_balance_positive_criterion_inverserighttableentryvalue ge_balance_negative_criterion_inverserighttableentryvalue. (((((dst_value_criterion_inverserighttable) = 2 * (ge_balance_positive_criterion_inverserighttableentryvalue) /\ (ge_balance_negative_criterion_inverserighttableentryvalue) = 0) \/ exists ge_signed_half_criterion_inverserighttableentryvaluedecode. (((dst_value_criterion_inverserighttable) = 2 * ge_signed_half_criterion_inverserighttableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserighttableentryvalue) = 0) /\ (ge_balance_negative_criterion_inverserighttableentryvalue) = S ge_signed_half_criterion_inverserighttableentryvaluedecode))) /\ ((dst_positive_criterion_inverserighttable) + ge_balance_negative_criterion_inverserighttableentryvalue = (dst_negative_criterion_inverserighttable) + ge_balance_positive_criterion_inverserighttableentryvalue))))))))) /\ (forall dc_input_criterion_inverseright dc_output_criterion_inverseright. ~(dc_input_criterion_inverseright=0) -> (exists pvs_le_gap_criterion_inverserightdomain. pvs_le_gap_criterion_inverserightdomain + (dc_input_criterion_inverseright) = (N)) -> (exists dst_positive_code_criterion_inverserightlookup dst_positive_scale_criterion_inverserightlookup dst_negative_code_criterion_inverserightlookup dst_negative_scale_criterion_inverserightlookup dst_positive_criterion_inverserightlookup dst_negative_criterion_inverserightlookup. (((di_delta_criterion_inverse) = (((((dst_positive_code_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup)) * S ((dst_positive_code_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup)) + ((dst_positive_scale_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup))) + (((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) * S ((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) + ((dst_negative_scale_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)))) * S ((((dst_positive_code_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup)) * S ((dst_positive_code_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup)) + ((dst_positive_scale_criterion_inverserightlookup) + (dst_positive_scale_criterion_inverserightlookup))) + (((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) * S ((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) + ((dst_negative_scale_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)))) + ((((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) * S ((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) + ((dst_negative_scale_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup))) + (((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) * S ((dst_negative_code_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)) + ((dst_negative_scale_criterion_inverserightlookup) + (dst_negative_scale_criterion_inverserightlookup)))))) /\ (((((exists ff_h_pvs_criterion_inverserightlookuppositive. ff_h_pvs_criterion_inverserightlookuppositive + S (dst_positive_criterion_inverserightlookup) = S ((S (dc_input_criterion_inverseright)) * dst_positive_scale_criterion_inverserightlookup)) /\ exists ff_q_pvs_criterion_inverserightlookuppositive. dst_positive_code_criterion_inverserightlookup = ff_q_pvs_criterion_inverserightlookuppositive * S ((S (dc_input_criterion_inverseright)) * dst_positive_scale_criterion_inverserightlookup) + (dst_positive_criterion_inverserightlookup))) /\ (((((exists ff_h_pvs_criterion_inverserightlookupnegative. ff_h_pvs_criterion_inverserightlookupnegative + S (dst_negative_criterion_inverserightlookup) = S ((S (dc_input_criterion_inverseright)) * dst_negative_scale_criterion_inverserightlookup)) /\ exists ff_q_pvs_criterion_inverserightlookupnegative. dst_negative_code_criterion_inverserightlookup = ff_q_pvs_criterion_inverserightlookupnegative * S ((S (dc_input_criterion_inverseright)) * dst_negative_scale_criterion_inverserightlookup) + (dst_negative_criterion_inverserightlookup))) /\ (exists ge_balance_positive_criterion_inverserightlookupvalue ge_balance_negative_criterion_inverserightlookupvalue. (((((dc_output_criterion_inverseright) = 2 * (ge_balance_positive_criterion_inverserightlookupvalue) /\ (ge_balance_negative_criterion_inverserightlookupvalue) = 0) \/ exists ge_signed_half_criterion_inverserightlookupvaluedecode. (((dc_output_criterion_inverseright) = 2 * ge_signed_half_criterion_inverserightlookupvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightlookupvalue) = 0) /\ (ge_balance_negative_criterion_inverserightlookupvalue) = S ge_signed_half_criterion_inverserightlookupvaluedecode))) /\ ((dst_positive_criterion_inverserightlookup) + ge_balance_negative_criterion_inverserightlookupvalue = (dst_negative_criterion_inverserightlookup) + ge_balance_positive_criterion_inverserightlookupvalue))))))))) -> (((~((dc_input_criterion_inverseright)=0)) /\ (exists dc_mask_criterion_inverserightvalue. ((((exists dst_positive_code_criterion_inverserightvaluemasktable dst_positive_scale_criterion_inverserightvaluemasktable dst_negative_code_criterion_inverserightvaluemasktable dst_negative_scale_criterion_inverserightvaluemasktable. (((dc_mask_criterion_inverserightvalue) = (((((dst_positive_code_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable))) + (((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)))) * S ((((dst_positive_code_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_criterion_inverserightvaluemasktable) + (dst_positive_scale_criterion_inverserightvaluemasktable))) + (((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)))) + ((((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable))) + (((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_scale_criterion_inverserightvaluemasktable)))))) /\ (forall dst_index_criterion_inverserightvaluemasktable. (exists pvs_le_gap_criterion_inverserightvaluemasktabledomain. pvs_le_gap_criterion_inverserightvaluemasktabledomain + (dst_index_criterion_inverserightvaluemasktable) = (dc_input_criterion_inverseright)) -> exists dst_positive_criterion_inverserightvaluemasktable dst_negative_criterion_inverserightvaluemasktable dst_value_criterion_inverserightvaluemasktable. ((((exists ff_h_pvs_criterion_inverserightvaluemasktableentrypositive. ff_h_pvs_criterion_inverserightvaluemasktableentrypositive + S (dst_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_criterion_inverserightvaluemasktable)) * dst_positive_scale_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_criterion_inverserightvaluemasktableentrypositive. dst_positive_code_criterion_inverserightvaluemasktable = ff_q_pvs_criterion_inverserightvaluemasktableentrypositive * S ((S (dst_index_criterion_inverserightvaluemasktable)) * dst_positive_scale_criterion_inverserightvaluemasktable) + (dst_positive_criterion_inverserightvaluemasktable))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemasktableentrynegative. ff_h_pvs_criterion_inverserightvaluemasktableentrynegative + S (dst_negative_criterion_inverserightvaluemasktable) = S ((S (dst_index_criterion_inverserightvaluemasktable)) * dst_negative_scale_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_criterion_inverserightvaluemasktableentrynegative. dst_negative_code_criterion_inverserightvaluemasktable = ff_q_pvs_criterion_inverserightvaluemasktableentrynegative * S ((S (dst_index_criterion_inverserightvaluemasktable)) * dst_negative_scale_criterion_inverserightvaluemasktable) + (dst_negative_criterion_inverserightvaluemasktable))) /\ (exists ge_balance_positive_criterion_inverserightvaluemasktableentryvalue ge_balance_negative_criterion_inverserightvaluemasktableentryvalue. (((((dst_value_criterion_inverserightvaluemasktable) = 2 * (ge_balance_positive_criterion_inverserightvaluemasktableentryvalue) /\ (ge_balance_negative_criterion_inverserightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemasktableentryvaluedecode. (((dst_value_criterion_inverserightvaluemasktable) = 2 * ge_signed_half_criterion_inverserightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_criterion_inverserightvaluemasktableentryvalue) = S ge_signed_half_criterion_inverserightvaluemasktableentryvaluedecode))) /\ ((dst_positive_criterion_inverserightvaluemasktable) + ge_balance_negative_criterion_inverserightvaluemasktableentryvalue = (dst_negative_criterion_inverserightvaluemasktable) + ge_balance_positive_criterion_inverserightvaluemasktableentryvalue))))))))) /\ (forall dc_index_criterion_inverserightvaluemask dc_value_criterion_inverserightvaluemask. (exists pvs_le_gap_criterion_inverserightvaluemaskdomain. pvs_le_gap_criterion_inverserightvaluemaskdomain + (dc_index_criterion_inverserightvaluemask) = (dc_input_criterion_inverseright)) -> (exists dst_positive_code_criterion_inverserightvaluemasklookup dst_positive_scale_criterion_inverserightvaluemasklookup dst_negative_code_criterion_inverserightvaluemasklookup dst_negative_scale_criterion_inverserightvaluemasklookup dst_positive_criterion_inverserightvaluemasklookup dst_negative_criterion_inverserightvaluemasklookup. (((dc_mask_criterion_inverserightvalue) = (((((dst_positive_code_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)))) * S ((((dst_positive_code_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_criterion_inverserightvaluemasklookup) + (dst_positive_scale_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)))) + ((((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_scale_criterion_inverserightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemasklookuppositive. ff_h_pvs_criterion_inverserightvaluemasklookuppositive + S (dst_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_criterion_inverserightvaluemask)) * dst_positive_scale_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_criterion_inverserightvaluemasklookuppositive. dst_positive_code_criterion_inverserightvaluemasklookup = ff_q_pvs_criterion_inverserightvaluemasklookuppositive * S ((S (dc_index_criterion_inverserightvaluemask)) * dst_positive_scale_criterion_inverserightvaluemasklookup) + (dst_positive_criterion_inverserightvaluemasklookup))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemasklookupnegative. ff_h_pvs_criterion_inverserightvaluemasklookupnegative + S (dst_negative_criterion_inverserightvaluemasklookup) = S ((S (dc_index_criterion_inverserightvaluemask)) * dst_negative_scale_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_criterion_inverserightvaluemasklookupnegative. dst_negative_code_criterion_inverserightvaluemasklookup = ff_q_pvs_criterion_inverserightvaluemasklookupnegative * S ((S (dc_index_criterion_inverserightvaluemask)) * dst_negative_scale_criterion_inverserightvaluemasklookup) + (dst_negative_criterion_inverserightvaluemasklookup))) /\ (exists ge_balance_positive_criterion_inverserightvaluemasklookupvalue ge_balance_negative_criterion_inverserightvaluemasklookupvalue. (((((dc_value_criterion_inverserightvaluemask) = 2 * (ge_balance_positive_criterion_inverserightvaluemasklookupvalue) /\ (ge_balance_negative_criterion_inverserightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemasklookupvaluedecode. (((dc_value_criterion_inverserightvaluemask) = 2 * ge_signed_half_criterion_inverserightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_criterion_inverserightvaluemasklookupvalue) = S ge_signed_half_criterion_inverserightvaluemasklookupvaluedecode))) /\ ((dst_positive_criterion_inverserightvaluemasklookup) + ge_balance_negative_criterion_inverserightvaluemasklookupvalue = (dst_negative_criterion_inverserightvaluemasklookup) + ge_balance_positive_criterion_inverserightvaluemasklookupvalue))))))))) -> ((((~((dc_index_criterion_inverserightvaluemask)=0)) /\ (exists dc_quotient_criterion_inverserightvaluemaskentry dc_left_criterion_inverserightvaluemaskentry dc_right_criterion_inverserightvaluemaskentry. (((dc_input_criterion_inverseright)=(dc_index_criterion_inverserightvaluemask)*dc_quotient_criterion_inverserightvaluemaskentry) /\ (((exists dst_positive_code_criterion_inverserightvaluemaskentryleft dst_positive_scale_criterion_inverserightvaluemaskentryleft dst_negative_code_criterion_inverserightvaluemaskentryleft dst_negative_scale_criterion_inverserightvaluemaskentryleft dst_positive_criterion_inverserightvaluemaskentryleft dst_negative_criterion_inverserightvaluemaskentryleft. (((G) = (((((dst_positive_code_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)))) * S ((((dst_positive_code_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)))) + ((((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_criterion_inverserightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemaskentryleftpositive. ff_h_pvs_criterion_inverserightvaluemaskentryleftpositive + S (dst_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_criterion_inverserightvaluemask)) * dst_positive_scale_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_criterion_inverserightvaluemaskentryleftpositive. dst_positive_code_criterion_inverserightvaluemaskentryleft = ff_q_pvs_criterion_inverserightvaluemaskentryleftpositive * S ((S (dc_index_criterion_inverserightvaluemask)) * dst_positive_scale_criterion_inverserightvaluemaskentryleft) + (dst_positive_criterion_inverserightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemaskentryleftnegative. ff_h_pvs_criterion_inverserightvaluemaskentryleftnegative + S (dst_negative_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_criterion_inverserightvaluemask)) * dst_negative_scale_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_criterion_inverserightvaluemaskentryleftnegative. dst_negative_code_criterion_inverserightvaluemaskentryleft = ff_q_pvs_criterion_inverserightvaluemaskentryleftnegative * S ((S (dc_index_criterion_inverserightvaluemask)) * dst_negative_scale_criterion_inverserightvaluemaskentryleft) + (dst_negative_criterion_inverserightvaluemaskentryleft))) /\ (exists ge_balance_positive_criterion_inverserightvaluemaskentryleftvalue ge_balance_negative_criterion_inverserightvaluemaskentryleftvalue. (((((dc_left_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_criterion_inverserightvaluemaskentryleftvalue) /\ (ge_balance_negative_criterion_inverserightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryleftvaluedecode. (((dc_left_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_criterion_inverserightvaluemaskentryleftvalue) = S ge_signed_half_criterion_inverserightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_negative_criterion_inverserightvaluemaskentryleftvalue = (dst_negative_criterion_inverserightvaluemaskentryleft) + ge_balance_positive_criterion_inverserightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_criterion_inverserightvaluemaskentryright dst_positive_scale_criterion_inverserightvaluemaskentryright dst_negative_code_criterion_inverserightvaluemaskentryright dst_negative_scale_criterion_inverserightvaluemaskentryright dst_positive_criterion_inverserightvaluemaskentryright dst_negative_criterion_inverserightvaluemaskentryright. (((F) = (((((dst_positive_code_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)))) * S ((((dst_positive_code_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)))) + ((((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_criterion_inverserightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemaskentryrightpositive. ff_h_pvs_criterion_inverserightvaluemaskentryrightpositive + S (dst_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_criterion_inverserightvaluemaskentry)) * dst_positive_scale_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_criterion_inverserightvaluemaskentryrightpositive. dst_positive_code_criterion_inverserightvaluemaskentryright = ff_q_pvs_criterion_inverserightvaluemaskentryrightpositive * S ((S (dc_quotient_criterion_inverserightvaluemaskentry)) * dst_positive_scale_criterion_inverserightvaluemaskentryright) + (dst_positive_criterion_inverserightvaluemaskentryright))) /\ (((((exists ff_h_pvs_criterion_inverserightvaluemaskentryrightnegative. ff_h_pvs_criterion_inverserightvaluemaskentryrightnegative + S (dst_negative_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_criterion_inverserightvaluemaskentry)) * dst_negative_scale_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_criterion_inverserightvaluemaskentryrightnegative. dst_negative_code_criterion_inverserightvaluemaskentryright = ff_q_pvs_criterion_inverserightvaluemaskentryrightnegative * S ((S (dc_quotient_criterion_inverserightvaluemaskentry)) * dst_negative_scale_criterion_inverserightvaluemaskentryright) + (dst_negative_criterion_inverserightvaluemaskentryright))) /\ (exists ge_balance_positive_criterion_inverserightvaluemaskentryrightvalue ge_balance_negative_criterion_inverserightvaluemaskentryrightvalue. (((((dc_right_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_criterion_inverserightvaluemaskentryrightvalue) /\ (ge_balance_negative_criterion_inverserightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryrightvaluedecode. (((dc_right_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_criterion_inverserightvaluemaskentryrightvalue) = S ge_signed_half_criterion_inverserightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_criterion_inverserightvaluemaskentryright) + ge_balance_negative_criterion_inverserightvaluemaskentryrightvalue = (dst_negative_criterion_inverserightvaluemaskentryright) + ge_balance_positive_criterion_inverserightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_criterion_inverserightvaluemaskentryproduct sto_an_criterion_inverserightvaluemaskentryproduct sto_bp_criterion_inverserightvaluemaskentryproduct sto_bn_criterion_inverserightvaluemaskentryproduct sto_cp_criterion_inverserightvaluemaskentryproduct sto_cn_criterion_inverserightvaluemaskentryproduct. (((((dc_left_criterion_inverserightvaluemaskentry) = 2 * (sto_ap_criterion_inverserightvaluemaskentryproduct) /\ (sto_an_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryproductleft. (((dc_left_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryproductleft + 1 /\ (sto_ap_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_an_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_criterion_inverserightvaluemaskentryproductleft))) /\ ((((((dc_right_criterion_inverserightvaluemaskentry) = 2 * (sto_bp_criterion_inverserightvaluemaskentryproduct) /\ (sto_bn_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryproductright. (((dc_right_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryproductright + 1 /\ (sto_bp_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_bn_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_criterion_inverserightvaluemaskentryproductright))) /\ ((((((dc_value_criterion_inverserightvaluemask) = 2 * (sto_cp_criterion_inverserightvaluemaskentryproduct) /\ (sto_cn_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_criterion_inverserightvaluemaskentryproductoutput. (((dc_value_criterion_inverserightvaluemask) = 2 * ge_signed_half_criterion_inverserightvaluemaskentryproductoutput + 1 /\ (sto_cp_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_cn_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_criterion_inverserightvaluemaskentryproductoutput))) /\ ((sto_ap_criterion_inverserightvaluemaskentryproduct * sto_bp_criterion_inverserightvaluemaskentryproduct + sto_an_criterion_inverserightvaluemaskentryproduct * sto_bn_criterion_inverserightvaluemaskentryproduct) + sto_cn_criterion_inverserightvaluemaskentryproduct = (sto_ap_criterion_inverserightvaluemaskentryproduct * sto_bn_criterion_inverserightvaluemaskentryproduct + sto_an_criterion_inverserightvaluemaskentryproduct * sto_bp_criterion_inverserightvaluemaskentryproduct) + sto_cp_criterion_inverserightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_criterion_inverserightvaluemask)=0 \/ ~(exists pvs_factor_criterion_inverserightvaluemaskentrynondivisor. (dc_input_criterion_inverseright) = (dc_index_criterion_inverserightvaluemask) * pvs_factor_criterion_inverserightvaluemaskentrynondivisor)) /\ ((dc_value_criterion_inverserightvaluemask)=0))))))) /\ (exists dst_positive_code_criterion_inverserightvaluefold dst_positive_scale_criterion_inverserightvaluefold dst_negative_code_criterion_inverserightvaluefold dst_negative_scale_criterion_inverserightvaluefold dst_positive_sum_criterion_inverserightvaluefold dst_negative_sum_criterion_inverserightvaluefold. (((dc_mask_criterion_inverserightvalue) = (((((dst_positive_code_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold)) * S ((dst_positive_code_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold)) + ((dst_positive_scale_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold))) + (((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) * S ((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) + ((dst_negative_scale_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)))) * S ((((dst_positive_code_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold)) * S ((dst_positive_code_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold)) + ((dst_positive_scale_criterion_inverserightvaluefold) + (dst_positive_scale_criterion_inverserightvaluefold))) + (((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) * S ((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) + ((dst_negative_scale_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)))) + ((((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) * S ((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) + ((dst_negative_scale_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold))) + (((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) * S ((dst_negative_code_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)) + ((dst_negative_scale_criterion_inverserightvaluefold) + (dst_negative_scale_criterion_inverserightvaluefold)))))) /\ (((exists fs_u_dst_criterion_inverserightvaluefoldpositive fs_v_dst_criterion_inverserightvaluefoldpositive. ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_start. fs_h_dst_criterion_inverserightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_start. fs_u_dst_criterion_inverserightvaluefoldpositive = fs_q_dst_criterion_inverserightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_criterion_inverserightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_terminal. fs_h_dst_criterion_inverserightvaluefoldpositive_body_terminal + S (dst_positive_sum_criterion_inverserightvaluefold) = S ((S (S (dc_input_criterion_inverseright))) * fs_v_dst_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_terminal. fs_u_dst_criterion_inverserightvaluefoldpositive = fs_q_dst_criterion_inverserightvaluefoldpositive_body_terminal * S ((S (S (dc_input_criterion_inverseright))) * fs_v_dst_criterion_inverserightvaluefoldpositive) + (dst_positive_sum_criterion_inverserightvaluefold))) /\ forall fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps. (exists fs_lt_dst_criterion_inverserightvaluefoldpositive_body_steps_bound. fs_lt_dst_criterion_inverserightvaluefoldpositive_body_steps_bound + S fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps = S (dc_input_criterion_inverseright)) -> exists fs_a_dst_criterion_inverserightvaluefoldpositive_body_steps fs_r_dst_criterion_inverserightvaluefoldpositive_body_steps fs_s_dst_criterion_inverserightvaluefoldpositive_body_steps. ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_summand. fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_summand + S (fs_a_dst_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_criterion_inverserightvaluefold)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_summand. dst_positive_code_criterion_inverserightvaluefold = fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_criterion_inverserightvaluefold) + (fs_a_dst_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_partial + S (fs_r_dst_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_u_dst_criterion_inverserightvaluefoldpositive = fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldpositive) + (fs_r_dst_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_h_dst_criterion_inverserightvaluefoldpositive_body_steps_successor + S (fs_s_dst_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_u_dst_criterion_inverserightvaluefoldpositive = fs_q_dst_criterion_inverserightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldpositive) + (fs_s_dst_criterion_inverserightvaluefoldpositive_body_steps))) /\ fs_s_dst_criterion_inverserightvaluefoldpositive_body_steps = fs_r_dst_criterion_inverserightvaluefoldpositive_body_steps + fs_a_dst_criterion_inverserightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_criterion_inverserightvaluefoldnegative fs_v_dst_criterion_inverserightvaluefoldnegative. ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_start. fs_h_dst_criterion_inverserightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_start. fs_u_dst_criterion_inverserightvaluefoldnegative = fs_q_dst_criterion_inverserightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_criterion_inverserightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_terminal. fs_h_dst_criterion_inverserightvaluefoldnegative_body_terminal + S (dst_negative_sum_criterion_inverserightvaluefold) = S ((S (S (dc_input_criterion_inverseright))) * fs_v_dst_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_terminal. fs_u_dst_criterion_inverserightvaluefoldnegative = fs_q_dst_criterion_inverserightvaluefoldnegative_body_terminal * S ((S (S (dc_input_criterion_inverseright))) * fs_v_dst_criterion_inverserightvaluefoldnegative) + (dst_negative_sum_criterion_inverserightvaluefold))) /\ forall fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps. (exists fs_lt_dst_criterion_inverserightvaluefoldnegative_body_steps_bound. fs_lt_dst_criterion_inverserightvaluefoldnegative_body_steps_bound + S fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps = S (dc_input_criterion_inverseright)) -> exists fs_a_dst_criterion_inverserightvaluefoldnegative_body_steps fs_r_dst_criterion_inverserightvaluefoldnegative_body_steps fs_s_dst_criterion_inverserightvaluefoldnegative_body_steps. ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_summand. fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_summand + S (fs_a_dst_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_criterion_inverserightvaluefold)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_summand. dst_negative_code_criterion_inverserightvaluefold = fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_criterion_inverserightvaluefold) + (fs_a_dst_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_partial + S (fs_r_dst_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_u_dst_criterion_inverserightvaluefoldnegative = fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldnegative) + (fs_r_dst_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_h_dst_criterion_inverserightvaluefoldnegative_body_steps_successor + S (fs_s_dst_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_u_dst_criterion_inverserightvaluefoldnegative = fs_q_dst_criterion_inverserightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_criterion_inverserightvaluefoldnegative) + (fs_s_dst_criterion_inverserightvaluefoldnegative_body_steps))) /\ fs_s_dst_criterion_inverserightvaluefoldnegative_body_steps = fs_r_dst_criterion_inverserightvaluefoldnegative_body_steps + fs_a_dst_criterion_inverserightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_criterion_inverserightvaluefoldresult ge_balance_negative_criterion_inverserightvaluefoldresult. (((((dc_output_criterion_inverseright) = 2 * (ge_balance_positive_criterion_inverserightvaluefoldresult) /\ (ge_balance_negative_criterion_inverserightvaluefoldresult) = 0) \/ exists ge_signed_half_criterion_inverserightvaluefoldresultdecode. (((dc_output_criterion_inverseright) = 2 * ge_signed_half_criterion_inverserightvaluefoldresultdecode + 1 /\ (ge_balance_positive_criterion_inverserightvaluefoldresult) = 0) /\ (ge_balance_negative_criterion_inverserightvaluefoldresult) = S ge_signed_half_criterion_inverserightvaluefoldresultdecode))) /\ ((dst_positive_sum_criterion_inverserightvaluefold) + ge_balance_negative_criterion_inverserightvaluefoldresult = (dst_negative_sum_criterion_inverserightvaluefold) + ge_balance_positive_criterion_inverserightvaluefoldresult))))))))))))))))))))))))))Complete tactic proof in conservative notation
All 32 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
32 script commands · 14 reading checkpoints · 2 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–3
02Separate the logical casesL4–4
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L4
split
03Fix variables and assumptionsL5–5
Work with arbitrary variables or the premises of the current implication.
- L5
intro hi
04Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
cases hi
05Establish hcL7–10
06Separate the logical casesL11–12
07Use earlier factsL13–13
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L13
exact hc_left
08Separate the logical casesL14–14
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L14
right
09Use earlier factsL15–20
Instantiate or apply named facts and discharge the corresponding proof obligations.
10Fix variables and assumptionsL21–21
Work with arbitrary variables or the premises of the current implication.
- L21
intro hc
11Establish hgL22–28
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet inverse construct.
- L22
have hg : ∃ G. DirichletInverse(N,F,G) ∧ ArithAt(G,0,0)Definitions: DirichletInverse(N,F,G)ArithAt(G,0,0)Original native command in the exact edition - L23
specialize dirichlet_inverse_construct (N) - L24
specialize dirichlet_inverse_construct (F) - L25
specialize dirichlet_inverse_construct (0) - L26
apply dirichlet_inverse_construct - L27
exact hF - L28
exact hc
12Separate the logical casesL29–30
13Construct an explicit witnessL31–31
Supply the displayed value, then prove that it has the required property.
- L31
exists x
14Use earlier factsL32–32
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L32
exact hg_witness_left
Original defined command ledger · 32 lines
- 0001
intro N - 0002
intro F - 0003
intro hF - 0004
split - 0005
intro hi - 0006
cases hi - 0007
have hc : N=0 \/ ~(N=0) - 0008
specialize eq_decidable (N) - 0009
specialize eq_decidable (0) - 0010
apply eq_decidable - 0011
cases hc - 0012
left - 0013
exact hc_left - 0014
right - 0015
specialize dirichlet_inverse_requires_unit_at_one (N) - 0016
specialize dirichlet_inverse_requires_unit_at_one (F) - 0017
specialize dirichlet_inverse_requires_unit_at_one (x) - 0018
apply dirichlet_inverse_requires_unit_at_one - 0019
exact hi_witness - 0020
exact hc_right - 0021
intro hc - 0022
have hg : ∃ G. DirichletInverse(N,F,G) ∧ ArithAt(G,0,0) - 0023
specialize dirichlet_inverse_construct (N) - 0024
specialize dirichlet_inverse_construct (F) - 0025
specialize dirichlet_inverse_construct (0) - 0026
apply dirichlet_inverse_construct - 0027
exact hF - 0028
exact hc - 0029
cases hg - 0030
cases hg_witness - 0031
exists x - 0032
exact hg_witness_left