Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
For an actual table an inverse exists exactly when N=0 or F(1) is signed +1 or -1. At a positive window this is the unit-at-one criterion; the empty window imposes no condition at one. Every inverse has actual delta and two-sided convolution witnesses. Its zeroth value is arbitrary, so uniqueness is positive-value equality, not equality of codes or of zeroth values. Multiplicative-function closure and full finite signed G009 are admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ u. ∀ w. ArithTable(N,F) → ArithAt(F,1,u) → SignedUnit(u) → ∃ x. DirichletInverse(N,F,x) ∧ ArithAt(x,0,w)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall N F u w. (exists dst_positive_code_inverse_unit_input dst_positive_scale_inverse_unit_input dst_negative_code_inverse_unit_input dst_negative_scale_inverse_unit_input. (((F) = (((((dst_positive_code_inverse_unit_input) + (dst_positive_scale_inverse_unit_input)) * S ((dst_positive_code_inverse_unit_input) + (dst_positive_scale_inverse_unit_input)) + ((dst_positive_scale_inverse_unit_input) + (dst_positive_scale_inverse_unit_input))) + (((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) * S ((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) + ((dst_negative_scale_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)))) * S ((((dst_positive_code_inverse_unit_input) + (dst_positive_scale_inverse_unit_input)) * S ((dst_positive_code_inverse_unit_input) + (dst_positive_scale_inverse_unit_input)) + ((dst_positive_scale_inverse_unit_input) + (dst_positive_scale_inverse_unit_input))) + (((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) * S ((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) + ((dst_negative_scale_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)))) + ((((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) * S ((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) + ((dst_negative_scale_inverse_unit_input) + (dst_negative_scale_inverse_unit_input))) + (((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) * S ((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) + ((dst_negative_scale_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)))))) /\ (forall dst_index_inverse_unit_input. (exists pvs_le_gap_inverse_unit_inputdomain. pvs_le_gap_inverse_unit_inputdomain + (dst_index_inverse_unit_input) = (N)) -> exists dst_positive_inverse_unit_input dst_negative_inverse_unit_input dst_value_inverse_unit_input. ((((exists ff_h_pvs_inverse_unit_inputentrypositive. ff_h_pvs_inverse_unit_inputentrypositive + S (dst_positive_inverse_unit_input) = S ((S (dst_index_inverse_unit_input)) * dst_positive_scale_inverse_unit_input)) /\ exists ff_q_pvs_inverse_unit_inputentrypositive. dst_positive_code_inverse_unit_input = ff_q_pvs_inverse_unit_inputentrypositive * S ((S (dst_index_inverse_unit_input)) * dst_positive_scale_inverse_unit_input) + (dst_positive_inverse_unit_input))) /\ (((((exists ff_h_pvs_inverse_unit_inputentrynegative. ff_h_pvs_inverse_unit_inputentrynegative + S (dst_negative_inverse_unit_input) = S ((S (dst_index_inverse_unit_input)) * dst_negative_scale_inverse_unit_input)) /\ exists ff_q_pvs_inverse_unit_inputentrynegative. dst_negative_code_inverse_unit_input = ff_q_pvs_inverse_unit_inputentrynegative * S ((S (dst_index_inverse_unit_input)) * dst_negative_scale_inverse_unit_input) + (dst_negative_inverse_unit_input))) /\ (exists ge_balance_positive_inverse_unit_inputentryvalue ge_balance_negative_inverse_unit_inputentryvalue. (((((dst_value_inverse_unit_input) = 2 * (ge_balance_positive_inverse_unit_inputentryvalue) /\ (ge_balance_negative_inverse_unit_inputentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_inputentryvaluedecode. (((dst_value_inverse_unit_input) = 2 * ge_signed_half_inverse_unit_inputentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_inputentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_inputentryvalue) = S ge_signed_half_inverse_unit_inputentryvaluedecode))) /\ ((dst_positive_inverse_unit_input) + ge_balance_negative_inverse_unit_inputentryvalue = (dst_negative_inverse_unit_input) + ge_balance_positive_inverse_unit_inputentryvalue))))))))) -> (exists dst_positive_code_inverse_unit_entry dst_positive_scale_inverse_unit_entry dst_negative_code_inverse_unit_entry dst_negative_scale_inverse_unit_entry dst_positive_inverse_unit_entry dst_negative_inverse_unit_entry. (((F) = (((((dst_positive_code_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry)) * S ((dst_positive_code_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry)) + ((dst_positive_scale_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry))) + (((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) * S ((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) + ((dst_negative_scale_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)))) * S ((((dst_positive_code_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry)) * S ((dst_positive_code_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry)) + ((dst_positive_scale_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry))) + (((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) * S ((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) + ((dst_negative_scale_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)))) + ((((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) * S ((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) + ((dst_negative_scale_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry))) + (((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) * S ((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) + ((dst_negative_scale_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)))))) /\ (((((exists ff_h_pvs_inverse_unit_entrypositive. ff_h_pvs_inverse_unit_entrypositive + S (dst_positive_inverse_unit_entry) = S ((S (1)) * dst_positive_scale_inverse_unit_entry)) /\ exists ff_q_pvs_inverse_unit_entrypositive. dst_positive_code_inverse_unit_entry = ff_q_pvs_inverse_unit_entrypositive * S ((S (1)) * dst_positive_scale_inverse_unit_entry) + (dst_positive_inverse_unit_entry))) /\ (((((exists ff_h_pvs_inverse_unit_entrynegative. ff_h_pvs_inverse_unit_entrynegative + S (dst_negative_inverse_unit_entry) = S ((S (1)) * dst_negative_scale_inverse_unit_entry)) /\ exists ff_q_pvs_inverse_unit_entrynegative. dst_negative_code_inverse_unit_entry = ff_q_pvs_inverse_unit_entrynegative * S ((S (1)) * dst_negative_scale_inverse_unit_entry) + (dst_negative_inverse_unit_entry))) /\ (exists ge_balance_positive_inverse_unit_entryvalue ge_balance_negative_inverse_unit_entryvalue. (((((u) = 2 * (ge_balance_positive_inverse_unit_entryvalue) /\ (ge_balance_negative_inverse_unit_entryvalue) = 0) \/ exists ge_signed_half_inverse_unit_entryvaluedecode. (((u) = 2 * ge_signed_half_inverse_unit_entryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_entryvalue) = 0) /\ (ge_balance_negative_inverse_unit_entryvalue) = S ge_signed_half_inverse_unit_entryvaluedecode))) /\ ((dst_positive_inverse_unit_entry) + ge_balance_negative_inverse_unit_entryvalue = (dst_negative_inverse_unit_entry) + ge_balance_positive_inverse_unit_entryvalue))))))))) -> (((u) = 2 \/ (u) = 1)) -> exists G. ((exists di_delta_inverse_unit_result. ((((exists dst_positive_code_inverse_unit_resultdeltatable dst_positive_scale_inverse_unit_resultdeltatable dst_negative_code_inverse_unit_resultdeltatable dst_negative_scale_inverse_unit_resultdeltatable. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable)) * S ((dst_positive_code_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable)) + ((dst_positive_scale_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable))) + (((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) * S ((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) + ((dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)))) * S ((((dst_positive_code_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable)) * S ((dst_positive_code_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable)) + ((dst_positive_scale_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable))) + (((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) * S ((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) + ((dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)))) + ((((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) * S ((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) + ((dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable))) + (((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) * S ((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) + ((dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)))))) /\ (forall dst_index_inverse_unit_resultdeltatable. (exists pvs_le_gap_inverse_unit_resultdeltatabledomain. pvs_le_gap_inverse_unit_resultdeltatabledomain + (dst_index_inverse_unit_resultdeltatable) = (N)) -> exists dst_positive_inverse_unit_resultdeltatable dst_negative_inverse_unit_resultdeltatable dst_value_inverse_unit_resultdeltatable. ((((exists ff_h_pvs_inverse_unit_resultdeltatableentrypositive. ff_h_pvs_inverse_unit_resultdeltatableentrypositive + S (dst_positive_inverse_unit_resultdeltatable) = S ((S (dst_index_inverse_unit_resultdeltatable)) * dst_positive_scale_inverse_unit_resultdeltatable)) /\ exists ff_q_pvs_inverse_unit_resultdeltatableentrypositive. dst_positive_code_inverse_unit_resultdeltatable = ff_q_pvs_inverse_unit_resultdeltatableentrypositive * S ((S (dst_index_inverse_unit_resultdeltatable)) * dst_positive_scale_inverse_unit_resultdeltatable) + (dst_positive_inverse_unit_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_unit_resultdeltatableentrynegative. ff_h_pvs_inverse_unit_resultdeltatableentrynegative + S (dst_negative_inverse_unit_resultdeltatable) = S ((S (dst_index_inverse_unit_resultdeltatable)) * dst_negative_scale_inverse_unit_resultdeltatable)) /\ exists ff_q_pvs_inverse_unit_resultdeltatableentrynegative. dst_negative_code_inverse_unit_resultdeltatable = ff_q_pvs_inverse_unit_resultdeltatableentrynegative * S ((S (dst_index_inverse_unit_resultdeltatable)) * dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_inverse_unit_resultdeltatable))) /\ (exists ge_balance_positive_inverse_unit_resultdeltatableentryvalue ge_balance_negative_inverse_unit_resultdeltatableentryvalue. (((((dst_value_inverse_unit_resultdeltatable) = 2 * (ge_balance_positive_inverse_unit_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_unit_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultdeltatableentryvaluedecode. (((dst_value_inverse_unit_resultdeltatable) = 2 * ge_signed_half_inverse_unit_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultdeltatableentryvalue) = S ge_signed_half_inverse_unit_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultdeltatable) + ge_balance_negative_inverse_unit_resultdeltatableentryvalue = (dst_negative_inverse_unit_resultdeltatable) + ge_balance_positive_inverse_unit_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_unit_resultdelta du_value_inverse_unit_resultdelta. ~(du_index_inverse_unit_resultdelta=0) -> (exists pvs_le_gap_inverse_unit_resultdeltabound. pvs_le_gap_inverse_unit_resultdeltabound + (du_index_inverse_unit_resultdelta) = (N)) -> (exists dst_positive_code_inverse_unit_resultdeltaentry dst_positive_scale_inverse_unit_resultdeltaentry dst_negative_code_inverse_unit_resultdeltaentry dst_negative_scale_inverse_unit_resultdeltaentry dst_positive_inverse_unit_resultdeltaentry dst_negative_inverse_unit_resultdeltaentry. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry)) * S ((dst_positive_code_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry)) + ((dst_positive_scale_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry))) + (((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) * S ((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) + ((dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)))) * S ((((dst_positive_code_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry)) * S ((dst_positive_code_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry)) + ((dst_positive_scale_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry))) + (((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) * S ((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) + ((dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)))) + ((((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) * S ((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) + ((dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry))) + (((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) * S ((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) + ((dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultdeltaentrypositive. ff_h_pvs_inverse_unit_resultdeltaentrypositive + S (dst_positive_inverse_unit_resultdeltaentry) = S ((S (du_index_inverse_unit_resultdelta)) * dst_positive_scale_inverse_unit_resultdeltaentry)) /\ exists ff_q_pvs_inverse_unit_resultdeltaentrypositive. dst_positive_code_inverse_unit_resultdeltaentry = ff_q_pvs_inverse_unit_resultdeltaentrypositive * S ((S (du_index_inverse_unit_resultdelta)) * dst_positive_scale_inverse_unit_resultdeltaentry) + (dst_positive_inverse_unit_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_unit_resultdeltaentrynegative. ff_h_pvs_inverse_unit_resultdeltaentrynegative + S (dst_negative_inverse_unit_resultdeltaentry) = S ((S (du_index_inverse_unit_resultdelta)) * dst_negative_scale_inverse_unit_resultdeltaentry)) /\ exists ff_q_pvs_inverse_unit_resultdeltaentrynegative. dst_negative_code_inverse_unit_resultdeltaentry = ff_q_pvs_inverse_unit_resultdeltaentrynegative * S ((S (du_index_inverse_unit_resultdelta)) * dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_inverse_unit_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_unit_resultdeltaentryvalue ge_balance_negative_inverse_unit_resultdeltaentryvalue. (((((du_value_inverse_unit_resultdelta) = 2 * (ge_balance_positive_inverse_unit_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_unit_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultdeltaentryvaluedecode. (((du_value_inverse_unit_resultdelta) = 2 * ge_signed_half_inverse_unit_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultdeltaentryvalue) = S ge_signed_half_inverse_unit_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultdeltaentry) + ge_balance_negative_inverse_unit_resultdeltaentryvalue = (dst_negative_inverse_unit_resultdeltaentry) + ge_balance_positive_inverse_unit_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_unit_resultdelta)=1 -> (du_value_inverse_unit_resultdelta)=2) /\ (~((du_index_inverse_unit_resultdelta)=1) -> (du_value_inverse_unit_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_unit_resultleftleft dst_positive_scale_inverse_unit_resultleftleft dst_negative_code_inverse_unit_resultleftleft dst_negative_scale_inverse_unit_resultleftleft. (((F) = (((((dst_positive_code_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft)) * S ((dst_positive_code_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft)) + ((dst_positive_scale_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft))) + (((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) * S ((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) + ((dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)))) * S ((((dst_positive_code_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft)) * S ((dst_positive_code_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft)) + ((dst_positive_scale_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft))) + (((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) * S ((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) + ((dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)))) + ((((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) * S ((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) + ((dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft))) + (((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) * S ((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) + ((dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)))))) /\ (forall dst_index_inverse_unit_resultleftleft. (exists pvs_le_gap_inverse_unit_resultleftleftdomain. pvs_le_gap_inverse_unit_resultleftleftdomain + (dst_index_inverse_unit_resultleftleft) = (N)) -> exists dst_positive_inverse_unit_resultleftleft dst_negative_inverse_unit_resultleftleft dst_value_inverse_unit_resultleftleft. ((((exists ff_h_pvs_inverse_unit_resultleftleftentrypositive. ff_h_pvs_inverse_unit_resultleftleftentrypositive + S (dst_positive_inverse_unit_resultleftleft) = S ((S (dst_index_inverse_unit_resultleftleft)) * dst_positive_scale_inverse_unit_resultleftleft)) /\ exists ff_q_pvs_inverse_unit_resultleftleftentrypositive. dst_positive_code_inverse_unit_resultleftleft = ff_q_pvs_inverse_unit_resultleftleftentrypositive * S ((S (dst_index_inverse_unit_resultleftleft)) * dst_positive_scale_inverse_unit_resultleftleft) + (dst_positive_inverse_unit_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftleftentrynegative. ff_h_pvs_inverse_unit_resultleftleftentrynegative + S (dst_negative_inverse_unit_resultleftleft) = S ((S (dst_index_inverse_unit_resultleftleft)) * dst_negative_scale_inverse_unit_resultleftleft)) /\ exists ff_q_pvs_inverse_unit_resultleftleftentrynegative. dst_negative_code_inverse_unit_resultleftleft = ff_q_pvs_inverse_unit_resultleftleftentrynegative * S ((S (dst_index_inverse_unit_resultleftleft)) * dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_inverse_unit_resultleftleft))) /\ (exists ge_balance_positive_inverse_unit_resultleftleftentryvalue ge_balance_negative_inverse_unit_resultleftleftentryvalue. (((((dst_value_inverse_unit_resultleftleft) = 2 * (ge_balance_positive_inverse_unit_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_unit_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftleftentryvaluedecode. (((dst_value_inverse_unit_resultleftleft) = 2 * ge_signed_half_inverse_unit_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftleftentryvalue) = S ge_signed_half_inverse_unit_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftleft) + ge_balance_negative_inverse_unit_resultleftleftentryvalue = (dst_negative_inverse_unit_resultleftleft) + ge_balance_positive_inverse_unit_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultleftright dst_positive_scale_inverse_unit_resultleftright dst_negative_code_inverse_unit_resultleftright dst_negative_scale_inverse_unit_resultleftright. (((G) = (((((dst_positive_code_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright)) * S ((dst_positive_code_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright)) + ((dst_positive_scale_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright))) + (((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) * S ((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) + ((dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)))) * S ((((dst_positive_code_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright)) * S ((dst_positive_code_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright)) + ((dst_positive_scale_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright))) + (((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) * S ((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) + ((dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)))) + ((((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) * S ((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) + ((dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright))) + (((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) * S ((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) + ((dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)))))) /\ (forall dst_index_inverse_unit_resultleftright. (exists pvs_le_gap_inverse_unit_resultleftrightdomain. pvs_le_gap_inverse_unit_resultleftrightdomain + (dst_index_inverse_unit_resultleftright) = (N)) -> exists dst_positive_inverse_unit_resultleftright dst_negative_inverse_unit_resultleftright dst_value_inverse_unit_resultleftright. ((((exists ff_h_pvs_inverse_unit_resultleftrightentrypositive. ff_h_pvs_inverse_unit_resultleftrightentrypositive + S (dst_positive_inverse_unit_resultleftright) = S ((S (dst_index_inverse_unit_resultleftright)) * dst_positive_scale_inverse_unit_resultleftright)) /\ exists ff_q_pvs_inverse_unit_resultleftrightentrypositive. dst_positive_code_inverse_unit_resultleftright = ff_q_pvs_inverse_unit_resultleftrightentrypositive * S ((S (dst_index_inverse_unit_resultleftright)) * dst_positive_scale_inverse_unit_resultleftright) + (dst_positive_inverse_unit_resultleftright))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftrightentrynegative. ff_h_pvs_inverse_unit_resultleftrightentrynegative + S (dst_negative_inverse_unit_resultleftright) = S ((S (dst_index_inverse_unit_resultleftright)) * dst_negative_scale_inverse_unit_resultleftright)) /\ exists ff_q_pvs_inverse_unit_resultleftrightentrynegative. dst_negative_code_inverse_unit_resultleftright = ff_q_pvs_inverse_unit_resultleftrightentrynegative * S ((S (dst_index_inverse_unit_resultleftright)) * dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_inverse_unit_resultleftright))) /\ (exists ge_balance_positive_inverse_unit_resultleftrightentryvalue ge_balance_negative_inverse_unit_resultleftrightentryvalue. (((((dst_value_inverse_unit_resultleftright) = 2 * (ge_balance_positive_inverse_unit_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_unit_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftrightentryvaluedecode. (((dst_value_inverse_unit_resultleftright) = 2 * ge_signed_half_inverse_unit_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftrightentryvalue) = S ge_signed_half_inverse_unit_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftright) + ge_balance_negative_inverse_unit_resultleftrightentryvalue = (dst_negative_inverse_unit_resultleftright) + ge_balance_positive_inverse_unit_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultlefttable dst_positive_scale_inverse_unit_resultlefttable dst_negative_code_inverse_unit_resultlefttable dst_negative_scale_inverse_unit_resultlefttable. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable)) * S ((dst_positive_code_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable)) + ((dst_positive_scale_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable))) + (((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) * S ((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) + ((dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)))) * S ((((dst_positive_code_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable)) * S ((dst_positive_code_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable)) + ((dst_positive_scale_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable))) + (((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) * S ((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) + ((dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)))) + ((((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) * S ((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) + ((dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable))) + (((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) * S ((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) + ((dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)))))) /\ (forall dst_index_inverse_unit_resultlefttable. (exists pvs_le_gap_inverse_unit_resultlefttabledomain. pvs_le_gap_inverse_unit_resultlefttabledomain + (dst_index_inverse_unit_resultlefttable) = (N)) -> exists dst_positive_inverse_unit_resultlefttable dst_negative_inverse_unit_resultlefttable dst_value_inverse_unit_resultlefttable. ((((exists ff_h_pvs_inverse_unit_resultlefttableentrypositive. ff_h_pvs_inverse_unit_resultlefttableentrypositive + S (dst_positive_inverse_unit_resultlefttable) = S ((S (dst_index_inverse_unit_resultlefttable)) * dst_positive_scale_inverse_unit_resultlefttable)) /\ exists ff_q_pvs_inverse_unit_resultlefttableentrypositive. dst_positive_code_inverse_unit_resultlefttable = ff_q_pvs_inverse_unit_resultlefttableentrypositive * S ((S (dst_index_inverse_unit_resultlefttable)) * dst_positive_scale_inverse_unit_resultlefttable) + (dst_positive_inverse_unit_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_unit_resultlefttableentrynegative. ff_h_pvs_inverse_unit_resultlefttableentrynegative + S (dst_negative_inverse_unit_resultlefttable) = S ((S (dst_index_inverse_unit_resultlefttable)) * dst_negative_scale_inverse_unit_resultlefttable)) /\ exists ff_q_pvs_inverse_unit_resultlefttableentrynegative. dst_negative_code_inverse_unit_resultlefttable = ff_q_pvs_inverse_unit_resultlefttableentrynegative * S ((S (dst_index_inverse_unit_resultlefttable)) * dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_inverse_unit_resultlefttable))) /\ (exists ge_balance_positive_inverse_unit_resultlefttableentryvalue ge_balance_negative_inverse_unit_resultlefttableentryvalue. (((((dst_value_inverse_unit_resultlefttable) = 2 * (ge_balance_positive_inverse_unit_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_unit_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultlefttableentryvaluedecode. (((dst_value_inverse_unit_resultlefttable) = 2 * ge_signed_half_inverse_unit_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultlefttableentryvalue) = S ge_signed_half_inverse_unit_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultlefttable) + ge_balance_negative_inverse_unit_resultlefttableentryvalue = (dst_negative_inverse_unit_resultlefttable) + ge_balance_positive_inverse_unit_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_unit_resultleft dc_output_inverse_unit_resultleft. ~(dc_input_inverse_unit_resultleft=0) -> (exists pvs_le_gap_inverse_unit_resultleftdomain. pvs_le_gap_inverse_unit_resultleftdomain + (dc_input_inverse_unit_resultleft) = (N)) -> (exists dst_positive_code_inverse_unit_resultleftlookup dst_positive_scale_inverse_unit_resultleftlookup dst_negative_code_inverse_unit_resultleftlookup dst_negative_scale_inverse_unit_resultleftlookup dst_positive_inverse_unit_resultleftlookup dst_negative_inverse_unit_resultleftlookup. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup)) * S ((dst_positive_code_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup)) + ((dst_positive_scale_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup))) + (((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) * S ((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) + ((dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)))) * S ((((dst_positive_code_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup)) * S ((dst_positive_code_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup)) + ((dst_positive_scale_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup))) + (((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) * S ((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) + ((dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)))) + ((((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) * S ((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) + ((dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup))) + (((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) * S ((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) + ((dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftlookuppositive. ff_h_pvs_inverse_unit_resultleftlookuppositive + S (dst_positive_inverse_unit_resultleftlookup) = S ((S (dc_input_inverse_unit_resultleft)) * dst_positive_scale_inverse_unit_resultleftlookup)) /\ exists ff_q_pvs_inverse_unit_resultleftlookuppositive. dst_positive_code_inverse_unit_resultleftlookup = ff_q_pvs_inverse_unit_resultleftlookuppositive * S ((S (dc_input_inverse_unit_resultleft)) * dst_positive_scale_inverse_unit_resultleftlookup) + (dst_positive_inverse_unit_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftlookupnegative. ff_h_pvs_inverse_unit_resultleftlookupnegative + S (dst_negative_inverse_unit_resultleftlookup) = S ((S (dc_input_inverse_unit_resultleft)) * dst_negative_scale_inverse_unit_resultleftlookup)) /\ exists ff_q_pvs_inverse_unit_resultleftlookupnegative. dst_negative_code_inverse_unit_resultleftlookup = ff_q_pvs_inverse_unit_resultleftlookupnegative * S ((S (dc_input_inverse_unit_resultleft)) * dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_inverse_unit_resultleftlookup))) /\ (exists ge_balance_positive_inverse_unit_resultleftlookupvalue ge_balance_negative_inverse_unit_resultleftlookupvalue. (((((dc_output_inverse_unit_resultleft) = 2 * (ge_balance_positive_inverse_unit_resultleftlookupvalue) /\ (ge_balance_negative_inverse_unit_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftlookupvaluedecode. (((dc_output_inverse_unit_resultleft) = 2 * ge_signed_half_inverse_unit_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftlookupvalue) = S ge_signed_half_inverse_unit_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftlookup) + ge_balance_negative_inverse_unit_resultleftlookupvalue = (dst_negative_inverse_unit_resultleftlookup) + ge_balance_positive_inverse_unit_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_unit_resultleft)=0)) /\ (exists dc_mask_inverse_unit_resultleftvalue. ((((exists dst_positive_code_inverse_unit_resultleftvaluemasktable dst_positive_scale_inverse_unit_resultleftvaluemasktable dst_negative_code_inverse_unit_resultleftvaluemasktable dst_negative_scale_inverse_unit_resultleftvaluemasktable. (((dc_mask_inverse_unit_resultleftvalue) = (((((dst_positive_code_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable))) + (((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable))) + (((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable))) + (((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_unit_resultleftvaluemasktable. (exists pvs_le_gap_inverse_unit_resultleftvaluemasktabledomain. pvs_le_gap_inverse_unit_resultleftvaluemasktabledomain + (dst_index_inverse_unit_resultleftvaluemasktable) = (dc_input_inverse_unit_resultleft)) -> exists dst_positive_inverse_unit_resultleftvaluemasktable dst_negative_inverse_unit_resultleftvaluemasktable dst_value_inverse_unit_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_unit_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_unit_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_unit_resultleftvaluemasktable) = S ((S (dst_index_inverse_unit_resultleftvaluemasktable)) * dst_positive_scale_inverse_unit_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_unit_resultleftvaluemasktable = ff_q_pvs_inverse_unit_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_unit_resultleftvaluemasktable)) * dst_positive_scale_inverse_unit_resultleftvaluemasktable) + (dst_positive_inverse_unit_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_unit_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_unit_resultleftvaluemasktable) = S ((S (dst_index_inverse_unit_resultleftvaluemasktable)) * dst_negative_scale_inverse_unit_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_unit_resultleftvaluemasktable = ff_q_pvs_inverse_unit_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_unit_resultleftvaluemasktable)) * dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_inverse_unit_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_unit_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_unit_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_unit_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_unit_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_unit_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_unit_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftvaluemasktable) + ge_balance_negative_inverse_unit_resultleftvaluemasktableentryvalue = (dst_negative_inverse_unit_resultleftvaluemasktable) + ge_balance_positive_inverse_unit_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_unit_resultleftvaluemask dc_value_inverse_unit_resultleftvaluemask. (exists pvs_le_gap_inverse_unit_resultleftvaluemaskdomain. pvs_le_gap_inverse_unit_resultleftvaluemaskdomain + (dc_index_inverse_unit_resultleftvaluemask) = (dc_input_inverse_unit_resultleft)) -> (exists dst_positive_code_inverse_unit_resultleftvaluemasklookup dst_positive_scale_inverse_unit_resultleftvaluemasklookup dst_negative_code_inverse_unit_resultleftvaluemasklookup dst_negative_scale_inverse_unit_resultleftvaluemasklookup dst_positive_inverse_unit_resultleftvaluemasklookup dst_negative_inverse_unit_resultleftvaluemasklookup. (((dc_mask_inverse_unit_resultleftvalue) = (((((dst_positive_code_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_unit_resultleftvaluemasklookuppositive + S (dst_positive_inverse_unit_resultleftvaluemasklookup) = S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemasklookuppositive. dst_positive_code_inverse_unit_resultleftvaluemasklookup = ff_q_pvs_inverse_unit_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_positive_scale_inverse_unit_resultleftvaluemasklookup) + (dst_positive_inverse_unit_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_unit_resultleftvaluemasklookupnegative + S (dst_negative_inverse_unit_resultleftvaluemasklookup) = S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemasklookupnegative. dst_negative_code_inverse_unit_resultleftvaluemasklookup = ff_q_pvs_inverse_unit_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_inverse_unit_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluemasklookupvalue ge_balance_negative_inverse_unit_resultleftvaluemasklookupvalue. (((((dc_value_inverse_unit_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_unit_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_unit_resultleftvaluemask) = 2 * ge_signed_half_inverse_unit_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_unit_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftvaluemasklookup) + ge_balance_negative_inverse_unit_resultleftvaluemasklookupvalue = (dst_negative_inverse_unit_resultleftvaluemasklookup) + ge_balance_positive_inverse_unit_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_unit_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_unit_resultleftvaluemaskentry dc_left_inverse_unit_resultleftvaluemaskentry dc_right_inverse_unit_resultleftvaluemaskentry. (((dc_input_inverse_unit_resultleft)=(dc_index_inverse_unit_resultleftvaluemask)*dc_quotient_inverse_unit_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_unit_resultleftvaluemaskentryleft dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft dst_negative_code_inverse_unit_resultleftvaluemaskentryleft dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft dst_positive_inverse_unit_resultleftvaluemaskentryleft dst_negative_inverse_unit_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_unit_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_unit_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_unit_resultleftvaluemaskentryleft = ff_q_pvs_inverse_unit_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_inverse_unit_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_unit_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_unit_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_unit_resultleftvaluemaskentryleft = ff_q_pvs_inverse_unit_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_inverse_unit_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_unit_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_unit_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_unit_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_unit_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_unit_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_unit_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_unit_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultleftvaluemaskentryright dst_positive_scale_inverse_unit_resultleftvaluemaskentryright dst_negative_code_inverse_unit_resultleftvaluemaskentryright dst_negative_scale_inverse_unit_resultleftvaluemaskentryright dst_positive_inverse_unit_resultleftvaluemaskentryright dst_negative_inverse_unit_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_unit_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_unit_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_unit_resultleftvaluemaskentry)) * dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_unit_resultleftvaluemaskentryright = ff_q_pvs_inverse_unit_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_unit_resultleftvaluemaskentry)) * dst_positive_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_inverse_unit_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_unit_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_unit_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_unit_resultleftvaluemaskentry)) * dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_unit_resultleftvaluemaskentryright = ff_q_pvs_inverse_unit_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_unit_resultleftvaluemaskentry)) * dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_inverse_unit_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_unit_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_unit_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_unit_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_unit_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftvaluemaskentryright) + ge_balance_negative_inverse_unit_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_unit_resultleftvaluemaskentryright) + ge_balance_positive_inverse_unit_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_unit_resultleftvaluemaskentryproduct sto_an_inverse_unit_resultleftvaluemaskentryproduct sto_bp_inverse_unit_resultleftvaluemaskentryproduct sto_bn_inverse_unit_resultleftvaluemaskentryproduct sto_cp_inverse_unit_resultleftvaluemaskentryproduct sto_cn_inverse_unit_resultleftvaluemaskentryproduct. (((((dc_left_inverse_unit_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_unit_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_unit_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryproductleft. (((dc_left_inverse_unit_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_unit_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_unit_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_unit_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_unit_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_unit_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryproductright. (((dc_right_inverse_unit_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_unit_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_unit_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_unit_resultleftvaluemask) = 2 * (sto_cp_inverse_unit_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_unit_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_unit_resultleftvaluemask) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_unit_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_unit_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_unit_resultleftvaluemaskentryproduct * sto_bp_inverse_unit_resultleftvaluemaskentryproduct + sto_an_inverse_unit_resultleftvaluemaskentryproduct * sto_bn_inverse_unit_resultleftvaluemaskentryproduct) + sto_cn_inverse_unit_resultleftvaluemaskentryproduct = (sto_ap_inverse_unit_resultleftvaluemaskentryproduct * sto_bn_inverse_unit_resultleftvaluemaskentryproduct + sto_an_inverse_unit_resultleftvaluemaskentryproduct * sto_bp_inverse_unit_resultleftvaluemaskentryproduct) + sto_cp_inverse_unit_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_unit_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_unit_resultleftvaluemaskentrynondivisor. (dc_input_inverse_unit_resultleft) = (dc_index_inverse_unit_resultleftvaluemask) * pvs_factor_inverse_unit_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_unit_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_unit_resultleftvaluefold dst_positive_scale_inverse_unit_resultleftvaluefold dst_negative_code_inverse_unit_resultleftvaluefold dst_negative_scale_inverse_unit_resultleftvaluefold dst_positive_sum_inverse_unit_resultleftvaluefold dst_negative_sum_inverse_unit_resultleftvaluefold. (((dc_mask_inverse_unit_resultleftvalue) = (((((dst_positive_code_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold)) * S ((dst_positive_code_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold)) + ((dst_positive_scale_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold))) + (((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) * S ((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) + ((dst_negative_scale_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold)) * S ((dst_positive_code_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold)) + ((dst_positive_scale_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold))) + (((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) * S ((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) + ((dst_negative_scale_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)))) + ((((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) * S ((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) + ((dst_negative_scale_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold))) + (((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) * S ((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) + ((dst_negative_scale_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_unit_resultleftvaluefoldpositive fs_v_dst_inverse_unit_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_unit_resultleftvaluefoldpositive = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_unit_resultleftvaluefold) = S ((S (S (dc_input_inverse_unit_resultleft))) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_unit_resultleftvaluefoldpositive = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_unit_resultleft))) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_unit_resultleftvaluefold))) /\ forall fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_unit_resultleft)) -> exists fs_a_dst_inverse_unit_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_unit_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_unit_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_unit_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_unit_resultleftvaluefold)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_unit_resultleftvaluefold = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_unit_resultleftvaluefold) + (fs_a_dst_inverse_unit_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_unit_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_unit_resultleftvaluefoldpositive = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive) + (fs_r_dst_inverse_unit_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_unit_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_unit_resultleftvaluefoldpositive = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive) + (fs_s_dst_inverse_unit_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_unit_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_unit_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_unit_resultleftvaluefoldnegative fs_v_dst_inverse_unit_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_unit_resultleftvaluefoldnegative = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_unit_resultleftvaluefold) = S ((S (S (dc_input_inverse_unit_resultleft))) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_unit_resultleftvaluefoldnegative = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_unit_resultleft))) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_unit_resultleftvaluefold))) /\ forall fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_unit_resultleft)) -> exists fs_a_dst_inverse_unit_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_unit_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_unit_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_unit_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_unit_resultleftvaluefold)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_unit_resultleftvaluefold = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_unit_resultleftvaluefold) + (fs_a_dst_inverse_unit_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_unit_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_unit_resultleftvaluefoldnegative = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative) + (fs_r_dst_inverse_unit_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_unit_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_unit_resultleftvaluefoldnegative = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative) + (fs_s_dst_inverse_unit_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_unit_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_unit_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluefoldresult ge_balance_negative_inverse_unit_resultleftvaluefoldresult. (((((dc_output_inverse_unit_resultleft) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_unit_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluefoldresultdecode. (((dc_output_inverse_unit_resultleft) = 2 * ge_signed_half_inverse_unit_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluefoldresult) = S ge_signed_half_inverse_unit_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_unit_resultleftvaluefold) + ge_balance_negative_inverse_unit_resultleftvaluefoldresult = (dst_negative_sum_inverse_unit_resultleftvaluefold) + ge_balance_positive_inverse_unit_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_unit_resultrightleft dst_positive_scale_inverse_unit_resultrightleft dst_negative_code_inverse_unit_resultrightleft dst_negative_scale_inverse_unit_resultrightleft. (((G) = (((((dst_positive_code_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft)) * S ((dst_positive_code_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft)) + ((dst_positive_scale_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft))) + (((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) * S ((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) + ((dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)))) * S ((((dst_positive_code_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft)) * S ((dst_positive_code_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft)) + ((dst_positive_scale_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft))) + (((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) * S ((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) + ((dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)))) + ((((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) * S ((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) + ((dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft))) + (((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) * S ((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) + ((dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)))))) /\ (forall dst_index_inverse_unit_resultrightleft. (exists pvs_le_gap_inverse_unit_resultrightleftdomain. pvs_le_gap_inverse_unit_resultrightleftdomain + (dst_index_inverse_unit_resultrightleft) = (N)) -> exists dst_positive_inverse_unit_resultrightleft dst_negative_inverse_unit_resultrightleft dst_value_inverse_unit_resultrightleft. ((((exists ff_h_pvs_inverse_unit_resultrightleftentrypositive. ff_h_pvs_inverse_unit_resultrightleftentrypositive + S (dst_positive_inverse_unit_resultrightleft) = S ((S (dst_index_inverse_unit_resultrightleft)) * dst_positive_scale_inverse_unit_resultrightleft)) /\ exists ff_q_pvs_inverse_unit_resultrightleftentrypositive. dst_positive_code_inverse_unit_resultrightleft = ff_q_pvs_inverse_unit_resultrightleftentrypositive * S ((S (dst_index_inverse_unit_resultrightleft)) * dst_positive_scale_inverse_unit_resultrightleft) + (dst_positive_inverse_unit_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightleftentrynegative. ff_h_pvs_inverse_unit_resultrightleftentrynegative + S (dst_negative_inverse_unit_resultrightleft) = S ((S (dst_index_inverse_unit_resultrightleft)) * dst_negative_scale_inverse_unit_resultrightleft)) /\ exists ff_q_pvs_inverse_unit_resultrightleftentrynegative. dst_negative_code_inverse_unit_resultrightleft = ff_q_pvs_inverse_unit_resultrightleftentrynegative * S ((S (dst_index_inverse_unit_resultrightleft)) * dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_inverse_unit_resultrightleft))) /\ (exists ge_balance_positive_inverse_unit_resultrightleftentryvalue ge_balance_negative_inverse_unit_resultrightleftentryvalue. (((((dst_value_inverse_unit_resultrightleft) = 2 * (ge_balance_positive_inverse_unit_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_unit_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightleftentryvaluedecode. (((dst_value_inverse_unit_resultrightleft) = 2 * ge_signed_half_inverse_unit_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightleftentryvalue) = S ge_signed_half_inverse_unit_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightleft) + ge_balance_negative_inverse_unit_resultrightleftentryvalue = (dst_negative_inverse_unit_resultrightleft) + ge_balance_positive_inverse_unit_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultrightright dst_positive_scale_inverse_unit_resultrightright dst_negative_code_inverse_unit_resultrightright dst_negative_scale_inverse_unit_resultrightright. (((F) = (((((dst_positive_code_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright)) * S ((dst_positive_code_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright)) + ((dst_positive_scale_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright))) + (((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) * S ((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) + ((dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)))) * S ((((dst_positive_code_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright)) * S ((dst_positive_code_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright)) + ((dst_positive_scale_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright))) + (((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) * S ((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) + ((dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)))) + ((((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) * S ((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) + ((dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright))) + (((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) * S ((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) + ((dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)))))) /\ (forall dst_index_inverse_unit_resultrightright. (exists pvs_le_gap_inverse_unit_resultrightrightdomain. pvs_le_gap_inverse_unit_resultrightrightdomain + (dst_index_inverse_unit_resultrightright) = (N)) -> exists dst_positive_inverse_unit_resultrightright dst_negative_inverse_unit_resultrightright dst_value_inverse_unit_resultrightright. ((((exists ff_h_pvs_inverse_unit_resultrightrightentrypositive. ff_h_pvs_inverse_unit_resultrightrightentrypositive + S (dst_positive_inverse_unit_resultrightright) = S ((S (dst_index_inverse_unit_resultrightright)) * dst_positive_scale_inverse_unit_resultrightright)) /\ exists ff_q_pvs_inverse_unit_resultrightrightentrypositive. dst_positive_code_inverse_unit_resultrightright = ff_q_pvs_inverse_unit_resultrightrightentrypositive * S ((S (dst_index_inverse_unit_resultrightright)) * dst_positive_scale_inverse_unit_resultrightright) + (dst_positive_inverse_unit_resultrightright))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightrightentrynegative. ff_h_pvs_inverse_unit_resultrightrightentrynegative + S (dst_negative_inverse_unit_resultrightright) = S ((S (dst_index_inverse_unit_resultrightright)) * dst_negative_scale_inverse_unit_resultrightright)) /\ exists ff_q_pvs_inverse_unit_resultrightrightentrynegative. dst_negative_code_inverse_unit_resultrightright = ff_q_pvs_inverse_unit_resultrightrightentrynegative * S ((S (dst_index_inverse_unit_resultrightright)) * dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_inverse_unit_resultrightright))) /\ (exists ge_balance_positive_inverse_unit_resultrightrightentryvalue ge_balance_negative_inverse_unit_resultrightrightentryvalue. (((((dst_value_inverse_unit_resultrightright) = 2 * (ge_balance_positive_inverse_unit_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_unit_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightrightentryvaluedecode. (((dst_value_inverse_unit_resultrightright) = 2 * ge_signed_half_inverse_unit_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightrightentryvalue) = S ge_signed_half_inverse_unit_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightright) + ge_balance_negative_inverse_unit_resultrightrightentryvalue = (dst_negative_inverse_unit_resultrightright) + ge_balance_positive_inverse_unit_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultrighttable dst_positive_scale_inverse_unit_resultrighttable dst_negative_code_inverse_unit_resultrighttable dst_negative_scale_inverse_unit_resultrighttable. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable)) * S ((dst_positive_code_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable)) + ((dst_positive_scale_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable))) + (((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) * S ((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) + ((dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)))) * S ((((dst_positive_code_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable)) * S ((dst_positive_code_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable)) + ((dst_positive_scale_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable))) + (((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) * S ((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) + ((dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)))) + ((((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) * S ((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) + ((dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable))) + (((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) * S ((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) + ((dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)))))) /\ (forall dst_index_inverse_unit_resultrighttable. (exists pvs_le_gap_inverse_unit_resultrighttabledomain. pvs_le_gap_inverse_unit_resultrighttabledomain + (dst_index_inverse_unit_resultrighttable) = (N)) -> exists dst_positive_inverse_unit_resultrighttable dst_negative_inverse_unit_resultrighttable dst_value_inverse_unit_resultrighttable. ((((exists ff_h_pvs_inverse_unit_resultrighttableentrypositive. ff_h_pvs_inverse_unit_resultrighttableentrypositive + S (dst_positive_inverse_unit_resultrighttable) = S ((S (dst_index_inverse_unit_resultrighttable)) * dst_positive_scale_inverse_unit_resultrighttable)) /\ exists ff_q_pvs_inverse_unit_resultrighttableentrypositive. dst_positive_code_inverse_unit_resultrighttable = ff_q_pvs_inverse_unit_resultrighttableentrypositive * S ((S (dst_index_inverse_unit_resultrighttable)) * dst_positive_scale_inverse_unit_resultrighttable) + (dst_positive_inverse_unit_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_unit_resultrighttableentrynegative. ff_h_pvs_inverse_unit_resultrighttableentrynegative + S (dst_negative_inverse_unit_resultrighttable) = S ((S (dst_index_inverse_unit_resultrighttable)) * dst_negative_scale_inverse_unit_resultrighttable)) /\ exists ff_q_pvs_inverse_unit_resultrighttableentrynegative. dst_negative_code_inverse_unit_resultrighttable = ff_q_pvs_inverse_unit_resultrighttableentrynegative * S ((S (dst_index_inverse_unit_resultrighttable)) * dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_inverse_unit_resultrighttable))) /\ (exists ge_balance_positive_inverse_unit_resultrighttableentryvalue ge_balance_negative_inverse_unit_resultrighttableentryvalue. (((((dst_value_inverse_unit_resultrighttable) = 2 * (ge_balance_positive_inverse_unit_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_unit_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrighttableentryvaluedecode. (((dst_value_inverse_unit_resultrighttable) = 2 * ge_signed_half_inverse_unit_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrighttableentryvalue) = S ge_signed_half_inverse_unit_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultrighttable) + ge_balance_negative_inverse_unit_resultrighttableentryvalue = (dst_negative_inverse_unit_resultrighttable) + ge_balance_positive_inverse_unit_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_unit_resultright dc_output_inverse_unit_resultright. ~(dc_input_inverse_unit_resultright=0) -> (exists pvs_le_gap_inverse_unit_resultrightdomain. pvs_le_gap_inverse_unit_resultrightdomain + (dc_input_inverse_unit_resultright) = (N)) -> (exists dst_positive_code_inverse_unit_resultrightlookup dst_positive_scale_inverse_unit_resultrightlookup dst_negative_code_inverse_unit_resultrightlookup dst_negative_scale_inverse_unit_resultrightlookup dst_positive_inverse_unit_resultrightlookup dst_negative_inverse_unit_resultrightlookup. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup)) * S ((dst_positive_code_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup)) + ((dst_positive_scale_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup))) + (((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) * S ((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) + ((dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)))) * S ((((dst_positive_code_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup)) * S ((dst_positive_code_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup)) + ((dst_positive_scale_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup))) + (((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) * S ((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) + ((dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)))) + ((((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) * S ((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) + ((dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup))) + (((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) * S ((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) + ((dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightlookuppositive. ff_h_pvs_inverse_unit_resultrightlookuppositive + S (dst_positive_inverse_unit_resultrightlookup) = S ((S (dc_input_inverse_unit_resultright)) * dst_positive_scale_inverse_unit_resultrightlookup)) /\ exists ff_q_pvs_inverse_unit_resultrightlookuppositive. dst_positive_code_inverse_unit_resultrightlookup = ff_q_pvs_inverse_unit_resultrightlookuppositive * S ((S (dc_input_inverse_unit_resultright)) * dst_positive_scale_inverse_unit_resultrightlookup) + (dst_positive_inverse_unit_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightlookupnegative. ff_h_pvs_inverse_unit_resultrightlookupnegative + S (dst_negative_inverse_unit_resultrightlookup) = S ((S (dc_input_inverse_unit_resultright)) * dst_negative_scale_inverse_unit_resultrightlookup)) /\ exists ff_q_pvs_inverse_unit_resultrightlookupnegative. dst_negative_code_inverse_unit_resultrightlookup = ff_q_pvs_inverse_unit_resultrightlookupnegative * S ((S (dc_input_inverse_unit_resultright)) * dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_inverse_unit_resultrightlookup))) /\ (exists ge_balance_positive_inverse_unit_resultrightlookupvalue ge_balance_negative_inverse_unit_resultrightlookupvalue. (((((dc_output_inverse_unit_resultright) = 2 * (ge_balance_positive_inverse_unit_resultrightlookupvalue) /\ (ge_balance_negative_inverse_unit_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightlookupvaluedecode. (((dc_output_inverse_unit_resultright) = 2 * ge_signed_half_inverse_unit_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightlookupvalue) = S ge_signed_half_inverse_unit_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightlookup) + ge_balance_negative_inverse_unit_resultrightlookupvalue = (dst_negative_inverse_unit_resultrightlookup) + ge_balance_positive_inverse_unit_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_unit_resultright)=0)) /\ (exists dc_mask_inverse_unit_resultrightvalue. ((((exists dst_positive_code_inverse_unit_resultrightvaluemasktable dst_positive_scale_inverse_unit_resultrightvaluemasktable dst_negative_code_inverse_unit_resultrightvaluemasktable dst_negative_scale_inverse_unit_resultrightvaluemasktable. (((dc_mask_inverse_unit_resultrightvalue) = (((((dst_positive_code_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable))) + (((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable))) + (((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable))) + (((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_unit_resultrightvaluemasktable. (exists pvs_le_gap_inverse_unit_resultrightvaluemasktabledomain. pvs_le_gap_inverse_unit_resultrightvaluemasktabledomain + (dst_index_inverse_unit_resultrightvaluemasktable) = (dc_input_inverse_unit_resultright)) -> exists dst_positive_inverse_unit_resultrightvaluemasktable dst_negative_inverse_unit_resultrightvaluemasktable dst_value_inverse_unit_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_unit_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_unit_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_unit_resultrightvaluemasktable) = S ((S (dst_index_inverse_unit_resultrightvaluemasktable)) * dst_positive_scale_inverse_unit_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_unit_resultrightvaluemasktable = ff_q_pvs_inverse_unit_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_unit_resultrightvaluemasktable)) * dst_positive_scale_inverse_unit_resultrightvaluemasktable) + (dst_positive_inverse_unit_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_unit_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_unit_resultrightvaluemasktable) = S ((S (dst_index_inverse_unit_resultrightvaluemasktable)) * dst_negative_scale_inverse_unit_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_unit_resultrightvaluemasktable = ff_q_pvs_inverse_unit_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_unit_resultrightvaluemasktable)) * dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_inverse_unit_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_unit_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_unit_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_unit_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_unit_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_unit_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_unit_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightvaluemasktable) + ge_balance_negative_inverse_unit_resultrightvaluemasktableentryvalue = (dst_negative_inverse_unit_resultrightvaluemasktable) + ge_balance_positive_inverse_unit_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_unit_resultrightvaluemask dc_value_inverse_unit_resultrightvaluemask. (exists pvs_le_gap_inverse_unit_resultrightvaluemaskdomain. pvs_le_gap_inverse_unit_resultrightvaluemaskdomain + (dc_index_inverse_unit_resultrightvaluemask) = (dc_input_inverse_unit_resultright)) -> (exists dst_positive_code_inverse_unit_resultrightvaluemasklookup dst_positive_scale_inverse_unit_resultrightvaluemasklookup dst_negative_code_inverse_unit_resultrightvaluemasklookup dst_negative_scale_inverse_unit_resultrightvaluemasklookup dst_positive_inverse_unit_resultrightvaluemasklookup dst_negative_inverse_unit_resultrightvaluemasklookup. (((dc_mask_inverse_unit_resultrightvalue) = (((((dst_positive_code_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_unit_resultrightvaluemasklookuppositive + S (dst_positive_inverse_unit_resultrightvaluemasklookup) = S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemasklookuppositive. dst_positive_code_inverse_unit_resultrightvaluemasklookup = ff_q_pvs_inverse_unit_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_positive_scale_inverse_unit_resultrightvaluemasklookup) + (dst_positive_inverse_unit_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_unit_resultrightvaluemasklookupnegative + S (dst_negative_inverse_unit_resultrightvaluemasklookup) = S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemasklookupnegative. dst_negative_code_inverse_unit_resultrightvaluemasklookup = ff_q_pvs_inverse_unit_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_inverse_unit_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluemasklookupvalue ge_balance_negative_inverse_unit_resultrightvaluemasklookupvalue. (((((dc_value_inverse_unit_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_unit_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_unit_resultrightvaluemask) = 2 * ge_signed_half_inverse_unit_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_unit_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightvaluemasklookup) + ge_balance_negative_inverse_unit_resultrightvaluemasklookupvalue = (dst_negative_inverse_unit_resultrightvaluemasklookup) + ge_balance_positive_inverse_unit_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_unit_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_unit_resultrightvaluemaskentry dc_left_inverse_unit_resultrightvaluemaskentry dc_right_inverse_unit_resultrightvaluemaskentry. (((dc_input_inverse_unit_resultright)=(dc_index_inverse_unit_resultrightvaluemask)*dc_quotient_inverse_unit_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_unit_resultrightvaluemaskentryleft dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft dst_negative_code_inverse_unit_resultrightvaluemaskentryleft dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft dst_positive_inverse_unit_resultrightvaluemaskentryleft dst_negative_inverse_unit_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_unit_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_unit_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_unit_resultrightvaluemaskentryleft = ff_q_pvs_inverse_unit_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_inverse_unit_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_unit_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_unit_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_unit_resultrightvaluemaskentryleft = ff_q_pvs_inverse_unit_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_inverse_unit_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_unit_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_unit_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_unit_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_unit_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_unit_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_unit_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_unit_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultrightvaluemaskentryright dst_positive_scale_inverse_unit_resultrightvaluemaskentryright dst_negative_code_inverse_unit_resultrightvaluemaskentryright dst_negative_scale_inverse_unit_resultrightvaluemaskentryright dst_positive_inverse_unit_resultrightvaluemaskentryright dst_negative_inverse_unit_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_unit_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_unit_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_unit_resultrightvaluemaskentry)) * dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_unit_resultrightvaluemaskentryright = ff_q_pvs_inverse_unit_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_unit_resultrightvaluemaskentry)) * dst_positive_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_inverse_unit_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_unit_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_unit_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_unit_resultrightvaluemaskentry)) * dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_unit_resultrightvaluemaskentryright = ff_q_pvs_inverse_unit_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_unit_resultrightvaluemaskentry)) * dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_inverse_unit_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_unit_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_unit_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_unit_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_unit_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightvaluemaskentryright) + ge_balance_negative_inverse_unit_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_unit_resultrightvaluemaskentryright) + ge_balance_positive_inverse_unit_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_unit_resultrightvaluemaskentryproduct sto_an_inverse_unit_resultrightvaluemaskentryproduct sto_bp_inverse_unit_resultrightvaluemaskentryproduct sto_bn_inverse_unit_resultrightvaluemaskentryproduct sto_cp_inverse_unit_resultrightvaluemaskentryproduct sto_cn_inverse_unit_resultrightvaluemaskentryproduct. (((((dc_left_inverse_unit_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_unit_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_unit_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryproductleft. (((dc_left_inverse_unit_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_unit_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_unit_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_unit_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_unit_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_unit_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryproductright. (((dc_right_inverse_unit_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_unit_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_unit_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_unit_resultrightvaluemask) = 2 * (sto_cp_inverse_unit_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_unit_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_unit_resultrightvaluemask) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_unit_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_unit_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_unit_resultrightvaluemaskentryproduct * sto_bp_inverse_unit_resultrightvaluemaskentryproduct + sto_an_inverse_unit_resultrightvaluemaskentryproduct * sto_bn_inverse_unit_resultrightvaluemaskentryproduct) + sto_cn_inverse_unit_resultrightvaluemaskentryproduct = (sto_ap_inverse_unit_resultrightvaluemaskentryproduct * sto_bn_inverse_unit_resultrightvaluemaskentryproduct + sto_an_inverse_unit_resultrightvaluemaskentryproduct * sto_bp_inverse_unit_resultrightvaluemaskentryproduct) + sto_cp_inverse_unit_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_unit_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_unit_resultrightvaluemaskentrynondivisor. (dc_input_inverse_unit_resultright) = (dc_index_inverse_unit_resultrightvaluemask) * pvs_factor_inverse_unit_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_unit_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_unit_resultrightvaluefold dst_positive_scale_inverse_unit_resultrightvaluefold dst_negative_code_inverse_unit_resultrightvaluefold dst_negative_scale_inverse_unit_resultrightvaluefold dst_positive_sum_inverse_unit_resultrightvaluefold dst_negative_sum_inverse_unit_resultrightvaluefold. (((dc_mask_inverse_unit_resultrightvalue) = (((((dst_positive_code_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold)) * S ((dst_positive_code_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold)) + ((dst_positive_scale_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold))) + (((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) * S ((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) + ((dst_negative_scale_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold)) * S ((dst_positive_code_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold)) + ((dst_positive_scale_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold))) + (((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) * S ((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) + ((dst_negative_scale_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)))) + ((((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) * S ((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) + ((dst_negative_scale_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold))) + (((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) * S ((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) + ((dst_negative_scale_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_unit_resultrightvaluefoldpositive fs_v_dst_inverse_unit_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_unit_resultrightvaluefoldpositive = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_unit_resultrightvaluefold) = S ((S (S (dc_input_inverse_unit_resultright))) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_unit_resultrightvaluefoldpositive = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_unit_resultright))) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_unit_resultrightvaluefold))) /\ forall fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_unit_resultright)) -> exists fs_a_dst_inverse_unit_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_unit_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_unit_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_unit_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_unit_resultrightvaluefold)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_unit_resultrightvaluefold = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_unit_resultrightvaluefold) + (fs_a_dst_inverse_unit_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_unit_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_unit_resultrightvaluefoldpositive = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive) + (fs_r_dst_inverse_unit_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_unit_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_unit_resultrightvaluefoldpositive = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive) + (fs_s_dst_inverse_unit_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_unit_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_unit_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_unit_resultrightvaluefoldnegative fs_v_dst_inverse_unit_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_unit_resultrightvaluefoldnegative = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_unit_resultrightvaluefold) = S ((S (S (dc_input_inverse_unit_resultright))) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_unit_resultrightvaluefoldnegative = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_unit_resultright))) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_unit_resultrightvaluefold))) /\ forall fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_unit_resultright)) -> exists fs_a_dst_inverse_unit_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_unit_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_unit_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_unit_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_unit_resultrightvaluefold)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_unit_resultrightvaluefold = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_unit_resultrightvaluefold) + (fs_a_dst_inverse_unit_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_unit_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_unit_resultrightvaluefoldnegative = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative) + (fs_r_dst_inverse_unit_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_unit_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_unit_resultrightvaluefoldnegative = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative) + (fs_s_dst_inverse_unit_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_unit_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_unit_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluefoldresult ge_balance_negative_inverse_unit_resultrightvaluefoldresult. (((((dc_output_inverse_unit_resultright) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_unit_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluefoldresultdecode. (((dc_output_inverse_unit_resultright) = 2 * ge_signed_half_inverse_unit_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluefoldresult) = S ge_signed_half_inverse_unit_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_unit_resultrightvaluefold) + ge_balance_negative_inverse_unit_resultrightvaluefoldresult = (dst_negative_sum_inverse_unit_resultrightvaluefold) + ge_balance_positive_inverse_unit_resultrightvaluefoldresult)))))))))))))))))))))))) /\ (exists dst_positive_code_inverse_unit_zero dst_positive_scale_inverse_unit_zero dst_negative_code_inverse_unit_zero dst_negative_scale_inverse_unit_zero dst_positive_inverse_unit_zero dst_negative_inverse_unit_zero. (((G) = (((((dst_positive_code_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero)) * S ((dst_positive_code_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero)) + ((dst_positive_scale_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero))) + (((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) * S ((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) + ((dst_negative_scale_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)))) * S ((((dst_positive_code_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero)) * S ((dst_positive_code_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero)) + ((dst_positive_scale_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero))) + (((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) * S ((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) + ((dst_negative_scale_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)))) + ((((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) * S ((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) + ((dst_negative_scale_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero))) + (((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) * S ((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) + ((dst_negative_scale_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)))))) /\ (((((exists ff_h_pvs_inverse_unit_zeropositive. ff_h_pvs_inverse_unit_zeropositive + S (dst_positive_inverse_unit_zero) = S ((S (0)) * dst_positive_scale_inverse_unit_zero)) /\ exists ff_q_pvs_inverse_unit_zeropositive. dst_positive_code_inverse_unit_zero = ff_q_pvs_inverse_unit_zeropositive * S ((S (0)) * dst_positive_scale_inverse_unit_zero) + (dst_positive_inverse_unit_zero))) /\ (((((exists ff_h_pvs_inverse_unit_zeronegative. ff_h_pvs_inverse_unit_zeronegative + S (dst_negative_inverse_unit_zero) = S ((S (0)) * dst_negative_scale_inverse_unit_zero)) /\ exists ff_q_pvs_inverse_unit_zeronegative. dst_negative_code_inverse_unit_zero = ff_q_pvs_inverse_unit_zeronegative * S ((S (0)) * dst_negative_scale_inverse_unit_zero) + (dst_negative_inverse_unit_zero))) /\ (exists ge_balance_positive_inverse_unit_zerovalue ge_balance_negative_inverse_unit_zerovalue. (((((w) = 2 * (ge_balance_positive_inverse_unit_zerovalue) /\ (ge_balance_negative_inverse_unit_zerovalue) = 0) \/ exists ge_signed_half_inverse_unit_zerovaluedecode. (((w) = 2 * ge_signed_half_inverse_unit_zerovaluedecode + 1 /\ (ge_balance_positive_inverse_unit_zerovalue) = 0) /\ (ge_balance_negative_inverse_unit_zerovalue) = S ge_signed_half_inverse_unit_zerovaluedecode))) /\ ((dst_positive_inverse_unit_zero) + ge_balance_negative_inverse_unit_zerovalue = (dst_negative_inverse_unit_zero) + ge_balance_positive_inverse_unit_zerovalue))))))))))Complete tactic proof in conservative notation
All 37 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
37 script commands · 9 reading checkpoints · 2 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (2)
01Fix variables and assumptionsL1–7
02Establish hdL8–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet kronecker delta table exists.
- L8
have hd : ∃ E. KroneckerDeltaTable(N,E) ∧ ArithAt(E,0,0)Definitions: KroneckerDeltaTable(N,E)ArithAt(E,0,0)Original native command in the exact edition - L9
specialize dirichlet_kronecker_delta_table_exists (N) - L10
specialize dirichlet_kronecker_delta_table_exists (0) - L11
apply dirichlet_kronecker_delta_table_exists
03Separate the logical casesL12–14
04Establish hgL15–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet unit equation construct.
- L15
have hg : ∃ G. DirichletTable(N,G,F,x) ∧ ArithAt(G,0,w)Definitions: DirichletTable(N,G,F,x)ArithAt(G,0,w)Original native command in the exact edition - L16
specialize dirichlet_unit_equation_construct (N) - L17
specialize dirichlet_unit_equation_construct (F) - L18
specialize dirichlet_unit_equation_construct (x) - L19
specialize dirichlet_unit_equation_construct (u) - L20
specialize dirichlet_unit_equation_construct (w) - L21
apply dirichlet_unit_equation_construct - L22
exact hF - L23
exact hd_witness_left_left - L24
exact hu
05Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact hunit
06Separate the logical casesL26–27
07Construct an explicit witnessL28–28
Supply the displayed value, then prove that it has the required property.
- L28
exists x1
08Separate the logical casesL29–29
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L29
split
09Use earlier factsL30–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L30
specialize dirichlet_inverse_from_right_delta (N) - L31
specialize dirichlet_inverse_from_right_delta (F) - L32
specialize dirichlet_inverse_from_right_delta (x1) - L33
specialize dirichlet_inverse_from_right_delta (x) - L34
apply dirichlet_inverse_from_right_delta - L35
exact hd_witness_left - L36
exact hg_witness_left - L37
exact hg_witness_right
Original defined command ledger · 37 lines
- 0001
intro N - 0002
intro F - 0003
intro u - 0004
intro w - 0005
intro hF - 0006
intro hu - 0007
intro hunit - 0008
have hd : ∃ E. KroneckerDeltaTable(N,E) ∧ ArithAt(E,0,0) - 0009
specialize dirichlet_kronecker_delta_table_exists (N) - 0010
specialize dirichlet_kronecker_delta_table_exists (0) - 0011
apply dirichlet_kronecker_delta_table_exists - 0012
cases hd - 0013
cases hd_witness - 0014
cases hd_witness_left - 0015
have hg : ∃ G. DirichletTable(N,G,F,x) ∧ ArithAt(G,0,w) - 0016
specialize dirichlet_unit_equation_construct (N) - 0017
specialize dirichlet_unit_equation_construct (F) - 0018
specialize dirichlet_unit_equation_construct (x) - 0019
specialize dirichlet_unit_equation_construct (u) - 0020
specialize dirichlet_unit_equation_construct (w) - 0021
apply dirichlet_unit_equation_construct - 0022
exact hF - 0023
exact hd_witness_left_left - 0024
exact hu - 0025
exact hunit - 0026
cases hg - 0027
cases hg_witness - 0028
exists x1 - 0029
split - 0030
specialize dirichlet_inverse_from_right_delta (N) - 0031
specialize dirichlet_inverse_from_right_delta (F) - 0032
specialize dirichlet_inverse_from_right_delta (x1) - 0033
specialize dirichlet_inverse_from_right_delta (x) - 0034
apply dirichlet_inverse_from_right_delta - 0035
exact hd_witness_left - 0036
exact hg_witness_left - 0037
exact hg_witness_right