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. ∀ K. ∀ F. ∀ G. DirichletInverse(N,F,G) → Le(K,N) → DirichletInverse(K,F,G)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N K F G. (exists di_delta_inverse_restrict_source. ((((exists dst_positive_code_inverse_restrict_sourcedeltatable dst_positive_scale_inverse_restrict_sourcedeltatable dst_negative_code_inverse_restrict_sourcedeltatable dst_negative_scale_inverse_restrict_sourcedeltatable. (((di_delta_inverse_restrict_source) = (((((dst_positive_code_inverse_restrict_sourcedeltatable) + (dst_positive_scale_inverse_restrict_sourcedeltatable)) * S ((dst_positive_code_inverse_restrict_sourcedeltatable) + (dst_positive_scale_inverse_restrict_sourcedeltatable)) + ((dst_positive_scale_inverse_restrict_sourcedeltatable) + (dst_positive_scale_inverse_restrict_sourcedeltatable))) + (((dst_negative_code_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)) * S ((dst_negative_code_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)) + ((dst_negative_scale_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)))) * S ((((dst_positive_code_inverse_restrict_sourcedeltatable) + (dst_positive_scale_inverse_restrict_sourcedeltatable)) * S ((dst_positive_code_inverse_restrict_sourcedeltatable) + (dst_positive_scale_inverse_restrict_sourcedeltatable)) + ((dst_positive_scale_inverse_restrict_sourcedeltatable) + (dst_positive_scale_inverse_restrict_sourcedeltatable))) + (((dst_negative_code_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)) * S ((dst_negative_code_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)) + ((dst_negative_scale_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)))) + ((((dst_negative_code_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)) * S ((dst_negative_code_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)) + ((dst_negative_scale_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable))) + (((dst_negative_code_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)) * S ((dst_negative_code_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)) + ((dst_negative_scale_inverse_restrict_sourcedeltatable) + (dst_negative_scale_inverse_restrict_sourcedeltatable)))))) /\ (forall dst_index_inverse_restrict_sourcedeltatable. (exists pvs_le_gap_inverse_restrict_sourcedeltatabledomain. pvs_le_gap_inverse_restrict_sourcedeltatabledomain + (dst_index_inverse_restrict_sourcedeltatable) = (N)) -> exists dst_positive_inverse_restrict_sourcedeltatable dst_negative_inverse_restrict_sourcedeltatable dst_value_inverse_restrict_sourcedeltatable. ((((exists ff_h_pvs_inverse_restrict_sourcedeltatableentrypositive. ff_h_pvs_inverse_restrict_sourcedeltatableentrypositive + S (dst_positive_inverse_restrict_sourcedeltatable) = S ((S (dst_index_inverse_restrict_sourcedeltatable)) * dst_positive_scale_inverse_restrict_sourcedeltatable)) /\ exists ff_q_pvs_inverse_restrict_sourcedeltatableentrypositive. dst_positive_code_inverse_restrict_sourcedeltatable = ff_q_pvs_inverse_restrict_sourcedeltatableentrypositive * S ((S (dst_index_inverse_restrict_sourcedeltatable)) * dst_positive_scale_inverse_restrict_sourcedeltatable) + (dst_positive_inverse_restrict_sourcedeltatable))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcedeltatableentrynegative. ff_h_pvs_inverse_restrict_sourcedeltatableentrynegative + S (dst_negative_inverse_restrict_sourcedeltatable) = S ((S (dst_index_inverse_restrict_sourcedeltatable)) * dst_negative_scale_inverse_restrict_sourcedeltatable)) /\ exists ff_q_pvs_inverse_restrict_sourcedeltatableentrynegative. dst_negative_code_inverse_restrict_sourcedeltatable = ff_q_pvs_inverse_restrict_sourcedeltatableentrynegative * S ((S (dst_index_inverse_restrict_sourcedeltatable)) * dst_negative_scale_inverse_restrict_sourcedeltatable) + (dst_negative_inverse_restrict_sourcedeltatable))) /\ (exists ge_balance_positive_inverse_restrict_sourcedeltatableentryvalue ge_balance_negative_inverse_restrict_sourcedeltatableentryvalue. (((((dst_value_inverse_restrict_sourcedeltatable) = 2 * (ge_balance_positive_inverse_restrict_sourcedeltatableentryvalue) /\ (ge_balance_negative_inverse_restrict_sourcedeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcedeltatableentryvaluedecode. (((dst_value_inverse_restrict_sourcedeltatable) = 2 * ge_signed_half_inverse_restrict_sourcedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcedeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcedeltatableentryvalue) = S ge_signed_half_inverse_restrict_sourcedeltatableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcedeltatable) + ge_balance_negative_inverse_restrict_sourcedeltatableentryvalue = (dst_negative_inverse_restrict_sourcedeltatable) + ge_balance_positive_inverse_restrict_sourcedeltatableentryvalue))))))))) /\ (forall du_index_inverse_restrict_sourcedelta du_value_inverse_restrict_sourcedelta. ~(du_index_inverse_restrict_sourcedelta=0) -> (exists pvs_le_gap_inverse_restrict_sourcedeltabound. pvs_le_gap_inverse_restrict_sourcedeltabound + (du_index_inverse_restrict_sourcedelta) = (N)) -> (exists dst_positive_code_inverse_restrict_sourcedeltaentry dst_positive_scale_inverse_restrict_sourcedeltaentry dst_negative_code_inverse_restrict_sourcedeltaentry dst_negative_scale_inverse_restrict_sourcedeltaentry dst_positive_inverse_restrict_sourcedeltaentry dst_negative_inverse_restrict_sourcedeltaentry. (((di_delta_inverse_restrict_source) = (((((dst_positive_code_inverse_restrict_sourcedeltaentry) + (dst_positive_scale_inverse_restrict_sourcedeltaentry)) * S ((dst_positive_code_inverse_restrict_sourcedeltaentry) + (dst_positive_scale_inverse_restrict_sourcedeltaentry)) + ((dst_positive_scale_inverse_restrict_sourcedeltaentry) + (dst_positive_scale_inverse_restrict_sourcedeltaentry))) + (((dst_negative_code_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)) * S ((dst_negative_code_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)) + ((dst_negative_scale_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)))) * S ((((dst_positive_code_inverse_restrict_sourcedeltaentry) + (dst_positive_scale_inverse_restrict_sourcedeltaentry)) * S ((dst_positive_code_inverse_restrict_sourcedeltaentry) + (dst_positive_scale_inverse_restrict_sourcedeltaentry)) + ((dst_positive_scale_inverse_restrict_sourcedeltaentry) + (dst_positive_scale_inverse_restrict_sourcedeltaentry))) + (((dst_negative_code_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)) * S ((dst_negative_code_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)) + ((dst_negative_scale_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)))) + ((((dst_negative_code_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)) * S ((dst_negative_code_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)) + ((dst_negative_scale_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry))) + (((dst_negative_code_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)) * S ((dst_negative_code_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)) + ((dst_negative_scale_inverse_restrict_sourcedeltaentry) + (dst_negative_scale_inverse_restrict_sourcedeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcedeltaentrypositive. ff_h_pvs_inverse_restrict_sourcedeltaentrypositive + S (dst_positive_inverse_restrict_sourcedeltaentry) = S ((S (du_index_inverse_restrict_sourcedelta)) * dst_positive_scale_inverse_restrict_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_restrict_sourcedeltaentrypositive. dst_positive_code_inverse_restrict_sourcedeltaentry = ff_q_pvs_inverse_restrict_sourcedeltaentrypositive * S ((S (du_index_inverse_restrict_sourcedelta)) * dst_positive_scale_inverse_restrict_sourcedeltaentry) + (dst_positive_inverse_restrict_sourcedeltaentry))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcedeltaentrynegative. ff_h_pvs_inverse_restrict_sourcedeltaentrynegative + S (dst_negative_inverse_restrict_sourcedeltaentry) = S ((S (du_index_inverse_restrict_sourcedelta)) * dst_negative_scale_inverse_restrict_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_restrict_sourcedeltaentrynegative. dst_negative_code_inverse_restrict_sourcedeltaentry = ff_q_pvs_inverse_restrict_sourcedeltaentrynegative * S ((S (du_index_inverse_restrict_sourcedelta)) * dst_negative_scale_inverse_restrict_sourcedeltaentry) + (dst_negative_inverse_restrict_sourcedeltaentry))) /\ (exists ge_balance_positive_inverse_restrict_sourcedeltaentryvalue ge_balance_negative_inverse_restrict_sourcedeltaentryvalue. (((((du_value_inverse_restrict_sourcedelta) = 2 * (ge_balance_positive_inverse_restrict_sourcedeltaentryvalue) /\ (ge_balance_negative_inverse_restrict_sourcedeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcedeltaentryvaluedecode. (((du_value_inverse_restrict_sourcedelta) = 2 * ge_signed_half_inverse_restrict_sourcedeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcedeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcedeltaentryvalue) = S ge_signed_half_inverse_restrict_sourcedeltaentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcedeltaentry) + ge_balance_negative_inverse_restrict_sourcedeltaentryvalue = (dst_negative_inverse_restrict_sourcedeltaentry) + ge_balance_positive_inverse_restrict_sourcedeltaentryvalue))))))))) -> ((((du_index_inverse_restrict_sourcedelta)=1 -> (du_value_inverse_restrict_sourcedelta)=2) /\ (~((du_index_inverse_restrict_sourcedelta)=1) -> (du_value_inverse_restrict_sourcedelta)=0)))))) /\ (((((exists dst_positive_code_inverse_restrict_sourceleftleft dst_positive_scale_inverse_restrict_sourceleftleft dst_negative_code_inverse_restrict_sourceleftleft dst_negative_scale_inverse_restrict_sourceleftleft. (((F) = (((((dst_positive_code_inverse_restrict_sourceleftleft) + (dst_positive_scale_inverse_restrict_sourceleftleft)) * S ((dst_positive_code_inverse_restrict_sourceleftleft) + (dst_positive_scale_inverse_restrict_sourceleftleft)) + ((dst_positive_scale_inverse_restrict_sourceleftleft) + (dst_positive_scale_inverse_restrict_sourceleftleft))) + (((dst_negative_code_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)) * S ((dst_negative_code_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)) + ((dst_negative_scale_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)))) * S ((((dst_positive_code_inverse_restrict_sourceleftleft) + (dst_positive_scale_inverse_restrict_sourceleftleft)) * S ((dst_positive_code_inverse_restrict_sourceleftleft) + (dst_positive_scale_inverse_restrict_sourceleftleft)) + ((dst_positive_scale_inverse_restrict_sourceleftleft) + (dst_positive_scale_inverse_restrict_sourceleftleft))) + (((dst_negative_code_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)) * S ((dst_negative_code_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)) + ((dst_negative_scale_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)))) + ((((dst_negative_code_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)) * S ((dst_negative_code_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)) + ((dst_negative_scale_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft))) + (((dst_negative_code_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)) * S ((dst_negative_code_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)) + ((dst_negative_scale_inverse_restrict_sourceleftleft) + (dst_negative_scale_inverse_restrict_sourceleftleft)))))) /\ (forall dst_index_inverse_restrict_sourceleftleft. (exists pvs_le_gap_inverse_restrict_sourceleftleftdomain. pvs_le_gap_inverse_restrict_sourceleftleftdomain + (dst_index_inverse_restrict_sourceleftleft) = (N)) -> exists dst_positive_inverse_restrict_sourceleftleft dst_negative_inverse_restrict_sourceleftleft dst_value_inverse_restrict_sourceleftleft. ((((exists ff_h_pvs_inverse_restrict_sourceleftleftentrypositive. ff_h_pvs_inverse_restrict_sourceleftleftentrypositive + S (dst_positive_inverse_restrict_sourceleftleft) = S ((S (dst_index_inverse_restrict_sourceleftleft)) * dst_positive_scale_inverse_restrict_sourceleftleft)) /\ exists ff_q_pvs_inverse_restrict_sourceleftleftentrypositive. dst_positive_code_inverse_restrict_sourceleftleft = ff_q_pvs_inverse_restrict_sourceleftleftentrypositive * S ((S (dst_index_inverse_restrict_sourceleftleft)) * dst_positive_scale_inverse_restrict_sourceleftleft) + (dst_positive_inverse_restrict_sourceleftleft))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftleftentrynegative. ff_h_pvs_inverse_restrict_sourceleftleftentrynegative + S (dst_negative_inverse_restrict_sourceleftleft) = S ((S (dst_index_inverse_restrict_sourceleftleft)) * dst_negative_scale_inverse_restrict_sourceleftleft)) /\ exists ff_q_pvs_inverse_restrict_sourceleftleftentrynegative. dst_negative_code_inverse_restrict_sourceleftleft = ff_q_pvs_inverse_restrict_sourceleftleftentrynegative * S ((S (dst_index_inverse_restrict_sourceleftleft)) * dst_negative_scale_inverse_restrict_sourceleftleft) + (dst_negative_inverse_restrict_sourceleftleft))) /\ (exists ge_balance_positive_inverse_restrict_sourceleftleftentryvalue ge_balance_negative_inverse_restrict_sourceleftleftentryvalue. (((((dst_value_inverse_restrict_sourceleftleft) = 2 * (ge_balance_positive_inverse_restrict_sourceleftleftentryvalue) /\ (ge_balance_negative_inverse_restrict_sourceleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftleftentryvaluedecode. (((dst_value_inverse_restrict_sourceleftleft) = 2 * ge_signed_half_inverse_restrict_sourceleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourceleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourceleftleftentryvalue) = S ge_signed_half_inverse_restrict_sourceleftleftentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourceleftleft) + ge_balance_negative_inverse_restrict_sourceleftleftentryvalue = (dst_negative_inverse_restrict_sourceleftleft) + ge_balance_positive_inverse_restrict_sourceleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_sourceleftright dst_positive_scale_inverse_restrict_sourceleftright dst_negative_code_inverse_restrict_sourceleftright dst_negative_scale_inverse_restrict_sourceleftright. (((G) = (((((dst_positive_code_inverse_restrict_sourceleftright) + (dst_positive_scale_inverse_restrict_sourceleftright)) * S ((dst_positive_code_inverse_restrict_sourceleftright) + (dst_positive_scale_inverse_restrict_sourceleftright)) + ((dst_positive_scale_inverse_restrict_sourceleftright) + (dst_positive_scale_inverse_restrict_sourceleftright))) + (((dst_negative_code_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)) * S ((dst_negative_code_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)) + ((dst_negative_scale_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)))) * S ((((dst_positive_code_inverse_restrict_sourceleftright) + (dst_positive_scale_inverse_restrict_sourceleftright)) * S ((dst_positive_code_inverse_restrict_sourceleftright) + (dst_positive_scale_inverse_restrict_sourceleftright)) + ((dst_positive_scale_inverse_restrict_sourceleftright) + (dst_positive_scale_inverse_restrict_sourceleftright))) + (((dst_negative_code_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)) * S ((dst_negative_code_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)) + ((dst_negative_scale_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)))) + ((((dst_negative_code_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)) * S ((dst_negative_code_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)) + ((dst_negative_scale_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright))) + (((dst_negative_code_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)) * S ((dst_negative_code_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)) + ((dst_negative_scale_inverse_restrict_sourceleftright) + (dst_negative_scale_inverse_restrict_sourceleftright)))))) /\ (forall dst_index_inverse_restrict_sourceleftright. (exists pvs_le_gap_inverse_restrict_sourceleftrightdomain. pvs_le_gap_inverse_restrict_sourceleftrightdomain + (dst_index_inverse_restrict_sourceleftright) = (N)) -> exists dst_positive_inverse_restrict_sourceleftright dst_negative_inverse_restrict_sourceleftright dst_value_inverse_restrict_sourceleftright. ((((exists ff_h_pvs_inverse_restrict_sourceleftrightentrypositive. ff_h_pvs_inverse_restrict_sourceleftrightentrypositive + S (dst_positive_inverse_restrict_sourceleftright) = S ((S (dst_index_inverse_restrict_sourceleftright)) * dst_positive_scale_inverse_restrict_sourceleftright)) /\ exists ff_q_pvs_inverse_restrict_sourceleftrightentrypositive. dst_positive_code_inverse_restrict_sourceleftright = ff_q_pvs_inverse_restrict_sourceleftrightentrypositive * S ((S (dst_index_inverse_restrict_sourceleftright)) * dst_positive_scale_inverse_restrict_sourceleftright) + (dst_positive_inverse_restrict_sourceleftright))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftrightentrynegative. ff_h_pvs_inverse_restrict_sourceleftrightentrynegative + S (dst_negative_inverse_restrict_sourceleftright) = S ((S (dst_index_inverse_restrict_sourceleftright)) * dst_negative_scale_inverse_restrict_sourceleftright)) /\ exists ff_q_pvs_inverse_restrict_sourceleftrightentrynegative. dst_negative_code_inverse_restrict_sourceleftright = ff_q_pvs_inverse_restrict_sourceleftrightentrynegative * S ((S (dst_index_inverse_restrict_sourceleftright)) * dst_negative_scale_inverse_restrict_sourceleftright) + (dst_negative_inverse_restrict_sourceleftright))) /\ (exists ge_balance_positive_inverse_restrict_sourceleftrightentryvalue ge_balance_negative_inverse_restrict_sourceleftrightentryvalue. (((((dst_value_inverse_restrict_sourceleftright) = 2 * (ge_balance_positive_inverse_restrict_sourceleftrightentryvalue) /\ (ge_balance_negative_inverse_restrict_sourceleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftrightentryvaluedecode. (((dst_value_inverse_restrict_sourceleftright) = 2 * ge_signed_half_inverse_restrict_sourceleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourceleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourceleftrightentryvalue) = S ge_signed_half_inverse_restrict_sourceleftrightentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourceleftright) + ge_balance_negative_inverse_restrict_sourceleftrightentryvalue = (dst_negative_inverse_restrict_sourceleftright) + ge_balance_positive_inverse_restrict_sourceleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_sourcelefttable dst_positive_scale_inverse_restrict_sourcelefttable dst_negative_code_inverse_restrict_sourcelefttable dst_negative_scale_inverse_restrict_sourcelefttable. (((di_delta_inverse_restrict_source) = (((((dst_positive_code_inverse_restrict_sourcelefttable) + (dst_positive_scale_inverse_restrict_sourcelefttable)) * S ((dst_positive_code_inverse_restrict_sourcelefttable) + (dst_positive_scale_inverse_restrict_sourcelefttable)) + ((dst_positive_scale_inverse_restrict_sourcelefttable) + (dst_positive_scale_inverse_restrict_sourcelefttable))) + (((dst_negative_code_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)) * S ((dst_negative_code_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)) + ((dst_negative_scale_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)))) * S ((((dst_positive_code_inverse_restrict_sourcelefttable) + (dst_positive_scale_inverse_restrict_sourcelefttable)) * S ((dst_positive_code_inverse_restrict_sourcelefttable) + (dst_positive_scale_inverse_restrict_sourcelefttable)) + ((dst_positive_scale_inverse_restrict_sourcelefttable) + (dst_positive_scale_inverse_restrict_sourcelefttable))) + (((dst_negative_code_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)) * S ((dst_negative_code_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)) + ((dst_negative_scale_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)))) + ((((dst_negative_code_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)) * S ((dst_negative_code_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)) + ((dst_negative_scale_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable))) + (((dst_negative_code_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)) * S ((dst_negative_code_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)) + ((dst_negative_scale_inverse_restrict_sourcelefttable) + (dst_negative_scale_inverse_restrict_sourcelefttable)))))) /\ (forall dst_index_inverse_restrict_sourcelefttable. (exists pvs_le_gap_inverse_restrict_sourcelefttabledomain. pvs_le_gap_inverse_restrict_sourcelefttabledomain + (dst_index_inverse_restrict_sourcelefttable) = (N)) -> exists dst_positive_inverse_restrict_sourcelefttable dst_negative_inverse_restrict_sourcelefttable dst_value_inverse_restrict_sourcelefttable. ((((exists ff_h_pvs_inverse_restrict_sourcelefttableentrypositive. ff_h_pvs_inverse_restrict_sourcelefttableentrypositive + S (dst_positive_inverse_restrict_sourcelefttable) = S ((S (dst_index_inverse_restrict_sourcelefttable)) * dst_positive_scale_inverse_restrict_sourcelefttable)) /\ exists ff_q_pvs_inverse_restrict_sourcelefttableentrypositive. dst_positive_code_inverse_restrict_sourcelefttable = ff_q_pvs_inverse_restrict_sourcelefttableentrypositive * S ((S (dst_index_inverse_restrict_sourcelefttable)) * dst_positive_scale_inverse_restrict_sourcelefttable) + (dst_positive_inverse_restrict_sourcelefttable))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcelefttableentrynegative. ff_h_pvs_inverse_restrict_sourcelefttableentrynegative + S (dst_negative_inverse_restrict_sourcelefttable) = S ((S (dst_index_inverse_restrict_sourcelefttable)) * dst_negative_scale_inverse_restrict_sourcelefttable)) /\ exists ff_q_pvs_inverse_restrict_sourcelefttableentrynegative. dst_negative_code_inverse_restrict_sourcelefttable = ff_q_pvs_inverse_restrict_sourcelefttableentrynegative * S ((S (dst_index_inverse_restrict_sourcelefttable)) * dst_negative_scale_inverse_restrict_sourcelefttable) + (dst_negative_inverse_restrict_sourcelefttable))) /\ (exists ge_balance_positive_inverse_restrict_sourcelefttableentryvalue ge_balance_negative_inverse_restrict_sourcelefttableentryvalue. (((((dst_value_inverse_restrict_sourcelefttable) = 2 * (ge_balance_positive_inverse_restrict_sourcelefttableentryvalue) /\ (ge_balance_negative_inverse_restrict_sourcelefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcelefttableentryvaluedecode. (((dst_value_inverse_restrict_sourcelefttable) = 2 * ge_signed_half_inverse_restrict_sourcelefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcelefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcelefttableentryvalue) = S ge_signed_half_inverse_restrict_sourcelefttableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcelefttable) + ge_balance_negative_inverse_restrict_sourcelefttableentryvalue = (dst_negative_inverse_restrict_sourcelefttable) + ge_balance_positive_inverse_restrict_sourcelefttableentryvalue))))))))) /\ (forall dc_input_inverse_restrict_sourceleft dc_output_inverse_restrict_sourceleft. ~(dc_input_inverse_restrict_sourceleft=0) -> (exists pvs_le_gap_inverse_restrict_sourceleftdomain. pvs_le_gap_inverse_restrict_sourceleftdomain + (dc_input_inverse_restrict_sourceleft) = (N)) -> (exists dst_positive_code_inverse_restrict_sourceleftlookup dst_positive_scale_inverse_restrict_sourceleftlookup dst_negative_code_inverse_restrict_sourceleftlookup dst_negative_scale_inverse_restrict_sourceleftlookup dst_positive_inverse_restrict_sourceleftlookup dst_negative_inverse_restrict_sourceleftlookup. (((di_delta_inverse_restrict_source) = (((((dst_positive_code_inverse_restrict_sourceleftlookup) + (dst_positive_scale_inverse_restrict_sourceleftlookup)) * S ((dst_positive_code_inverse_restrict_sourceleftlookup) + (dst_positive_scale_inverse_restrict_sourceleftlookup)) + ((dst_positive_scale_inverse_restrict_sourceleftlookup) + (dst_positive_scale_inverse_restrict_sourceleftlookup))) + (((dst_negative_code_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)) * S ((dst_negative_code_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)) + ((dst_negative_scale_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)))) * S ((((dst_positive_code_inverse_restrict_sourceleftlookup) + (dst_positive_scale_inverse_restrict_sourceleftlookup)) * S ((dst_positive_code_inverse_restrict_sourceleftlookup) + (dst_positive_scale_inverse_restrict_sourceleftlookup)) + ((dst_positive_scale_inverse_restrict_sourceleftlookup) + (dst_positive_scale_inverse_restrict_sourceleftlookup))) + (((dst_negative_code_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)) * S ((dst_negative_code_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)) + ((dst_negative_scale_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)))) + ((((dst_negative_code_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)) * S ((dst_negative_code_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)) + ((dst_negative_scale_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup))) + (((dst_negative_code_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)) * S ((dst_negative_code_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)) + ((dst_negative_scale_inverse_restrict_sourceleftlookup) + (dst_negative_scale_inverse_restrict_sourceleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftlookuppositive. ff_h_pvs_inverse_restrict_sourceleftlookuppositive + S (dst_positive_inverse_restrict_sourceleftlookup) = S ((S (dc_input_inverse_restrict_sourceleft)) * dst_positive_scale_inverse_restrict_sourceleftlookup)) /\ exists ff_q_pvs_inverse_restrict_sourceleftlookuppositive. dst_positive_code_inverse_restrict_sourceleftlookup = ff_q_pvs_inverse_restrict_sourceleftlookuppositive * S ((S (dc_input_inverse_restrict_sourceleft)) * dst_positive_scale_inverse_restrict_sourceleftlookup) + (dst_positive_inverse_restrict_sourceleftlookup))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftlookupnegative. ff_h_pvs_inverse_restrict_sourceleftlookupnegative + S (dst_negative_inverse_restrict_sourceleftlookup) = S ((S (dc_input_inverse_restrict_sourceleft)) * dst_negative_scale_inverse_restrict_sourceleftlookup)) /\ exists ff_q_pvs_inverse_restrict_sourceleftlookupnegative. dst_negative_code_inverse_restrict_sourceleftlookup = ff_q_pvs_inverse_restrict_sourceleftlookupnegative * S ((S (dc_input_inverse_restrict_sourceleft)) * dst_negative_scale_inverse_restrict_sourceleftlookup) + (dst_negative_inverse_restrict_sourceleftlookup))) /\ (exists ge_balance_positive_inverse_restrict_sourceleftlookupvalue ge_balance_negative_inverse_restrict_sourceleftlookupvalue. (((((dc_output_inverse_restrict_sourceleft) = 2 * (ge_balance_positive_inverse_restrict_sourceleftlookupvalue) /\ (ge_balance_negative_inverse_restrict_sourceleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftlookupvaluedecode. (((dc_output_inverse_restrict_sourceleft) = 2 * ge_signed_half_inverse_restrict_sourceleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourceleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourceleftlookupvalue) = S ge_signed_half_inverse_restrict_sourceleftlookupvaluedecode))) /\ ((dst_positive_inverse_restrict_sourceleftlookup) + ge_balance_negative_inverse_restrict_sourceleftlookupvalue = (dst_negative_inverse_restrict_sourceleftlookup) + ge_balance_positive_inverse_restrict_sourceleftlookupvalue))))))))) -> (((~((dc_input_inverse_restrict_sourceleft)=0)) /\ (exists dc_mask_inverse_restrict_sourceleftvalue. ((((exists dst_positive_code_inverse_restrict_sourceleftvaluemasktable dst_positive_scale_inverse_restrict_sourceleftvaluemasktable dst_negative_code_inverse_restrict_sourceleftvaluemasktable dst_negative_scale_inverse_restrict_sourceleftvaluemasktable. (((dc_mask_inverse_restrict_sourceleftvalue) = (((((dst_positive_code_inverse_restrict_sourceleftvaluemasktable) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluemasktable) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluemasktable) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)))) * S ((((dst_positive_code_inverse_restrict_sourceleftvaluemasktable) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluemasktable) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluemasktable) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)))) + ((((dst_negative_code_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)))))) /\ (forall dst_index_inverse_restrict_sourceleftvaluemasktable. (exists pvs_le_gap_inverse_restrict_sourceleftvaluemasktabledomain. pvs_le_gap_inverse_restrict_sourceleftvaluemasktabledomain + (dst_index_inverse_restrict_sourceleftvaluemasktable) = (dc_input_inverse_restrict_sourceleft)) -> exists dst_positive_inverse_restrict_sourceleftvaluemasktable dst_negative_inverse_restrict_sourceleftvaluemasktable dst_value_inverse_restrict_sourceleftvaluemasktable. ((((exists ff_h_pvs_inverse_restrict_sourceleftvaluemasktableentrypositive. ff_h_pvs_inverse_restrict_sourceleftvaluemasktableentrypositive + S (dst_positive_inverse_restrict_sourceleftvaluemasktable) = S ((S (dst_index_inverse_restrict_sourceleftvaluemasktable)) * dst_positive_scale_inverse_restrict_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_restrict_sourceleftvaluemasktableentrypositive. dst_positive_code_inverse_restrict_sourceleftvaluemasktable = ff_q_pvs_inverse_restrict_sourceleftvaluemasktableentrypositive * S ((S (dst_index_inverse_restrict_sourceleftvaluemasktable)) * dst_positive_scale_inverse_restrict_sourceleftvaluemasktable) + (dst_positive_inverse_restrict_sourceleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftvaluemasktableentrynegative. ff_h_pvs_inverse_restrict_sourceleftvaluemasktableentrynegative + S (dst_negative_inverse_restrict_sourceleftvaluemasktable) = S ((S (dst_index_inverse_restrict_sourceleftvaluemasktable)) * dst_negative_scale_inverse_restrict_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_restrict_sourceleftvaluemasktableentrynegative. dst_negative_code_inverse_restrict_sourceleftvaluemasktable = ff_q_pvs_inverse_restrict_sourceleftvaluemasktableentrynegative * S ((S (dst_index_inverse_restrict_sourceleftvaluemasktable)) * dst_negative_scale_inverse_restrict_sourceleftvaluemasktable) + (dst_negative_inverse_restrict_sourceleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_restrict_sourceleftvaluemasktableentryvalue ge_balance_negative_inverse_restrict_sourceleftvaluemasktableentryvalue. (((((dst_value_inverse_restrict_sourceleftvaluemasktable) = 2 * (ge_balance_positive_inverse_restrict_sourceleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftvaluemasktableentryvaluedecode. (((dst_value_inverse_restrict_sourceleftvaluemasktable) = 2 * ge_signed_half_inverse_restrict_sourceleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourceleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluemasktableentryvalue) = S ge_signed_half_inverse_restrict_sourceleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourceleftvaluemasktable) + ge_balance_negative_inverse_restrict_sourceleftvaluemasktableentryvalue = (dst_negative_inverse_restrict_sourceleftvaluemasktable) + ge_balance_positive_inverse_restrict_sourceleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_restrict_sourceleftvaluemask dc_value_inverse_restrict_sourceleftvaluemask. (exists pvs_le_gap_inverse_restrict_sourceleftvaluemaskdomain. pvs_le_gap_inverse_restrict_sourceleftvaluemaskdomain + (dc_index_inverse_restrict_sourceleftvaluemask) = (dc_input_inverse_restrict_sourceleft)) -> (exists dst_positive_code_inverse_restrict_sourceleftvaluemasklookup dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup dst_negative_code_inverse_restrict_sourceleftvaluemasklookup dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup dst_positive_inverse_restrict_sourceleftvaluemasklookup dst_negative_inverse_restrict_sourceleftvaluemasklookup. (((dc_mask_inverse_restrict_sourceleftvalue) = (((((dst_positive_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)))) + ((((dst_negative_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftvaluemasklookuppositive. ff_h_pvs_inverse_restrict_sourceleftvaluemasklookuppositive + S (dst_positive_inverse_restrict_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_restrict_sourceleftvaluemask)) * dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_restrict_sourceleftvaluemasklookuppositive. dst_positive_code_inverse_restrict_sourceleftvaluemasklookup = ff_q_pvs_inverse_restrict_sourceleftvaluemasklookuppositive * S ((S (dc_index_inverse_restrict_sourceleftvaluemask)) * dst_positive_scale_inverse_restrict_sourceleftvaluemasklookup) + (dst_positive_inverse_restrict_sourceleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftvaluemasklookupnegative. ff_h_pvs_inverse_restrict_sourceleftvaluemasklookupnegative + S (dst_negative_inverse_restrict_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_restrict_sourceleftvaluemask)) * dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_restrict_sourceleftvaluemasklookupnegative. dst_negative_code_inverse_restrict_sourceleftvaluemasklookup = ff_q_pvs_inverse_restrict_sourceleftvaluemasklookupnegative * S ((S (dc_index_inverse_restrict_sourceleftvaluemask)) * dst_negative_scale_inverse_restrict_sourceleftvaluemasklookup) + (dst_negative_inverse_restrict_sourceleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_restrict_sourceleftvaluemasklookupvalue ge_balance_negative_inverse_restrict_sourceleftvaluemasklookupvalue. (((((dc_value_inverse_restrict_sourceleftvaluemask) = 2 * (ge_balance_positive_inverse_restrict_sourceleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftvaluemasklookupvaluedecode. (((dc_value_inverse_restrict_sourceleftvaluemask) = 2 * ge_signed_half_inverse_restrict_sourceleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourceleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluemasklookupvalue) = S ge_signed_half_inverse_restrict_sourceleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_restrict_sourceleftvaluemasklookup) + ge_balance_negative_inverse_restrict_sourceleftvaluemasklookupvalue = (dst_negative_inverse_restrict_sourceleftvaluemasklookup) + ge_balance_positive_inverse_restrict_sourceleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_restrict_sourceleftvaluemask)=0)) /\ (exists dc_quotient_inverse_restrict_sourceleftvaluemaskentry dc_left_inverse_restrict_sourceleftvaluemaskentry dc_right_inverse_restrict_sourceleftvaluemaskentry. (((dc_input_inverse_restrict_sourceleft)=(dc_index_inverse_restrict_sourceleftvaluemask)*dc_quotient_inverse_restrict_sourceleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_restrict_sourceleftvaluemaskentryleft dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft dst_positive_inverse_restrict_sourceleftvaluemaskentryleft dst_negative_inverse_restrict_sourceleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftvaluemaskentryleftpositive. ff_h_pvs_inverse_restrict_sourceleftvaluemaskentryleftpositive + S (dst_positive_inverse_restrict_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_restrict_sourceleftvaluemask)) * dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_restrict_sourceleftvaluemaskentryleftpositive. dst_positive_code_inverse_restrict_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_restrict_sourceleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_restrict_sourceleftvaluemask)) * dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_positive_inverse_restrict_sourceleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftvaluemaskentryleftnegative. ff_h_pvs_inverse_restrict_sourceleftvaluemaskentryleftnegative + S (dst_negative_inverse_restrict_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_restrict_sourceleftvaluemask)) * dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_restrict_sourceleftvaluemaskentryleftnegative. dst_negative_code_inverse_restrict_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_restrict_sourceleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_restrict_sourceleftvaluemask)) * dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryleft) + (dst_negative_inverse_restrict_sourceleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_restrict_sourceleftvaluemaskentryleftvalue ge_balance_negative_inverse_restrict_sourceleftvaluemaskentryleftvalue. (((((dc_left_inverse_restrict_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_restrict_sourceleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_restrict_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_sourceleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourceleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_restrict_sourceleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_restrict_sourceleftvaluemaskentryleft) + ge_balance_negative_inverse_restrict_sourceleftvaluemaskentryleftvalue = (dst_negative_inverse_restrict_sourceleftvaluemaskentryleft) + ge_balance_positive_inverse_restrict_sourceleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_sourceleftvaluemaskentryright dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright dst_positive_inverse_restrict_sourceleftvaluemaskentryright dst_negative_inverse_restrict_sourceleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftvaluemaskentryrightpositive. ff_h_pvs_inverse_restrict_sourceleftvaluemaskentryrightpositive + S (dst_positive_inverse_restrict_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_restrict_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_restrict_sourceleftvaluemaskentryrightpositive. dst_positive_code_inverse_restrict_sourceleftvaluemaskentryright = ff_q_pvs_inverse_restrict_sourceleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_restrict_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_restrict_sourceleftvaluemaskentryright) + (dst_positive_inverse_restrict_sourceleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_restrict_sourceleftvaluemaskentryrightnegative. ff_h_pvs_inverse_restrict_sourceleftvaluemaskentryrightnegative + S (dst_negative_inverse_restrict_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_restrict_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_restrict_sourceleftvaluemaskentryrightnegative. dst_negative_code_inverse_restrict_sourceleftvaluemaskentryright = ff_q_pvs_inverse_restrict_sourceleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_restrict_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_restrict_sourceleftvaluemaskentryright) + (dst_negative_inverse_restrict_sourceleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_restrict_sourceleftvaluemaskentryrightvalue ge_balance_negative_inverse_restrict_sourceleftvaluemaskentryrightvalue. (((((dc_right_inverse_restrict_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_restrict_sourceleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_restrict_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_sourceleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourceleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_restrict_sourceleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_restrict_sourceleftvaluemaskentryright) + ge_balance_negative_inverse_restrict_sourceleftvaluemaskentryrightvalue = (dst_negative_inverse_restrict_sourceleftvaluemaskentryright) + ge_balance_positive_inverse_restrict_sourceleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_restrict_sourceleftvaluemaskentryproduct sto_an_inverse_restrict_sourceleftvaluemaskentryproduct sto_bp_inverse_restrict_sourceleftvaluemaskentryproduct sto_bn_inverse_restrict_sourceleftvaluemaskentryproduct sto_cp_inverse_restrict_sourceleftvaluemaskentryproduct sto_cn_inverse_restrict_sourceleftvaluemaskentryproduct. (((((dc_left_inverse_restrict_sourceleftvaluemaskentry) = 2 * (sto_ap_inverse_restrict_sourceleftvaluemaskentryproduct) /\ (sto_an_inverse_restrict_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductleft. (((dc_left_inverse_restrict_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_restrict_sourceleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_restrict_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_restrict_sourceleftvaluemaskentry) = 2 * (sto_bp_inverse_restrict_sourceleftvaluemaskentryproduct) /\ (sto_bn_inverse_restrict_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductright. (((dc_right_inverse_restrict_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_restrict_sourceleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_restrict_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_restrict_sourceleftvaluemask) = 2 * (sto_cp_inverse_restrict_sourceleftvaluemaskentryproduct) /\ (sto_cn_inverse_restrict_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductoutput. (((dc_value_inverse_restrict_sourceleftvaluemask) = 2 * ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_restrict_sourceleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_restrict_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_sourceleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_restrict_sourceleftvaluemaskentryproduct * sto_bp_inverse_restrict_sourceleftvaluemaskentryproduct + sto_an_inverse_restrict_sourceleftvaluemaskentryproduct * sto_bn_inverse_restrict_sourceleftvaluemaskentryproduct) + sto_cn_inverse_restrict_sourceleftvaluemaskentryproduct = (sto_ap_inverse_restrict_sourceleftvaluemaskentryproduct * sto_bn_inverse_restrict_sourceleftvaluemaskentryproduct + sto_an_inverse_restrict_sourceleftvaluemaskentryproduct * sto_bp_inverse_restrict_sourceleftvaluemaskentryproduct) + sto_cp_inverse_restrict_sourceleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_restrict_sourceleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_restrict_sourceleftvaluemaskentrynondivisor. (dc_input_inverse_restrict_sourceleft) = (dc_index_inverse_restrict_sourceleftvaluemask) * pvs_factor_inverse_restrict_sourceleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_restrict_sourceleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_restrict_sourceleftvaluefold dst_positive_scale_inverse_restrict_sourceleftvaluefold dst_negative_code_inverse_restrict_sourceleftvaluefold dst_negative_scale_inverse_restrict_sourceleftvaluefold dst_positive_sum_inverse_restrict_sourceleftvaluefold dst_negative_sum_inverse_restrict_sourceleftvaluefold. (((dc_mask_inverse_restrict_sourceleftvalue) = (((((dst_positive_code_inverse_restrict_sourceleftvaluefold) + (dst_positive_scale_inverse_restrict_sourceleftvaluefold)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluefold) + (dst_positive_scale_inverse_restrict_sourceleftvaluefold)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluefold) + (dst_positive_scale_inverse_restrict_sourceleftvaluefold))) + (((dst_negative_code_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)))) * S ((((dst_positive_code_inverse_restrict_sourceleftvaluefold) + (dst_positive_scale_inverse_restrict_sourceleftvaluefold)) * S ((dst_positive_code_inverse_restrict_sourceleftvaluefold) + (dst_positive_scale_inverse_restrict_sourceleftvaluefold)) + ((dst_positive_scale_inverse_restrict_sourceleftvaluefold) + (dst_positive_scale_inverse_restrict_sourceleftvaluefold))) + (((dst_negative_code_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)))) + ((((dst_negative_code_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold))) + (((dst_negative_code_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)) * S ((dst_negative_code_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)) + ((dst_negative_scale_inverse_restrict_sourceleftvaluefold) + (dst_negative_scale_inverse_restrict_sourceleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_restrict_sourceleftvaluefoldpositive fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive. ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_start. fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_start. fs_u_dst_inverse_restrict_sourceleftvaluefoldpositive = fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_restrict_sourceleftvaluefold) = S ((S (S (dc_input_inverse_restrict_sourceleft))) * fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_restrict_sourceleftvaluefoldpositive = fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_restrict_sourceleft))) * fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive) + (dst_positive_sum_inverse_restrict_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps = S (dc_input_inverse_restrict_sourceleft)) -> exists fs_a_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps fs_r_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps fs_s_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_restrict_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_restrict_sourceleftvaluefold = fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_restrict_sourceleftvaluefold) + (fs_a_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_restrict_sourceleftvaluefoldpositive = fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive) + (fs_r_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_restrict_sourceleftvaluefoldpositive = fs_q_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldpositive) + (fs_s_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps = fs_r_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps + fs_a_dst_inverse_restrict_sourceleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_restrict_sourceleftvaluefoldnegative fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative. ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_start. fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_start. fs_u_dst_inverse_restrict_sourceleftvaluefoldnegative = fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_restrict_sourceleftvaluefold) = S ((S (S (dc_input_inverse_restrict_sourceleft))) * fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_restrict_sourceleftvaluefoldnegative = fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_restrict_sourceleft))) * fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative) + (dst_negative_sum_inverse_restrict_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps = S (dc_input_inverse_restrict_sourceleft)) -> exists fs_a_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps fs_r_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps fs_s_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_restrict_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_restrict_sourceleftvaluefold = fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_restrict_sourceleftvaluefold) + (fs_a_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_restrict_sourceleftvaluefoldnegative = fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative) + (fs_r_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_restrict_sourceleftvaluefoldnegative = fs_q_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_sourceleftvaluefoldnegative) + (fs_s_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps = fs_r_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps + fs_a_dst_inverse_restrict_sourceleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_restrict_sourceleftvaluefoldresult ge_balance_negative_inverse_restrict_sourceleftvaluefoldresult. (((((dc_output_inverse_restrict_sourceleft) = 2 * (ge_balance_positive_inverse_restrict_sourceleftvaluefoldresult) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_restrict_sourceleftvaluefoldresultdecode. (((dc_output_inverse_restrict_sourceleft) = 2 * ge_signed_half_inverse_restrict_sourceleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_restrict_sourceleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_restrict_sourceleftvaluefoldresult) = S ge_signed_half_inverse_restrict_sourceleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_restrict_sourceleftvaluefold) + ge_balance_negative_inverse_restrict_sourceleftvaluefoldresult = (dst_negative_sum_inverse_restrict_sourceleftvaluefold) + ge_balance_positive_inverse_restrict_sourceleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_restrict_sourcerightleft dst_positive_scale_inverse_restrict_sourcerightleft dst_negative_code_inverse_restrict_sourcerightleft dst_negative_scale_inverse_restrict_sourcerightleft. (((G) = (((((dst_positive_code_inverse_restrict_sourcerightleft) + (dst_positive_scale_inverse_restrict_sourcerightleft)) * S ((dst_positive_code_inverse_restrict_sourcerightleft) + (dst_positive_scale_inverse_restrict_sourcerightleft)) + ((dst_positive_scale_inverse_restrict_sourcerightleft) + (dst_positive_scale_inverse_restrict_sourcerightleft))) + (((dst_negative_code_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)) * S ((dst_negative_code_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)) + ((dst_negative_scale_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)))) * S ((((dst_positive_code_inverse_restrict_sourcerightleft) + (dst_positive_scale_inverse_restrict_sourcerightleft)) * S ((dst_positive_code_inverse_restrict_sourcerightleft) + (dst_positive_scale_inverse_restrict_sourcerightleft)) + ((dst_positive_scale_inverse_restrict_sourcerightleft) + (dst_positive_scale_inverse_restrict_sourcerightleft))) + (((dst_negative_code_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)) * S ((dst_negative_code_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)) + ((dst_negative_scale_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)))) + ((((dst_negative_code_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)) * S ((dst_negative_code_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)) + ((dst_negative_scale_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft))) + (((dst_negative_code_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)) * S ((dst_negative_code_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)) + ((dst_negative_scale_inverse_restrict_sourcerightleft) + (dst_negative_scale_inverse_restrict_sourcerightleft)))))) /\ (forall dst_index_inverse_restrict_sourcerightleft. (exists pvs_le_gap_inverse_restrict_sourcerightleftdomain. pvs_le_gap_inverse_restrict_sourcerightleftdomain + (dst_index_inverse_restrict_sourcerightleft) = (N)) -> exists dst_positive_inverse_restrict_sourcerightleft dst_negative_inverse_restrict_sourcerightleft dst_value_inverse_restrict_sourcerightleft. ((((exists ff_h_pvs_inverse_restrict_sourcerightleftentrypositive. ff_h_pvs_inverse_restrict_sourcerightleftentrypositive + S (dst_positive_inverse_restrict_sourcerightleft) = S ((S (dst_index_inverse_restrict_sourcerightleft)) * dst_positive_scale_inverse_restrict_sourcerightleft)) /\ exists ff_q_pvs_inverse_restrict_sourcerightleftentrypositive. dst_positive_code_inverse_restrict_sourcerightleft = ff_q_pvs_inverse_restrict_sourcerightleftentrypositive * S ((S (dst_index_inverse_restrict_sourcerightleft)) * dst_positive_scale_inverse_restrict_sourcerightleft) + (dst_positive_inverse_restrict_sourcerightleft))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightleftentrynegative. ff_h_pvs_inverse_restrict_sourcerightleftentrynegative + S (dst_negative_inverse_restrict_sourcerightleft) = S ((S (dst_index_inverse_restrict_sourcerightleft)) * dst_negative_scale_inverse_restrict_sourcerightleft)) /\ exists ff_q_pvs_inverse_restrict_sourcerightleftentrynegative. dst_negative_code_inverse_restrict_sourcerightleft = ff_q_pvs_inverse_restrict_sourcerightleftentrynegative * S ((S (dst_index_inverse_restrict_sourcerightleft)) * dst_negative_scale_inverse_restrict_sourcerightleft) + (dst_negative_inverse_restrict_sourcerightleft))) /\ (exists ge_balance_positive_inverse_restrict_sourcerightleftentryvalue ge_balance_negative_inverse_restrict_sourcerightleftentryvalue. (((((dst_value_inverse_restrict_sourcerightleft) = 2 * (ge_balance_positive_inverse_restrict_sourcerightleftentryvalue) /\ (ge_balance_negative_inverse_restrict_sourcerightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightleftentryvaluedecode. (((dst_value_inverse_restrict_sourcerightleft) = 2 * ge_signed_half_inverse_restrict_sourcerightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerightleftentryvalue) = S ge_signed_half_inverse_restrict_sourcerightleftentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcerightleft) + ge_balance_negative_inverse_restrict_sourcerightleftentryvalue = (dst_negative_inverse_restrict_sourcerightleft) + ge_balance_positive_inverse_restrict_sourcerightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_sourcerightright dst_positive_scale_inverse_restrict_sourcerightright dst_negative_code_inverse_restrict_sourcerightright dst_negative_scale_inverse_restrict_sourcerightright. (((F) = (((((dst_positive_code_inverse_restrict_sourcerightright) + (dst_positive_scale_inverse_restrict_sourcerightright)) * S ((dst_positive_code_inverse_restrict_sourcerightright) + (dst_positive_scale_inverse_restrict_sourcerightright)) + ((dst_positive_scale_inverse_restrict_sourcerightright) + (dst_positive_scale_inverse_restrict_sourcerightright))) + (((dst_negative_code_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)) * S ((dst_negative_code_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)) + ((dst_negative_scale_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)))) * S ((((dst_positive_code_inverse_restrict_sourcerightright) + (dst_positive_scale_inverse_restrict_sourcerightright)) * S ((dst_positive_code_inverse_restrict_sourcerightright) + (dst_positive_scale_inverse_restrict_sourcerightright)) + ((dst_positive_scale_inverse_restrict_sourcerightright) + (dst_positive_scale_inverse_restrict_sourcerightright))) + (((dst_negative_code_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)) * S ((dst_negative_code_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)) + ((dst_negative_scale_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)))) + ((((dst_negative_code_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)) * S ((dst_negative_code_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)) + ((dst_negative_scale_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright))) + (((dst_negative_code_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)) * S ((dst_negative_code_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)) + ((dst_negative_scale_inverse_restrict_sourcerightright) + (dst_negative_scale_inverse_restrict_sourcerightright)))))) /\ (forall dst_index_inverse_restrict_sourcerightright. (exists pvs_le_gap_inverse_restrict_sourcerightrightdomain. pvs_le_gap_inverse_restrict_sourcerightrightdomain + (dst_index_inverse_restrict_sourcerightright) = (N)) -> exists dst_positive_inverse_restrict_sourcerightright dst_negative_inverse_restrict_sourcerightright dst_value_inverse_restrict_sourcerightright. ((((exists ff_h_pvs_inverse_restrict_sourcerightrightentrypositive. ff_h_pvs_inverse_restrict_sourcerightrightentrypositive + S (dst_positive_inverse_restrict_sourcerightright) = S ((S (dst_index_inverse_restrict_sourcerightright)) * dst_positive_scale_inverse_restrict_sourcerightright)) /\ exists ff_q_pvs_inverse_restrict_sourcerightrightentrypositive. dst_positive_code_inverse_restrict_sourcerightright = ff_q_pvs_inverse_restrict_sourcerightrightentrypositive * S ((S (dst_index_inverse_restrict_sourcerightright)) * dst_positive_scale_inverse_restrict_sourcerightright) + (dst_positive_inverse_restrict_sourcerightright))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightrightentrynegative. ff_h_pvs_inverse_restrict_sourcerightrightentrynegative + S (dst_negative_inverse_restrict_sourcerightright) = S ((S (dst_index_inverse_restrict_sourcerightright)) * dst_negative_scale_inverse_restrict_sourcerightright)) /\ exists ff_q_pvs_inverse_restrict_sourcerightrightentrynegative. dst_negative_code_inverse_restrict_sourcerightright = ff_q_pvs_inverse_restrict_sourcerightrightentrynegative * S ((S (dst_index_inverse_restrict_sourcerightright)) * dst_negative_scale_inverse_restrict_sourcerightright) + (dst_negative_inverse_restrict_sourcerightright))) /\ (exists ge_balance_positive_inverse_restrict_sourcerightrightentryvalue ge_balance_negative_inverse_restrict_sourcerightrightentryvalue. (((((dst_value_inverse_restrict_sourcerightright) = 2 * (ge_balance_positive_inverse_restrict_sourcerightrightentryvalue) /\ (ge_balance_negative_inverse_restrict_sourcerightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightrightentryvaluedecode. (((dst_value_inverse_restrict_sourcerightright) = 2 * ge_signed_half_inverse_restrict_sourcerightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerightrightentryvalue) = S ge_signed_half_inverse_restrict_sourcerightrightentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcerightright) + ge_balance_negative_inverse_restrict_sourcerightrightentryvalue = (dst_negative_inverse_restrict_sourcerightright) + ge_balance_positive_inverse_restrict_sourcerightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_sourcerighttable dst_positive_scale_inverse_restrict_sourcerighttable dst_negative_code_inverse_restrict_sourcerighttable dst_negative_scale_inverse_restrict_sourcerighttable. (((di_delta_inverse_restrict_source) = (((((dst_positive_code_inverse_restrict_sourcerighttable) + (dst_positive_scale_inverse_restrict_sourcerighttable)) * S ((dst_positive_code_inverse_restrict_sourcerighttable) + (dst_positive_scale_inverse_restrict_sourcerighttable)) + ((dst_positive_scale_inverse_restrict_sourcerighttable) + (dst_positive_scale_inverse_restrict_sourcerighttable))) + (((dst_negative_code_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)) * S ((dst_negative_code_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)) + ((dst_negative_scale_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)))) * S ((((dst_positive_code_inverse_restrict_sourcerighttable) + (dst_positive_scale_inverse_restrict_sourcerighttable)) * S ((dst_positive_code_inverse_restrict_sourcerighttable) + (dst_positive_scale_inverse_restrict_sourcerighttable)) + ((dst_positive_scale_inverse_restrict_sourcerighttable) + (dst_positive_scale_inverse_restrict_sourcerighttable))) + (((dst_negative_code_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)) * S ((dst_negative_code_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)) + ((dst_negative_scale_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)))) + ((((dst_negative_code_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)) * S ((dst_negative_code_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)) + ((dst_negative_scale_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable))) + (((dst_negative_code_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)) * S ((dst_negative_code_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)) + ((dst_negative_scale_inverse_restrict_sourcerighttable) + (dst_negative_scale_inverse_restrict_sourcerighttable)))))) /\ (forall dst_index_inverse_restrict_sourcerighttable. (exists pvs_le_gap_inverse_restrict_sourcerighttabledomain. pvs_le_gap_inverse_restrict_sourcerighttabledomain + (dst_index_inverse_restrict_sourcerighttable) = (N)) -> exists dst_positive_inverse_restrict_sourcerighttable dst_negative_inverse_restrict_sourcerighttable dst_value_inverse_restrict_sourcerighttable. ((((exists ff_h_pvs_inverse_restrict_sourcerighttableentrypositive. ff_h_pvs_inverse_restrict_sourcerighttableentrypositive + S (dst_positive_inverse_restrict_sourcerighttable) = S ((S (dst_index_inverse_restrict_sourcerighttable)) * dst_positive_scale_inverse_restrict_sourcerighttable)) /\ exists ff_q_pvs_inverse_restrict_sourcerighttableentrypositive. dst_positive_code_inverse_restrict_sourcerighttable = ff_q_pvs_inverse_restrict_sourcerighttableentrypositive * S ((S (dst_index_inverse_restrict_sourcerighttable)) * dst_positive_scale_inverse_restrict_sourcerighttable) + (dst_positive_inverse_restrict_sourcerighttable))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerighttableentrynegative. ff_h_pvs_inverse_restrict_sourcerighttableentrynegative + S (dst_negative_inverse_restrict_sourcerighttable) = S ((S (dst_index_inverse_restrict_sourcerighttable)) * dst_negative_scale_inverse_restrict_sourcerighttable)) /\ exists ff_q_pvs_inverse_restrict_sourcerighttableentrynegative. dst_negative_code_inverse_restrict_sourcerighttable = ff_q_pvs_inverse_restrict_sourcerighttableentrynegative * S ((S (dst_index_inverse_restrict_sourcerighttable)) * dst_negative_scale_inverse_restrict_sourcerighttable) + (dst_negative_inverse_restrict_sourcerighttable))) /\ (exists ge_balance_positive_inverse_restrict_sourcerighttableentryvalue ge_balance_negative_inverse_restrict_sourcerighttableentryvalue. (((((dst_value_inverse_restrict_sourcerighttable) = 2 * (ge_balance_positive_inverse_restrict_sourcerighttableentryvalue) /\ (ge_balance_negative_inverse_restrict_sourcerighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerighttableentryvaluedecode. (((dst_value_inverse_restrict_sourcerighttable) = 2 * ge_signed_half_inverse_restrict_sourcerighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerighttableentryvalue) = S ge_signed_half_inverse_restrict_sourcerighttableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcerighttable) + ge_balance_negative_inverse_restrict_sourcerighttableentryvalue = (dst_negative_inverse_restrict_sourcerighttable) + ge_balance_positive_inverse_restrict_sourcerighttableentryvalue))))))))) /\ (forall dc_input_inverse_restrict_sourceright dc_output_inverse_restrict_sourceright. ~(dc_input_inverse_restrict_sourceright=0) -> (exists pvs_le_gap_inverse_restrict_sourcerightdomain. pvs_le_gap_inverse_restrict_sourcerightdomain + (dc_input_inverse_restrict_sourceright) = (N)) -> (exists dst_positive_code_inverse_restrict_sourcerightlookup dst_positive_scale_inverse_restrict_sourcerightlookup dst_negative_code_inverse_restrict_sourcerightlookup dst_negative_scale_inverse_restrict_sourcerightlookup dst_positive_inverse_restrict_sourcerightlookup dst_negative_inverse_restrict_sourcerightlookup. (((di_delta_inverse_restrict_source) = (((((dst_positive_code_inverse_restrict_sourcerightlookup) + (dst_positive_scale_inverse_restrict_sourcerightlookup)) * S ((dst_positive_code_inverse_restrict_sourcerightlookup) + (dst_positive_scale_inverse_restrict_sourcerightlookup)) + ((dst_positive_scale_inverse_restrict_sourcerightlookup) + (dst_positive_scale_inverse_restrict_sourcerightlookup))) + (((dst_negative_code_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)) * S ((dst_negative_code_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)) + ((dst_negative_scale_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)))) * S ((((dst_positive_code_inverse_restrict_sourcerightlookup) + (dst_positive_scale_inverse_restrict_sourcerightlookup)) * S ((dst_positive_code_inverse_restrict_sourcerightlookup) + (dst_positive_scale_inverse_restrict_sourcerightlookup)) + ((dst_positive_scale_inverse_restrict_sourcerightlookup) + (dst_positive_scale_inverse_restrict_sourcerightlookup))) + (((dst_negative_code_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)) * S ((dst_negative_code_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)) + ((dst_negative_scale_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)))) + ((((dst_negative_code_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)) * S ((dst_negative_code_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)) + ((dst_negative_scale_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup))) + (((dst_negative_code_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)) * S ((dst_negative_code_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)) + ((dst_negative_scale_inverse_restrict_sourcerightlookup) + (dst_negative_scale_inverse_restrict_sourcerightlookup)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightlookuppositive. ff_h_pvs_inverse_restrict_sourcerightlookuppositive + S (dst_positive_inverse_restrict_sourcerightlookup) = S ((S (dc_input_inverse_restrict_sourceright)) * dst_positive_scale_inverse_restrict_sourcerightlookup)) /\ exists ff_q_pvs_inverse_restrict_sourcerightlookuppositive. dst_positive_code_inverse_restrict_sourcerightlookup = ff_q_pvs_inverse_restrict_sourcerightlookuppositive * S ((S (dc_input_inverse_restrict_sourceright)) * dst_positive_scale_inverse_restrict_sourcerightlookup) + (dst_positive_inverse_restrict_sourcerightlookup))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightlookupnegative. ff_h_pvs_inverse_restrict_sourcerightlookupnegative + S (dst_negative_inverse_restrict_sourcerightlookup) = S ((S (dc_input_inverse_restrict_sourceright)) * dst_negative_scale_inverse_restrict_sourcerightlookup)) /\ exists ff_q_pvs_inverse_restrict_sourcerightlookupnegative. dst_negative_code_inverse_restrict_sourcerightlookup = ff_q_pvs_inverse_restrict_sourcerightlookupnegative * S ((S (dc_input_inverse_restrict_sourceright)) * dst_negative_scale_inverse_restrict_sourcerightlookup) + (dst_negative_inverse_restrict_sourcerightlookup))) /\ (exists ge_balance_positive_inverse_restrict_sourcerightlookupvalue ge_balance_negative_inverse_restrict_sourcerightlookupvalue. (((((dc_output_inverse_restrict_sourceright) = 2 * (ge_balance_positive_inverse_restrict_sourcerightlookupvalue) /\ (ge_balance_negative_inverse_restrict_sourcerightlookupvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightlookupvaluedecode. (((dc_output_inverse_restrict_sourceright) = 2 * ge_signed_half_inverse_restrict_sourcerightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerightlookupvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerightlookupvalue) = S ge_signed_half_inverse_restrict_sourcerightlookupvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcerightlookup) + ge_balance_negative_inverse_restrict_sourcerightlookupvalue = (dst_negative_inverse_restrict_sourcerightlookup) + ge_balance_positive_inverse_restrict_sourcerightlookupvalue))))))))) -> (((~((dc_input_inverse_restrict_sourceright)=0)) /\ (exists dc_mask_inverse_restrict_sourcerightvalue. ((((exists dst_positive_code_inverse_restrict_sourcerightvaluemasktable dst_positive_scale_inverse_restrict_sourcerightvaluemasktable dst_negative_code_inverse_restrict_sourcerightvaluemasktable dst_negative_scale_inverse_restrict_sourcerightvaluemasktable. (((dc_mask_inverse_restrict_sourcerightvalue) = (((((dst_positive_code_inverse_restrict_sourcerightvaluemasktable) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluemasktable) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluemasktable) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)))) * S ((((dst_positive_code_inverse_restrict_sourcerightvaluemasktable) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluemasktable) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluemasktable) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)))) + ((((dst_negative_code_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)))))) /\ (forall dst_index_inverse_restrict_sourcerightvaluemasktable. (exists pvs_le_gap_inverse_restrict_sourcerightvaluemasktabledomain. pvs_le_gap_inverse_restrict_sourcerightvaluemasktabledomain + (dst_index_inverse_restrict_sourcerightvaluemasktable) = (dc_input_inverse_restrict_sourceright)) -> exists dst_positive_inverse_restrict_sourcerightvaluemasktable dst_negative_inverse_restrict_sourcerightvaluemasktable dst_value_inverse_restrict_sourcerightvaluemasktable. ((((exists ff_h_pvs_inverse_restrict_sourcerightvaluemasktableentrypositive. ff_h_pvs_inverse_restrict_sourcerightvaluemasktableentrypositive + S (dst_positive_inverse_restrict_sourcerightvaluemasktable) = S ((S (dst_index_inverse_restrict_sourcerightvaluemasktable)) * dst_positive_scale_inverse_restrict_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_restrict_sourcerightvaluemasktableentrypositive. dst_positive_code_inverse_restrict_sourcerightvaluemasktable = ff_q_pvs_inverse_restrict_sourcerightvaluemasktableentrypositive * S ((S (dst_index_inverse_restrict_sourcerightvaluemasktable)) * dst_positive_scale_inverse_restrict_sourcerightvaluemasktable) + (dst_positive_inverse_restrict_sourcerightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightvaluemasktableentrynegative. ff_h_pvs_inverse_restrict_sourcerightvaluemasktableentrynegative + S (dst_negative_inverse_restrict_sourcerightvaluemasktable) = S ((S (dst_index_inverse_restrict_sourcerightvaluemasktable)) * dst_negative_scale_inverse_restrict_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_restrict_sourcerightvaluemasktableentrynegative. dst_negative_code_inverse_restrict_sourcerightvaluemasktable = ff_q_pvs_inverse_restrict_sourcerightvaluemasktableentrynegative * S ((S (dst_index_inverse_restrict_sourcerightvaluemasktable)) * dst_negative_scale_inverse_restrict_sourcerightvaluemasktable) + (dst_negative_inverse_restrict_sourcerightvaluemasktable))) /\ (exists ge_balance_positive_inverse_restrict_sourcerightvaluemasktableentryvalue ge_balance_negative_inverse_restrict_sourcerightvaluemasktableentryvalue. (((((dst_value_inverse_restrict_sourcerightvaluemasktable) = 2 * (ge_balance_positive_inverse_restrict_sourcerightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightvaluemasktableentryvaluedecode. (((dst_value_inverse_restrict_sourcerightvaluemasktable) = 2 * ge_signed_half_inverse_restrict_sourcerightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluemasktableentryvalue) = S ge_signed_half_inverse_restrict_sourcerightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcerightvaluemasktable) + ge_balance_negative_inverse_restrict_sourcerightvaluemasktableentryvalue = (dst_negative_inverse_restrict_sourcerightvaluemasktable) + ge_balance_positive_inverse_restrict_sourcerightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_restrict_sourcerightvaluemask dc_value_inverse_restrict_sourcerightvaluemask. (exists pvs_le_gap_inverse_restrict_sourcerightvaluemaskdomain. pvs_le_gap_inverse_restrict_sourcerightvaluemaskdomain + (dc_index_inverse_restrict_sourcerightvaluemask) = (dc_input_inverse_restrict_sourceright)) -> (exists dst_positive_code_inverse_restrict_sourcerightvaluemasklookup dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup dst_negative_code_inverse_restrict_sourcerightvaluemasklookup dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup dst_positive_inverse_restrict_sourcerightvaluemasklookup dst_negative_inverse_restrict_sourcerightvaluemasklookup. (((dc_mask_inverse_restrict_sourcerightvalue) = (((((dst_positive_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)))) * S ((((dst_positive_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)))) + ((((dst_negative_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightvaluemasklookuppositive. ff_h_pvs_inverse_restrict_sourcerightvaluemasklookuppositive + S (dst_positive_inverse_restrict_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_restrict_sourcerightvaluemask)) * dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_restrict_sourcerightvaluemasklookuppositive. dst_positive_code_inverse_restrict_sourcerightvaluemasklookup = ff_q_pvs_inverse_restrict_sourcerightvaluemasklookuppositive * S ((S (dc_index_inverse_restrict_sourcerightvaluemask)) * dst_positive_scale_inverse_restrict_sourcerightvaluemasklookup) + (dst_positive_inverse_restrict_sourcerightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightvaluemasklookupnegative. ff_h_pvs_inverse_restrict_sourcerightvaluemasklookupnegative + S (dst_negative_inverse_restrict_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_restrict_sourcerightvaluemask)) * dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_restrict_sourcerightvaluemasklookupnegative. dst_negative_code_inverse_restrict_sourcerightvaluemasklookup = ff_q_pvs_inverse_restrict_sourcerightvaluemasklookupnegative * S ((S (dc_index_inverse_restrict_sourcerightvaluemask)) * dst_negative_scale_inverse_restrict_sourcerightvaluemasklookup) + (dst_negative_inverse_restrict_sourcerightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_restrict_sourcerightvaluemasklookupvalue ge_balance_negative_inverse_restrict_sourcerightvaluemasklookupvalue. (((((dc_value_inverse_restrict_sourcerightvaluemask) = 2 * (ge_balance_positive_inverse_restrict_sourcerightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightvaluemasklookupvaluedecode. (((dc_value_inverse_restrict_sourcerightvaluemask) = 2 * ge_signed_half_inverse_restrict_sourcerightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluemasklookupvalue) = S ge_signed_half_inverse_restrict_sourcerightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcerightvaluemasklookup) + ge_balance_negative_inverse_restrict_sourcerightvaluemasklookupvalue = (dst_negative_inverse_restrict_sourcerightvaluemasklookup) + ge_balance_positive_inverse_restrict_sourcerightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_restrict_sourcerightvaluemask)=0)) /\ (exists dc_quotient_inverse_restrict_sourcerightvaluemaskentry dc_left_inverse_restrict_sourcerightvaluemaskentry dc_right_inverse_restrict_sourcerightvaluemaskentry. (((dc_input_inverse_restrict_sourceright)=(dc_index_inverse_restrict_sourcerightvaluemask)*dc_quotient_inverse_restrict_sourcerightvaluemaskentry) /\ (((exists dst_positive_code_inverse_restrict_sourcerightvaluemaskentryleft dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft dst_positive_inverse_restrict_sourcerightvaluemaskentryleft dst_negative_inverse_restrict_sourcerightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightvaluemaskentryleftpositive. ff_h_pvs_inverse_restrict_sourcerightvaluemaskentryleftpositive + S (dst_positive_inverse_restrict_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_restrict_sourcerightvaluemask)) * dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_restrict_sourcerightvaluemaskentryleftpositive. dst_positive_code_inverse_restrict_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_restrict_sourcerightvaluemaskentryleftpositive * S ((S (dc_index_inverse_restrict_sourcerightvaluemask)) * dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_positive_inverse_restrict_sourcerightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightvaluemaskentryleftnegative. ff_h_pvs_inverse_restrict_sourcerightvaluemaskentryleftnegative + S (dst_negative_inverse_restrict_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_restrict_sourcerightvaluemask)) * dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_restrict_sourcerightvaluemaskentryleftnegative. dst_negative_code_inverse_restrict_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_restrict_sourcerightvaluemaskentryleftnegative * S ((S (dc_index_inverse_restrict_sourcerightvaluemask)) * dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryleft) + (dst_negative_inverse_restrict_sourcerightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_restrict_sourcerightvaluemaskentryleftvalue ge_balance_negative_inverse_restrict_sourcerightvaluemaskentryleftvalue. (((((dc_left_inverse_restrict_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_restrict_sourcerightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightvaluemaskentryleftvaluedecode. (((dc_left_inverse_restrict_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_sourcerightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluemaskentryleftvalue) = S ge_signed_half_inverse_restrict_sourcerightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcerightvaluemaskentryleft) + ge_balance_negative_inverse_restrict_sourcerightvaluemaskentryleftvalue = (dst_negative_inverse_restrict_sourcerightvaluemaskentryleft) + ge_balance_positive_inverse_restrict_sourcerightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_sourcerightvaluemaskentryright dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright dst_positive_inverse_restrict_sourcerightvaluemaskentryright dst_negative_inverse_restrict_sourcerightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)))) + ((((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightvaluemaskentryrightpositive. ff_h_pvs_inverse_restrict_sourcerightvaluemaskentryrightpositive + S (dst_positive_inverse_restrict_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_restrict_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_restrict_sourcerightvaluemaskentryrightpositive. dst_positive_code_inverse_restrict_sourcerightvaluemaskentryright = ff_q_pvs_inverse_restrict_sourcerightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_restrict_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_restrict_sourcerightvaluemaskentryright) + (dst_positive_inverse_restrict_sourcerightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_restrict_sourcerightvaluemaskentryrightnegative. ff_h_pvs_inverse_restrict_sourcerightvaluemaskentryrightnegative + S (dst_negative_inverse_restrict_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_restrict_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_restrict_sourcerightvaluemaskentryrightnegative. dst_negative_code_inverse_restrict_sourcerightvaluemaskentryright = ff_q_pvs_inverse_restrict_sourcerightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_restrict_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_restrict_sourcerightvaluemaskentryright) + (dst_negative_inverse_restrict_sourcerightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_restrict_sourcerightvaluemaskentryrightvalue ge_balance_negative_inverse_restrict_sourcerightvaluemaskentryrightvalue. (((((dc_right_inverse_restrict_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_restrict_sourcerightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightvaluemaskentryrightvaluedecode. (((dc_right_inverse_restrict_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_sourcerightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluemaskentryrightvalue) = S ge_signed_half_inverse_restrict_sourcerightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_restrict_sourcerightvaluemaskentryright) + ge_balance_negative_inverse_restrict_sourcerightvaluemaskentryrightvalue = (dst_negative_inverse_restrict_sourcerightvaluemaskentryright) + ge_balance_positive_inverse_restrict_sourcerightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_restrict_sourcerightvaluemaskentryproduct sto_an_inverse_restrict_sourcerightvaluemaskentryproduct sto_bp_inverse_restrict_sourcerightvaluemaskentryproduct sto_bn_inverse_restrict_sourcerightvaluemaskentryproduct sto_cp_inverse_restrict_sourcerightvaluemaskentryproduct sto_cn_inverse_restrict_sourcerightvaluemaskentryproduct. (((((dc_left_inverse_restrict_sourcerightvaluemaskentry) = 2 * (sto_ap_inverse_restrict_sourcerightvaluemaskentryproduct) /\ (sto_an_inverse_restrict_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductleft. (((dc_left_inverse_restrict_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_restrict_sourcerightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_restrict_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_restrict_sourcerightvaluemaskentry) = 2 * (sto_bp_inverse_restrict_sourcerightvaluemaskentryproduct) /\ (sto_bn_inverse_restrict_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductright. (((dc_right_inverse_restrict_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_restrict_sourcerightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_restrict_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_restrict_sourcerightvaluemask) = 2 * (sto_cp_inverse_restrict_sourcerightvaluemaskentryproduct) /\ (sto_cn_inverse_restrict_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductoutput. (((dc_value_inverse_restrict_sourcerightvaluemask) = 2 * ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_restrict_sourcerightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_restrict_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_sourcerightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_restrict_sourcerightvaluemaskentryproduct * sto_bp_inverse_restrict_sourcerightvaluemaskentryproduct + sto_an_inverse_restrict_sourcerightvaluemaskentryproduct * sto_bn_inverse_restrict_sourcerightvaluemaskentryproduct) + sto_cn_inverse_restrict_sourcerightvaluemaskentryproduct = (sto_ap_inverse_restrict_sourcerightvaluemaskentryproduct * sto_bn_inverse_restrict_sourcerightvaluemaskentryproduct + sto_an_inverse_restrict_sourcerightvaluemaskentryproduct * sto_bp_inverse_restrict_sourcerightvaluemaskentryproduct) + sto_cp_inverse_restrict_sourcerightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_restrict_sourcerightvaluemask)=0 \/ ~(exists pvs_factor_inverse_restrict_sourcerightvaluemaskentrynondivisor. (dc_input_inverse_restrict_sourceright) = (dc_index_inverse_restrict_sourcerightvaluemask) * pvs_factor_inverse_restrict_sourcerightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_restrict_sourcerightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_restrict_sourcerightvaluefold dst_positive_scale_inverse_restrict_sourcerightvaluefold dst_negative_code_inverse_restrict_sourcerightvaluefold dst_negative_scale_inverse_restrict_sourcerightvaluefold dst_positive_sum_inverse_restrict_sourcerightvaluefold dst_negative_sum_inverse_restrict_sourcerightvaluefold. (((dc_mask_inverse_restrict_sourcerightvalue) = (((((dst_positive_code_inverse_restrict_sourcerightvaluefold) + (dst_positive_scale_inverse_restrict_sourcerightvaluefold)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluefold) + (dst_positive_scale_inverse_restrict_sourcerightvaluefold)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluefold) + (dst_positive_scale_inverse_restrict_sourcerightvaluefold))) + (((dst_negative_code_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)))) * S ((((dst_positive_code_inverse_restrict_sourcerightvaluefold) + (dst_positive_scale_inverse_restrict_sourcerightvaluefold)) * S ((dst_positive_code_inverse_restrict_sourcerightvaluefold) + (dst_positive_scale_inverse_restrict_sourcerightvaluefold)) + ((dst_positive_scale_inverse_restrict_sourcerightvaluefold) + (dst_positive_scale_inverse_restrict_sourcerightvaluefold))) + (((dst_negative_code_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)))) + ((((dst_negative_code_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold))) + (((dst_negative_code_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)) * S ((dst_negative_code_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)) + ((dst_negative_scale_inverse_restrict_sourcerightvaluefold) + (dst_negative_scale_inverse_restrict_sourcerightvaluefold)))))) /\ (((exists fs_u_dst_inverse_restrict_sourcerightvaluefoldpositive fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive. ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_start. fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_start. fs_u_dst_inverse_restrict_sourcerightvaluefoldpositive = fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_terminal. fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_restrict_sourcerightvaluefold) = S ((S (S (dc_input_inverse_restrict_sourceright))) * fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_terminal. fs_u_dst_inverse_restrict_sourcerightvaluefoldpositive = fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_restrict_sourceright))) * fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive) + (dst_positive_sum_inverse_restrict_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps = S (dc_input_inverse_restrict_sourceright)) -> exists fs_a_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps fs_r_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps fs_s_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_restrict_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_restrict_sourcerightvaluefold = fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_restrict_sourcerightvaluefold) + (fs_a_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_restrict_sourcerightvaluefoldpositive = fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive) + (fs_r_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_restrict_sourcerightvaluefoldpositive = fs_q_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldpositive) + (fs_s_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps = fs_r_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps + fs_a_dst_inverse_restrict_sourcerightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_restrict_sourcerightvaluefoldnegative fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative. ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_start. fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_start. fs_u_dst_inverse_restrict_sourcerightvaluefoldnegative = fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_terminal. fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_restrict_sourcerightvaluefold) = S ((S (S (dc_input_inverse_restrict_sourceright))) * fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_terminal. fs_u_dst_inverse_restrict_sourcerightvaluefoldnegative = fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_restrict_sourceright))) * fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative) + (dst_negative_sum_inverse_restrict_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps = S (dc_input_inverse_restrict_sourceright)) -> exists fs_a_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps fs_r_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps fs_s_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_restrict_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_restrict_sourcerightvaluefold = fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_restrict_sourcerightvaluefold) + (fs_a_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_restrict_sourcerightvaluefoldnegative = fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative) + (fs_r_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_restrict_sourcerightvaluefoldnegative = fs_q_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_sourcerightvaluefoldnegative) + (fs_s_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps = fs_r_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps + fs_a_dst_inverse_restrict_sourcerightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_restrict_sourcerightvaluefoldresult ge_balance_negative_inverse_restrict_sourcerightvaluefoldresult. (((((dc_output_inverse_restrict_sourceright) = 2 * (ge_balance_positive_inverse_restrict_sourcerightvaluefoldresult) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_restrict_sourcerightvaluefoldresultdecode. (((dc_output_inverse_restrict_sourceright) = 2 * ge_signed_half_inverse_restrict_sourcerightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_restrict_sourcerightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_restrict_sourcerightvaluefoldresult) = S ge_signed_half_inverse_restrict_sourcerightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_restrict_sourcerightvaluefold) + ge_balance_negative_inverse_restrict_sourcerightvaluefoldresult = (dst_negative_sum_inverse_restrict_sourcerightvaluefold) + ge_balance_positive_inverse_restrict_sourcerightvaluefoldresult)))))))))))))))))))))))) -> (exists pvs_le_gap_inverse_restrict_bound. pvs_le_gap_inverse_restrict_bound + (K) = (N)) -> (exists di_delta_inverse_restrict_result. ((((exists dst_positive_code_inverse_restrict_resultdeltatable dst_positive_scale_inverse_restrict_resultdeltatable dst_negative_code_inverse_restrict_resultdeltatable dst_negative_scale_inverse_restrict_resultdeltatable. (((di_delta_inverse_restrict_result) = (((((dst_positive_code_inverse_restrict_resultdeltatable) + (dst_positive_scale_inverse_restrict_resultdeltatable)) * S ((dst_positive_code_inverse_restrict_resultdeltatable) + (dst_positive_scale_inverse_restrict_resultdeltatable)) + ((dst_positive_scale_inverse_restrict_resultdeltatable) + (dst_positive_scale_inverse_restrict_resultdeltatable))) + (((dst_negative_code_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)) * S ((dst_negative_code_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)) + ((dst_negative_scale_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)))) * S ((((dst_positive_code_inverse_restrict_resultdeltatable) + (dst_positive_scale_inverse_restrict_resultdeltatable)) * S ((dst_positive_code_inverse_restrict_resultdeltatable) + (dst_positive_scale_inverse_restrict_resultdeltatable)) + ((dst_positive_scale_inverse_restrict_resultdeltatable) + (dst_positive_scale_inverse_restrict_resultdeltatable))) + (((dst_negative_code_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)) * S ((dst_negative_code_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)) + ((dst_negative_scale_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)))) + ((((dst_negative_code_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)) * S ((dst_negative_code_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)) + ((dst_negative_scale_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable))) + (((dst_negative_code_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)) * S ((dst_negative_code_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)) + ((dst_negative_scale_inverse_restrict_resultdeltatable) + (dst_negative_scale_inverse_restrict_resultdeltatable)))))) /\ (forall dst_index_inverse_restrict_resultdeltatable. (exists pvs_le_gap_inverse_restrict_resultdeltatabledomain. pvs_le_gap_inverse_restrict_resultdeltatabledomain + (dst_index_inverse_restrict_resultdeltatable) = (K)) -> exists dst_positive_inverse_restrict_resultdeltatable dst_negative_inverse_restrict_resultdeltatable dst_value_inverse_restrict_resultdeltatable. ((((exists ff_h_pvs_inverse_restrict_resultdeltatableentrypositive. ff_h_pvs_inverse_restrict_resultdeltatableentrypositive + S (dst_positive_inverse_restrict_resultdeltatable) = S ((S (dst_index_inverse_restrict_resultdeltatable)) * dst_positive_scale_inverse_restrict_resultdeltatable)) /\ exists ff_q_pvs_inverse_restrict_resultdeltatableentrypositive. dst_positive_code_inverse_restrict_resultdeltatable = ff_q_pvs_inverse_restrict_resultdeltatableentrypositive * S ((S (dst_index_inverse_restrict_resultdeltatable)) * dst_positive_scale_inverse_restrict_resultdeltatable) + (dst_positive_inverse_restrict_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_restrict_resultdeltatableentrynegative. ff_h_pvs_inverse_restrict_resultdeltatableentrynegative + S (dst_negative_inverse_restrict_resultdeltatable) = S ((S (dst_index_inverse_restrict_resultdeltatable)) * dst_negative_scale_inverse_restrict_resultdeltatable)) /\ exists ff_q_pvs_inverse_restrict_resultdeltatableentrynegative. dst_negative_code_inverse_restrict_resultdeltatable = ff_q_pvs_inverse_restrict_resultdeltatableentrynegative * S ((S (dst_index_inverse_restrict_resultdeltatable)) * dst_negative_scale_inverse_restrict_resultdeltatable) + (dst_negative_inverse_restrict_resultdeltatable))) /\ (exists ge_balance_positive_inverse_restrict_resultdeltatableentryvalue ge_balance_negative_inverse_restrict_resultdeltatableentryvalue. (((((dst_value_inverse_restrict_resultdeltatable) = 2 * (ge_balance_positive_inverse_restrict_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_restrict_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultdeltatableentryvaluedecode. (((dst_value_inverse_restrict_resultdeltatable) = 2 * ge_signed_half_inverse_restrict_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultdeltatableentryvalue) = S ge_signed_half_inverse_restrict_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultdeltatable) + ge_balance_negative_inverse_restrict_resultdeltatableentryvalue = (dst_negative_inverse_restrict_resultdeltatable) + ge_balance_positive_inverse_restrict_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_restrict_resultdelta du_value_inverse_restrict_resultdelta. ~(du_index_inverse_restrict_resultdelta=0) -> (exists pvs_le_gap_inverse_restrict_resultdeltabound. pvs_le_gap_inverse_restrict_resultdeltabound + (du_index_inverse_restrict_resultdelta) = (K)) -> (exists dst_positive_code_inverse_restrict_resultdeltaentry dst_positive_scale_inverse_restrict_resultdeltaentry dst_negative_code_inverse_restrict_resultdeltaentry dst_negative_scale_inverse_restrict_resultdeltaentry dst_positive_inverse_restrict_resultdeltaentry dst_negative_inverse_restrict_resultdeltaentry. (((di_delta_inverse_restrict_result) = (((((dst_positive_code_inverse_restrict_resultdeltaentry) + (dst_positive_scale_inverse_restrict_resultdeltaentry)) * S ((dst_positive_code_inverse_restrict_resultdeltaentry) + (dst_positive_scale_inverse_restrict_resultdeltaentry)) + ((dst_positive_scale_inverse_restrict_resultdeltaentry) + (dst_positive_scale_inverse_restrict_resultdeltaentry))) + (((dst_negative_code_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)) * S ((dst_negative_code_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)) + ((dst_negative_scale_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)))) * S ((((dst_positive_code_inverse_restrict_resultdeltaentry) + (dst_positive_scale_inverse_restrict_resultdeltaentry)) * S ((dst_positive_code_inverse_restrict_resultdeltaentry) + (dst_positive_scale_inverse_restrict_resultdeltaentry)) + ((dst_positive_scale_inverse_restrict_resultdeltaentry) + (dst_positive_scale_inverse_restrict_resultdeltaentry))) + (((dst_negative_code_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)) * S ((dst_negative_code_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)) + ((dst_negative_scale_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)))) + ((((dst_negative_code_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)) * S ((dst_negative_code_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)) + ((dst_negative_scale_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry))) + (((dst_negative_code_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)) * S ((dst_negative_code_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)) + ((dst_negative_scale_inverse_restrict_resultdeltaentry) + (dst_negative_scale_inverse_restrict_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultdeltaentrypositive. ff_h_pvs_inverse_restrict_resultdeltaentrypositive + S (dst_positive_inverse_restrict_resultdeltaentry) = S ((S (du_index_inverse_restrict_resultdelta)) * dst_positive_scale_inverse_restrict_resultdeltaentry)) /\ exists ff_q_pvs_inverse_restrict_resultdeltaentrypositive. dst_positive_code_inverse_restrict_resultdeltaentry = ff_q_pvs_inverse_restrict_resultdeltaentrypositive * S ((S (du_index_inverse_restrict_resultdelta)) * dst_positive_scale_inverse_restrict_resultdeltaentry) + (dst_positive_inverse_restrict_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_restrict_resultdeltaentrynegative. ff_h_pvs_inverse_restrict_resultdeltaentrynegative + S (dst_negative_inverse_restrict_resultdeltaentry) = S ((S (du_index_inverse_restrict_resultdelta)) * dst_negative_scale_inverse_restrict_resultdeltaentry)) /\ exists ff_q_pvs_inverse_restrict_resultdeltaentrynegative. dst_negative_code_inverse_restrict_resultdeltaentry = ff_q_pvs_inverse_restrict_resultdeltaentrynegative * S ((S (du_index_inverse_restrict_resultdelta)) * dst_negative_scale_inverse_restrict_resultdeltaentry) + (dst_negative_inverse_restrict_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_restrict_resultdeltaentryvalue ge_balance_negative_inverse_restrict_resultdeltaentryvalue. (((((du_value_inverse_restrict_resultdelta) = 2 * (ge_balance_positive_inverse_restrict_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_restrict_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultdeltaentryvaluedecode. (((du_value_inverse_restrict_resultdelta) = 2 * ge_signed_half_inverse_restrict_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultdeltaentryvalue) = S ge_signed_half_inverse_restrict_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultdeltaentry) + ge_balance_negative_inverse_restrict_resultdeltaentryvalue = (dst_negative_inverse_restrict_resultdeltaentry) + ge_balance_positive_inverse_restrict_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_restrict_resultdelta)=1 -> (du_value_inverse_restrict_resultdelta)=2) /\ (~((du_index_inverse_restrict_resultdelta)=1) -> (du_value_inverse_restrict_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_restrict_resultleftleft dst_positive_scale_inverse_restrict_resultleftleft dst_negative_code_inverse_restrict_resultleftleft dst_negative_scale_inverse_restrict_resultleftleft. (((F) = (((((dst_positive_code_inverse_restrict_resultleftleft) + (dst_positive_scale_inverse_restrict_resultleftleft)) * S ((dst_positive_code_inverse_restrict_resultleftleft) + (dst_positive_scale_inverse_restrict_resultleftleft)) + ((dst_positive_scale_inverse_restrict_resultleftleft) + (dst_positive_scale_inverse_restrict_resultleftleft))) + (((dst_negative_code_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)) * S ((dst_negative_code_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)) + ((dst_negative_scale_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)))) * S ((((dst_positive_code_inverse_restrict_resultleftleft) + (dst_positive_scale_inverse_restrict_resultleftleft)) * S ((dst_positive_code_inverse_restrict_resultleftleft) + (dst_positive_scale_inverse_restrict_resultleftleft)) + ((dst_positive_scale_inverse_restrict_resultleftleft) + (dst_positive_scale_inverse_restrict_resultleftleft))) + (((dst_negative_code_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)) * S ((dst_negative_code_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)) + ((dst_negative_scale_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)))) + ((((dst_negative_code_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)) * S ((dst_negative_code_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)) + ((dst_negative_scale_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft))) + (((dst_negative_code_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)) * S ((dst_negative_code_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)) + ((dst_negative_scale_inverse_restrict_resultleftleft) + (dst_negative_scale_inverse_restrict_resultleftleft)))))) /\ (forall dst_index_inverse_restrict_resultleftleft. (exists pvs_le_gap_inverse_restrict_resultleftleftdomain. pvs_le_gap_inverse_restrict_resultleftleftdomain + (dst_index_inverse_restrict_resultleftleft) = (K)) -> exists dst_positive_inverse_restrict_resultleftleft dst_negative_inverse_restrict_resultleftleft dst_value_inverse_restrict_resultleftleft. ((((exists ff_h_pvs_inverse_restrict_resultleftleftentrypositive. ff_h_pvs_inverse_restrict_resultleftleftentrypositive + S (dst_positive_inverse_restrict_resultleftleft) = S ((S (dst_index_inverse_restrict_resultleftleft)) * dst_positive_scale_inverse_restrict_resultleftleft)) /\ exists ff_q_pvs_inverse_restrict_resultleftleftentrypositive. dst_positive_code_inverse_restrict_resultleftleft = ff_q_pvs_inverse_restrict_resultleftleftentrypositive * S ((S (dst_index_inverse_restrict_resultleftleft)) * dst_positive_scale_inverse_restrict_resultleftleft) + (dst_positive_inverse_restrict_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftleftentrynegative. ff_h_pvs_inverse_restrict_resultleftleftentrynegative + S (dst_negative_inverse_restrict_resultleftleft) = S ((S (dst_index_inverse_restrict_resultleftleft)) * dst_negative_scale_inverse_restrict_resultleftleft)) /\ exists ff_q_pvs_inverse_restrict_resultleftleftentrynegative. dst_negative_code_inverse_restrict_resultleftleft = ff_q_pvs_inverse_restrict_resultleftleftentrynegative * S ((S (dst_index_inverse_restrict_resultleftleft)) * dst_negative_scale_inverse_restrict_resultleftleft) + (dst_negative_inverse_restrict_resultleftleft))) /\ (exists ge_balance_positive_inverse_restrict_resultleftleftentryvalue ge_balance_negative_inverse_restrict_resultleftleftentryvalue. (((((dst_value_inverse_restrict_resultleftleft) = 2 * (ge_balance_positive_inverse_restrict_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_restrict_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftleftentryvaluedecode. (((dst_value_inverse_restrict_resultleftleft) = 2 * ge_signed_half_inverse_restrict_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultleftleftentryvalue) = S ge_signed_half_inverse_restrict_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultleftleft) + ge_balance_negative_inverse_restrict_resultleftleftentryvalue = (dst_negative_inverse_restrict_resultleftleft) + ge_balance_positive_inverse_restrict_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_resultleftright dst_positive_scale_inverse_restrict_resultleftright dst_negative_code_inverse_restrict_resultleftright dst_negative_scale_inverse_restrict_resultleftright. (((G) = (((((dst_positive_code_inverse_restrict_resultleftright) + (dst_positive_scale_inverse_restrict_resultleftright)) * S ((dst_positive_code_inverse_restrict_resultleftright) + (dst_positive_scale_inverse_restrict_resultleftright)) + ((dst_positive_scale_inverse_restrict_resultleftright) + (dst_positive_scale_inverse_restrict_resultleftright))) + (((dst_negative_code_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)) * S ((dst_negative_code_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)) + ((dst_negative_scale_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)))) * S ((((dst_positive_code_inverse_restrict_resultleftright) + (dst_positive_scale_inverse_restrict_resultleftright)) * S ((dst_positive_code_inverse_restrict_resultleftright) + (dst_positive_scale_inverse_restrict_resultleftright)) + ((dst_positive_scale_inverse_restrict_resultleftright) + (dst_positive_scale_inverse_restrict_resultleftright))) + (((dst_negative_code_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)) * S ((dst_negative_code_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)) + ((dst_negative_scale_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)))) + ((((dst_negative_code_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)) * S ((dst_negative_code_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)) + ((dst_negative_scale_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright))) + (((dst_negative_code_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)) * S ((dst_negative_code_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)) + ((dst_negative_scale_inverse_restrict_resultleftright) + (dst_negative_scale_inverse_restrict_resultleftright)))))) /\ (forall dst_index_inverse_restrict_resultleftright. (exists pvs_le_gap_inverse_restrict_resultleftrightdomain. pvs_le_gap_inverse_restrict_resultleftrightdomain + (dst_index_inverse_restrict_resultleftright) = (K)) -> exists dst_positive_inverse_restrict_resultleftright dst_negative_inverse_restrict_resultleftright dst_value_inverse_restrict_resultleftright. ((((exists ff_h_pvs_inverse_restrict_resultleftrightentrypositive. ff_h_pvs_inverse_restrict_resultleftrightentrypositive + S (dst_positive_inverse_restrict_resultleftright) = S ((S (dst_index_inverse_restrict_resultleftright)) * dst_positive_scale_inverse_restrict_resultleftright)) /\ exists ff_q_pvs_inverse_restrict_resultleftrightentrypositive. dst_positive_code_inverse_restrict_resultleftright = ff_q_pvs_inverse_restrict_resultleftrightentrypositive * S ((S (dst_index_inverse_restrict_resultleftright)) * dst_positive_scale_inverse_restrict_resultleftright) + (dst_positive_inverse_restrict_resultleftright))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftrightentrynegative. ff_h_pvs_inverse_restrict_resultleftrightentrynegative + S (dst_negative_inverse_restrict_resultleftright) = S ((S (dst_index_inverse_restrict_resultleftright)) * dst_negative_scale_inverse_restrict_resultleftright)) /\ exists ff_q_pvs_inverse_restrict_resultleftrightentrynegative. dst_negative_code_inverse_restrict_resultleftright = ff_q_pvs_inverse_restrict_resultleftrightentrynegative * S ((S (dst_index_inverse_restrict_resultleftright)) * dst_negative_scale_inverse_restrict_resultleftright) + (dst_negative_inverse_restrict_resultleftright))) /\ (exists ge_balance_positive_inverse_restrict_resultleftrightentryvalue ge_balance_negative_inverse_restrict_resultleftrightentryvalue. (((((dst_value_inverse_restrict_resultleftright) = 2 * (ge_balance_positive_inverse_restrict_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_restrict_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftrightentryvaluedecode. (((dst_value_inverse_restrict_resultleftright) = 2 * ge_signed_half_inverse_restrict_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultleftrightentryvalue) = S ge_signed_half_inverse_restrict_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultleftright) + ge_balance_negative_inverse_restrict_resultleftrightentryvalue = (dst_negative_inverse_restrict_resultleftright) + ge_balance_positive_inverse_restrict_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_resultlefttable dst_positive_scale_inverse_restrict_resultlefttable dst_negative_code_inverse_restrict_resultlefttable dst_negative_scale_inverse_restrict_resultlefttable. (((di_delta_inverse_restrict_result) = (((((dst_positive_code_inverse_restrict_resultlefttable) + (dst_positive_scale_inverse_restrict_resultlefttable)) * S ((dst_positive_code_inverse_restrict_resultlefttable) + (dst_positive_scale_inverse_restrict_resultlefttable)) + ((dst_positive_scale_inverse_restrict_resultlefttable) + (dst_positive_scale_inverse_restrict_resultlefttable))) + (((dst_negative_code_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)) * S ((dst_negative_code_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)) + ((dst_negative_scale_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)))) * S ((((dst_positive_code_inverse_restrict_resultlefttable) + (dst_positive_scale_inverse_restrict_resultlefttable)) * S ((dst_positive_code_inverse_restrict_resultlefttable) + (dst_positive_scale_inverse_restrict_resultlefttable)) + ((dst_positive_scale_inverse_restrict_resultlefttable) + (dst_positive_scale_inverse_restrict_resultlefttable))) + (((dst_negative_code_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)) * S ((dst_negative_code_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)) + ((dst_negative_scale_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)))) + ((((dst_negative_code_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)) * S ((dst_negative_code_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)) + ((dst_negative_scale_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable))) + (((dst_negative_code_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)) * S ((dst_negative_code_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)) + ((dst_negative_scale_inverse_restrict_resultlefttable) + (dst_negative_scale_inverse_restrict_resultlefttable)))))) /\ (forall dst_index_inverse_restrict_resultlefttable. (exists pvs_le_gap_inverse_restrict_resultlefttabledomain. pvs_le_gap_inverse_restrict_resultlefttabledomain + (dst_index_inverse_restrict_resultlefttable) = (K)) -> exists dst_positive_inverse_restrict_resultlefttable dst_negative_inverse_restrict_resultlefttable dst_value_inverse_restrict_resultlefttable. ((((exists ff_h_pvs_inverse_restrict_resultlefttableentrypositive. ff_h_pvs_inverse_restrict_resultlefttableentrypositive + S (dst_positive_inverse_restrict_resultlefttable) = S ((S (dst_index_inverse_restrict_resultlefttable)) * dst_positive_scale_inverse_restrict_resultlefttable)) /\ exists ff_q_pvs_inverse_restrict_resultlefttableentrypositive. dst_positive_code_inverse_restrict_resultlefttable = ff_q_pvs_inverse_restrict_resultlefttableentrypositive * S ((S (dst_index_inverse_restrict_resultlefttable)) * dst_positive_scale_inverse_restrict_resultlefttable) + (dst_positive_inverse_restrict_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_restrict_resultlefttableentrynegative. ff_h_pvs_inverse_restrict_resultlefttableentrynegative + S (dst_negative_inverse_restrict_resultlefttable) = S ((S (dst_index_inverse_restrict_resultlefttable)) * dst_negative_scale_inverse_restrict_resultlefttable)) /\ exists ff_q_pvs_inverse_restrict_resultlefttableentrynegative. dst_negative_code_inverse_restrict_resultlefttable = ff_q_pvs_inverse_restrict_resultlefttableentrynegative * S ((S (dst_index_inverse_restrict_resultlefttable)) * dst_negative_scale_inverse_restrict_resultlefttable) + (dst_negative_inverse_restrict_resultlefttable))) /\ (exists ge_balance_positive_inverse_restrict_resultlefttableentryvalue ge_balance_negative_inverse_restrict_resultlefttableentryvalue. (((((dst_value_inverse_restrict_resultlefttable) = 2 * (ge_balance_positive_inverse_restrict_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_restrict_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultlefttableentryvaluedecode. (((dst_value_inverse_restrict_resultlefttable) = 2 * ge_signed_half_inverse_restrict_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultlefttableentryvalue) = S ge_signed_half_inverse_restrict_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultlefttable) + ge_balance_negative_inverse_restrict_resultlefttableentryvalue = (dst_negative_inverse_restrict_resultlefttable) + ge_balance_positive_inverse_restrict_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_restrict_resultleft dc_output_inverse_restrict_resultleft. ~(dc_input_inverse_restrict_resultleft=0) -> (exists pvs_le_gap_inverse_restrict_resultleftdomain. pvs_le_gap_inverse_restrict_resultleftdomain + (dc_input_inverse_restrict_resultleft) = (K)) -> (exists dst_positive_code_inverse_restrict_resultleftlookup dst_positive_scale_inverse_restrict_resultleftlookup dst_negative_code_inverse_restrict_resultleftlookup dst_negative_scale_inverse_restrict_resultleftlookup dst_positive_inverse_restrict_resultleftlookup dst_negative_inverse_restrict_resultleftlookup. (((di_delta_inverse_restrict_result) = (((((dst_positive_code_inverse_restrict_resultleftlookup) + (dst_positive_scale_inverse_restrict_resultleftlookup)) * S ((dst_positive_code_inverse_restrict_resultleftlookup) + (dst_positive_scale_inverse_restrict_resultleftlookup)) + ((dst_positive_scale_inverse_restrict_resultleftlookup) + (dst_positive_scale_inverse_restrict_resultleftlookup))) + (((dst_negative_code_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)) * S ((dst_negative_code_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)) + ((dst_negative_scale_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)))) * S ((((dst_positive_code_inverse_restrict_resultleftlookup) + (dst_positive_scale_inverse_restrict_resultleftlookup)) * S ((dst_positive_code_inverse_restrict_resultleftlookup) + (dst_positive_scale_inverse_restrict_resultleftlookup)) + ((dst_positive_scale_inverse_restrict_resultleftlookup) + (dst_positive_scale_inverse_restrict_resultleftlookup))) + (((dst_negative_code_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)) * S ((dst_negative_code_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)) + ((dst_negative_scale_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)))) + ((((dst_negative_code_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)) * S ((dst_negative_code_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)) + ((dst_negative_scale_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup))) + (((dst_negative_code_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)) * S ((dst_negative_code_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)) + ((dst_negative_scale_inverse_restrict_resultleftlookup) + (dst_negative_scale_inverse_restrict_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftlookuppositive. ff_h_pvs_inverse_restrict_resultleftlookuppositive + S (dst_positive_inverse_restrict_resultleftlookup) = S ((S (dc_input_inverse_restrict_resultleft)) * dst_positive_scale_inverse_restrict_resultleftlookup)) /\ exists ff_q_pvs_inverse_restrict_resultleftlookuppositive. dst_positive_code_inverse_restrict_resultleftlookup = ff_q_pvs_inverse_restrict_resultleftlookuppositive * S ((S (dc_input_inverse_restrict_resultleft)) * dst_positive_scale_inverse_restrict_resultleftlookup) + (dst_positive_inverse_restrict_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftlookupnegative. ff_h_pvs_inverse_restrict_resultleftlookupnegative + S (dst_negative_inverse_restrict_resultleftlookup) = S ((S (dc_input_inverse_restrict_resultleft)) * dst_negative_scale_inverse_restrict_resultleftlookup)) /\ exists ff_q_pvs_inverse_restrict_resultleftlookupnegative. dst_negative_code_inverse_restrict_resultleftlookup = ff_q_pvs_inverse_restrict_resultleftlookupnegative * S ((S (dc_input_inverse_restrict_resultleft)) * dst_negative_scale_inverse_restrict_resultleftlookup) + (dst_negative_inverse_restrict_resultleftlookup))) /\ (exists ge_balance_positive_inverse_restrict_resultleftlookupvalue ge_balance_negative_inverse_restrict_resultleftlookupvalue. (((((dc_output_inverse_restrict_resultleft) = 2 * (ge_balance_positive_inverse_restrict_resultleftlookupvalue) /\ (ge_balance_negative_inverse_restrict_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftlookupvaluedecode. (((dc_output_inverse_restrict_resultleft) = 2 * ge_signed_half_inverse_restrict_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultleftlookupvalue) = S ge_signed_half_inverse_restrict_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_restrict_resultleftlookup) + ge_balance_negative_inverse_restrict_resultleftlookupvalue = (dst_negative_inverse_restrict_resultleftlookup) + ge_balance_positive_inverse_restrict_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_restrict_resultleft)=0)) /\ (exists dc_mask_inverse_restrict_resultleftvalue. ((((exists dst_positive_code_inverse_restrict_resultleftvaluemasktable dst_positive_scale_inverse_restrict_resultleftvaluemasktable dst_negative_code_inverse_restrict_resultleftvaluemasktable dst_negative_scale_inverse_restrict_resultleftvaluemasktable. (((dc_mask_inverse_restrict_resultleftvalue) = (((((dst_positive_code_inverse_restrict_resultleftvaluemasktable) + (dst_positive_scale_inverse_restrict_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_restrict_resultleftvaluemasktable) + (dst_positive_scale_inverse_restrict_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_restrict_resultleftvaluemasktable) + (dst_positive_scale_inverse_restrict_resultleftvaluemasktable))) + (((dst_negative_code_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_restrict_resultleftvaluemasktable) + (dst_positive_scale_inverse_restrict_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_restrict_resultleftvaluemasktable) + (dst_positive_scale_inverse_restrict_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_restrict_resultleftvaluemasktable) + (dst_positive_scale_inverse_restrict_resultleftvaluemasktable))) + (((dst_negative_code_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable))) + (((dst_negative_code_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemasktable) + (dst_negative_scale_inverse_restrict_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_restrict_resultleftvaluemasktable. (exists pvs_le_gap_inverse_restrict_resultleftvaluemasktabledomain. pvs_le_gap_inverse_restrict_resultleftvaluemasktabledomain + (dst_index_inverse_restrict_resultleftvaluemasktable) = (dc_input_inverse_restrict_resultleft)) -> exists dst_positive_inverse_restrict_resultleftvaluemasktable dst_negative_inverse_restrict_resultleftvaluemasktable dst_value_inverse_restrict_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_restrict_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_restrict_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_restrict_resultleftvaluemasktable) = S ((S (dst_index_inverse_restrict_resultleftvaluemasktable)) * dst_positive_scale_inverse_restrict_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_restrict_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_restrict_resultleftvaluemasktable = ff_q_pvs_inverse_restrict_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_restrict_resultleftvaluemasktable)) * dst_positive_scale_inverse_restrict_resultleftvaluemasktable) + (dst_positive_inverse_restrict_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_restrict_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_restrict_resultleftvaluemasktable) = S ((S (dst_index_inverse_restrict_resultleftvaluemasktable)) * dst_negative_scale_inverse_restrict_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_restrict_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_restrict_resultleftvaluemasktable = ff_q_pvs_inverse_restrict_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_restrict_resultleftvaluemasktable)) * dst_negative_scale_inverse_restrict_resultleftvaluemasktable) + (dst_negative_inverse_restrict_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_restrict_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_restrict_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_restrict_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_restrict_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_restrict_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_restrict_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_restrict_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_restrict_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultleftvaluemasktable) + ge_balance_negative_inverse_restrict_resultleftvaluemasktableentryvalue = (dst_negative_inverse_restrict_resultleftvaluemasktable) + ge_balance_positive_inverse_restrict_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_restrict_resultleftvaluemask dc_value_inverse_restrict_resultleftvaluemask. (exists pvs_le_gap_inverse_restrict_resultleftvaluemaskdomain. pvs_le_gap_inverse_restrict_resultleftvaluemaskdomain + (dc_index_inverse_restrict_resultleftvaluemask) = (dc_input_inverse_restrict_resultleft)) -> (exists dst_positive_code_inverse_restrict_resultleftvaluemasklookup dst_positive_scale_inverse_restrict_resultleftvaluemasklookup dst_negative_code_inverse_restrict_resultleftvaluemasklookup dst_negative_scale_inverse_restrict_resultleftvaluemasklookup dst_positive_inverse_restrict_resultleftvaluemasklookup dst_negative_inverse_restrict_resultleftvaluemasklookup. (((dc_mask_inverse_restrict_resultleftvalue) = (((((dst_positive_code_inverse_restrict_resultleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_restrict_resultleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_restrict_resultleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_restrict_resultleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_restrict_resultleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_restrict_resultleftvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_restrict_resultleftvaluemasklookuppositive + S (dst_positive_inverse_restrict_resultleftvaluemasklookup) = S ((S (dc_index_inverse_restrict_resultleftvaluemask)) * dst_positive_scale_inverse_restrict_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_restrict_resultleftvaluemasklookuppositive. dst_positive_code_inverse_restrict_resultleftvaluemasklookup = ff_q_pvs_inverse_restrict_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_restrict_resultleftvaluemask)) * dst_positive_scale_inverse_restrict_resultleftvaluemasklookup) + (dst_positive_inverse_restrict_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_restrict_resultleftvaluemasklookupnegative + S (dst_negative_inverse_restrict_resultleftvaluemasklookup) = S ((S (dc_index_inverse_restrict_resultleftvaluemask)) * dst_negative_scale_inverse_restrict_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_restrict_resultleftvaluemasklookupnegative. dst_negative_code_inverse_restrict_resultleftvaluemasklookup = ff_q_pvs_inverse_restrict_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_restrict_resultleftvaluemask)) * dst_negative_scale_inverse_restrict_resultleftvaluemasklookup) + (dst_negative_inverse_restrict_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_restrict_resultleftvaluemasklookupvalue ge_balance_negative_inverse_restrict_resultleftvaluemasklookupvalue. (((((dc_value_inverse_restrict_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_restrict_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_restrict_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_restrict_resultleftvaluemask) = 2 * ge_signed_half_inverse_restrict_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_restrict_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_restrict_resultleftvaluemasklookup) + ge_balance_negative_inverse_restrict_resultleftvaluemasklookupvalue = (dst_negative_inverse_restrict_resultleftvaluemasklookup) + ge_balance_positive_inverse_restrict_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_restrict_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_restrict_resultleftvaluemaskentry dc_left_inverse_restrict_resultleftvaluemaskentry dc_right_inverse_restrict_resultleftvaluemaskentry. (((dc_input_inverse_restrict_resultleft)=(dc_index_inverse_restrict_resultleftvaluemask)*dc_quotient_inverse_restrict_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_restrict_resultleftvaluemaskentryleft dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft dst_positive_inverse_restrict_resultleftvaluemaskentryleft dst_negative_inverse_restrict_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_restrict_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_restrict_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_restrict_resultleftvaluemask)) * dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_restrict_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_restrict_resultleftvaluemaskentryleft = ff_q_pvs_inverse_restrict_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_restrict_resultleftvaluemask)) * dst_positive_scale_inverse_restrict_resultleftvaluemaskentryleft) + (dst_positive_inverse_restrict_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_restrict_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_restrict_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_restrict_resultleftvaluemask)) * dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_restrict_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_restrict_resultleftvaluemaskentryleft = ff_q_pvs_inverse_restrict_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_restrict_resultleftvaluemask)) * dst_negative_scale_inverse_restrict_resultleftvaluemaskentryleft) + (dst_negative_inverse_restrict_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_restrict_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_restrict_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_restrict_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_restrict_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_restrict_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_restrict_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_restrict_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_restrict_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_restrict_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_restrict_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_restrict_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_resultleftvaluemaskentryright dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright dst_negative_code_inverse_restrict_resultleftvaluemaskentryright dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright dst_positive_inverse_restrict_resultleftvaluemaskentryright dst_negative_inverse_restrict_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_restrict_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_restrict_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_restrict_resultleftvaluemaskentry)) * dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_restrict_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_restrict_resultleftvaluemaskentryright = ff_q_pvs_inverse_restrict_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_restrict_resultleftvaluemaskentry)) * dst_positive_scale_inverse_restrict_resultleftvaluemaskentryright) + (dst_positive_inverse_restrict_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_restrict_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_restrict_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_restrict_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_restrict_resultleftvaluemaskentry)) * dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_restrict_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_restrict_resultleftvaluemaskentryright = ff_q_pvs_inverse_restrict_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_restrict_resultleftvaluemaskentry)) * dst_negative_scale_inverse_restrict_resultleftvaluemaskentryright) + (dst_negative_inverse_restrict_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_restrict_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_restrict_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_restrict_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_restrict_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_restrict_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_restrict_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_restrict_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_restrict_resultleftvaluemaskentryright) + ge_balance_negative_inverse_restrict_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_restrict_resultleftvaluemaskentryright) + ge_balance_positive_inverse_restrict_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_restrict_resultleftvaluemaskentryproduct sto_an_inverse_restrict_resultleftvaluemaskentryproduct sto_bp_inverse_restrict_resultleftvaluemaskentryproduct sto_bn_inverse_restrict_resultleftvaluemaskentryproduct sto_cp_inverse_restrict_resultleftvaluemaskentryproduct sto_cn_inverse_restrict_resultleftvaluemaskentryproduct. (((((dc_left_inverse_restrict_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_restrict_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_restrict_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductleft. (((dc_left_inverse_restrict_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_restrict_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_restrict_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_restrict_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_restrict_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_restrict_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductright. (((dc_right_inverse_restrict_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_restrict_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_restrict_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_restrict_resultleftvaluemask) = 2 * (sto_cp_inverse_restrict_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_restrict_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_restrict_resultleftvaluemask) = 2 * ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_restrict_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_restrict_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_restrict_resultleftvaluemaskentryproduct * sto_bp_inverse_restrict_resultleftvaluemaskentryproduct + sto_an_inverse_restrict_resultleftvaluemaskentryproduct * sto_bn_inverse_restrict_resultleftvaluemaskentryproduct) + sto_cn_inverse_restrict_resultleftvaluemaskentryproduct = (sto_ap_inverse_restrict_resultleftvaluemaskentryproduct * sto_bn_inverse_restrict_resultleftvaluemaskentryproduct + sto_an_inverse_restrict_resultleftvaluemaskentryproduct * sto_bp_inverse_restrict_resultleftvaluemaskentryproduct) + sto_cp_inverse_restrict_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_restrict_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_restrict_resultleftvaluemaskentrynondivisor. (dc_input_inverse_restrict_resultleft) = (dc_index_inverse_restrict_resultleftvaluemask) * pvs_factor_inverse_restrict_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_restrict_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_restrict_resultleftvaluefold dst_positive_scale_inverse_restrict_resultleftvaluefold dst_negative_code_inverse_restrict_resultleftvaluefold dst_negative_scale_inverse_restrict_resultleftvaluefold dst_positive_sum_inverse_restrict_resultleftvaluefold dst_negative_sum_inverse_restrict_resultleftvaluefold. (((dc_mask_inverse_restrict_resultleftvalue) = (((((dst_positive_code_inverse_restrict_resultleftvaluefold) + (dst_positive_scale_inverse_restrict_resultleftvaluefold)) * S ((dst_positive_code_inverse_restrict_resultleftvaluefold) + (dst_positive_scale_inverse_restrict_resultleftvaluefold)) + ((dst_positive_scale_inverse_restrict_resultleftvaluefold) + (dst_positive_scale_inverse_restrict_resultleftvaluefold))) + (((dst_negative_code_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)) * S ((dst_negative_code_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)) + ((dst_negative_scale_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_restrict_resultleftvaluefold) + (dst_positive_scale_inverse_restrict_resultleftvaluefold)) * S ((dst_positive_code_inverse_restrict_resultleftvaluefold) + (dst_positive_scale_inverse_restrict_resultleftvaluefold)) + ((dst_positive_scale_inverse_restrict_resultleftvaluefold) + (dst_positive_scale_inverse_restrict_resultleftvaluefold))) + (((dst_negative_code_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)) * S ((dst_negative_code_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)) + ((dst_negative_scale_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)))) + ((((dst_negative_code_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)) * S ((dst_negative_code_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)) + ((dst_negative_scale_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold))) + (((dst_negative_code_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)) * S ((dst_negative_code_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)) + ((dst_negative_scale_inverse_restrict_resultleftvaluefold) + (dst_negative_scale_inverse_restrict_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_restrict_resultleftvaluefoldpositive fs_v_dst_inverse_restrict_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_restrict_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_restrict_resultleftvaluefoldpositive = fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_restrict_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_restrict_resultleftvaluefold) = S ((S (S (dc_input_inverse_restrict_resultleft))) * fs_v_dst_inverse_restrict_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_restrict_resultleftvaluefoldpositive = fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_restrict_resultleft))) * fs_v_dst_inverse_restrict_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_restrict_resultleftvaluefold))) /\ forall fs_i_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_restrict_resultleft)) -> exists fs_a_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_restrict_resultleftvaluefold)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_restrict_resultleftvaluefold = fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_restrict_resultleftvaluefold) + (fs_a_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_restrict_resultleftvaluefoldpositive = fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_resultleftvaluefoldpositive) + (fs_r_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_restrict_resultleftvaluefoldpositive = fs_q_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_resultleftvaluefoldpositive) + (fs_s_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_restrict_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_restrict_resultleftvaluefoldnegative fs_v_dst_inverse_restrict_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_restrict_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_restrict_resultleftvaluefoldnegative = fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_restrict_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_restrict_resultleftvaluefold) = S ((S (S (dc_input_inverse_restrict_resultleft))) * fs_v_dst_inverse_restrict_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_restrict_resultleftvaluefoldnegative = fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_restrict_resultleft))) * fs_v_dst_inverse_restrict_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_restrict_resultleftvaluefold))) /\ forall fs_i_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_restrict_resultleft)) -> exists fs_a_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_restrict_resultleftvaluefold)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_restrict_resultleftvaluefold = fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_restrict_resultleftvaluefold) + (fs_a_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_restrict_resultleftvaluefoldnegative = fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_resultleftvaluefoldnegative) + (fs_r_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_restrict_resultleftvaluefoldnegative = fs_q_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_resultleftvaluefoldnegative) + (fs_s_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_restrict_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_restrict_resultleftvaluefoldresult ge_balance_negative_inverse_restrict_resultleftvaluefoldresult. (((((dc_output_inverse_restrict_resultleft) = 2 * (ge_balance_positive_inverse_restrict_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_restrict_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_restrict_resultleftvaluefoldresultdecode. (((dc_output_inverse_restrict_resultleft) = 2 * ge_signed_half_inverse_restrict_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_restrict_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_restrict_resultleftvaluefoldresult) = S ge_signed_half_inverse_restrict_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_restrict_resultleftvaluefold) + ge_balance_negative_inverse_restrict_resultleftvaluefoldresult = (dst_negative_sum_inverse_restrict_resultleftvaluefold) + ge_balance_positive_inverse_restrict_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_restrict_resultrightleft dst_positive_scale_inverse_restrict_resultrightleft dst_negative_code_inverse_restrict_resultrightleft dst_negative_scale_inverse_restrict_resultrightleft. (((G) = (((((dst_positive_code_inverse_restrict_resultrightleft) + (dst_positive_scale_inverse_restrict_resultrightleft)) * S ((dst_positive_code_inverse_restrict_resultrightleft) + (dst_positive_scale_inverse_restrict_resultrightleft)) + ((dst_positive_scale_inverse_restrict_resultrightleft) + (dst_positive_scale_inverse_restrict_resultrightleft))) + (((dst_negative_code_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)) * S ((dst_negative_code_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)) + ((dst_negative_scale_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)))) * S ((((dst_positive_code_inverse_restrict_resultrightleft) + (dst_positive_scale_inverse_restrict_resultrightleft)) * S ((dst_positive_code_inverse_restrict_resultrightleft) + (dst_positive_scale_inverse_restrict_resultrightleft)) + ((dst_positive_scale_inverse_restrict_resultrightleft) + (dst_positive_scale_inverse_restrict_resultrightleft))) + (((dst_negative_code_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)) * S ((dst_negative_code_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)) + ((dst_negative_scale_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)))) + ((((dst_negative_code_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)) * S ((dst_negative_code_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)) + ((dst_negative_scale_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft))) + (((dst_negative_code_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)) * S ((dst_negative_code_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)) + ((dst_negative_scale_inverse_restrict_resultrightleft) + (dst_negative_scale_inverse_restrict_resultrightleft)))))) /\ (forall dst_index_inverse_restrict_resultrightleft. (exists pvs_le_gap_inverse_restrict_resultrightleftdomain. pvs_le_gap_inverse_restrict_resultrightleftdomain + (dst_index_inverse_restrict_resultrightleft) = (K)) -> exists dst_positive_inverse_restrict_resultrightleft dst_negative_inverse_restrict_resultrightleft dst_value_inverse_restrict_resultrightleft. ((((exists ff_h_pvs_inverse_restrict_resultrightleftentrypositive. ff_h_pvs_inverse_restrict_resultrightleftentrypositive + S (dst_positive_inverse_restrict_resultrightleft) = S ((S (dst_index_inverse_restrict_resultrightleft)) * dst_positive_scale_inverse_restrict_resultrightleft)) /\ exists ff_q_pvs_inverse_restrict_resultrightleftentrypositive. dst_positive_code_inverse_restrict_resultrightleft = ff_q_pvs_inverse_restrict_resultrightleftentrypositive * S ((S (dst_index_inverse_restrict_resultrightleft)) * dst_positive_scale_inverse_restrict_resultrightleft) + (dst_positive_inverse_restrict_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightleftentrynegative. ff_h_pvs_inverse_restrict_resultrightleftentrynegative + S (dst_negative_inverse_restrict_resultrightleft) = S ((S (dst_index_inverse_restrict_resultrightleft)) * dst_negative_scale_inverse_restrict_resultrightleft)) /\ exists ff_q_pvs_inverse_restrict_resultrightleftentrynegative. dst_negative_code_inverse_restrict_resultrightleft = ff_q_pvs_inverse_restrict_resultrightleftentrynegative * S ((S (dst_index_inverse_restrict_resultrightleft)) * dst_negative_scale_inverse_restrict_resultrightleft) + (dst_negative_inverse_restrict_resultrightleft))) /\ (exists ge_balance_positive_inverse_restrict_resultrightleftentryvalue ge_balance_negative_inverse_restrict_resultrightleftentryvalue. (((((dst_value_inverse_restrict_resultrightleft) = 2 * (ge_balance_positive_inverse_restrict_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_restrict_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightleftentryvaluedecode. (((dst_value_inverse_restrict_resultrightleft) = 2 * ge_signed_half_inverse_restrict_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultrightleftentryvalue) = S ge_signed_half_inverse_restrict_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultrightleft) + ge_balance_negative_inverse_restrict_resultrightleftentryvalue = (dst_negative_inverse_restrict_resultrightleft) + ge_balance_positive_inverse_restrict_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_resultrightright dst_positive_scale_inverse_restrict_resultrightright dst_negative_code_inverse_restrict_resultrightright dst_negative_scale_inverse_restrict_resultrightright. (((F) = (((((dst_positive_code_inverse_restrict_resultrightright) + (dst_positive_scale_inverse_restrict_resultrightright)) * S ((dst_positive_code_inverse_restrict_resultrightright) + (dst_positive_scale_inverse_restrict_resultrightright)) + ((dst_positive_scale_inverse_restrict_resultrightright) + (dst_positive_scale_inverse_restrict_resultrightright))) + (((dst_negative_code_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)) * S ((dst_negative_code_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)) + ((dst_negative_scale_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)))) * S ((((dst_positive_code_inverse_restrict_resultrightright) + (dst_positive_scale_inverse_restrict_resultrightright)) * S ((dst_positive_code_inverse_restrict_resultrightright) + (dst_positive_scale_inverse_restrict_resultrightright)) + ((dst_positive_scale_inverse_restrict_resultrightright) + (dst_positive_scale_inverse_restrict_resultrightright))) + (((dst_negative_code_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)) * S ((dst_negative_code_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)) + ((dst_negative_scale_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)))) + ((((dst_negative_code_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)) * S ((dst_negative_code_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)) + ((dst_negative_scale_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright))) + (((dst_negative_code_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)) * S ((dst_negative_code_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)) + ((dst_negative_scale_inverse_restrict_resultrightright) + (dst_negative_scale_inverse_restrict_resultrightright)))))) /\ (forall dst_index_inverse_restrict_resultrightright. (exists pvs_le_gap_inverse_restrict_resultrightrightdomain. pvs_le_gap_inverse_restrict_resultrightrightdomain + (dst_index_inverse_restrict_resultrightright) = (K)) -> exists dst_positive_inverse_restrict_resultrightright dst_negative_inverse_restrict_resultrightright dst_value_inverse_restrict_resultrightright. ((((exists ff_h_pvs_inverse_restrict_resultrightrightentrypositive. ff_h_pvs_inverse_restrict_resultrightrightentrypositive + S (dst_positive_inverse_restrict_resultrightright) = S ((S (dst_index_inverse_restrict_resultrightright)) * dst_positive_scale_inverse_restrict_resultrightright)) /\ exists ff_q_pvs_inverse_restrict_resultrightrightentrypositive. dst_positive_code_inverse_restrict_resultrightright = ff_q_pvs_inverse_restrict_resultrightrightentrypositive * S ((S (dst_index_inverse_restrict_resultrightright)) * dst_positive_scale_inverse_restrict_resultrightright) + (dst_positive_inverse_restrict_resultrightright))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightrightentrynegative. ff_h_pvs_inverse_restrict_resultrightrightentrynegative + S (dst_negative_inverse_restrict_resultrightright) = S ((S (dst_index_inverse_restrict_resultrightright)) * dst_negative_scale_inverse_restrict_resultrightright)) /\ exists ff_q_pvs_inverse_restrict_resultrightrightentrynegative. dst_negative_code_inverse_restrict_resultrightright = ff_q_pvs_inverse_restrict_resultrightrightentrynegative * S ((S (dst_index_inverse_restrict_resultrightright)) * dst_negative_scale_inverse_restrict_resultrightright) + (dst_negative_inverse_restrict_resultrightright))) /\ (exists ge_balance_positive_inverse_restrict_resultrightrightentryvalue ge_balance_negative_inverse_restrict_resultrightrightentryvalue. (((((dst_value_inverse_restrict_resultrightright) = 2 * (ge_balance_positive_inverse_restrict_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_restrict_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightrightentryvaluedecode. (((dst_value_inverse_restrict_resultrightright) = 2 * ge_signed_half_inverse_restrict_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultrightrightentryvalue) = S ge_signed_half_inverse_restrict_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultrightright) + ge_balance_negative_inverse_restrict_resultrightrightentryvalue = (dst_negative_inverse_restrict_resultrightright) + ge_balance_positive_inverse_restrict_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_resultrighttable dst_positive_scale_inverse_restrict_resultrighttable dst_negative_code_inverse_restrict_resultrighttable dst_negative_scale_inverse_restrict_resultrighttable. (((di_delta_inverse_restrict_result) = (((((dst_positive_code_inverse_restrict_resultrighttable) + (dst_positive_scale_inverse_restrict_resultrighttable)) * S ((dst_positive_code_inverse_restrict_resultrighttable) + (dst_positive_scale_inverse_restrict_resultrighttable)) + ((dst_positive_scale_inverse_restrict_resultrighttable) + (dst_positive_scale_inverse_restrict_resultrighttable))) + (((dst_negative_code_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)) * S ((dst_negative_code_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)) + ((dst_negative_scale_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)))) * S ((((dst_positive_code_inverse_restrict_resultrighttable) + (dst_positive_scale_inverse_restrict_resultrighttable)) * S ((dst_positive_code_inverse_restrict_resultrighttable) + (dst_positive_scale_inverse_restrict_resultrighttable)) + ((dst_positive_scale_inverse_restrict_resultrighttable) + (dst_positive_scale_inverse_restrict_resultrighttable))) + (((dst_negative_code_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)) * S ((dst_negative_code_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)) + ((dst_negative_scale_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)))) + ((((dst_negative_code_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)) * S ((dst_negative_code_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)) + ((dst_negative_scale_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable))) + (((dst_negative_code_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)) * S ((dst_negative_code_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)) + ((dst_negative_scale_inverse_restrict_resultrighttable) + (dst_negative_scale_inverse_restrict_resultrighttable)))))) /\ (forall dst_index_inverse_restrict_resultrighttable. (exists pvs_le_gap_inverse_restrict_resultrighttabledomain. pvs_le_gap_inverse_restrict_resultrighttabledomain + (dst_index_inverse_restrict_resultrighttable) = (K)) -> exists dst_positive_inverse_restrict_resultrighttable dst_negative_inverse_restrict_resultrighttable dst_value_inverse_restrict_resultrighttable. ((((exists ff_h_pvs_inverse_restrict_resultrighttableentrypositive. ff_h_pvs_inverse_restrict_resultrighttableentrypositive + S (dst_positive_inverse_restrict_resultrighttable) = S ((S (dst_index_inverse_restrict_resultrighttable)) * dst_positive_scale_inverse_restrict_resultrighttable)) /\ exists ff_q_pvs_inverse_restrict_resultrighttableentrypositive. dst_positive_code_inverse_restrict_resultrighttable = ff_q_pvs_inverse_restrict_resultrighttableentrypositive * S ((S (dst_index_inverse_restrict_resultrighttable)) * dst_positive_scale_inverse_restrict_resultrighttable) + (dst_positive_inverse_restrict_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrighttableentrynegative. ff_h_pvs_inverse_restrict_resultrighttableentrynegative + S (dst_negative_inverse_restrict_resultrighttable) = S ((S (dst_index_inverse_restrict_resultrighttable)) * dst_negative_scale_inverse_restrict_resultrighttable)) /\ exists ff_q_pvs_inverse_restrict_resultrighttableentrynegative. dst_negative_code_inverse_restrict_resultrighttable = ff_q_pvs_inverse_restrict_resultrighttableentrynegative * S ((S (dst_index_inverse_restrict_resultrighttable)) * dst_negative_scale_inverse_restrict_resultrighttable) + (dst_negative_inverse_restrict_resultrighttable))) /\ (exists ge_balance_positive_inverse_restrict_resultrighttableentryvalue ge_balance_negative_inverse_restrict_resultrighttableentryvalue. (((((dst_value_inverse_restrict_resultrighttable) = 2 * (ge_balance_positive_inverse_restrict_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_restrict_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultrighttableentryvaluedecode. (((dst_value_inverse_restrict_resultrighttable) = 2 * ge_signed_half_inverse_restrict_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultrighttableentryvalue) = S ge_signed_half_inverse_restrict_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultrighttable) + ge_balance_negative_inverse_restrict_resultrighttableentryvalue = (dst_negative_inverse_restrict_resultrighttable) + ge_balance_positive_inverse_restrict_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_restrict_resultright dc_output_inverse_restrict_resultright. ~(dc_input_inverse_restrict_resultright=0) -> (exists pvs_le_gap_inverse_restrict_resultrightdomain. pvs_le_gap_inverse_restrict_resultrightdomain + (dc_input_inverse_restrict_resultright) = (K)) -> (exists dst_positive_code_inverse_restrict_resultrightlookup dst_positive_scale_inverse_restrict_resultrightlookup dst_negative_code_inverse_restrict_resultrightlookup dst_negative_scale_inverse_restrict_resultrightlookup dst_positive_inverse_restrict_resultrightlookup dst_negative_inverse_restrict_resultrightlookup. (((di_delta_inverse_restrict_result) = (((((dst_positive_code_inverse_restrict_resultrightlookup) + (dst_positive_scale_inverse_restrict_resultrightlookup)) * S ((dst_positive_code_inverse_restrict_resultrightlookup) + (dst_positive_scale_inverse_restrict_resultrightlookup)) + ((dst_positive_scale_inverse_restrict_resultrightlookup) + (dst_positive_scale_inverse_restrict_resultrightlookup))) + (((dst_negative_code_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)) * S ((dst_negative_code_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)) + ((dst_negative_scale_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)))) * S ((((dst_positive_code_inverse_restrict_resultrightlookup) + (dst_positive_scale_inverse_restrict_resultrightlookup)) * S ((dst_positive_code_inverse_restrict_resultrightlookup) + (dst_positive_scale_inverse_restrict_resultrightlookup)) + ((dst_positive_scale_inverse_restrict_resultrightlookup) + (dst_positive_scale_inverse_restrict_resultrightlookup))) + (((dst_negative_code_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)) * S ((dst_negative_code_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)) + ((dst_negative_scale_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)))) + ((((dst_negative_code_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)) * S ((dst_negative_code_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)) + ((dst_negative_scale_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup))) + (((dst_negative_code_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)) * S ((dst_negative_code_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)) + ((dst_negative_scale_inverse_restrict_resultrightlookup) + (dst_negative_scale_inverse_restrict_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightlookuppositive. ff_h_pvs_inverse_restrict_resultrightlookuppositive + S (dst_positive_inverse_restrict_resultrightlookup) = S ((S (dc_input_inverse_restrict_resultright)) * dst_positive_scale_inverse_restrict_resultrightlookup)) /\ exists ff_q_pvs_inverse_restrict_resultrightlookuppositive. dst_positive_code_inverse_restrict_resultrightlookup = ff_q_pvs_inverse_restrict_resultrightlookuppositive * S ((S (dc_input_inverse_restrict_resultright)) * dst_positive_scale_inverse_restrict_resultrightlookup) + (dst_positive_inverse_restrict_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightlookupnegative. ff_h_pvs_inverse_restrict_resultrightlookupnegative + S (dst_negative_inverse_restrict_resultrightlookup) = S ((S (dc_input_inverse_restrict_resultright)) * dst_negative_scale_inverse_restrict_resultrightlookup)) /\ exists ff_q_pvs_inverse_restrict_resultrightlookupnegative. dst_negative_code_inverse_restrict_resultrightlookup = ff_q_pvs_inverse_restrict_resultrightlookupnegative * S ((S (dc_input_inverse_restrict_resultright)) * dst_negative_scale_inverse_restrict_resultrightlookup) + (dst_negative_inverse_restrict_resultrightlookup))) /\ (exists ge_balance_positive_inverse_restrict_resultrightlookupvalue ge_balance_negative_inverse_restrict_resultrightlookupvalue. (((((dc_output_inverse_restrict_resultright) = 2 * (ge_balance_positive_inverse_restrict_resultrightlookupvalue) /\ (ge_balance_negative_inverse_restrict_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightlookupvaluedecode. (((dc_output_inverse_restrict_resultright) = 2 * ge_signed_half_inverse_restrict_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultrightlookupvalue) = S ge_signed_half_inverse_restrict_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_restrict_resultrightlookup) + ge_balance_negative_inverse_restrict_resultrightlookupvalue = (dst_negative_inverse_restrict_resultrightlookup) + ge_balance_positive_inverse_restrict_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_restrict_resultright)=0)) /\ (exists dc_mask_inverse_restrict_resultrightvalue. ((((exists dst_positive_code_inverse_restrict_resultrightvaluemasktable dst_positive_scale_inverse_restrict_resultrightvaluemasktable dst_negative_code_inverse_restrict_resultrightvaluemasktable dst_negative_scale_inverse_restrict_resultrightvaluemasktable. (((dc_mask_inverse_restrict_resultrightvalue) = (((((dst_positive_code_inverse_restrict_resultrightvaluemasktable) + (dst_positive_scale_inverse_restrict_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_restrict_resultrightvaluemasktable) + (dst_positive_scale_inverse_restrict_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_restrict_resultrightvaluemasktable) + (dst_positive_scale_inverse_restrict_resultrightvaluemasktable))) + (((dst_negative_code_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_restrict_resultrightvaluemasktable) + (dst_positive_scale_inverse_restrict_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_restrict_resultrightvaluemasktable) + (dst_positive_scale_inverse_restrict_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_restrict_resultrightvaluemasktable) + (dst_positive_scale_inverse_restrict_resultrightvaluemasktable))) + (((dst_negative_code_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable))) + (((dst_negative_code_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemasktable) + (dst_negative_scale_inverse_restrict_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_restrict_resultrightvaluemasktable. (exists pvs_le_gap_inverse_restrict_resultrightvaluemasktabledomain. pvs_le_gap_inverse_restrict_resultrightvaluemasktabledomain + (dst_index_inverse_restrict_resultrightvaluemasktable) = (dc_input_inverse_restrict_resultright)) -> exists dst_positive_inverse_restrict_resultrightvaluemasktable dst_negative_inverse_restrict_resultrightvaluemasktable dst_value_inverse_restrict_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_restrict_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_restrict_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_restrict_resultrightvaluemasktable) = S ((S (dst_index_inverse_restrict_resultrightvaluemasktable)) * dst_positive_scale_inverse_restrict_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_restrict_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_restrict_resultrightvaluemasktable = ff_q_pvs_inverse_restrict_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_restrict_resultrightvaluemasktable)) * dst_positive_scale_inverse_restrict_resultrightvaluemasktable) + (dst_positive_inverse_restrict_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_restrict_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_restrict_resultrightvaluemasktable) = S ((S (dst_index_inverse_restrict_resultrightvaluemasktable)) * dst_negative_scale_inverse_restrict_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_restrict_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_restrict_resultrightvaluemasktable = ff_q_pvs_inverse_restrict_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_restrict_resultrightvaluemasktable)) * dst_negative_scale_inverse_restrict_resultrightvaluemasktable) + (dst_negative_inverse_restrict_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_restrict_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_restrict_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_restrict_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_restrict_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_restrict_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_restrict_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_restrict_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_restrict_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_restrict_resultrightvaluemasktable) + ge_balance_negative_inverse_restrict_resultrightvaluemasktableentryvalue = (dst_negative_inverse_restrict_resultrightvaluemasktable) + ge_balance_positive_inverse_restrict_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_restrict_resultrightvaluemask dc_value_inverse_restrict_resultrightvaluemask. (exists pvs_le_gap_inverse_restrict_resultrightvaluemaskdomain. pvs_le_gap_inverse_restrict_resultrightvaluemaskdomain + (dc_index_inverse_restrict_resultrightvaluemask) = (dc_input_inverse_restrict_resultright)) -> (exists dst_positive_code_inverse_restrict_resultrightvaluemasklookup dst_positive_scale_inverse_restrict_resultrightvaluemasklookup dst_negative_code_inverse_restrict_resultrightvaluemasklookup dst_negative_scale_inverse_restrict_resultrightvaluemasklookup dst_positive_inverse_restrict_resultrightvaluemasklookup dst_negative_inverse_restrict_resultrightvaluemasklookup. (((dc_mask_inverse_restrict_resultrightvalue) = (((((dst_positive_code_inverse_restrict_resultrightvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_restrict_resultrightvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_restrict_resultrightvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_restrict_resultrightvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_restrict_resultrightvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_restrict_resultrightvaluemasklookup) + (dst_positive_scale_inverse_restrict_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_restrict_resultrightvaluemasklookuppositive + S (dst_positive_inverse_restrict_resultrightvaluemasklookup) = S ((S (dc_index_inverse_restrict_resultrightvaluemask)) * dst_positive_scale_inverse_restrict_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_restrict_resultrightvaluemasklookuppositive. dst_positive_code_inverse_restrict_resultrightvaluemasklookup = ff_q_pvs_inverse_restrict_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_restrict_resultrightvaluemask)) * dst_positive_scale_inverse_restrict_resultrightvaluemasklookup) + (dst_positive_inverse_restrict_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_restrict_resultrightvaluemasklookupnegative + S (dst_negative_inverse_restrict_resultrightvaluemasklookup) = S ((S (dc_index_inverse_restrict_resultrightvaluemask)) * dst_negative_scale_inverse_restrict_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_restrict_resultrightvaluemasklookupnegative. dst_negative_code_inverse_restrict_resultrightvaluemasklookup = ff_q_pvs_inverse_restrict_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_restrict_resultrightvaluemask)) * dst_negative_scale_inverse_restrict_resultrightvaluemasklookup) + (dst_negative_inverse_restrict_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_restrict_resultrightvaluemasklookupvalue ge_balance_negative_inverse_restrict_resultrightvaluemasklookupvalue. (((((dc_value_inverse_restrict_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_restrict_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_restrict_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_restrict_resultrightvaluemask) = 2 * ge_signed_half_inverse_restrict_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_restrict_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_restrict_resultrightvaluemasklookup) + ge_balance_negative_inverse_restrict_resultrightvaluemasklookupvalue = (dst_negative_inverse_restrict_resultrightvaluemasklookup) + ge_balance_positive_inverse_restrict_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_restrict_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_restrict_resultrightvaluemaskentry dc_left_inverse_restrict_resultrightvaluemaskentry dc_right_inverse_restrict_resultrightvaluemaskentry. (((dc_input_inverse_restrict_resultright)=(dc_index_inverse_restrict_resultrightvaluemask)*dc_quotient_inverse_restrict_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_restrict_resultrightvaluemaskentryleft dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft dst_positive_inverse_restrict_resultrightvaluemaskentryleft dst_negative_inverse_restrict_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_restrict_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_restrict_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_restrict_resultrightvaluemask)) * dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_restrict_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_restrict_resultrightvaluemaskentryleft = ff_q_pvs_inverse_restrict_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_restrict_resultrightvaluemask)) * dst_positive_scale_inverse_restrict_resultrightvaluemaskentryleft) + (dst_positive_inverse_restrict_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_restrict_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_restrict_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_restrict_resultrightvaluemask)) * dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_restrict_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_restrict_resultrightvaluemaskentryleft = ff_q_pvs_inverse_restrict_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_restrict_resultrightvaluemask)) * dst_negative_scale_inverse_restrict_resultrightvaluemaskentryleft) + (dst_negative_inverse_restrict_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_restrict_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_restrict_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_restrict_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_restrict_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_restrict_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_restrict_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_restrict_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_restrict_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_restrict_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_restrict_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_restrict_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_restrict_resultrightvaluemaskentryright dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright dst_negative_code_inverse_restrict_resultrightvaluemaskentryright dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright dst_positive_inverse_restrict_resultrightvaluemaskentryright dst_negative_inverse_restrict_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_restrict_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_restrict_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_restrict_resultrightvaluemaskentry)) * dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_restrict_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_restrict_resultrightvaluemaskentryright = ff_q_pvs_inverse_restrict_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_restrict_resultrightvaluemaskentry)) * dst_positive_scale_inverse_restrict_resultrightvaluemaskentryright) + (dst_positive_inverse_restrict_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_restrict_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_restrict_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_restrict_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_restrict_resultrightvaluemaskentry)) * dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_restrict_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_restrict_resultrightvaluemaskentryright = ff_q_pvs_inverse_restrict_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_restrict_resultrightvaluemaskentry)) * dst_negative_scale_inverse_restrict_resultrightvaluemaskentryright) + (dst_negative_inverse_restrict_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_restrict_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_restrict_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_restrict_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_restrict_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_restrict_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_restrict_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_restrict_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_restrict_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_restrict_resultrightvaluemaskentryright) + ge_balance_negative_inverse_restrict_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_restrict_resultrightvaluemaskentryright) + ge_balance_positive_inverse_restrict_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_restrict_resultrightvaluemaskentryproduct sto_an_inverse_restrict_resultrightvaluemaskentryproduct sto_bp_inverse_restrict_resultrightvaluemaskentryproduct sto_bn_inverse_restrict_resultrightvaluemaskentryproduct sto_cp_inverse_restrict_resultrightvaluemaskentryproduct sto_cn_inverse_restrict_resultrightvaluemaskentryproduct. (((((dc_left_inverse_restrict_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_restrict_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_restrict_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductleft. (((dc_left_inverse_restrict_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_restrict_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_restrict_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_restrict_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_restrict_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_restrict_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductright. (((dc_right_inverse_restrict_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_restrict_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_restrict_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_restrict_resultrightvaluemask) = 2 * (sto_cp_inverse_restrict_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_restrict_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_restrict_resultrightvaluemask) = 2 * ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_restrict_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_restrict_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_restrict_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_restrict_resultrightvaluemaskentryproduct * sto_bp_inverse_restrict_resultrightvaluemaskentryproduct + sto_an_inverse_restrict_resultrightvaluemaskentryproduct * sto_bn_inverse_restrict_resultrightvaluemaskentryproduct) + sto_cn_inverse_restrict_resultrightvaluemaskentryproduct = (sto_ap_inverse_restrict_resultrightvaluemaskentryproduct * sto_bn_inverse_restrict_resultrightvaluemaskentryproduct + sto_an_inverse_restrict_resultrightvaluemaskentryproduct * sto_bp_inverse_restrict_resultrightvaluemaskentryproduct) + sto_cp_inverse_restrict_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_restrict_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_restrict_resultrightvaluemaskentrynondivisor. (dc_input_inverse_restrict_resultright) = (dc_index_inverse_restrict_resultrightvaluemask) * pvs_factor_inverse_restrict_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_restrict_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_restrict_resultrightvaluefold dst_positive_scale_inverse_restrict_resultrightvaluefold dst_negative_code_inverse_restrict_resultrightvaluefold dst_negative_scale_inverse_restrict_resultrightvaluefold dst_positive_sum_inverse_restrict_resultrightvaluefold dst_negative_sum_inverse_restrict_resultrightvaluefold. (((dc_mask_inverse_restrict_resultrightvalue) = (((((dst_positive_code_inverse_restrict_resultrightvaluefold) + (dst_positive_scale_inverse_restrict_resultrightvaluefold)) * S ((dst_positive_code_inverse_restrict_resultrightvaluefold) + (dst_positive_scale_inverse_restrict_resultrightvaluefold)) + ((dst_positive_scale_inverse_restrict_resultrightvaluefold) + (dst_positive_scale_inverse_restrict_resultrightvaluefold))) + (((dst_negative_code_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)) * S ((dst_negative_code_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)) + ((dst_negative_scale_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_restrict_resultrightvaluefold) + (dst_positive_scale_inverse_restrict_resultrightvaluefold)) * S ((dst_positive_code_inverse_restrict_resultrightvaluefold) + (dst_positive_scale_inverse_restrict_resultrightvaluefold)) + ((dst_positive_scale_inverse_restrict_resultrightvaluefold) + (dst_positive_scale_inverse_restrict_resultrightvaluefold))) + (((dst_negative_code_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)) * S ((dst_negative_code_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)) + ((dst_negative_scale_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)))) + ((((dst_negative_code_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)) * S ((dst_negative_code_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)) + ((dst_negative_scale_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold))) + (((dst_negative_code_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)) * S ((dst_negative_code_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)) + ((dst_negative_scale_inverse_restrict_resultrightvaluefold) + (dst_negative_scale_inverse_restrict_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_restrict_resultrightvaluefoldpositive fs_v_dst_inverse_restrict_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_restrict_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_restrict_resultrightvaluefoldpositive = fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_restrict_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_restrict_resultrightvaluefold) = S ((S (S (dc_input_inverse_restrict_resultright))) * fs_v_dst_inverse_restrict_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_restrict_resultrightvaluefoldpositive = fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_restrict_resultright))) * fs_v_dst_inverse_restrict_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_restrict_resultrightvaluefold))) /\ forall fs_i_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_restrict_resultright)) -> exists fs_a_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_restrict_resultrightvaluefold)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_restrict_resultrightvaluefold = fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_restrict_resultrightvaluefold) + (fs_a_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_restrict_resultrightvaluefoldpositive = fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_resultrightvaluefoldpositive) + (fs_r_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_restrict_resultrightvaluefoldpositive = fs_q_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_restrict_resultrightvaluefoldpositive) + (fs_s_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_restrict_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_restrict_resultrightvaluefoldnegative fs_v_dst_inverse_restrict_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_restrict_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_restrict_resultrightvaluefoldnegative = fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_restrict_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_restrict_resultrightvaluefold) = S ((S (S (dc_input_inverse_restrict_resultright))) * fs_v_dst_inverse_restrict_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_restrict_resultrightvaluefoldnegative = fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_restrict_resultright))) * fs_v_dst_inverse_restrict_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_restrict_resultrightvaluefold))) /\ forall fs_i_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_restrict_resultright)) -> exists fs_a_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_restrict_resultrightvaluefold)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_restrict_resultrightvaluefold = fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_restrict_resultrightvaluefold) + (fs_a_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_restrict_resultrightvaluefoldnegative = fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_resultrightvaluefoldnegative) + (fs_r_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_restrict_resultrightvaluefoldnegative = fs_q_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_restrict_resultrightvaluefoldnegative) + (fs_s_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_restrict_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_restrict_resultrightvaluefoldresult ge_balance_negative_inverse_restrict_resultrightvaluefoldresult. (((((dc_output_inverse_restrict_resultright) = 2 * (ge_balance_positive_inverse_restrict_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_restrict_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_restrict_resultrightvaluefoldresultdecode. (((dc_output_inverse_restrict_resultright) = 2 * ge_signed_half_inverse_restrict_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_restrict_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_restrict_resultrightvaluefoldresult) = S ge_signed_half_inverse_restrict_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_restrict_resultrightvaluefold) + ge_balance_negative_inverse_restrict_resultrightvaluefoldresult = (dst_negative_sum_inverse_restrict_resultrightvaluefold) + ge_balance_positive_inverse_restrict_resultrightvaluefoldresult))))))))))))))))))))))))Complete tactic proof in conservative notation
All 34 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
34 script commands · 8 reading checkpoints · 0 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 (1)
01Fix variables and assumptionsL1–6
02Separate the logical casesL7–9
03Construct an explicit witnessL10–10
Supply the displayed value, then prove that it has the required property.
- L10
exists x
04Separate the logical casesL11–11
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L11
split
05Use earlier factsL12–17
Instantiate or apply named facts and discharge the corresponding proof obligations.
06Separate the logical casesL18–18
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L18
split
07Use earlier factsL19–28
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L19
specialize dirichlet_convolution_table_restrict (N) - L20
specialize dirichlet_convolution_table_restrict (K) - L21
specialize dirichlet_convolution_table_restrict (F) - L22
specialize dirichlet_convolution_table_restrict (G) - L23
specialize dirichlet_convolution_table_restrict (x) - L24
apply dirichlet_convolution_table_restrict - L25
exact hi_witness_right_left - L26
exact hb - L27
specialize dirichlet_convolution_table_restrict (N) - L28
specialize dirichlet_convolution_table_restrict (K)
08Use earlier factsL29–34
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original defined command ledger · 34 lines
- 0001
intro N - 0002
intro K - 0003
intro F - 0004
intro G - 0005
intro hi - 0006
intro hb - 0007
cases hi - 0008
cases hi_witness - 0009
cases hi_witness_right - 0010
exists x - 0011
split - 0012
specialize dirichlet_kronecker_delta_table_restrict (N) - 0013
specialize dirichlet_kronecker_delta_table_restrict (K) - 0014
specialize dirichlet_kronecker_delta_table_restrict (x) - 0015
apply dirichlet_kronecker_delta_table_restrict - 0016
exact hi_witness_left - 0017
exact hb - 0018
split - 0019
specialize dirichlet_convolution_table_restrict (N) - 0020
specialize dirichlet_convolution_table_restrict (K) - 0021
specialize dirichlet_convolution_table_restrict (F) - 0022
specialize dirichlet_convolution_table_restrict (G) - 0023
specialize dirichlet_convolution_table_restrict (x) - 0024
apply dirichlet_convolution_table_restrict - 0025
exact hi_witness_right_left - 0026
exact hb - 0027
specialize dirichlet_convolution_table_restrict (N) - 0028
specialize dirichlet_convolution_table_restrict (K) - 0029
specialize dirichlet_convolution_table_restrict (G) - 0030
specialize dirichlet_convolution_table_restrict (F) - 0031
specialize dirichlet_convolution_table_restrict (x) - 0032
apply dirichlet_convolution_table_restrict - 0033
exact hi_witness_right_right - 0034
exact hb