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) → ¬N = 0 → ((∃ x. DirichletInverse(N,F,x)) → DirichletUnitAtOne(F)) ∧ (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_positive_criterion_input dst_positive_scale_positive_criterion_input dst_negative_code_positive_criterion_input dst_negative_scale_positive_criterion_input. (((F) = (((((dst_positive_code_positive_criterion_input) + (dst_positive_scale_positive_criterion_input)) * S ((dst_positive_code_positive_criterion_input) + (dst_positive_scale_positive_criterion_input)) + ((dst_positive_scale_positive_criterion_input) + (dst_positive_scale_positive_criterion_input))) + (((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) * S ((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) + ((dst_negative_scale_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)))) * S ((((dst_positive_code_positive_criterion_input) + (dst_positive_scale_positive_criterion_input)) * S ((dst_positive_code_positive_criterion_input) + (dst_positive_scale_positive_criterion_input)) + ((dst_positive_scale_positive_criterion_input) + (dst_positive_scale_positive_criterion_input))) + (((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) * S ((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) + ((dst_negative_scale_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)))) + ((((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) * S ((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) + ((dst_negative_scale_positive_criterion_input) + (dst_negative_scale_positive_criterion_input))) + (((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) * S ((dst_negative_code_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)) + ((dst_negative_scale_positive_criterion_input) + (dst_negative_scale_positive_criterion_input)))))) /\ (forall dst_index_positive_criterion_input. (exists pvs_le_gap_positive_criterion_inputdomain. pvs_le_gap_positive_criterion_inputdomain + (dst_index_positive_criterion_input) = (N)) -> exists dst_positive_positive_criterion_input dst_negative_positive_criterion_input dst_value_positive_criterion_input. ((((exists ff_h_pvs_positive_criterion_inputentrypositive. ff_h_pvs_positive_criterion_inputentrypositive + S (dst_positive_positive_criterion_input) = S ((S (dst_index_positive_criterion_input)) * dst_positive_scale_positive_criterion_input)) /\ exists ff_q_pvs_positive_criterion_inputentrypositive. dst_positive_code_positive_criterion_input = ff_q_pvs_positive_criterion_inputentrypositive * S ((S (dst_index_positive_criterion_input)) * dst_positive_scale_positive_criterion_input) + (dst_positive_positive_criterion_input))) /\ (((((exists ff_h_pvs_positive_criterion_inputentrynegative. ff_h_pvs_positive_criterion_inputentrynegative + S (dst_negative_positive_criterion_input) = S ((S (dst_index_positive_criterion_input)) * dst_negative_scale_positive_criterion_input)) /\ exists ff_q_pvs_positive_criterion_inputentrynegative. dst_negative_code_positive_criterion_input = ff_q_pvs_positive_criterion_inputentrynegative * S ((S (dst_index_positive_criterion_input)) * dst_negative_scale_positive_criterion_input) + (dst_negative_positive_criterion_input))) /\ (exists ge_balance_positive_positive_criterion_inputentryvalue ge_balance_negative_positive_criterion_inputentryvalue. (((((dst_value_positive_criterion_input) = 2 * (ge_balance_positive_positive_criterion_inputentryvalue) /\ (ge_balance_negative_positive_criterion_inputentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inputentryvaluedecode. (((dst_value_positive_criterion_input) = 2 * ge_signed_half_positive_criterion_inputentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inputentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inputentryvalue) = S ge_signed_half_positive_criterion_inputentryvaluedecode))) /\ ((dst_positive_positive_criterion_input) + ge_balance_negative_positive_criterion_inputentryvalue = (dst_negative_positive_criterion_input) + ge_balance_positive_positive_criterion_inputentryvalue))))))))) -> ~(N=0) -> (((exists G. (exists di_delta_positive_criterion_inverse. ((((exists dst_positive_code_positive_criterion_inversedeltatable dst_positive_scale_positive_criterion_inversedeltatable dst_negative_code_positive_criterion_inversedeltatable dst_negative_scale_positive_criterion_inversedeltatable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) * S ((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) + ((dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))) * S ((((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) * S ((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) + ((dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))) + ((((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))))) /\ (forall dst_index_positive_criterion_inversedeltatable. (exists pvs_le_gap_positive_criterion_inversedeltatabledomain. pvs_le_gap_positive_criterion_inversedeltatabledomain + (dst_index_positive_criterion_inversedeltatable) = (N)) -> exists dst_positive_positive_criterion_inversedeltatable dst_negative_positive_criterion_inversedeltatable dst_value_positive_criterion_inversedeltatable. ((((exists ff_h_pvs_positive_criterion_inversedeltatableentrypositive. ff_h_pvs_positive_criterion_inversedeltatableentrypositive + S (dst_positive_positive_criterion_inversedeltatable) = S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_positive_scale_positive_criterion_inversedeltatable)) /\ exists ff_q_pvs_positive_criterion_inversedeltatableentrypositive. dst_positive_code_positive_criterion_inversedeltatable = ff_q_pvs_positive_criterion_inversedeltatableentrypositive * S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_positive_criterion_inversedeltatable))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltatableentrynegative. ff_h_pvs_positive_criterion_inversedeltatableentrynegative + S (dst_negative_positive_criterion_inversedeltatable) = S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_negative_scale_positive_criterion_inversedeltatable)) /\ exists ff_q_pvs_positive_criterion_inversedeltatableentrynegative. dst_negative_code_positive_criterion_inversedeltatable = ff_q_pvs_positive_criterion_inversedeltatableentrynegative * S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_positive_criterion_inversedeltatable))) /\ (exists ge_balance_positive_positive_criterion_inversedeltatableentryvalue ge_balance_negative_positive_criterion_inversedeltatableentryvalue. (((((dst_value_positive_criterion_inversedeltatable) = 2 * (ge_balance_positive_positive_criterion_inversedeltatableentryvalue) /\ (ge_balance_negative_positive_criterion_inversedeltatableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode. (((dst_value_positive_criterion_inversedeltatable) = 2 * ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inversedeltatableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inversedeltatableentryvalue) = S ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inversedeltatable) + ge_balance_negative_positive_criterion_inversedeltatableentryvalue = (dst_negative_positive_criterion_inversedeltatable) + ge_balance_positive_positive_criterion_inversedeltatableentryvalue))))))))) /\ (forall du_index_positive_criterion_inversedelta du_value_positive_criterion_inversedelta. ~(du_index_positive_criterion_inversedelta=0) -> (exists pvs_le_gap_positive_criterion_inversedeltabound. pvs_le_gap_positive_criterion_inversedeltabound + (du_index_positive_criterion_inversedelta) = (N)) -> (exists dst_positive_code_positive_criterion_inversedeltaentry dst_positive_scale_positive_criterion_inversedeltaentry dst_negative_code_positive_criterion_inversedeltaentry dst_negative_scale_positive_criterion_inversedeltaentry dst_positive_positive_criterion_inversedeltaentry dst_negative_positive_criterion_inversedeltaentry. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) * S ((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) + ((dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))) * S ((((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) * S ((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) + ((dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))) + ((((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltaentrypositive. ff_h_pvs_positive_criterion_inversedeltaentrypositive + S (dst_positive_positive_criterion_inversedeltaentry) = S ((S (du_index_positive_criterion_inversedelta)) * dst_positive_scale_positive_criterion_inversedeltaentry)) /\ exists ff_q_pvs_positive_criterion_inversedeltaentrypositive. dst_positive_code_positive_criterion_inversedeltaentry = ff_q_pvs_positive_criterion_inversedeltaentrypositive * S ((S (du_index_positive_criterion_inversedelta)) * dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_positive_criterion_inversedeltaentry))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltaentrynegative. ff_h_pvs_positive_criterion_inversedeltaentrynegative + S (dst_negative_positive_criterion_inversedeltaentry) = S ((S (du_index_positive_criterion_inversedelta)) * dst_negative_scale_positive_criterion_inversedeltaentry)) /\ exists ff_q_pvs_positive_criterion_inversedeltaentrynegative. dst_negative_code_positive_criterion_inversedeltaentry = ff_q_pvs_positive_criterion_inversedeltaentrynegative * S ((S (du_index_positive_criterion_inversedelta)) * dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_positive_criterion_inversedeltaentry))) /\ (exists ge_balance_positive_positive_criterion_inversedeltaentryvalue ge_balance_negative_positive_criterion_inversedeltaentryvalue. (((((du_value_positive_criterion_inversedelta) = 2 * (ge_balance_positive_positive_criterion_inversedeltaentryvalue) /\ (ge_balance_negative_positive_criterion_inversedeltaentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inversedeltaentryvaluedecode. (((du_value_positive_criterion_inversedelta) = 2 * ge_signed_half_positive_criterion_inversedeltaentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inversedeltaentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inversedeltaentryvalue) = S ge_signed_half_positive_criterion_inversedeltaentryvaluedecode))) /\ ((dst_positive_positive_criterion_inversedeltaentry) + ge_balance_negative_positive_criterion_inversedeltaentryvalue = (dst_negative_positive_criterion_inversedeltaentry) + ge_balance_positive_positive_criterion_inversedeltaentryvalue))))))))) -> ((((du_index_positive_criterion_inversedelta)=1 -> (du_value_positive_criterion_inversedelta)=2) /\ (~((du_index_positive_criterion_inversedelta)=1) -> (du_value_positive_criterion_inversedelta)=0)))))) /\ (((((exists dst_positive_code_positive_criterion_inverseleftleft dst_positive_scale_positive_criterion_inverseleftleft dst_negative_code_positive_criterion_inverseleftleft dst_negative_scale_positive_criterion_inverseleftleft. (((F) = (((((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) * S ((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) + ((dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))) * S ((((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) * S ((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) + ((dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))) + ((((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))))) /\ (forall dst_index_positive_criterion_inverseleftleft. (exists pvs_le_gap_positive_criterion_inverseleftleftdomain. pvs_le_gap_positive_criterion_inverseleftleftdomain + (dst_index_positive_criterion_inverseleftleft) = (N)) -> exists dst_positive_positive_criterion_inverseleftleft dst_negative_positive_criterion_inverseleftleft dst_value_positive_criterion_inverseleftleft. ((((exists ff_h_pvs_positive_criterion_inverseleftleftentrypositive. ff_h_pvs_positive_criterion_inverseleftleftentrypositive + S (dst_positive_positive_criterion_inverseleftleft) = S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_positive_scale_positive_criterion_inverseleftleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftleftentrypositive. dst_positive_code_positive_criterion_inverseleftleft = ff_q_pvs_positive_criterion_inverseleftleftentrypositive * S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_positive_criterion_inverseleftleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftleftentrynegative. ff_h_pvs_positive_criterion_inverseleftleftentrynegative + S (dst_negative_positive_criterion_inverseleftleft) = S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_negative_scale_positive_criterion_inverseleftleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftleftentrynegative. dst_negative_code_positive_criterion_inverseleftleft = ff_q_pvs_positive_criterion_inverseleftleftentrynegative * S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_positive_criterion_inverseleftleft))) /\ (exists ge_balance_positive_positive_criterion_inverseleftleftentryvalue ge_balance_negative_positive_criterion_inverseleftleftentryvalue. (((((dst_value_positive_criterion_inverseleftleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftleftentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftleftentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode. (((dst_value_positive_criterion_inverseleftleft) = 2 * ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftleftentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftleftentryvalue) = S ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftleft) + ge_balance_negative_positive_criterion_inverseleftleftentryvalue = (dst_negative_positive_criterion_inverseleftleft) + ge_balance_positive_positive_criterion_inverseleftleftentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverseleftright dst_positive_scale_positive_criterion_inverseleftright dst_negative_code_positive_criterion_inverseleftright dst_negative_scale_positive_criterion_inverseleftright. (((G) = (((((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) * S ((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) + ((dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))) * S ((((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) * S ((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) + ((dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))) + ((((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))))) /\ (forall dst_index_positive_criterion_inverseleftright. (exists pvs_le_gap_positive_criterion_inverseleftrightdomain. pvs_le_gap_positive_criterion_inverseleftrightdomain + (dst_index_positive_criterion_inverseleftright) = (N)) -> exists dst_positive_positive_criterion_inverseleftright dst_negative_positive_criterion_inverseleftright dst_value_positive_criterion_inverseleftright. ((((exists ff_h_pvs_positive_criterion_inverseleftrightentrypositive. ff_h_pvs_positive_criterion_inverseleftrightentrypositive + S (dst_positive_positive_criterion_inverseleftright) = S ((S (dst_index_positive_criterion_inverseleftright)) * dst_positive_scale_positive_criterion_inverseleftright)) /\ exists ff_q_pvs_positive_criterion_inverseleftrightentrypositive. dst_positive_code_positive_criterion_inverseleftright = ff_q_pvs_positive_criterion_inverseleftrightentrypositive * S ((S (dst_index_positive_criterion_inverseleftright)) * dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_positive_criterion_inverseleftright))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftrightentrynegative. ff_h_pvs_positive_criterion_inverseleftrightentrynegative + S (dst_negative_positive_criterion_inverseleftright) = S ((S (dst_index_positive_criterion_inverseleftright)) * dst_negative_scale_positive_criterion_inverseleftright)) /\ exists ff_q_pvs_positive_criterion_inverseleftrightentrynegative. dst_negative_code_positive_criterion_inverseleftright = ff_q_pvs_positive_criterion_inverseleftrightentrynegative * S ((S (dst_index_positive_criterion_inverseleftright)) * dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_positive_criterion_inverseleftright))) /\ (exists ge_balance_positive_positive_criterion_inverseleftrightentryvalue ge_balance_negative_positive_criterion_inverseleftrightentryvalue. (((((dst_value_positive_criterion_inverseleftright) = 2 * (ge_balance_positive_positive_criterion_inverseleftrightentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftrightentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode. (((dst_value_positive_criterion_inverseleftright) = 2 * ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftrightentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftrightentryvalue) = S ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftright) + ge_balance_negative_positive_criterion_inverseleftrightentryvalue = (dst_negative_positive_criterion_inverseleftright) + ge_balance_positive_positive_criterion_inverseleftrightentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverselefttable dst_positive_scale_positive_criterion_inverselefttable dst_negative_code_positive_criterion_inverselefttable dst_negative_scale_positive_criterion_inverselefttable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) * S ((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) + ((dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))) * S ((((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) * S ((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) + ((dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))) + ((((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))))) /\ (forall dst_index_positive_criterion_inverselefttable. (exists pvs_le_gap_positive_criterion_inverselefttabledomain. pvs_le_gap_positive_criterion_inverselefttabledomain + (dst_index_positive_criterion_inverselefttable) = (N)) -> exists dst_positive_positive_criterion_inverselefttable dst_negative_positive_criterion_inverselefttable dst_value_positive_criterion_inverselefttable. ((((exists ff_h_pvs_positive_criterion_inverselefttableentrypositive. ff_h_pvs_positive_criterion_inverselefttableentrypositive + S (dst_positive_positive_criterion_inverselefttable) = S ((S (dst_index_positive_criterion_inverselefttable)) * dst_positive_scale_positive_criterion_inverselefttable)) /\ exists ff_q_pvs_positive_criterion_inverselefttableentrypositive. dst_positive_code_positive_criterion_inverselefttable = ff_q_pvs_positive_criterion_inverselefttableentrypositive * S ((S (dst_index_positive_criterion_inverselefttable)) * dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_positive_criterion_inverselefttable))) /\ (((((exists ff_h_pvs_positive_criterion_inverselefttableentrynegative. ff_h_pvs_positive_criterion_inverselefttableentrynegative + S (dst_negative_positive_criterion_inverselefttable) = S ((S (dst_index_positive_criterion_inverselefttable)) * dst_negative_scale_positive_criterion_inverselefttable)) /\ exists ff_q_pvs_positive_criterion_inverselefttableentrynegative. dst_negative_code_positive_criterion_inverselefttable = ff_q_pvs_positive_criterion_inverselefttableentrynegative * S ((S (dst_index_positive_criterion_inverselefttable)) * dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_positive_criterion_inverselefttable))) /\ (exists ge_balance_positive_positive_criterion_inverselefttableentryvalue ge_balance_negative_positive_criterion_inverselefttableentryvalue. (((((dst_value_positive_criterion_inverselefttable) = 2 * (ge_balance_positive_positive_criterion_inverselefttableentryvalue) /\ (ge_balance_negative_positive_criterion_inverselefttableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverselefttableentryvaluedecode. (((dst_value_positive_criterion_inverselefttable) = 2 * ge_signed_half_positive_criterion_inverselefttableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverselefttableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverselefttableentryvalue) = S ge_signed_half_positive_criterion_inverselefttableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverselefttable) + ge_balance_negative_positive_criterion_inverselefttableentryvalue = (dst_negative_positive_criterion_inverselefttable) + ge_balance_positive_positive_criterion_inverselefttableentryvalue))))))))) /\ (forall dc_input_positive_criterion_inverseleft dc_output_positive_criterion_inverseleft. ~(dc_input_positive_criterion_inverseleft=0) -> (exists pvs_le_gap_positive_criterion_inverseleftdomain. pvs_le_gap_positive_criterion_inverseleftdomain + (dc_input_positive_criterion_inverseleft) = (N)) -> (exists dst_positive_code_positive_criterion_inverseleftlookup dst_positive_scale_positive_criterion_inverseleftlookup dst_negative_code_positive_criterion_inverseleftlookup dst_negative_scale_positive_criterion_inverseleftlookup dst_positive_positive_criterion_inverseleftlookup dst_negative_positive_criterion_inverseleftlookup. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) * S ((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) + ((dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))) * S ((((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) * S ((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) + ((dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))) + ((((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftlookuppositive. ff_h_pvs_positive_criterion_inverseleftlookuppositive + S (dst_positive_positive_criterion_inverseleftlookup) = S ((S (dc_input_positive_criterion_inverseleft)) * dst_positive_scale_positive_criterion_inverseleftlookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftlookuppositive. dst_positive_code_positive_criterion_inverseleftlookup = ff_q_pvs_positive_criterion_inverseleftlookuppositive * S ((S (dc_input_positive_criterion_inverseleft)) * dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_positive_criterion_inverseleftlookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftlookupnegative. ff_h_pvs_positive_criterion_inverseleftlookupnegative + S (dst_negative_positive_criterion_inverseleftlookup) = S ((S (dc_input_positive_criterion_inverseleft)) * dst_negative_scale_positive_criterion_inverseleftlookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftlookupnegative. dst_negative_code_positive_criterion_inverseleftlookup = ff_q_pvs_positive_criterion_inverseleftlookupnegative * S ((S (dc_input_positive_criterion_inverseleft)) * dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_positive_criterion_inverseleftlookup))) /\ (exists ge_balance_positive_positive_criterion_inverseleftlookupvalue ge_balance_negative_positive_criterion_inverseleftlookupvalue. (((((dc_output_positive_criterion_inverseleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftlookupvalue) /\ (ge_balance_negative_positive_criterion_inverseleftlookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftlookupvaluedecode. (((dc_output_positive_criterion_inverseleft) = 2 * ge_signed_half_positive_criterion_inverseleftlookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftlookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftlookupvalue) = S ge_signed_half_positive_criterion_inverseleftlookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftlookup) + ge_balance_negative_positive_criterion_inverseleftlookupvalue = (dst_negative_positive_criterion_inverseleftlookup) + ge_balance_positive_positive_criterion_inverseleftlookupvalue))))))))) -> (((~((dc_input_positive_criterion_inverseleft)=0)) /\ (exists dc_mask_positive_criterion_inverseleftvalue. ((((exists dst_positive_code_positive_criterion_inverseleftvaluemasktable dst_positive_scale_positive_criterion_inverseleftvaluemasktable dst_negative_code_positive_criterion_inverseleftvaluemasktable dst_negative_scale_positive_criterion_inverseleftvaluemasktable. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))))) /\ (forall dst_index_positive_criterion_inverseleftvaluemasktable. (exists pvs_le_gap_positive_criterion_inverseleftvaluemasktabledomain. pvs_le_gap_positive_criterion_inverseleftvaluemasktabledomain + (dst_index_positive_criterion_inverseleftvaluemasktable) = (dc_input_positive_criterion_inverseleft)) -> exists dst_positive_positive_criterion_inverseleftvaluemasktable dst_negative_positive_criterion_inverseleftvaluemasktable dst_value_positive_criterion_inverseleftvaluemasktable. ((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrypositive. ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrypositive + S (dst_positive_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrypositive. dst_positive_code_positive_criterion_inverseleftvaluemasktable = ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrypositive * S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_positive_criterion_inverseleftvaluemasktable))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrynegative. ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrynegative + S (dst_negative_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrynegative. dst_negative_code_positive_criterion_inverseleftvaluemasktable = ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrynegative * S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_positive_criterion_inverseleftvaluemasktable))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue. (((((dst_value_positive_criterion_inverseleftvaluemasktable) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode. (((dst_value_positive_criterion_inverseleftvaluemasktable) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemasktable) + ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue = (dst_negative_positive_criterion_inverseleftvaluemasktable) + ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_positive_criterion_inverseleftvaluemask dc_value_positive_criterion_inverseleftvaluemask. (exists pvs_le_gap_positive_criterion_inverseleftvaluemaskdomain. pvs_le_gap_positive_criterion_inverseleftvaluemaskdomain + (dc_index_positive_criterion_inverseleftvaluemask) = (dc_input_positive_criterion_inverseleft)) -> (exists dst_positive_code_positive_criterion_inverseleftvaluemasklookup dst_positive_scale_positive_criterion_inverseleftvaluemasklookup dst_negative_code_positive_criterion_inverseleftvaluemasklookup dst_negative_scale_positive_criterion_inverseleftvaluemasklookup dst_positive_positive_criterion_inverseleftvaluemasklookup dst_negative_positive_criterion_inverseleftvaluemasklookup. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasklookuppositive. ff_h_pvs_positive_criterion_inverseleftvaluemasklookuppositive + S (dst_positive_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasklookuppositive. dst_positive_code_positive_criterion_inverseleftvaluemasklookup = ff_q_pvs_positive_criterion_inverseleftvaluemasklookuppositive * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_positive_criterion_inverseleftvaluemasklookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasklookupnegative. ff_h_pvs_positive_criterion_inverseleftvaluemasklookupnegative + S (dst_negative_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasklookupnegative. dst_negative_code_positive_criterion_inverseleftvaluemasklookup = ff_q_pvs_positive_criterion_inverseleftvaluemasklookupnegative * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_positive_criterion_inverseleftvaluemasklookup))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue. (((((dc_value_positive_criterion_inverseleftvaluemask) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode. (((dc_value_positive_criterion_inverseleftvaluemask) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemasklookup) + ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue = (dst_negative_positive_criterion_inverseleftvaluemasklookup) + ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_positive_criterion_inverseleftvaluemask)=0)) /\ (exists dc_quotient_positive_criterion_inverseleftvaluemaskentry dc_left_positive_criterion_inverseleftvaluemaskentry dc_right_positive_criterion_inverseleftvaluemaskentry. (((dc_input_positive_criterion_inverseleft)=(dc_index_positive_criterion_inverseleftvaluemask)*dc_quotient_positive_criterion_inverseleftvaluemaskentry) /\ (((exists dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft dst_positive_positive_criterion_inverseleftvaluemaskentryleft dst_negative_positive_criterion_inverseleftvaluemaskentryleft. (((F) = (((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive + S (dst_positive_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive. dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_positive_criterion_inverseleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative + S (dst_negative_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative. dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_positive_criterion_inverseleftvaluemaskentryleft))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue. (((((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode. (((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue = (dst_negative_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverseleftvaluemaskentryright dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright dst_negative_code_positive_criterion_inverseleftvaluemaskentryright dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright dst_positive_positive_criterion_inverseleftvaluemaskentryright dst_negative_positive_criterion_inverseleftvaluemaskentryright. (((G) = (((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive + S (dst_positive_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive. dst_positive_code_positive_criterion_inverseleftvaluemaskentryright = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive * S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_positive_criterion_inverseleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative + S (dst_negative_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative. dst_negative_code_positive_criterion_inverseleftvaluemaskentryright = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative * S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_positive_criterion_inverseleftvaluemaskentryright))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue. (((((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode. (((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue = (dst_negative_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_positive_criterion_inverseleftvaluemaskentryproduct sto_an_positive_criterion_inverseleftvaluemaskentryproduct sto_bp_positive_criterion_inverseleftvaluemaskentryproduct sto_bn_positive_criterion_inverseleftvaluemaskentryproduct sto_cp_positive_criterion_inverseleftvaluemaskentryproduct sto_cn_positive_criterion_inverseleftvaluemaskentryproduct. (((((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_an_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft. (((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft + 1 /\ (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_an_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft))) /\ ((((((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * (sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright. (((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright + 1 /\ (sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright))) /\ ((((((dc_value_positive_criterion_inverseleftvaluemask) = 2 * (sto_cp_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_cn_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput. (((dc_value_positive_criterion_inverseleftvaluemask) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput + 1 /\ (sto_cp_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_cn_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput))) /\ ((sto_ap_positive_criterion_inverseleftvaluemaskentryproduct * sto_bp_positive_criterion_inverseleftvaluemaskentryproduct + sto_an_positive_criterion_inverseleftvaluemaskentryproduct * sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) + sto_cn_positive_criterion_inverseleftvaluemaskentryproduct = (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct * sto_bn_positive_criterion_inverseleftvaluemaskentryproduct + sto_an_positive_criterion_inverseleftvaluemaskentryproduct * sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) + sto_cp_positive_criterion_inverseleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_positive_criterion_inverseleftvaluemask)=0 \/ ~(exists pvs_factor_positive_criterion_inverseleftvaluemaskentrynondivisor. (dc_input_positive_criterion_inverseleft) = (dc_index_positive_criterion_inverseleftvaluemask) * pvs_factor_positive_criterion_inverseleftvaluemaskentrynondivisor)) /\ ((dc_value_positive_criterion_inverseleftvaluemask)=0))))))) /\ (exists dst_positive_code_positive_criterion_inverseleftvaluefold dst_positive_scale_positive_criterion_inverseleftvaluefold dst_negative_code_positive_criterion_inverseleftvaluefold dst_negative_scale_positive_criterion_inverseleftvaluefold dst_positive_sum_positive_criterion_inverseleftvaluefold dst_negative_sum_positive_criterion_inverseleftvaluefold. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) + ((dst_positive_scale_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) + ((dst_positive_scale_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))))) /\ (((exists fs_u_dst_positive_criterion_inverseleftvaluefoldpositive fs_v_dst_positive_criterion_inverseleftvaluefoldpositive. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_start. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_start. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal + S (dst_positive_sum_positive_criterion_inverseleftvaluefold) = S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (dst_positive_sum_positive_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps. (exists fs_lt_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_bound. fs_lt_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_bound + S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps = S (dc_input_positive_criterion_inverseleft)) -> exists fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand. dst_positive_code_positive_criterion_inverseleftvaluefold = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverseleftvaluefold) + (fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps = fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps + fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_positive_criterion_inverseleftvaluefoldnegative fs_v_dst_positive_criterion_inverseleftvaluefoldnegative. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_start. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_start. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal + S (dst_negative_sum_positive_criterion_inverseleftvaluefold) = S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (dst_negative_sum_positive_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps. (exists fs_lt_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_bound. fs_lt_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_bound + S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps = S (dc_input_positive_criterion_inverseleft)) -> exists fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand. dst_negative_code_positive_criterion_inverseleftvaluefold = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverseleftvaluefold) + (fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps = fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps + fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluefoldresult ge_balance_negative_positive_criterion_inverseleftvaluefoldresult. (((((dc_output_positive_criterion_inverseleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluefoldresult) /\ (ge_balance_negative_positive_criterion_inverseleftvaluefoldresult) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode. (((dc_output_positive_criterion_inverseleft) = 2 * ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluefoldresult) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluefoldresult) = S ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode))) /\ ((dst_positive_sum_positive_criterion_inverseleftvaluefold) + ge_balance_negative_positive_criterion_inverseleftvaluefoldresult = (dst_negative_sum_positive_criterion_inverseleftvaluefold) + ge_balance_positive_positive_criterion_inverseleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightleft dst_positive_scale_positive_criterion_inverserightleft dst_negative_code_positive_criterion_inverserightleft dst_negative_scale_positive_criterion_inverserightleft. (((G) = (((((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) * S ((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) + ((dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))) * S ((((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) * S ((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) + ((dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))) + ((((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))))) /\ (forall dst_index_positive_criterion_inverserightleft. (exists pvs_le_gap_positive_criterion_inverserightleftdomain. pvs_le_gap_positive_criterion_inverserightleftdomain + (dst_index_positive_criterion_inverserightleft) = (N)) -> exists dst_positive_positive_criterion_inverserightleft dst_negative_positive_criterion_inverserightleft dst_value_positive_criterion_inverserightleft. ((((exists ff_h_pvs_positive_criterion_inverserightleftentrypositive. ff_h_pvs_positive_criterion_inverserightleftentrypositive + S (dst_positive_positive_criterion_inverserightleft) = S ((S (dst_index_positive_criterion_inverserightleft)) * dst_positive_scale_positive_criterion_inverserightleft)) /\ exists ff_q_pvs_positive_criterion_inverserightleftentrypositive. dst_positive_code_positive_criterion_inverserightleft = ff_q_pvs_positive_criterion_inverserightleftentrypositive * S ((S (dst_index_positive_criterion_inverserightleft)) * dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_positive_criterion_inverserightleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightleftentrynegative. ff_h_pvs_positive_criterion_inverserightleftentrynegative + S (dst_negative_positive_criterion_inverserightleft) = S ((S (dst_index_positive_criterion_inverserightleft)) * dst_negative_scale_positive_criterion_inverserightleft)) /\ exists ff_q_pvs_positive_criterion_inverserightleftentrynegative. dst_negative_code_positive_criterion_inverserightleft = ff_q_pvs_positive_criterion_inverserightleftentrynegative * S ((S (dst_index_positive_criterion_inverserightleft)) * dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_positive_criterion_inverserightleft))) /\ (exists ge_balance_positive_positive_criterion_inverserightleftentryvalue ge_balance_negative_positive_criterion_inverserightleftentryvalue. (((((dst_value_positive_criterion_inverserightleft) = 2 * (ge_balance_positive_positive_criterion_inverserightleftentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightleftentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightleftentryvaluedecode. (((dst_value_positive_criterion_inverserightleft) = 2 * ge_signed_half_positive_criterion_inverserightleftentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightleftentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightleftentryvalue) = S ge_signed_half_positive_criterion_inverserightleftentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightleft) + ge_balance_negative_positive_criterion_inverserightleftentryvalue = (dst_negative_positive_criterion_inverserightleft) + ge_balance_positive_positive_criterion_inverserightleftentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightright dst_positive_scale_positive_criterion_inverserightright dst_negative_code_positive_criterion_inverserightright dst_negative_scale_positive_criterion_inverserightright. (((F) = (((((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) * S ((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) + ((dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))) * S ((((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) * S ((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) + ((dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))) + ((((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))))) /\ (forall dst_index_positive_criterion_inverserightright. (exists pvs_le_gap_positive_criterion_inverserightrightdomain. pvs_le_gap_positive_criterion_inverserightrightdomain + (dst_index_positive_criterion_inverserightright) = (N)) -> exists dst_positive_positive_criterion_inverserightright dst_negative_positive_criterion_inverserightright dst_value_positive_criterion_inverserightright. ((((exists ff_h_pvs_positive_criterion_inverserightrightentrypositive. ff_h_pvs_positive_criterion_inverserightrightentrypositive + S (dst_positive_positive_criterion_inverserightright) = S ((S (dst_index_positive_criterion_inverserightright)) * dst_positive_scale_positive_criterion_inverserightright)) /\ exists ff_q_pvs_positive_criterion_inverserightrightentrypositive. dst_positive_code_positive_criterion_inverserightright = ff_q_pvs_positive_criterion_inverserightrightentrypositive * S ((S (dst_index_positive_criterion_inverserightright)) * dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_positive_criterion_inverserightright))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightrightentrynegative. ff_h_pvs_positive_criterion_inverserightrightentrynegative + S (dst_negative_positive_criterion_inverserightright) = S ((S (dst_index_positive_criterion_inverserightright)) * dst_negative_scale_positive_criterion_inverserightright)) /\ exists ff_q_pvs_positive_criterion_inverserightrightentrynegative. dst_negative_code_positive_criterion_inverserightright = ff_q_pvs_positive_criterion_inverserightrightentrynegative * S ((S (dst_index_positive_criterion_inverserightright)) * dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_positive_criterion_inverserightright))) /\ (exists ge_balance_positive_positive_criterion_inverserightrightentryvalue ge_balance_negative_positive_criterion_inverserightrightentryvalue. (((((dst_value_positive_criterion_inverserightright) = 2 * (ge_balance_positive_positive_criterion_inverserightrightentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightrightentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightrightentryvaluedecode. (((dst_value_positive_criterion_inverserightright) = 2 * ge_signed_half_positive_criterion_inverserightrightentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightrightentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightrightentryvalue) = S ge_signed_half_positive_criterion_inverserightrightentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightright) + ge_balance_negative_positive_criterion_inverserightrightentryvalue = (dst_negative_positive_criterion_inverserightright) + ge_balance_positive_positive_criterion_inverserightrightentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserighttable dst_positive_scale_positive_criterion_inverserighttable dst_negative_code_positive_criterion_inverserighttable dst_negative_scale_positive_criterion_inverserighttable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) * S ((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) + ((dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))) * S ((((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) * S ((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) + ((dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))) + ((((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))))) /\ (forall dst_index_positive_criterion_inverserighttable. (exists pvs_le_gap_positive_criterion_inverserighttabledomain. pvs_le_gap_positive_criterion_inverserighttabledomain + (dst_index_positive_criterion_inverserighttable) = (N)) -> exists dst_positive_positive_criterion_inverserighttable dst_negative_positive_criterion_inverserighttable dst_value_positive_criterion_inverserighttable. ((((exists ff_h_pvs_positive_criterion_inverserighttableentrypositive. ff_h_pvs_positive_criterion_inverserighttableentrypositive + S (dst_positive_positive_criterion_inverserighttable) = S ((S (dst_index_positive_criterion_inverserighttable)) * dst_positive_scale_positive_criterion_inverserighttable)) /\ exists ff_q_pvs_positive_criterion_inverserighttableentrypositive. dst_positive_code_positive_criterion_inverserighttable = ff_q_pvs_positive_criterion_inverserighttableentrypositive * S ((S (dst_index_positive_criterion_inverserighttable)) * dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_positive_criterion_inverserighttable))) /\ (((((exists ff_h_pvs_positive_criterion_inverserighttableentrynegative. ff_h_pvs_positive_criterion_inverserighttableentrynegative + S (dst_negative_positive_criterion_inverserighttable) = S ((S (dst_index_positive_criterion_inverserighttable)) * dst_negative_scale_positive_criterion_inverserighttable)) /\ exists ff_q_pvs_positive_criterion_inverserighttableentrynegative. dst_negative_code_positive_criterion_inverserighttable = ff_q_pvs_positive_criterion_inverserighttableentrynegative * S ((S (dst_index_positive_criterion_inverserighttable)) * dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_positive_criterion_inverserighttable))) /\ (exists ge_balance_positive_positive_criterion_inverserighttableentryvalue ge_balance_negative_positive_criterion_inverserighttableentryvalue. (((((dst_value_positive_criterion_inverserighttable) = 2 * (ge_balance_positive_positive_criterion_inverserighttableentryvalue) /\ (ge_balance_negative_positive_criterion_inverserighttableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserighttableentryvaluedecode. (((dst_value_positive_criterion_inverserighttable) = 2 * ge_signed_half_positive_criterion_inverserighttableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserighttableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserighttableentryvalue) = S ge_signed_half_positive_criterion_inverserighttableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserighttable) + ge_balance_negative_positive_criterion_inverserighttableentryvalue = (dst_negative_positive_criterion_inverserighttable) + ge_balance_positive_positive_criterion_inverserighttableentryvalue))))))))) /\ (forall dc_input_positive_criterion_inverseright dc_output_positive_criterion_inverseright. ~(dc_input_positive_criterion_inverseright=0) -> (exists pvs_le_gap_positive_criterion_inverserightdomain. pvs_le_gap_positive_criterion_inverserightdomain + (dc_input_positive_criterion_inverseright) = (N)) -> (exists dst_positive_code_positive_criterion_inverserightlookup dst_positive_scale_positive_criterion_inverserightlookup dst_negative_code_positive_criterion_inverserightlookup dst_negative_scale_positive_criterion_inverserightlookup dst_positive_positive_criterion_inverserightlookup dst_negative_positive_criterion_inverserightlookup. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) * S ((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) + ((dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))) * S ((((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) * S ((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) + ((dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))) + ((((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightlookuppositive. ff_h_pvs_positive_criterion_inverserightlookuppositive + S (dst_positive_positive_criterion_inverserightlookup) = S ((S (dc_input_positive_criterion_inverseright)) * dst_positive_scale_positive_criterion_inverserightlookup)) /\ exists ff_q_pvs_positive_criterion_inverserightlookuppositive. dst_positive_code_positive_criterion_inverserightlookup = ff_q_pvs_positive_criterion_inverserightlookuppositive * S ((S (dc_input_positive_criterion_inverseright)) * dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_positive_criterion_inverserightlookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightlookupnegative. ff_h_pvs_positive_criterion_inverserightlookupnegative + S (dst_negative_positive_criterion_inverserightlookup) = S ((S (dc_input_positive_criterion_inverseright)) * dst_negative_scale_positive_criterion_inverserightlookup)) /\ exists ff_q_pvs_positive_criterion_inverserightlookupnegative. dst_negative_code_positive_criterion_inverserightlookup = ff_q_pvs_positive_criterion_inverserightlookupnegative * S ((S (dc_input_positive_criterion_inverseright)) * dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_positive_criterion_inverserightlookup))) /\ (exists ge_balance_positive_positive_criterion_inverserightlookupvalue ge_balance_negative_positive_criterion_inverserightlookupvalue. (((((dc_output_positive_criterion_inverseright) = 2 * (ge_balance_positive_positive_criterion_inverserightlookupvalue) /\ (ge_balance_negative_positive_criterion_inverserightlookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightlookupvaluedecode. (((dc_output_positive_criterion_inverseright) = 2 * ge_signed_half_positive_criterion_inverserightlookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightlookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightlookupvalue) = S ge_signed_half_positive_criterion_inverserightlookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightlookup) + ge_balance_negative_positive_criterion_inverserightlookupvalue = (dst_negative_positive_criterion_inverserightlookup) + ge_balance_positive_positive_criterion_inverserightlookupvalue))))))))) -> (((~((dc_input_positive_criterion_inverseright)=0)) /\ (exists dc_mask_positive_criterion_inverserightvalue. ((((exists dst_positive_code_positive_criterion_inverserightvaluemasktable dst_positive_scale_positive_criterion_inverserightvaluemasktable dst_negative_code_positive_criterion_inverserightvaluemasktable dst_negative_scale_positive_criterion_inverserightvaluemasktable. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))))) /\ (forall dst_index_positive_criterion_inverserightvaluemasktable. (exists pvs_le_gap_positive_criterion_inverserightvaluemasktabledomain. pvs_le_gap_positive_criterion_inverserightvaluemasktabledomain + (dst_index_positive_criterion_inverserightvaluemasktable) = (dc_input_positive_criterion_inverseright)) -> exists dst_positive_positive_criterion_inverserightvaluemasktable dst_negative_positive_criterion_inverserightvaluemasktable dst_value_positive_criterion_inverserightvaluemasktable. ((((exists ff_h_pvs_positive_criterion_inverserightvaluemasktableentrypositive. ff_h_pvs_positive_criterion_inverserightvaluemasktableentrypositive + S (dst_positive_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_positive_scale_positive_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasktableentrypositive. dst_positive_code_positive_criterion_inverserightvaluemasktable = ff_q_pvs_positive_criterion_inverserightvaluemasktableentrypositive * S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_positive_criterion_inverserightvaluemasktable))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasktableentrynegative. ff_h_pvs_positive_criterion_inverserightvaluemasktableentrynegative + S (dst_negative_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_negative_scale_positive_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasktableentrynegative. dst_negative_code_positive_criterion_inverserightvaluemasktable = ff_q_pvs_positive_criterion_inverserightvaluemasktableentrynegative * S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_positive_criterion_inverserightvaluemasktable))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue. (((((dst_value_positive_criterion_inverserightvaluemasktable) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode. (((dst_value_positive_criterion_inverserightvaluemasktable) = 2 * ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue) = S ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemasktable) + ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue = (dst_negative_positive_criterion_inverserightvaluemasktable) + ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue))))))))) /\ (forall dc_index_positive_criterion_inverserightvaluemask dc_value_positive_criterion_inverserightvaluemask. (exists pvs_le_gap_positive_criterion_inverserightvaluemaskdomain. pvs_le_gap_positive_criterion_inverserightvaluemaskdomain + (dc_index_positive_criterion_inverserightvaluemask) = (dc_input_positive_criterion_inverseright)) -> (exists dst_positive_code_positive_criterion_inverserightvaluemasklookup dst_positive_scale_positive_criterion_inverserightvaluemasklookup dst_negative_code_positive_criterion_inverserightvaluemasklookup dst_negative_scale_positive_criterion_inverserightvaluemasklookup dst_positive_positive_criterion_inverserightvaluemasklookup dst_negative_positive_criterion_inverserightvaluemasklookup. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasklookuppositive. ff_h_pvs_positive_criterion_inverserightvaluemasklookuppositive + S (dst_positive_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasklookuppositive. dst_positive_code_positive_criterion_inverserightvaluemasklookup = ff_q_pvs_positive_criterion_inverserightvaluemasklookuppositive * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_positive_criterion_inverserightvaluemasklookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasklookupnegative. ff_h_pvs_positive_criterion_inverserightvaluemasklookupnegative + S (dst_negative_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasklookupnegative. dst_negative_code_positive_criterion_inverserightvaluemasklookup = ff_q_pvs_positive_criterion_inverserightvaluemasklookupnegative * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_positive_criterion_inverserightvaluemasklookup))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue. (((((dc_value_positive_criterion_inverserightvaluemask) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode. (((dc_value_positive_criterion_inverserightvaluemask) = 2 * ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue) = S ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemasklookup) + ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue = (dst_negative_positive_criterion_inverserightvaluemasklookup) + ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue))))))))) -> ((((~((dc_index_positive_criterion_inverserightvaluemask)=0)) /\ (exists dc_quotient_positive_criterion_inverserightvaluemaskentry dc_left_positive_criterion_inverserightvaluemaskentry dc_right_positive_criterion_inverserightvaluemaskentry. (((dc_input_positive_criterion_inverseright)=(dc_index_positive_criterion_inverserightvaluemask)*dc_quotient_positive_criterion_inverserightvaluemaskentry) /\ (((exists dst_positive_code_positive_criterion_inverserightvaluemaskentryleft dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft dst_negative_code_positive_criterion_inverserightvaluemaskentryleft dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft dst_positive_positive_criterion_inverserightvaluemaskentryleft dst_negative_positive_criterion_inverserightvaluemaskentryleft. (((G) = (((((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftpositive. ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftpositive + S (dst_positive_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftpositive. dst_positive_code_positive_criterion_inverserightvaluemaskentryleft = ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftpositive * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_positive_criterion_inverserightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftnegative. ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftnegative + S (dst_negative_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftnegative. dst_negative_code_positive_criterion_inverserightvaluemaskentryleft = ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftnegative * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_positive_criterion_inverserightvaluemaskentryleft))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue. (((((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode. (((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue = (dst_negative_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightvaluemaskentryright dst_positive_scale_positive_criterion_inverserightvaluemaskentryright dst_negative_code_positive_criterion_inverserightvaluemaskentryright dst_negative_scale_positive_criterion_inverserightvaluemaskentryright dst_positive_positive_criterion_inverserightvaluemaskentryright dst_negative_positive_criterion_inverserightvaluemaskentryright. (((F) = (((((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightpositive. ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightpositive + S (dst_positive_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightpositive. dst_positive_code_positive_criterion_inverserightvaluemaskentryright = ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightpositive * S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_positive_criterion_inverserightvaluemaskentryright))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightnegative. ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightnegative + S (dst_negative_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightnegative. dst_negative_code_positive_criterion_inverserightvaluemaskentryright = ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightnegative * S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_positive_criterion_inverserightvaluemaskentryright))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue. (((((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode. (((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemaskentryright) + ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue = (dst_negative_positive_criterion_inverserightvaluemaskentryright) + ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_positive_criterion_inverserightvaluemaskentryproduct sto_an_positive_criterion_inverserightvaluemaskentryproduct sto_bp_positive_criterion_inverserightvaluemaskentryproduct sto_bn_positive_criterion_inverserightvaluemaskentryproduct sto_cp_positive_criterion_inverserightvaluemaskentryproduct sto_cn_positive_criterion_inverserightvaluemaskentryproduct. (((((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * (sto_ap_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_an_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft. (((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft + 1 /\ (sto_ap_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_an_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft))) /\ ((((((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * (sto_bp_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_bn_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright. (((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright + 1 /\ (sto_bp_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_bn_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright))) /\ ((((((dc_value_positive_criterion_inverserightvaluemask) = 2 * (sto_cp_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_cn_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput. (((dc_value_positive_criterion_inverserightvaluemask) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput + 1 /\ (sto_cp_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_cn_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput))) /\ ((sto_ap_positive_criterion_inverserightvaluemaskentryproduct * sto_bp_positive_criterion_inverserightvaluemaskentryproduct + sto_an_positive_criterion_inverserightvaluemaskentryproduct * sto_bn_positive_criterion_inverserightvaluemaskentryproduct) + sto_cn_positive_criterion_inverserightvaluemaskentryproduct = (sto_ap_positive_criterion_inverserightvaluemaskentryproduct * sto_bn_positive_criterion_inverserightvaluemaskentryproduct + sto_an_positive_criterion_inverserightvaluemaskentryproduct * sto_bp_positive_criterion_inverserightvaluemaskentryproduct) + sto_cp_positive_criterion_inverserightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_positive_criterion_inverserightvaluemask)=0 \/ ~(exists pvs_factor_positive_criterion_inverserightvaluemaskentrynondivisor. (dc_input_positive_criterion_inverseright) = (dc_index_positive_criterion_inverserightvaluemask) * pvs_factor_positive_criterion_inverserightvaluemaskentrynondivisor)) /\ ((dc_value_positive_criterion_inverserightvaluemask)=0))))))) /\ (exists dst_positive_code_positive_criterion_inverserightvaluefold dst_positive_scale_positive_criterion_inverserightvaluefold dst_negative_code_positive_criterion_inverserightvaluefold dst_negative_scale_positive_criterion_inverserightvaluefold dst_positive_sum_positive_criterion_inverserightvaluefold dst_negative_sum_positive_criterion_inverserightvaluefold. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) * S ((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) + ((dst_positive_scale_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) * S ((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) + ((dst_positive_scale_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))) + ((((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))))) /\ (((exists fs_u_dst_positive_criterion_inverserightvaluefoldpositive fs_v_dst_positive_criterion_inverserightvaluefoldpositive. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_start. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_start. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal + S (dst_positive_sum_positive_criterion_inverserightvaluefold) = S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal * S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (dst_positive_sum_positive_criterion_inverserightvaluefold))) /\ forall fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps. (exists fs_lt_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_bound. fs_lt_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_bound + S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps = S (dc_input_positive_criterion_inverseright)) -> exists fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand + S (fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverserightvaluefold)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand. dst_positive_code_positive_criterion_inverserightvaluefold = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverserightvaluefold) + (fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial + S (fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor + S (fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps = fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps + fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_positive_criterion_inverserightvaluefoldnegative fs_v_dst_positive_criterion_inverserightvaluefoldnegative. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_start. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_start. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal + S (dst_negative_sum_positive_criterion_inverserightvaluefold) = S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal * S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (dst_negative_sum_positive_criterion_inverserightvaluefold))) /\ forall fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps. (exists fs_lt_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_bound. fs_lt_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_bound + S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps = S (dc_input_positive_criterion_inverseright)) -> exists fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand + S (fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverserightvaluefold)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand. dst_negative_code_positive_criterion_inverserightvaluefold = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverserightvaluefold) + (fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial + S (fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor + S (fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps = fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps + fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluefoldresult ge_balance_negative_positive_criterion_inverserightvaluefoldresult. (((((dc_output_positive_criterion_inverseright) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluefoldresult) /\ (ge_balance_negative_positive_criterion_inverserightvaluefoldresult) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode. (((dc_output_positive_criterion_inverseright) = 2 * ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluefoldresult) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluefoldresult) = S ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode))) /\ ((dst_positive_sum_positive_criterion_inverserightvaluefold) + ge_balance_negative_positive_criterion_inverserightvaluefoldresult = (dst_negative_sum_positive_criterion_inverserightvaluefold) + ge_balance_positive_positive_criterion_inverserightvaluefoldresult))))))))))))))))))))))))) -> ((exists dst_positive_code_positive_criterion_unitpositive dst_positive_scale_positive_criterion_unitpositive dst_negative_code_positive_criterion_unitpositive dst_negative_scale_positive_criterion_unitpositive dst_positive_positive_criterion_unitpositive dst_negative_positive_criterion_unitpositive. (((F) = (((((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) * S ((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) + ((dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))) * S ((((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) * S ((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) + ((dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))) + ((((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))))) /\ (((((exists ff_h_pvs_positive_criterion_unitpositivepositive. ff_h_pvs_positive_criterion_unitpositivepositive + S (dst_positive_positive_criterion_unitpositive) = S ((S (1)) * dst_positive_scale_positive_criterion_unitpositive)) /\ exists ff_q_pvs_positive_criterion_unitpositivepositive. dst_positive_code_positive_criterion_unitpositive = ff_q_pvs_positive_criterion_unitpositivepositive * S ((S (1)) * dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_positive_criterion_unitpositive))) /\ (((((exists ff_h_pvs_positive_criterion_unitpositivenegative. ff_h_pvs_positive_criterion_unitpositivenegative + S (dst_negative_positive_criterion_unitpositive) = S ((S (1)) * dst_negative_scale_positive_criterion_unitpositive)) /\ exists ff_q_pvs_positive_criterion_unitpositivenegative. dst_negative_code_positive_criterion_unitpositive = ff_q_pvs_positive_criterion_unitpositivenegative * S ((S (1)) * dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_positive_criterion_unitpositive))) /\ (exists ge_balance_positive_positive_criterion_unitpositivevalue ge_balance_negative_positive_criterion_unitpositivevalue. (((((2) = 2 * (ge_balance_positive_positive_criterion_unitpositivevalue) /\ (ge_balance_negative_positive_criterion_unitpositivevalue) = 0) \/ exists ge_signed_half_positive_criterion_unitpositivevaluedecode. (((2) = 2 * ge_signed_half_positive_criterion_unitpositivevaluedecode + 1 /\ (ge_balance_positive_positive_criterion_unitpositivevalue) = 0) /\ (ge_balance_negative_positive_criterion_unitpositivevalue) = S ge_signed_half_positive_criterion_unitpositivevaluedecode))) /\ ((dst_positive_positive_criterion_unitpositive) + ge_balance_negative_positive_criterion_unitpositivevalue = (dst_negative_positive_criterion_unitpositive) + ge_balance_positive_positive_criterion_unitpositivevalue))))))))) \/ (exists dst_positive_code_positive_criterion_unitnegative dst_positive_scale_positive_criterion_unitnegative dst_negative_code_positive_criterion_unitnegative dst_negative_scale_positive_criterion_unitnegative dst_positive_positive_criterion_unitnegative dst_negative_positive_criterion_unitnegative. (((F) = (((((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) * S ((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) + ((dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))) * S ((((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) * S ((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) + ((dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))) + ((((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))))) /\ (((((exists ff_h_pvs_positive_criterion_unitnegativepositive. ff_h_pvs_positive_criterion_unitnegativepositive + S (dst_positive_positive_criterion_unitnegative) = S ((S (1)) * dst_positive_scale_positive_criterion_unitnegative)) /\ exists ff_q_pvs_positive_criterion_unitnegativepositive. dst_positive_code_positive_criterion_unitnegative = ff_q_pvs_positive_criterion_unitnegativepositive * S ((S (1)) * dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_positive_criterion_unitnegative))) /\ (((((exists ff_h_pvs_positive_criterion_unitnegativenegative. ff_h_pvs_positive_criterion_unitnegativenegative + S (dst_negative_positive_criterion_unitnegative) = S ((S (1)) * dst_negative_scale_positive_criterion_unitnegative)) /\ exists ff_q_pvs_positive_criterion_unitnegativenegative. dst_negative_code_positive_criterion_unitnegative = ff_q_pvs_positive_criterion_unitnegativenegative * S ((S (1)) * dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_positive_criterion_unitnegative))) /\ (exists ge_balance_positive_positive_criterion_unitnegativevalue ge_balance_negative_positive_criterion_unitnegativevalue. (((((1) = 2 * (ge_balance_positive_positive_criterion_unitnegativevalue) /\ (ge_balance_negative_positive_criterion_unitnegativevalue) = 0) \/ exists ge_signed_half_positive_criterion_unitnegativevaluedecode. (((1) = 2 * ge_signed_half_positive_criterion_unitnegativevaluedecode + 1 /\ (ge_balance_positive_positive_criterion_unitnegativevalue) = 0) /\ (ge_balance_negative_positive_criterion_unitnegativevalue) = S ge_signed_half_positive_criterion_unitnegativevaluedecode))) /\ ((dst_positive_positive_criterion_unitnegative) + ge_balance_negative_positive_criterion_unitnegativevalue = (dst_negative_positive_criterion_unitnegative) + ge_balance_positive_positive_criterion_unitnegativevalue))))))))))) /\ (((exists dst_positive_code_positive_criterion_unitpositive dst_positive_scale_positive_criterion_unitpositive dst_negative_code_positive_criterion_unitpositive dst_negative_scale_positive_criterion_unitpositive dst_positive_positive_criterion_unitpositive dst_negative_positive_criterion_unitpositive. (((F) = (((((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) * S ((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) + ((dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))) * S ((((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) * S ((dst_positive_code_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive)) + ((dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))) + ((((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive))) + (((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) * S ((dst_negative_code_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)) + ((dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_scale_positive_criterion_unitpositive)))))) /\ (((((exists ff_h_pvs_positive_criterion_unitpositivepositive. ff_h_pvs_positive_criterion_unitpositivepositive + S (dst_positive_positive_criterion_unitpositive) = S ((S (1)) * dst_positive_scale_positive_criterion_unitpositive)) /\ exists ff_q_pvs_positive_criterion_unitpositivepositive. dst_positive_code_positive_criterion_unitpositive = ff_q_pvs_positive_criterion_unitpositivepositive * S ((S (1)) * dst_positive_scale_positive_criterion_unitpositive) + (dst_positive_positive_criterion_unitpositive))) /\ (((((exists ff_h_pvs_positive_criterion_unitpositivenegative. ff_h_pvs_positive_criterion_unitpositivenegative + S (dst_negative_positive_criterion_unitpositive) = S ((S (1)) * dst_negative_scale_positive_criterion_unitpositive)) /\ exists ff_q_pvs_positive_criterion_unitpositivenegative. dst_negative_code_positive_criterion_unitpositive = ff_q_pvs_positive_criterion_unitpositivenegative * S ((S (1)) * dst_negative_scale_positive_criterion_unitpositive) + (dst_negative_positive_criterion_unitpositive))) /\ (exists ge_balance_positive_positive_criterion_unitpositivevalue ge_balance_negative_positive_criterion_unitpositivevalue. (((((2) = 2 * (ge_balance_positive_positive_criterion_unitpositivevalue) /\ (ge_balance_negative_positive_criterion_unitpositivevalue) = 0) \/ exists ge_signed_half_positive_criterion_unitpositivevaluedecode. (((2) = 2 * ge_signed_half_positive_criterion_unitpositivevaluedecode + 1 /\ (ge_balance_positive_positive_criterion_unitpositivevalue) = 0) /\ (ge_balance_negative_positive_criterion_unitpositivevalue) = S ge_signed_half_positive_criterion_unitpositivevaluedecode))) /\ ((dst_positive_positive_criterion_unitpositive) + ge_balance_negative_positive_criterion_unitpositivevalue = (dst_negative_positive_criterion_unitpositive) + ge_balance_positive_positive_criterion_unitpositivevalue))))))))) \/ (exists dst_positive_code_positive_criterion_unitnegative dst_positive_scale_positive_criterion_unitnegative dst_negative_code_positive_criterion_unitnegative dst_negative_scale_positive_criterion_unitnegative dst_positive_positive_criterion_unitnegative dst_negative_positive_criterion_unitnegative. (((F) = (((((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) * S ((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) + ((dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))) * S ((((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) * S ((dst_positive_code_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative)) + ((dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))) + ((((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative))) + (((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) * S ((dst_negative_code_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)) + ((dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_scale_positive_criterion_unitnegative)))))) /\ (((((exists ff_h_pvs_positive_criterion_unitnegativepositive. ff_h_pvs_positive_criterion_unitnegativepositive + S (dst_positive_positive_criterion_unitnegative) = S ((S (1)) * dst_positive_scale_positive_criterion_unitnegative)) /\ exists ff_q_pvs_positive_criterion_unitnegativepositive. dst_positive_code_positive_criterion_unitnegative = ff_q_pvs_positive_criterion_unitnegativepositive * S ((S (1)) * dst_positive_scale_positive_criterion_unitnegative) + (dst_positive_positive_criterion_unitnegative))) /\ (((((exists ff_h_pvs_positive_criterion_unitnegativenegative. ff_h_pvs_positive_criterion_unitnegativenegative + S (dst_negative_positive_criterion_unitnegative) = S ((S (1)) * dst_negative_scale_positive_criterion_unitnegative)) /\ exists ff_q_pvs_positive_criterion_unitnegativenegative. dst_negative_code_positive_criterion_unitnegative = ff_q_pvs_positive_criterion_unitnegativenegative * S ((S (1)) * dst_negative_scale_positive_criterion_unitnegative) + (dst_negative_positive_criterion_unitnegative))) /\ (exists ge_balance_positive_positive_criterion_unitnegativevalue ge_balance_negative_positive_criterion_unitnegativevalue. (((((1) = 2 * (ge_balance_positive_positive_criterion_unitnegativevalue) /\ (ge_balance_negative_positive_criterion_unitnegativevalue) = 0) \/ exists ge_signed_half_positive_criterion_unitnegativevaluedecode. (((1) = 2 * ge_signed_half_positive_criterion_unitnegativevaluedecode + 1 /\ (ge_balance_positive_positive_criterion_unitnegativevalue) = 0) /\ (ge_balance_negative_positive_criterion_unitnegativevalue) = S ge_signed_half_positive_criterion_unitnegativevaluedecode))) /\ ((dst_positive_positive_criterion_unitnegative) + ge_balance_negative_positive_criterion_unitnegativevalue = (dst_negative_positive_criterion_unitnegative) + ge_balance_positive_positive_criterion_unitnegativevalue)))))))))) -> exists G. (exists di_delta_positive_criterion_inverse. ((((exists dst_positive_code_positive_criterion_inversedeltatable dst_positive_scale_positive_criterion_inversedeltatable dst_negative_code_positive_criterion_inversedeltatable dst_negative_scale_positive_criterion_inversedeltatable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) * S ((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) + ((dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))) * S ((((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) * S ((dst_positive_code_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable)) + ((dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))) + ((((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable))) + (((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) * S ((dst_negative_code_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)) + ((dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_scale_positive_criterion_inversedeltatable)))))) /\ (forall dst_index_positive_criterion_inversedeltatable. (exists pvs_le_gap_positive_criterion_inversedeltatabledomain. pvs_le_gap_positive_criterion_inversedeltatabledomain + (dst_index_positive_criterion_inversedeltatable) = (N)) -> exists dst_positive_positive_criterion_inversedeltatable dst_negative_positive_criterion_inversedeltatable dst_value_positive_criterion_inversedeltatable. ((((exists ff_h_pvs_positive_criterion_inversedeltatableentrypositive. ff_h_pvs_positive_criterion_inversedeltatableentrypositive + S (dst_positive_positive_criterion_inversedeltatable) = S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_positive_scale_positive_criterion_inversedeltatable)) /\ exists ff_q_pvs_positive_criterion_inversedeltatableentrypositive. dst_positive_code_positive_criterion_inversedeltatable = ff_q_pvs_positive_criterion_inversedeltatableentrypositive * S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_positive_scale_positive_criterion_inversedeltatable) + (dst_positive_positive_criterion_inversedeltatable))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltatableentrynegative. ff_h_pvs_positive_criterion_inversedeltatableentrynegative + S (dst_negative_positive_criterion_inversedeltatable) = S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_negative_scale_positive_criterion_inversedeltatable)) /\ exists ff_q_pvs_positive_criterion_inversedeltatableentrynegative. dst_negative_code_positive_criterion_inversedeltatable = ff_q_pvs_positive_criterion_inversedeltatableentrynegative * S ((S (dst_index_positive_criterion_inversedeltatable)) * dst_negative_scale_positive_criterion_inversedeltatable) + (dst_negative_positive_criterion_inversedeltatable))) /\ (exists ge_balance_positive_positive_criterion_inversedeltatableentryvalue ge_balance_negative_positive_criterion_inversedeltatableentryvalue. (((((dst_value_positive_criterion_inversedeltatable) = 2 * (ge_balance_positive_positive_criterion_inversedeltatableentryvalue) /\ (ge_balance_negative_positive_criterion_inversedeltatableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode. (((dst_value_positive_criterion_inversedeltatable) = 2 * ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inversedeltatableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inversedeltatableentryvalue) = S ge_signed_half_positive_criterion_inversedeltatableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inversedeltatable) + ge_balance_negative_positive_criterion_inversedeltatableentryvalue = (dst_negative_positive_criterion_inversedeltatable) + ge_balance_positive_positive_criterion_inversedeltatableentryvalue))))))))) /\ (forall du_index_positive_criterion_inversedelta du_value_positive_criterion_inversedelta. ~(du_index_positive_criterion_inversedelta=0) -> (exists pvs_le_gap_positive_criterion_inversedeltabound. pvs_le_gap_positive_criterion_inversedeltabound + (du_index_positive_criterion_inversedelta) = (N)) -> (exists dst_positive_code_positive_criterion_inversedeltaentry dst_positive_scale_positive_criterion_inversedeltaentry dst_negative_code_positive_criterion_inversedeltaentry dst_negative_scale_positive_criterion_inversedeltaentry dst_positive_positive_criterion_inversedeltaentry dst_negative_positive_criterion_inversedeltaentry. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) * S ((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) + ((dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))) * S ((((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) * S ((dst_positive_code_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry)) + ((dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))) + ((((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry))) + (((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) * S ((dst_negative_code_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)) + ((dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_scale_positive_criterion_inversedeltaentry)))))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltaentrypositive. ff_h_pvs_positive_criterion_inversedeltaentrypositive + S (dst_positive_positive_criterion_inversedeltaentry) = S ((S (du_index_positive_criterion_inversedelta)) * dst_positive_scale_positive_criterion_inversedeltaentry)) /\ exists ff_q_pvs_positive_criterion_inversedeltaentrypositive. dst_positive_code_positive_criterion_inversedeltaentry = ff_q_pvs_positive_criterion_inversedeltaentrypositive * S ((S (du_index_positive_criterion_inversedelta)) * dst_positive_scale_positive_criterion_inversedeltaentry) + (dst_positive_positive_criterion_inversedeltaentry))) /\ (((((exists ff_h_pvs_positive_criterion_inversedeltaentrynegative. ff_h_pvs_positive_criterion_inversedeltaentrynegative + S (dst_negative_positive_criterion_inversedeltaentry) = S ((S (du_index_positive_criterion_inversedelta)) * dst_negative_scale_positive_criterion_inversedeltaentry)) /\ exists ff_q_pvs_positive_criterion_inversedeltaentrynegative. dst_negative_code_positive_criterion_inversedeltaentry = ff_q_pvs_positive_criterion_inversedeltaentrynegative * S ((S (du_index_positive_criterion_inversedelta)) * dst_negative_scale_positive_criterion_inversedeltaentry) + (dst_negative_positive_criterion_inversedeltaentry))) /\ (exists ge_balance_positive_positive_criterion_inversedeltaentryvalue ge_balance_negative_positive_criterion_inversedeltaentryvalue. (((((du_value_positive_criterion_inversedelta) = 2 * (ge_balance_positive_positive_criterion_inversedeltaentryvalue) /\ (ge_balance_negative_positive_criterion_inversedeltaentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inversedeltaentryvaluedecode. (((du_value_positive_criterion_inversedelta) = 2 * ge_signed_half_positive_criterion_inversedeltaentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inversedeltaentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inversedeltaentryvalue) = S ge_signed_half_positive_criterion_inversedeltaentryvaluedecode))) /\ ((dst_positive_positive_criterion_inversedeltaentry) + ge_balance_negative_positive_criterion_inversedeltaentryvalue = (dst_negative_positive_criterion_inversedeltaentry) + ge_balance_positive_positive_criterion_inversedeltaentryvalue))))))))) -> ((((du_index_positive_criterion_inversedelta)=1 -> (du_value_positive_criterion_inversedelta)=2) /\ (~((du_index_positive_criterion_inversedelta)=1) -> (du_value_positive_criterion_inversedelta)=0)))))) /\ (((((exists dst_positive_code_positive_criterion_inverseleftleft dst_positive_scale_positive_criterion_inverseleftleft dst_negative_code_positive_criterion_inverseleftleft dst_negative_scale_positive_criterion_inverseleftleft. (((F) = (((((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) * S ((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) + ((dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))) * S ((((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) * S ((dst_positive_code_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft)) + ((dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))) + ((((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft))) + (((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) * S ((dst_negative_code_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)) + ((dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_scale_positive_criterion_inverseleftleft)))))) /\ (forall dst_index_positive_criterion_inverseleftleft. (exists pvs_le_gap_positive_criterion_inverseleftleftdomain. pvs_le_gap_positive_criterion_inverseleftleftdomain + (dst_index_positive_criterion_inverseleftleft) = (N)) -> exists dst_positive_positive_criterion_inverseleftleft dst_negative_positive_criterion_inverseleftleft dst_value_positive_criterion_inverseleftleft. ((((exists ff_h_pvs_positive_criterion_inverseleftleftentrypositive. ff_h_pvs_positive_criterion_inverseleftleftentrypositive + S (dst_positive_positive_criterion_inverseleftleft) = S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_positive_scale_positive_criterion_inverseleftleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftleftentrypositive. dst_positive_code_positive_criterion_inverseleftleft = ff_q_pvs_positive_criterion_inverseleftleftentrypositive * S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_positive_scale_positive_criterion_inverseleftleft) + (dst_positive_positive_criterion_inverseleftleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftleftentrynegative. ff_h_pvs_positive_criterion_inverseleftleftentrynegative + S (dst_negative_positive_criterion_inverseleftleft) = S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_negative_scale_positive_criterion_inverseleftleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftleftentrynegative. dst_negative_code_positive_criterion_inverseleftleft = ff_q_pvs_positive_criterion_inverseleftleftentrynegative * S ((S (dst_index_positive_criterion_inverseleftleft)) * dst_negative_scale_positive_criterion_inverseleftleft) + (dst_negative_positive_criterion_inverseleftleft))) /\ (exists ge_balance_positive_positive_criterion_inverseleftleftentryvalue ge_balance_negative_positive_criterion_inverseleftleftentryvalue. (((((dst_value_positive_criterion_inverseleftleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftleftentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftleftentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode. (((dst_value_positive_criterion_inverseleftleft) = 2 * ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftleftentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftleftentryvalue) = S ge_signed_half_positive_criterion_inverseleftleftentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftleft) + ge_balance_negative_positive_criterion_inverseleftleftentryvalue = (dst_negative_positive_criterion_inverseleftleft) + ge_balance_positive_positive_criterion_inverseleftleftentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverseleftright dst_positive_scale_positive_criterion_inverseleftright dst_negative_code_positive_criterion_inverseleftright dst_negative_scale_positive_criterion_inverseleftright. (((G) = (((((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) * S ((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) + ((dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))) * S ((((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) * S ((dst_positive_code_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright)) + ((dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))) + ((((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright))) + (((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) * S ((dst_negative_code_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)) + ((dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_scale_positive_criterion_inverseleftright)))))) /\ (forall dst_index_positive_criterion_inverseleftright. (exists pvs_le_gap_positive_criterion_inverseleftrightdomain. pvs_le_gap_positive_criterion_inverseleftrightdomain + (dst_index_positive_criterion_inverseleftright) = (N)) -> exists dst_positive_positive_criterion_inverseleftright dst_negative_positive_criterion_inverseleftright dst_value_positive_criterion_inverseleftright. ((((exists ff_h_pvs_positive_criterion_inverseleftrightentrypositive. ff_h_pvs_positive_criterion_inverseleftrightentrypositive + S (dst_positive_positive_criterion_inverseleftright) = S ((S (dst_index_positive_criterion_inverseleftright)) * dst_positive_scale_positive_criterion_inverseleftright)) /\ exists ff_q_pvs_positive_criterion_inverseleftrightentrypositive. dst_positive_code_positive_criterion_inverseleftright = ff_q_pvs_positive_criterion_inverseleftrightentrypositive * S ((S (dst_index_positive_criterion_inverseleftright)) * dst_positive_scale_positive_criterion_inverseleftright) + (dst_positive_positive_criterion_inverseleftright))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftrightentrynegative. ff_h_pvs_positive_criterion_inverseleftrightentrynegative + S (dst_negative_positive_criterion_inverseleftright) = S ((S (dst_index_positive_criterion_inverseleftright)) * dst_negative_scale_positive_criterion_inverseleftright)) /\ exists ff_q_pvs_positive_criterion_inverseleftrightentrynegative. dst_negative_code_positive_criterion_inverseleftright = ff_q_pvs_positive_criterion_inverseleftrightentrynegative * S ((S (dst_index_positive_criterion_inverseleftright)) * dst_negative_scale_positive_criterion_inverseleftright) + (dst_negative_positive_criterion_inverseleftright))) /\ (exists ge_balance_positive_positive_criterion_inverseleftrightentryvalue ge_balance_negative_positive_criterion_inverseleftrightentryvalue. (((((dst_value_positive_criterion_inverseleftright) = 2 * (ge_balance_positive_positive_criterion_inverseleftrightentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftrightentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode. (((dst_value_positive_criterion_inverseleftright) = 2 * ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftrightentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftrightentryvalue) = S ge_signed_half_positive_criterion_inverseleftrightentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftright) + ge_balance_negative_positive_criterion_inverseleftrightentryvalue = (dst_negative_positive_criterion_inverseleftright) + ge_balance_positive_positive_criterion_inverseleftrightentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverselefttable dst_positive_scale_positive_criterion_inverselefttable dst_negative_code_positive_criterion_inverselefttable dst_negative_scale_positive_criterion_inverselefttable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) * S ((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) + ((dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))) * S ((((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) * S ((dst_positive_code_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable)) + ((dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))) + ((((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable))) + (((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) * S ((dst_negative_code_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)) + ((dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_scale_positive_criterion_inverselefttable)))))) /\ (forall dst_index_positive_criterion_inverselefttable. (exists pvs_le_gap_positive_criterion_inverselefttabledomain. pvs_le_gap_positive_criterion_inverselefttabledomain + (dst_index_positive_criterion_inverselefttable) = (N)) -> exists dst_positive_positive_criterion_inverselefttable dst_negative_positive_criterion_inverselefttable dst_value_positive_criterion_inverselefttable. ((((exists ff_h_pvs_positive_criterion_inverselefttableentrypositive. ff_h_pvs_positive_criterion_inverselefttableentrypositive + S (dst_positive_positive_criterion_inverselefttable) = S ((S (dst_index_positive_criterion_inverselefttable)) * dst_positive_scale_positive_criterion_inverselefttable)) /\ exists ff_q_pvs_positive_criterion_inverselefttableentrypositive. dst_positive_code_positive_criterion_inverselefttable = ff_q_pvs_positive_criterion_inverselefttableentrypositive * S ((S (dst_index_positive_criterion_inverselefttable)) * dst_positive_scale_positive_criterion_inverselefttable) + (dst_positive_positive_criterion_inverselefttable))) /\ (((((exists ff_h_pvs_positive_criterion_inverselefttableentrynegative. ff_h_pvs_positive_criterion_inverselefttableentrynegative + S (dst_negative_positive_criterion_inverselefttable) = S ((S (dst_index_positive_criterion_inverselefttable)) * dst_negative_scale_positive_criterion_inverselefttable)) /\ exists ff_q_pvs_positive_criterion_inverselefttableentrynegative. dst_negative_code_positive_criterion_inverselefttable = ff_q_pvs_positive_criterion_inverselefttableentrynegative * S ((S (dst_index_positive_criterion_inverselefttable)) * dst_negative_scale_positive_criterion_inverselefttable) + (dst_negative_positive_criterion_inverselefttable))) /\ (exists ge_balance_positive_positive_criterion_inverselefttableentryvalue ge_balance_negative_positive_criterion_inverselefttableentryvalue. (((((dst_value_positive_criterion_inverselefttable) = 2 * (ge_balance_positive_positive_criterion_inverselefttableentryvalue) /\ (ge_balance_negative_positive_criterion_inverselefttableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverselefttableentryvaluedecode. (((dst_value_positive_criterion_inverselefttable) = 2 * ge_signed_half_positive_criterion_inverselefttableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverselefttableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverselefttableentryvalue) = S ge_signed_half_positive_criterion_inverselefttableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverselefttable) + ge_balance_negative_positive_criterion_inverselefttableentryvalue = (dst_negative_positive_criterion_inverselefttable) + ge_balance_positive_positive_criterion_inverselefttableentryvalue))))))))) /\ (forall dc_input_positive_criterion_inverseleft dc_output_positive_criterion_inverseleft. ~(dc_input_positive_criterion_inverseleft=0) -> (exists pvs_le_gap_positive_criterion_inverseleftdomain. pvs_le_gap_positive_criterion_inverseleftdomain + (dc_input_positive_criterion_inverseleft) = (N)) -> (exists dst_positive_code_positive_criterion_inverseleftlookup dst_positive_scale_positive_criterion_inverseleftlookup dst_negative_code_positive_criterion_inverseleftlookup dst_negative_scale_positive_criterion_inverseleftlookup dst_positive_positive_criterion_inverseleftlookup dst_negative_positive_criterion_inverseleftlookup. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) * S ((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) + ((dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))) * S ((((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) * S ((dst_positive_code_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup)) + ((dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))) + ((((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup))) + (((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) * S ((dst_negative_code_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)) + ((dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_scale_positive_criterion_inverseleftlookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftlookuppositive. ff_h_pvs_positive_criterion_inverseleftlookuppositive + S (dst_positive_positive_criterion_inverseleftlookup) = S ((S (dc_input_positive_criterion_inverseleft)) * dst_positive_scale_positive_criterion_inverseleftlookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftlookuppositive. dst_positive_code_positive_criterion_inverseleftlookup = ff_q_pvs_positive_criterion_inverseleftlookuppositive * S ((S (dc_input_positive_criterion_inverseleft)) * dst_positive_scale_positive_criterion_inverseleftlookup) + (dst_positive_positive_criterion_inverseleftlookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftlookupnegative. ff_h_pvs_positive_criterion_inverseleftlookupnegative + S (dst_negative_positive_criterion_inverseleftlookup) = S ((S (dc_input_positive_criterion_inverseleft)) * dst_negative_scale_positive_criterion_inverseleftlookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftlookupnegative. dst_negative_code_positive_criterion_inverseleftlookup = ff_q_pvs_positive_criterion_inverseleftlookupnegative * S ((S (dc_input_positive_criterion_inverseleft)) * dst_negative_scale_positive_criterion_inverseleftlookup) + (dst_negative_positive_criterion_inverseleftlookup))) /\ (exists ge_balance_positive_positive_criterion_inverseleftlookupvalue ge_balance_negative_positive_criterion_inverseleftlookupvalue. (((((dc_output_positive_criterion_inverseleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftlookupvalue) /\ (ge_balance_negative_positive_criterion_inverseleftlookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftlookupvaluedecode. (((dc_output_positive_criterion_inverseleft) = 2 * ge_signed_half_positive_criterion_inverseleftlookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftlookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftlookupvalue) = S ge_signed_half_positive_criterion_inverseleftlookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftlookup) + ge_balance_negative_positive_criterion_inverseleftlookupvalue = (dst_negative_positive_criterion_inverseleftlookup) + ge_balance_positive_positive_criterion_inverseleftlookupvalue))))))))) -> (((~((dc_input_positive_criterion_inverseleft)=0)) /\ (exists dc_mask_positive_criterion_inverseleftvalue. ((((exists dst_positive_code_positive_criterion_inverseleftvaluemasktable dst_positive_scale_positive_criterion_inverseleftvaluemasktable dst_negative_code_positive_criterion_inverseleftvaluemasktable dst_negative_scale_positive_criterion_inverseleftvaluemasktable. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_scale_positive_criterion_inverseleftvaluemasktable)))))) /\ (forall dst_index_positive_criterion_inverseleftvaluemasktable. (exists pvs_le_gap_positive_criterion_inverseleftvaluemasktabledomain. pvs_le_gap_positive_criterion_inverseleftvaluemasktabledomain + (dst_index_positive_criterion_inverseleftvaluemasktable) = (dc_input_positive_criterion_inverseleft)) -> exists dst_positive_positive_criterion_inverseleftvaluemasktable dst_negative_positive_criterion_inverseleftvaluemasktable dst_value_positive_criterion_inverseleftvaluemasktable. ((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrypositive. ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrypositive + S (dst_positive_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_positive_scale_positive_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrypositive. dst_positive_code_positive_criterion_inverseleftvaluemasktable = ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrypositive * S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_positive_scale_positive_criterion_inverseleftvaluemasktable) + (dst_positive_positive_criterion_inverseleftvaluemasktable))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrynegative. ff_h_pvs_positive_criterion_inverseleftvaluemasktableentrynegative + S (dst_negative_positive_criterion_inverseleftvaluemasktable) = S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_negative_scale_positive_criterion_inverseleftvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrynegative. dst_negative_code_positive_criterion_inverseleftvaluemasktable = ff_q_pvs_positive_criterion_inverseleftvaluemasktableentrynegative * S ((S (dst_index_positive_criterion_inverseleftvaluemasktable)) * dst_negative_scale_positive_criterion_inverseleftvaluemasktable) + (dst_negative_positive_criterion_inverseleftvaluemasktable))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue. (((((dst_value_positive_criterion_inverseleftvaluemasktable) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode. (((dst_value_positive_criterion_inverseleftvaluemasktable) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemasktable) + ge_balance_negative_positive_criterion_inverseleftvaluemasktableentryvalue = (dst_negative_positive_criterion_inverseleftvaluemasktable) + ge_balance_positive_positive_criterion_inverseleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_positive_criterion_inverseleftvaluemask dc_value_positive_criterion_inverseleftvaluemask. (exists pvs_le_gap_positive_criterion_inverseleftvaluemaskdomain. pvs_le_gap_positive_criterion_inverseleftvaluemaskdomain + (dc_index_positive_criterion_inverseleftvaluemask) = (dc_input_positive_criterion_inverseleft)) -> (exists dst_positive_code_positive_criterion_inverseleftvaluemasklookup dst_positive_scale_positive_criterion_inverseleftvaluemasklookup dst_negative_code_positive_criterion_inverseleftvaluemasklookup dst_negative_scale_positive_criterion_inverseleftvaluemasklookup dst_positive_positive_criterion_inverseleftvaluemasklookup dst_negative_positive_criterion_inverseleftvaluemasklookup. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasklookuppositive. ff_h_pvs_positive_criterion_inverseleftvaluemasklookuppositive + S (dst_positive_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasklookuppositive. dst_positive_code_positive_criterion_inverseleftvaluemasklookup = ff_q_pvs_positive_criterion_inverseleftvaluemasklookuppositive * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_positive_positive_criterion_inverseleftvaluemasklookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemasklookupnegative. ff_h_pvs_positive_criterion_inverseleftvaluemasklookupnegative + S (dst_negative_positive_criterion_inverseleftvaluemasklookup) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemasklookupnegative. dst_negative_code_positive_criterion_inverseleftvaluemasklookup = ff_q_pvs_positive_criterion_inverseleftvaluemasklookupnegative * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemasklookup) + (dst_negative_positive_criterion_inverseleftvaluemasklookup))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue. (((((dc_value_positive_criterion_inverseleftvaluemask) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode. (((dc_value_positive_criterion_inverseleftvaluemask) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemasklookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemasklookup) + ge_balance_negative_positive_criterion_inverseleftvaluemasklookupvalue = (dst_negative_positive_criterion_inverseleftvaluemasklookup) + ge_balance_positive_positive_criterion_inverseleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_positive_criterion_inverseleftvaluemask)=0)) /\ (exists dc_quotient_positive_criterion_inverseleftvaluemaskentry dc_left_positive_criterion_inverseleftvaluemaskentry dc_right_positive_criterion_inverseleftvaluemaskentry. (((dc_input_positive_criterion_inverseleft)=(dc_index_positive_criterion_inverseleftvaluemask)*dc_quotient_positive_criterion_inverseleftvaluemaskentry) /\ (((exists dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft dst_positive_positive_criterion_inverseleftvaluemaskentryleft dst_negative_positive_criterion_inverseleftvaluemaskentryleft. (((F) = (((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive + S (dst_positive_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive. dst_positive_code_positive_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftpositive * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_positive_positive_criterion_inverseleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative + S (dst_negative_positive_criterion_inverseleftvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative. dst_negative_code_positive_criterion_inverseleftvaluemaskentryleft = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryleftnegative * S ((S (dc_index_positive_criterion_inverseleftvaluemask)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryleft) + (dst_negative_positive_criterion_inverseleftvaluemaskentryleft))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue. (((((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode. (((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_negative_positive_criterion_inverseleftvaluemaskentryleftvalue = (dst_negative_positive_criterion_inverseleftvaluemaskentryleft) + ge_balance_positive_positive_criterion_inverseleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverseleftvaluemaskentryright dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright dst_negative_code_positive_criterion_inverseleftvaluemaskentryright dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright dst_positive_positive_criterion_inverseleftvaluemaskentryright dst_negative_positive_criterion_inverseleftvaluemaskentryright. (((G) = (((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive + S (dst_positive_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive. dst_positive_code_positive_criterion_inverseleftvaluemaskentryright = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightpositive * S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_positive_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_positive_positive_criterion_inverseleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative. ff_h_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative + S (dst_negative_positive_criterion_inverseleftvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative. dst_negative_code_positive_criterion_inverseleftvaluemaskentryright = ff_q_pvs_positive_criterion_inverseleftvaluemaskentryrightnegative * S ((S (dc_quotient_positive_criterion_inverseleftvaluemaskentry)) * dst_negative_scale_positive_criterion_inverseleftvaluemaskentryright) + (dst_negative_positive_criterion_inverseleftvaluemaskentryright))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue. (((((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode. (((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_negative_positive_criterion_inverseleftvaluemaskentryrightvalue = (dst_negative_positive_criterion_inverseleftvaluemaskentryright) + ge_balance_positive_positive_criterion_inverseleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_positive_criterion_inverseleftvaluemaskentryproduct sto_an_positive_criterion_inverseleftvaluemaskentryproduct sto_bp_positive_criterion_inverseleftvaluemaskentryproduct sto_bn_positive_criterion_inverseleftvaluemaskentryproduct sto_cp_positive_criterion_inverseleftvaluemaskentryproduct sto_cn_positive_criterion_inverseleftvaluemaskentryproduct. (((((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_an_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft. (((dc_left_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft + 1 /\ (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_an_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductleft))) /\ ((((((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * (sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright. (((dc_right_positive_criterion_inverseleftvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright + 1 /\ (sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductright))) /\ ((((((dc_value_positive_criterion_inverseleftvaluemask) = 2 * (sto_cp_positive_criterion_inverseleftvaluemaskentryproduct) /\ (sto_cn_positive_criterion_inverseleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput. (((dc_value_positive_criterion_inverseleftvaluemask) = 2 * ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput + 1 /\ (sto_cp_positive_criterion_inverseleftvaluemaskentryproduct) = 0) /\ (sto_cn_positive_criterion_inverseleftvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverseleftvaluemaskentryproductoutput))) /\ ((sto_ap_positive_criterion_inverseleftvaluemaskentryproduct * sto_bp_positive_criterion_inverseleftvaluemaskentryproduct + sto_an_positive_criterion_inverseleftvaluemaskentryproduct * sto_bn_positive_criterion_inverseleftvaluemaskentryproduct) + sto_cn_positive_criterion_inverseleftvaluemaskentryproduct = (sto_ap_positive_criterion_inverseleftvaluemaskentryproduct * sto_bn_positive_criterion_inverseleftvaluemaskentryproduct + sto_an_positive_criterion_inverseleftvaluemaskentryproduct * sto_bp_positive_criterion_inverseleftvaluemaskentryproduct) + sto_cp_positive_criterion_inverseleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_positive_criterion_inverseleftvaluemask)=0 \/ ~(exists pvs_factor_positive_criterion_inverseleftvaluemaskentrynondivisor. (dc_input_positive_criterion_inverseleft) = (dc_index_positive_criterion_inverseleftvaluemask) * pvs_factor_positive_criterion_inverseleftvaluemaskentrynondivisor)) /\ ((dc_value_positive_criterion_inverseleftvaluemask)=0))))))) /\ (exists dst_positive_code_positive_criterion_inverseleftvaluefold dst_positive_scale_positive_criterion_inverseleftvaluefold dst_negative_code_positive_criterion_inverseleftvaluefold dst_negative_scale_positive_criterion_inverseleftvaluefold dst_positive_sum_positive_criterion_inverseleftvaluefold dst_negative_sum_positive_criterion_inverseleftvaluefold. (((dc_mask_positive_criterion_inverseleftvalue) = (((((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) + ((dst_positive_scale_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))) * S ((((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_positive_code_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold)) + ((dst_positive_scale_positive_criterion_inverseleftvaluefold) + (dst_positive_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))) + ((((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold))) + (((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) * S ((dst_negative_code_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)) + ((dst_negative_scale_positive_criterion_inverseleftvaluefold) + (dst_negative_scale_positive_criterion_inverseleftvaluefold)))))) /\ (((exists fs_u_dst_positive_criterion_inverseleftvaluefoldpositive fs_v_dst_positive_criterion_inverseleftvaluefoldpositive. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_start. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_start. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal + S (dst_positive_sum_positive_criterion_inverseleftvaluefold) = S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (dst_positive_sum_positive_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps. (exists fs_lt_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_bound. fs_lt_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_bound + S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps = S (dc_input_positive_criterion_inverseleft)) -> exists fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand. dst_positive_code_positive_criterion_inverseleftvaluefold = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverseleftvaluefold) + (fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_h_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor. fs_u_dst_positive_criterion_inverseleftvaluefoldpositive = fs_q_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldpositive) + (fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps))) /\ fs_s_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps = fs_r_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps + fs_a_dst_positive_criterion_inverseleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_positive_criterion_inverseleftvaluefoldnegative fs_v_dst_positive_criterion_inverseleftvaluefoldnegative. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_start. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_start. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal + S (dst_negative_sum_positive_criterion_inverseleftvaluefold) = S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_positive_criterion_inverseleft))) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (dst_negative_sum_positive_criterion_inverseleftvaluefold))) /\ forall fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps. (exists fs_lt_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_bound. fs_lt_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_bound + S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps = S (dc_input_positive_criterion_inverseleft)) -> exists fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverseleftvaluefold)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand. dst_negative_code_positive_criterion_inverseleftvaluefold = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverseleftvaluefold) + (fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_h_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor. fs_u_dst_positive_criterion_inverseleftvaluefoldnegative = fs_q_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverseleftvaluefoldnegative) + (fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps))) /\ fs_s_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps = fs_r_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps + fs_a_dst_positive_criterion_inverseleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_positive_criterion_inverseleftvaluefoldresult ge_balance_negative_positive_criterion_inverseleftvaluefoldresult. (((((dc_output_positive_criterion_inverseleft) = 2 * (ge_balance_positive_positive_criterion_inverseleftvaluefoldresult) /\ (ge_balance_negative_positive_criterion_inverseleftvaluefoldresult) = 0) \/ exists ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode. (((dc_output_positive_criterion_inverseleft) = 2 * ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_positive_criterion_inverseleftvaluefoldresult) = 0) /\ (ge_balance_negative_positive_criterion_inverseleftvaluefoldresult) = S ge_signed_half_positive_criterion_inverseleftvaluefoldresultdecode))) /\ ((dst_positive_sum_positive_criterion_inverseleftvaluefold) + ge_balance_negative_positive_criterion_inverseleftvaluefoldresult = (dst_negative_sum_positive_criterion_inverseleftvaluefold) + ge_balance_positive_positive_criterion_inverseleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightleft dst_positive_scale_positive_criterion_inverserightleft dst_negative_code_positive_criterion_inverserightleft dst_negative_scale_positive_criterion_inverserightleft. (((G) = (((((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) * S ((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) + ((dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))) * S ((((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) * S ((dst_positive_code_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft)) + ((dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))) + ((((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft))) + (((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) * S ((dst_negative_code_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)) + ((dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_scale_positive_criterion_inverserightleft)))))) /\ (forall dst_index_positive_criterion_inverserightleft. (exists pvs_le_gap_positive_criterion_inverserightleftdomain. pvs_le_gap_positive_criterion_inverserightleftdomain + (dst_index_positive_criterion_inverserightleft) = (N)) -> exists dst_positive_positive_criterion_inverserightleft dst_negative_positive_criterion_inverserightleft dst_value_positive_criterion_inverserightleft. ((((exists ff_h_pvs_positive_criterion_inverserightleftentrypositive. ff_h_pvs_positive_criterion_inverserightleftentrypositive + S (dst_positive_positive_criterion_inverserightleft) = S ((S (dst_index_positive_criterion_inverserightleft)) * dst_positive_scale_positive_criterion_inverserightleft)) /\ exists ff_q_pvs_positive_criterion_inverserightleftentrypositive. dst_positive_code_positive_criterion_inverserightleft = ff_q_pvs_positive_criterion_inverserightleftentrypositive * S ((S (dst_index_positive_criterion_inverserightleft)) * dst_positive_scale_positive_criterion_inverserightleft) + (dst_positive_positive_criterion_inverserightleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightleftentrynegative. ff_h_pvs_positive_criterion_inverserightleftentrynegative + S (dst_negative_positive_criterion_inverserightleft) = S ((S (dst_index_positive_criterion_inverserightleft)) * dst_negative_scale_positive_criterion_inverserightleft)) /\ exists ff_q_pvs_positive_criterion_inverserightleftentrynegative. dst_negative_code_positive_criterion_inverserightleft = ff_q_pvs_positive_criterion_inverserightleftentrynegative * S ((S (dst_index_positive_criterion_inverserightleft)) * dst_negative_scale_positive_criterion_inverserightleft) + (dst_negative_positive_criterion_inverserightleft))) /\ (exists ge_balance_positive_positive_criterion_inverserightleftentryvalue ge_balance_negative_positive_criterion_inverserightleftentryvalue. (((((dst_value_positive_criterion_inverserightleft) = 2 * (ge_balance_positive_positive_criterion_inverserightleftentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightleftentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightleftentryvaluedecode. (((dst_value_positive_criterion_inverserightleft) = 2 * ge_signed_half_positive_criterion_inverserightleftentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightleftentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightleftentryvalue) = S ge_signed_half_positive_criterion_inverserightleftentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightleft) + ge_balance_negative_positive_criterion_inverserightleftentryvalue = (dst_negative_positive_criterion_inverserightleft) + ge_balance_positive_positive_criterion_inverserightleftentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightright dst_positive_scale_positive_criterion_inverserightright dst_negative_code_positive_criterion_inverserightright dst_negative_scale_positive_criterion_inverserightright. (((F) = (((((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) * S ((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) + ((dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))) * S ((((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) * S ((dst_positive_code_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright)) + ((dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))) + ((((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright))) + (((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) * S ((dst_negative_code_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)) + ((dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_scale_positive_criterion_inverserightright)))))) /\ (forall dst_index_positive_criterion_inverserightright. (exists pvs_le_gap_positive_criterion_inverserightrightdomain. pvs_le_gap_positive_criterion_inverserightrightdomain + (dst_index_positive_criterion_inverserightright) = (N)) -> exists dst_positive_positive_criterion_inverserightright dst_negative_positive_criterion_inverserightright dst_value_positive_criterion_inverserightright. ((((exists ff_h_pvs_positive_criterion_inverserightrightentrypositive. ff_h_pvs_positive_criterion_inverserightrightentrypositive + S (dst_positive_positive_criterion_inverserightright) = S ((S (dst_index_positive_criterion_inverserightright)) * dst_positive_scale_positive_criterion_inverserightright)) /\ exists ff_q_pvs_positive_criterion_inverserightrightentrypositive. dst_positive_code_positive_criterion_inverserightright = ff_q_pvs_positive_criterion_inverserightrightentrypositive * S ((S (dst_index_positive_criterion_inverserightright)) * dst_positive_scale_positive_criterion_inverserightright) + (dst_positive_positive_criterion_inverserightright))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightrightentrynegative. ff_h_pvs_positive_criterion_inverserightrightentrynegative + S (dst_negative_positive_criterion_inverserightright) = S ((S (dst_index_positive_criterion_inverserightright)) * dst_negative_scale_positive_criterion_inverserightright)) /\ exists ff_q_pvs_positive_criterion_inverserightrightentrynegative. dst_negative_code_positive_criterion_inverserightright = ff_q_pvs_positive_criterion_inverserightrightentrynegative * S ((S (dst_index_positive_criterion_inverserightright)) * dst_negative_scale_positive_criterion_inverserightright) + (dst_negative_positive_criterion_inverserightright))) /\ (exists ge_balance_positive_positive_criterion_inverserightrightentryvalue ge_balance_negative_positive_criterion_inverserightrightentryvalue. (((((dst_value_positive_criterion_inverserightright) = 2 * (ge_balance_positive_positive_criterion_inverserightrightentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightrightentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightrightentryvaluedecode. (((dst_value_positive_criterion_inverserightright) = 2 * ge_signed_half_positive_criterion_inverserightrightentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightrightentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightrightentryvalue) = S ge_signed_half_positive_criterion_inverserightrightentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightright) + ge_balance_negative_positive_criterion_inverserightrightentryvalue = (dst_negative_positive_criterion_inverserightright) + ge_balance_positive_positive_criterion_inverserightrightentryvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserighttable dst_positive_scale_positive_criterion_inverserighttable dst_negative_code_positive_criterion_inverserighttable dst_negative_scale_positive_criterion_inverserighttable. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) * S ((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) + ((dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))) * S ((((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) * S ((dst_positive_code_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable)) + ((dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))) + ((((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable))) + (((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) * S ((dst_negative_code_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)) + ((dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_scale_positive_criterion_inverserighttable)))))) /\ (forall dst_index_positive_criterion_inverserighttable. (exists pvs_le_gap_positive_criterion_inverserighttabledomain. pvs_le_gap_positive_criterion_inverserighttabledomain + (dst_index_positive_criterion_inverserighttable) = (N)) -> exists dst_positive_positive_criterion_inverserighttable dst_negative_positive_criterion_inverserighttable dst_value_positive_criterion_inverserighttable. ((((exists ff_h_pvs_positive_criterion_inverserighttableentrypositive. ff_h_pvs_positive_criterion_inverserighttableentrypositive + S (dst_positive_positive_criterion_inverserighttable) = S ((S (dst_index_positive_criterion_inverserighttable)) * dst_positive_scale_positive_criterion_inverserighttable)) /\ exists ff_q_pvs_positive_criterion_inverserighttableentrypositive. dst_positive_code_positive_criterion_inverserighttable = ff_q_pvs_positive_criterion_inverserighttableentrypositive * S ((S (dst_index_positive_criterion_inverserighttable)) * dst_positive_scale_positive_criterion_inverserighttable) + (dst_positive_positive_criterion_inverserighttable))) /\ (((((exists ff_h_pvs_positive_criterion_inverserighttableentrynegative. ff_h_pvs_positive_criterion_inverserighttableentrynegative + S (dst_negative_positive_criterion_inverserighttable) = S ((S (dst_index_positive_criterion_inverserighttable)) * dst_negative_scale_positive_criterion_inverserighttable)) /\ exists ff_q_pvs_positive_criterion_inverserighttableentrynegative. dst_negative_code_positive_criterion_inverserighttable = ff_q_pvs_positive_criterion_inverserighttableentrynegative * S ((S (dst_index_positive_criterion_inverserighttable)) * dst_negative_scale_positive_criterion_inverserighttable) + (dst_negative_positive_criterion_inverserighttable))) /\ (exists ge_balance_positive_positive_criterion_inverserighttableentryvalue ge_balance_negative_positive_criterion_inverserighttableentryvalue. (((((dst_value_positive_criterion_inverserighttable) = 2 * (ge_balance_positive_positive_criterion_inverserighttableentryvalue) /\ (ge_balance_negative_positive_criterion_inverserighttableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserighttableentryvaluedecode. (((dst_value_positive_criterion_inverserighttable) = 2 * ge_signed_half_positive_criterion_inverserighttableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserighttableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserighttableentryvalue) = S ge_signed_half_positive_criterion_inverserighttableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserighttable) + ge_balance_negative_positive_criterion_inverserighttableentryvalue = (dst_negative_positive_criterion_inverserighttable) + ge_balance_positive_positive_criterion_inverserighttableentryvalue))))))))) /\ (forall dc_input_positive_criterion_inverseright dc_output_positive_criterion_inverseright. ~(dc_input_positive_criterion_inverseright=0) -> (exists pvs_le_gap_positive_criterion_inverserightdomain. pvs_le_gap_positive_criterion_inverserightdomain + (dc_input_positive_criterion_inverseright) = (N)) -> (exists dst_positive_code_positive_criterion_inverserightlookup dst_positive_scale_positive_criterion_inverserightlookup dst_negative_code_positive_criterion_inverserightlookup dst_negative_scale_positive_criterion_inverserightlookup dst_positive_positive_criterion_inverserightlookup dst_negative_positive_criterion_inverserightlookup. (((di_delta_positive_criterion_inverse) = (((((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) * S ((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) + ((dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))) * S ((((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) * S ((dst_positive_code_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup)) + ((dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))) + ((((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup))) + (((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) * S ((dst_negative_code_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)) + ((dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_scale_positive_criterion_inverserightlookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightlookuppositive. ff_h_pvs_positive_criterion_inverserightlookuppositive + S (dst_positive_positive_criterion_inverserightlookup) = S ((S (dc_input_positive_criterion_inverseright)) * dst_positive_scale_positive_criterion_inverserightlookup)) /\ exists ff_q_pvs_positive_criterion_inverserightlookuppositive. dst_positive_code_positive_criterion_inverserightlookup = ff_q_pvs_positive_criterion_inverserightlookuppositive * S ((S (dc_input_positive_criterion_inverseright)) * dst_positive_scale_positive_criterion_inverserightlookup) + (dst_positive_positive_criterion_inverserightlookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightlookupnegative. ff_h_pvs_positive_criterion_inverserightlookupnegative + S (dst_negative_positive_criterion_inverserightlookup) = S ((S (dc_input_positive_criterion_inverseright)) * dst_negative_scale_positive_criterion_inverserightlookup)) /\ exists ff_q_pvs_positive_criterion_inverserightlookupnegative. dst_negative_code_positive_criterion_inverserightlookup = ff_q_pvs_positive_criterion_inverserightlookupnegative * S ((S (dc_input_positive_criterion_inverseright)) * dst_negative_scale_positive_criterion_inverserightlookup) + (dst_negative_positive_criterion_inverserightlookup))) /\ (exists ge_balance_positive_positive_criterion_inverserightlookupvalue ge_balance_negative_positive_criterion_inverserightlookupvalue. (((((dc_output_positive_criterion_inverseright) = 2 * (ge_balance_positive_positive_criterion_inverserightlookupvalue) /\ (ge_balance_negative_positive_criterion_inverserightlookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightlookupvaluedecode. (((dc_output_positive_criterion_inverseright) = 2 * ge_signed_half_positive_criterion_inverserightlookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightlookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightlookupvalue) = S ge_signed_half_positive_criterion_inverserightlookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightlookup) + ge_balance_negative_positive_criterion_inverserightlookupvalue = (dst_negative_positive_criterion_inverserightlookup) + ge_balance_positive_positive_criterion_inverserightlookupvalue))))))))) -> (((~((dc_input_positive_criterion_inverseright)=0)) /\ (exists dc_mask_positive_criterion_inverserightvalue. ((((exists dst_positive_code_positive_criterion_inverserightvaluemasktable dst_positive_scale_positive_criterion_inverserightvaluemasktable dst_negative_code_positive_criterion_inverserightvaluemasktable dst_negative_scale_positive_criterion_inverserightvaluemasktable. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable))) + (((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_scale_positive_criterion_inverserightvaluemasktable)))))) /\ (forall dst_index_positive_criterion_inverserightvaluemasktable. (exists pvs_le_gap_positive_criterion_inverserightvaluemasktabledomain. pvs_le_gap_positive_criterion_inverserightvaluemasktabledomain + (dst_index_positive_criterion_inverserightvaluemasktable) = (dc_input_positive_criterion_inverseright)) -> exists dst_positive_positive_criterion_inverserightvaluemasktable dst_negative_positive_criterion_inverserightvaluemasktable dst_value_positive_criterion_inverserightvaluemasktable. ((((exists ff_h_pvs_positive_criterion_inverserightvaluemasktableentrypositive. ff_h_pvs_positive_criterion_inverserightvaluemasktableentrypositive + S (dst_positive_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_positive_scale_positive_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasktableentrypositive. dst_positive_code_positive_criterion_inverserightvaluemasktable = ff_q_pvs_positive_criterion_inverserightvaluemasktableentrypositive * S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_positive_scale_positive_criterion_inverserightvaluemasktable) + (dst_positive_positive_criterion_inverserightvaluemasktable))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasktableentrynegative. ff_h_pvs_positive_criterion_inverserightvaluemasktableentrynegative + S (dst_negative_positive_criterion_inverserightvaluemasktable) = S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_negative_scale_positive_criterion_inverserightvaluemasktable)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasktableentrynegative. dst_negative_code_positive_criterion_inverserightvaluemasktable = ff_q_pvs_positive_criterion_inverserightvaluemasktableentrynegative * S ((S (dst_index_positive_criterion_inverserightvaluemasktable)) * dst_negative_scale_positive_criterion_inverserightvaluemasktable) + (dst_negative_positive_criterion_inverserightvaluemasktable))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue. (((((dst_value_positive_criterion_inverserightvaluemasktable) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode. (((dst_value_positive_criterion_inverserightvaluemasktable) = 2 * ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue) = S ge_signed_half_positive_criterion_inverserightvaluemasktableentryvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemasktable) + ge_balance_negative_positive_criterion_inverserightvaluemasktableentryvalue = (dst_negative_positive_criterion_inverserightvaluemasktable) + ge_balance_positive_positive_criterion_inverserightvaluemasktableentryvalue))))))))) /\ (forall dc_index_positive_criterion_inverserightvaluemask dc_value_positive_criterion_inverserightvaluemask. (exists pvs_le_gap_positive_criterion_inverserightvaluemaskdomain. pvs_le_gap_positive_criterion_inverserightvaluemaskdomain + (dc_index_positive_criterion_inverserightvaluemask) = (dc_input_positive_criterion_inverseright)) -> (exists dst_positive_code_positive_criterion_inverserightvaluemasklookup dst_positive_scale_positive_criterion_inverserightvaluemasklookup dst_negative_code_positive_criterion_inverserightvaluemasklookup dst_negative_scale_positive_criterion_inverserightvaluemasklookup dst_positive_positive_criterion_inverserightvaluemasklookup dst_negative_positive_criterion_inverserightvaluemasklookup. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_positive_code_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup))) + (((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) * S ((dst_negative_code_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) + ((dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_scale_positive_criterion_inverserightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasklookuppositive. ff_h_pvs_positive_criterion_inverserightvaluemasklookuppositive + S (dst_positive_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasklookuppositive. dst_positive_code_positive_criterion_inverserightvaluemasklookup = ff_q_pvs_positive_criterion_inverserightvaluemasklookuppositive * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemasklookup) + (dst_positive_positive_criterion_inverserightvaluemasklookup))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemasklookupnegative. ff_h_pvs_positive_criterion_inverserightvaluemasklookupnegative + S (dst_negative_positive_criterion_inverserightvaluemasklookup) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemasklookup)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemasklookupnegative. dst_negative_code_positive_criterion_inverserightvaluemasklookup = ff_q_pvs_positive_criterion_inverserightvaluemasklookupnegative * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemasklookup) + (dst_negative_positive_criterion_inverserightvaluemasklookup))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue. (((((dc_value_positive_criterion_inverserightvaluemask) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode. (((dc_value_positive_criterion_inverserightvaluemask) = 2 * ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue) = S ge_signed_half_positive_criterion_inverserightvaluemasklookupvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemasklookup) + ge_balance_negative_positive_criterion_inverserightvaluemasklookupvalue = (dst_negative_positive_criterion_inverserightvaluemasklookup) + ge_balance_positive_positive_criterion_inverserightvaluemasklookupvalue))))))))) -> ((((~((dc_index_positive_criterion_inverserightvaluemask)=0)) /\ (exists dc_quotient_positive_criterion_inverserightvaluemaskentry dc_left_positive_criterion_inverserightvaluemaskentry dc_right_positive_criterion_inverserightvaluemaskentry. (((dc_input_positive_criterion_inverseright)=(dc_index_positive_criterion_inverserightvaluemask)*dc_quotient_positive_criterion_inverserightvaluemaskentry) /\ (((exists dst_positive_code_positive_criterion_inverserightvaluemaskentryleft dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft dst_negative_code_positive_criterion_inverserightvaluemaskentryleft dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft dst_positive_positive_criterion_inverserightvaluemaskentryleft dst_negative_positive_criterion_inverserightvaluemaskentryleft. (((G) = (((((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftpositive. ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftpositive + S (dst_positive_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftpositive. dst_positive_code_positive_criterion_inverserightvaluemaskentryleft = ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftpositive * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_positive_positive_criterion_inverserightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftnegative. ff_h_pvs_positive_criterion_inverserightvaluemaskentryleftnegative + S (dst_negative_positive_criterion_inverserightvaluemaskentryleft) = S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftnegative. dst_negative_code_positive_criterion_inverserightvaluemaskentryleft = ff_q_pvs_positive_criterion_inverserightvaluemaskentryleftnegative * S ((S (dc_index_positive_criterion_inverserightvaluemask)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryleft) + (dst_negative_positive_criterion_inverserightvaluemaskentryleft))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue. (((((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode. (((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_negative_positive_criterion_inverserightvaluemaskentryleftvalue = (dst_negative_positive_criterion_inverserightvaluemaskentryleft) + ge_balance_positive_positive_criterion_inverserightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_positive_criterion_inverserightvaluemaskentryright dst_positive_scale_positive_criterion_inverserightvaluemaskentryright dst_negative_code_positive_criterion_inverserightvaluemaskentryright dst_negative_scale_positive_criterion_inverserightvaluemaskentryright dst_positive_positive_criterion_inverserightvaluemaskentryright dst_negative_positive_criterion_inverserightvaluemaskentryright. (((F) = (((((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_positive_code_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))) + ((((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright))) + (((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) * S ((dst_negative_code_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) + ((dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightpositive. ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightpositive + S (dst_positive_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightpositive. dst_positive_code_positive_criterion_inverserightvaluemaskentryright = ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightpositive * S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_positive_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_positive_positive_criterion_inverserightvaluemaskentryright))) /\ (((((exists ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightnegative. ff_h_pvs_positive_criterion_inverserightvaluemaskentryrightnegative + S (dst_negative_positive_criterion_inverserightvaluemaskentryright) = S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryright)) /\ exists ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightnegative. dst_negative_code_positive_criterion_inverserightvaluemaskentryright = ff_q_pvs_positive_criterion_inverserightvaluemaskentryrightnegative * S ((S (dc_quotient_positive_criterion_inverserightvaluemaskentry)) * dst_negative_scale_positive_criterion_inverserightvaluemaskentryright) + (dst_negative_positive_criterion_inverserightvaluemaskentryright))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue. (((((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode. (((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_positive_criterion_inverserightvaluemaskentryright) + ge_balance_negative_positive_criterion_inverserightvaluemaskentryrightvalue = (dst_negative_positive_criterion_inverserightvaluemaskentryright) + ge_balance_positive_positive_criterion_inverserightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_positive_criterion_inverserightvaluemaskentryproduct sto_an_positive_criterion_inverserightvaluemaskentryproduct sto_bp_positive_criterion_inverserightvaluemaskentryproduct sto_bn_positive_criterion_inverserightvaluemaskentryproduct sto_cp_positive_criterion_inverserightvaluemaskentryproduct sto_cn_positive_criterion_inverserightvaluemaskentryproduct. (((((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * (sto_ap_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_an_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft. (((dc_left_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft + 1 /\ (sto_ap_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_an_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductleft))) /\ ((((((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * (sto_bp_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_bn_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright. (((dc_right_positive_criterion_inverserightvaluemaskentry) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright + 1 /\ (sto_bp_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_bn_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductright))) /\ ((((((dc_value_positive_criterion_inverserightvaluemask) = 2 * (sto_cp_positive_criterion_inverserightvaluemaskentryproduct) /\ (sto_cn_positive_criterion_inverserightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput. (((dc_value_positive_criterion_inverserightvaluemask) = 2 * ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput + 1 /\ (sto_cp_positive_criterion_inverserightvaluemaskentryproduct) = 0) /\ (sto_cn_positive_criterion_inverserightvaluemaskentryproduct) = S ge_signed_half_positive_criterion_inverserightvaluemaskentryproductoutput))) /\ ((sto_ap_positive_criterion_inverserightvaluemaskentryproduct * sto_bp_positive_criterion_inverserightvaluemaskentryproduct + sto_an_positive_criterion_inverserightvaluemaskentryproduct * sto_bn_positive_criterion_inverserightvaluemaskentryproduct) + sto_cn_positive_criterion_inverserightvaluemaskentryproduct = (sto_ap_positive_criterion_inverserightvaluemaskentryproduct * sto_bn_positive_criterion_inverserightvaluemaskentryproduct + sto_an_positive_criterion_inverserightvaluemaskentryproduct * sto_bp_positive_criterion_inverserightvaluemaskentryproduct) + sto_cp_positive_criterion_inverserightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_positive_criterion_inverserightvaluemask)=0 \/ ~(exists pvs_factor_positive_criterion_inverserightvaluemaskentrynondivisor. (dc_input_positive_criterion_inverseright) = (dc_index_positive_criterion_inverserightvaluemask) * pvs_factor_positive_criterion_inverserightvaluemaskentrynondivisor)) /\ ((dc_value_positive_criterion_inverserightvaluemask)=0))))))) /\ (exists dst_positive_code_positive_criterion_inverserightvaluefold dst_positive_scale_positive_criterion_inverserightvaluefold dst_negative_code_positive_criterion_inverserightvaluefold dst_negative_scale_positive_criterion_inverserightvaluefold dst_positive_sum_positive_criterion_inverserightvaluefold dst_negative_sum_positive_criterion_inverserightvaluefold. (((dc_mask_positive_criterion_inverserightvalue) = (((((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) * S ((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) + ((dst_positive_scale_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))) * S ((((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) * S ((dst_positive_code_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold)) + ((dst_positive_scale_positive_criterion_inverserightvaluefold) + (dst_positive_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))) + ((((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold))) + (((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) * S ((dst_negative_code_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)) + ((dst_negative_scale_positive_criterion_inverserightvaluefold) + (dst_negative_scale_positive_criterion_inverserightvaluefold)))))) /\ (((exists fs_u_dst_positive_criterion_inverserightvaluefoldpositive fs_v_dst_positive_criterion_inverserightvaluefoldpositive. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_start. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_start. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal + S (dst_positive_sum_positive_criterion_inverserightvaluefold) = S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_terminal * S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (dst_positive_sum_positive_criterion_inverserightvaluefold))) /\ forall fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps. (exists fs_lt_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_bound. fs_lt_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_bound + S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps = S (dc_input_positive_criterion_inverseright)) -> exists fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand + S (fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverserightvaluefold)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand. dst_positive_code_positive_criterion_inverserightvaluefold = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * dst_positive_scale_positive_criterion_inverserightvaluefold) + (fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial + S (fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_h_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor + S (fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor. fs_u_dst_positive_criterion_inverserightvaluefoldpositive = fs_q_dst_positive_criterion_inverserightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldpositive) + (fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps))) /\ fs_s_dst_positive_criterion_inverserightvaluefoldpositive_body_steps = fs_r_dst_positive_criterion_inverserightvaluefoldpositive_body_steps + fs_a_dst_positive_criterion_inverserightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_positive_criterion_inverserightvaluefoldnegative fs_v_dst_positive_criterion_inverserightvaluefoldnegative. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_start. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_start. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal + S (dst_negative_sum_positive_criterion_inverserightvaluefold) = S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_terminal * S ((S (S (dc_input_positive_criterion_inverseright))) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (dst_negative_sum_positive_criterion_inverserightvaluefold))) /\ forall fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps. (exists fs_lt_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_bound. fs_lt_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_bound + S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps = S (dc_input_positive_criterion_inverseright)) -> exists fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps. ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand + S (fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverserightvaluefold)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand. dst_negative_code_positive_criterion_inverserightvaluefold = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * dst_negative_scale_positive_criterion_inverserightvaluefold) + (fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial + S (fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_h_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor + S (fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative)) /\ exists fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor. fs_u_dst_positive_criterion_inverserightvaluefoldnegative = fs_q_dst_positive_criterion_inverserightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)) * fs_v_dst_positive_criterion_inverserightvaluefoldnegative) + (fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps))) /\ fs_s_dst_positive_criterion_inverserightvaluefoldnegative_body_steps = fs_r_dst_positive_criterion_inverserightvaluefoldnegative_body_steps + fs_a_dst_positive_criterion_inverserightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_positive_criterion_inverserightvaluefoldresult ge_balance_negative_positive_criterion_inverserightvaluefoldresult. (((((dc_output_positive_criterion_inverseright) = 2 * (ge_balance_positive_positive_criterion_inverserightvaluefoldresult) /\ (ge_balance_negative_positive_criterion_inverserightvaluefoldresult) = 0) \/ exists ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode. (((dc_output_positive_criterion_inverseright) = 2 * ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode + 1 /\ (ge_balance_positive_positive_criterion_inverserightvaluefoldresult) = 0) /\ (ge_balance_negative_positive_criterion_inverserightvaluefoldresult) = S ge_signed_half_positive_criterion_inverserightvaluefoldresultdecode))) /\ ((dst_positive_sum_positive_criterion_inverserightvaluefold) + ge_balance_negative_positive_criterion_inverserightvaluefoldresult = (dst_negative_sum_positive_criterion_inverserightvaluefold) + ge_balance_positive_positive_criterion_inverserightvaluefoldresult))))))))))))))))))))))))))Complete tactic proof in conservative notation
All 25 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
25 script commands · 10 reading checkpoints · 1 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–4
02Separate the logical casesL5–5
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L5
split
03Fix variables and assumptionsL6–6
Work with arbitrary variables or the premises of the current implication.
- L6
intro hi
04Separate the logical casesL7–7
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L7
cases hi
05Use earlier factsL8–13
Instantiate or apply named facts and discharge the corresponding proof obligations.
06Fix variables and assumptionsL14–14
Work with arbitrary variables or the premises of the current implication.
- L14
intro hu
07Establish hgL15–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet inverse from unit at one.
- L15
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 - L16
specialize dirichlet_inverse_from_unit_at_one (N) - L17
specialize dirichlet_inverse_from_unit_at_one (F) - L18
specialize dirichlet_inverse_from_unit_at_one (0) - L19
apply dirichlet_inverse_from_unit_at_one - L20
exact hF - L21
exact hu
08Separate the logical casesL22–23
09Construct an explicit witnessL24–24
Supply the displayed value, then prove that it has the required property.
- L24
exists x
10Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact hg_witness_left
Original defined command ledger · 25 lines
- 0001
intro N - 0002
intro F - 0003
intro hF - 0004
intro hn - 0005
split - 0006
intro hi - 0007
cases hi - 0008
specialize dirichlet_inverse_requires_unit_at_one (N) - 0009
specialize dirichlet_inverse_requires_unit_at_one (F) - 0010
specialize dirichlet_inverse_requires_unit_at_one (x) - 0011
apply dirichlet_inverse_requires_unit_at_one - 0012
exact hi_witness - 0013
exact hn - 0014
intro hu - 0015
have hg : ∃ G. DirichletInverse(N,F,G) ∧ ArithAt(G,0,0) - 0016
specialize dirichlet_inverse_from_unit_at_one (N) - 0017
specialize dirichlet_inverse_from_unit_at_one (F) - 0018
specialize dirichlet_inverse_from_unit_at_one (0) - 0019
apply dirichlet_inverse_from_unit_at_one - 0020
exact hF - 0021
exact hu - 0022
cases hg - 0023
cases hg_witness - 0024
exists x - 0025
exact hg_witness_left