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
∀ F. ∀ w. ArithTable(0,F) → ∃ x. DirichletInverse(0,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 F w. (exists dst_positive_code_inverse_zero_construct_input dst_positive_scale_inverse_zero_construct_input dst_negative_code_inverse_zero_construct_input dst_negative_scale_inverse_zero_construct_input. (((F) = (((((dst_positive_code_inverse_zero_construct_input) + (dst_positive_scale_inverse_zero_construct_input)) * S ((dst_positive_code_inverse_zero_construct_input) + (dst_positive_scale_inverse_zero_construct_input)) + ((dst_positive_scale_inverse_zero_construct_input) + (dst_positive_scale_inverse_zero_construct_input))) + (((dst_negative_code_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)) * S ((dst_negative_code_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)) + ((dst_negative_scale_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)))) * S ((((dst_positive_code_inverse_zero_construct_input) + (dst_positive_scale_inverse_zero_construct_input)) * S ((dst_positive_code_inverse_zero_construct_input) + (dst_positive_scale_inverse_zero_construct_input)) + ((dst_positive_scale_inverse_zero_construct_input) + (dst_positive_scale_inverse_zero_construct_input))) + (((dst_negative_code_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)) * S ((dst_negative_code_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)) + ((dst_negative_scale_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)))) + ((((dst_negative_code_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)) * S ((dst_negative_code_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)) + ((dst_negative_scale_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input))) + (((dst_negative_code_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)) * S ((dst_negative_code_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)) + ((dst_negative_scale_inverse_zero_construct_input) + (dst_negative_scale_inverse_zero_construct_input)))))) /\ (forall dst_index_inverse_zero_construct_input. (exists pvs_le_gap_inverse_zero_construct_inputdomain. pvs_le_gap_inverse_zero_construct_inputdomain + (dst_index_inverse_zero_construct_input) = (0)) -> exists dst_positive_inverse_zero_construct_input dst_negative_inverse_zero_construct_input dst_value_inverse_zero_construct_input. ((((exists ff_h_pvs_inverse_zero_construct_inputentrypositive. ff_h_pvs_inverse_zero_construct_inputentrypositive + S (dst_positive_inverse_zero_construct_input) = S ((S (dst_index_inverse_zero_construct_input)) * dst_positive_scale_inverse_zero_construct_input)) /\ exists ff_q_pvs_inverse_zero_construct_inputentrypositive. dst_positive_code_inverse_zero_construct_input = ff_q_pvs_inverse_zero_construct_inputentrypositive * S ((S (dst_index_inverse_zero_construct_input)) * dst_positive_scale_inverse_zero_construct_input) + (dst_positive_inverse_zero_construct_input))) /\ (((((exists ff_h_pvs_inverse_zero_construct_inputentrynegative. ff_h_pvs_inverse_zero_construct_inputentrynegative + S (dst_negative_inverse_zero_construct_input) = S ((S (dst_index_inverse_zero_construct_input)) * dst_negative_scale_inverse_zero_construct_input)) /\ exists ff_q_pvs_inverse_zero_construct_inputentrynegative. dst_negative_code_inverse_zero_construct_input = ff_q_pvs_inverse_zero_construct_inputentrynegative * S ((S (dst_index_inverse_zero_construct_input)) * dst_negative_scale_inverse_zero_construct_input) + (dst_negative_inverse_zero_construct_input))) /\ (exists ge_balance_positive_inverse_zero_construct_inputentryvalue ge_balance_negative_inverse_zero_construct_inputentryvalue. (((((dst_value_inverse_zero_construct_input) = 2 * (ge_balance_positive_inverse_zero_construct_inputentryvalue) /\ (ge_balance_negative_inverse_zero_construct_inputentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_inputentryvaluedecode. (((dst_value_inverse_zero_construct_input) = 2 * ge_signed_half_inverse_zero_construct_inputentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_inputentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_inputentryvalue) = S ge_signed_half_inverse_zero_construct_inputentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_input) + ge_balance_negative_inverse_zero_construct_inputentryvalue = (dst_negative_inverse_zero_construct_input) + ge_balance_positive_inverse_zero_construct_inputentryvalue))))))))) -> exists G. ((exists di_delta_inverse_zero_construct_result. ((((exists dst_positive_code_inverse_zero_construct_resultdeltatable dst_positive_scale_inverse_zero_construct_resultdeltatable dst_negative_code_inverse_zero_construct_resultdeltatable dst_negative_scale_inverse_zero_construct_resultdeltatable. (((di_delta_inverse_zero_construct_result) = (((((dst_positive_code_inverse_zero_construct_resultdeltatable) + (dst_positive_scale_inverse_zero_construct_resultdeltatable)) * S ((dst_positive_code_inverse_zero_construct_resultdeltatable) + (dst_positive_scale_inverse_zero_construct_resultdeltatable)) + ((dst_positive_scale_inverse_zero_construct_resultdeltatable) + (dst_positive_scale_inverse_zero_construct_resultdeltatable))) + (((dst_negative_code_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)) * S ((dst_negative_code_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)) + ((dst_negative_scale_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)))) * S ((((dst_positive_code_inverse_zero_construct_resultdeltatable) + (dst_positive_scale_inverse_zero_construct_resultdeltatable)) * S ((dst_positive_code_inverse_zero_construct_resultdeltatable) + (dst_positive_scale_inverse_zero_construct_resultdeltatable)) + ((dst_positive_scale_inverse_zero_construct_resultdeltatable) + (dst_positive_scale_inverse_zero_construct_resultdeltatable))) + (((dst_negative_code_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)) * S ((dst_negative_code_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)) + ((dst_negative_scale_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)))) + ((((dst_negative_code_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)) * S ((dst_negative_code_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)) + ((dst_negative_scale_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable))) + (((dst_negative_code_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)) * S ((dst_negative_code_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)) + ((dst_negative_scale_inverse_zero_construct_resultdeltatable) + (dst_negative_scale_inverse_zero_construct_resultdeltatable)))))) /\ (forall dst_index_inverse_zero_construct_resultdeltatable. (exists pvs_le_gap_inverse_zero_construct_resultdeltatabledomain. pvs_le_gap_inverse_zero_construct_resultdeltatabledomain + (dst_index_inverse_zero_construct_resultdeltatable) = (0)) -> exists dst_positive_inverse_zero_construct_resultdeltatable dst_negative_inverse_zero_construct_resultdeltatable dst_value_inverse_zero_construct_resultdeltatable. ((((exists ff_h_pvs_inverse_zero_construct_resultdeltatableentrypositive. ff_h_pvs_inverse_zero_construct_resultdeltatableentrypositive + S (dst_positive_inverse_zero_construct_resultdeltatable) = S ((S (dst_index_inverse_zero_construct_resultdeltatable)) * dst_positive_scale_inverse_zero_construct_resultdeltatable)) /\ exists ff_q_pvs_inverse_zero_construct_resultdeltatableentrypositive. dst_positive_code_inverse_zero_construct_resultdeltatable = ff_q_pvs_inverse_zero_construct_resultdeltatableentrypositive * S ((S (dst_index_inverse_zero_construct_resultdeltatable)) * dst_positive_scale_inverse_zero_construct_resultdeltatable) + (dst_positive_inverse_zero_construct_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultdeltatableentrynegative. ff_h_pvs_inverse_zero_construct_resultdeltatableentrynegative + S (dst_negative_inverse_zero_construct_resultdeltatable) = S ((S (dst_index_inverse_zero_construct_resultdeltatable)) * dst_negative_scale_inverse_zero_construct_resultdeltatable)) /\ exists ff_q_pvs_inverse_zero_construct_resultdeltatableentrynegative. dst_negative_code_inverse_zero_construct_resultdeltatable = ff_q_pvs_inverse_zero_construct_resultdeltatableentrynegative * S ((S (dst_index_inverse_zero_construct_resultdeltatable)) * dst_negative_scale_inverse_zero_construct_resultdeltatable) + (dst_negative_inverse_zero_construct_resultdeltatable))) /\ (exists ge_balance_positive_inverse_zero_construct_resultdeltatableentryvalue ge_balance_negative_inverse_zero_construct_resultdeltatableentryvalue. (((((dst_value_inverse_zero_construct_resultdeltatable) = 2 * (ge_balance_positive_inverse_zero_construct_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultdeltatableentryvaluedecode. (((dst_value_inverse_zero_construct_resultdeltatable) = 2 * ge_signed_half_inverse_zero_construct_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultdeltatableentryvalue) = S ge_signed_half_inverse_zero_construct_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultdeltatable) + ge_balance_negative_inverse_zero_construct_resultdeltatableentryvalue = (dst_negative_inverse_zero_construct_resultdeltatable) + ge_balance_positive_inverse_zero_construct_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_zero_construct_resultdelta du_value_inverse_zero_construct_resultdelta. ~(du_index_inverse_zero_construct_resultdelta=0) -> (exists pvs_le_gap_inverse_zero_construct_resultdeltabound. pvs_le_gap_inverse_zero_construct_resultdeltabound + (du_index_inverse_zero_construct_resultdelta) = (0)) -> (exists dst_positive_code_inverse_zero_construct_resultdeltaentry dst_positive_scale_inverse_zero_construct_resultdeltaentry dst_negative_code_inverse_zero_construct_resultdeltaentry dst_negative_scale_inverse_zero_construct_resultdeltaentry dst_positive_inverse_zero_construct_resultdeltaentry dst_negative_inverse_zero_construct_resultdeltaentry. (((di_delta_inverse_zero_construct_result) = (((((dst_positive_code_inverse_zero_construct_resultdeltaentry) + (dst_positive_scale_inverse_zero_construct_resultdeltaentry)) * S ((dst_positive_code_inverse_zero_construct_resultdeltaentry) + (dst_positive_scale_inverse_zero_construct_resultdeltaentry)) + ((dst_positive_scale_inverse_zero_construct_resultdeltaentry) + (dst_positive_scale_inverse_zero_construct_resultdeltaentry))) + (((dst_negative_code_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)))) * S ((((dst_positive_code_inverse_zero_construct_resultdeltaentry) + (dst_positive_scale_inverse_zero_construct_resultdeltaentry)) * S ((dst_positive_code_inverse_zero_construct_resultdeltaentry) + (dst_positive_scale_inverse_zero_construct_resultdeltaentry)) + ((dst_positive_scale_inverse_zero_construct_resultdeltaentry) + (dst_positive_scale_inverse_zero_construct_resultdeltaentry))) + (((dst_negative_code_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)))) + ((((dst_negative_code_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry))) + (((dst_negative_code_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_construct_resultdeltaentry) + (dst_negative_scale_inverse_zero_construct_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultdeltaentrypositive. ff_h_pvs_inverse_zero_construct_resultdeltaentrypositive + S (dst_positive_inverse_zero_construct_resultdeltaentry) = S ((S (du_index_inverse_zero_construct_resultdelta)) * dst_positive_scale_inverse_zero_construct_resultdeltaentry)) /\ exists ff_q_pvs_inverse_zero_construct_resultdeltaentrypositive. dst_positive_code_inverse_zero_construct_resultdeltaentry = ff_q_pvs_inverse_zero_construct_resultdeltaentrypositive * S ((S (du_index_inverse_zero_construct_resultdelta)) * dst_positive_scale_inverse_zero_construct_resultdeltaentry) + (dst_positive_inverse_zero_construct_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultdeltaentrynegative. ff_h_pvs_inverse_zero_construct_resultdeltaentrynegative + S (dst_negative_inverse_zero_construct_resultdeltaentry) = S ((S (du_index_inverse_zero_construct_resultdelta)) * dst_negative_scale_inverse_zero_construct_resultdeltaentry)) /\ exists ff_q_pvs_inverse_zero_construct_resultdeltaentrynegative. dst_negative_code_inverse_zero_construct_resultdeltaentry = ff_q_pvs_inverse_zero_construct_resultdeltaentrynegative * S ((S (du_index_inverse_zero_construct_resultdelta)) * dst_negative_scale_inverse_zero_construct_resultdeltaentry) + (dst_negative_inverse_zero_construct_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_zero_construct_resultdeltaentryvalue ge_balance_negative_inverse_zero_construct_resultdeltaentryvalue. (((((du_value_inverse_zero_construct_resultdelta) = 2 * (ge_balance_positive_inverse_zero_construct_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultdeltaentryvaluedecode. (((du_value_inverse_zero_construct_resultdelta) = 2 * ge_signed_half_inverse_zero_construct_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultdeltaentryvalue) = S ge_signed_half_inverse_zero_construct_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultdeltaentry) + ge_balance_negative_inverse_zero_construct_resultdeltaentryvalue = (dst_negative_inverse_zero_construct_resultdeltaentry) + ge_balance_positive_inverse_zero_construct_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_zero_construct_resultdelta)=1 -> (du_value_inverse_zero_construct_resultdelta)=2) /\ (~((du_index_inverse_zero_construct_resultdelta)=1) -> (du_value_inverse_zero_construct_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_zero_construct_resultleftleft dst_positive_scale_inverse_zero_construct_resultleftleft dst_negative_code_inverse_zero_construct_resultleftleft dst_negative_scale_inverse_zero_construct_resultleftleft. (((F) = (((((dst_positive_code_inverse_zero_construct_resultleftleft) + (dst_positive_scale_inverse_zero_construct_resultleftleft)) * S ((dst_positive_code_inverse_zero_construct_resultleftleft) + (dst_positive_scale_inverse_zero_construct_resultleftleft)) + ((dst_positive_scale_inverse_zero_construct_resultleftleft) + (dst_positive_scale_inverse_zero_construct_resultleftleft))) + (((dst_negative_code_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)) * S ((dst_negative_code_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)) + ((dst_negative_scale_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)))) * S ((((dst_positive_code_inverse_zero_construct_resultleftleft) + (dst_positive_scale_inverse_zero_construct_resultleftleft)) * S ((dst_positive_code_inverse_zero_construct_resultleftleft) + (dst_positive_scale_inverse_zero_construct_resultleftleft)) + ((dst_positive_scale_inverse_zero_construct_resultleftleft) + (dst_positive_scale_inverse_zero_construct_resultleftleft))) + (((dst_negative_code_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)) * S ((dst_negative_code_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)) + ((dst_negative_scale_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)))) + ((((dst_negative_code_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)) * S ((dst_negative_code_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)) + ((dst_negative_scale_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft))) + (((dst_negative_code_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)) * S ((dst_negative_code_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)) + ((dst_negative_scale_inverse_zero_construct_resultleftleft) + (dst_negative_scale_inverse_zero_construct_resultleftleft)))))) /\ (forall dst_index_inverse_zero_construct_resultleftleft. (exists pvs_le_gap_inverse_zero_construct_resultleftleftdomain. pvs_le_gap_inverse_zero_construct_resultleftleftdomain + (dst_index_inverse_zero_construct_resultleftleft) = (0)) -> exists dst_positive_inverse_zero_construct_resultleftleft dst_negative_inverse_zero_construct_resultleftleft dst_value_inverse_zero_construct_resultleftleft. ((((exists ff_h_pvs_inverse_zero_construct_resultleftleftentrypositive. ff_h_pvs_inverse_zero_construct_resultleftleftentrypositive + S (dst_positive_inverse_zero_construct_resultleftleft) = S ((S (dst_index_inverse_zero_construct_resultleftleft)) * dst_positive_scale_inverse_zero_construct_resultleftleft)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftleftentrypositive. dst_positive_code_inverse_zero_construct_resultleftleft = ff_q_pvs_inverse_zero_construct_resultleftleftentrypositive * S ((S (dst_index_inverse_zero_construct_resultleftleft)) * dst_positive_scale_inverse_zero_construct_resultleftleft) + (dst_positive_inverse_zero_construct_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftleftentrynegative. ff_h_pvs_inverse_zero_construct_resultleftleftentrynegative + S (dst_negative_inverse_zero_construct_resultleftleft) = S ((S (dst_index_inverse_zero_construct_resultleftleft)) * dst_negative_scale_inverse_zero_construct_resultleftleft)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftleftentrynegative. dst_negative_code_inverse_zero_construct_resultleftleft = ff_q_pvs_inverse_zero_construct_resultleftleftentrynegative * S ((S (dst_index_inverse_zero_construct_resultleftleft)) * dst_negative_scale_inverse_zero_construct_resultleftleft) + (dst_negative_inverse_zero_construct_resultleftleft))) /\ (exists ge_balance_positive_inverse_zero_construct_resultleftleftentryvalue ge_balance_negative_inverse_zero_construct_resultleftleftentryvalue. (((((dst_value_inverse_zero_construct_resultleftleft) = 2 * (ge_balance_positive_inverse_zero_construct_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftleftentryvaluedecode. (((dst_value_inverse_zero_construct_resultleftleft) = 2 * ge_signed_half_inverse_zero_construct_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultleftleftentryvalue) = S ge_signed_half_inverse_zero_construct_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultleftleft) + ge_balance_negative_inverse_zero_construct_resultleftleftentryvalue = (dst_negative_inverse_zero_construct_resultleftleft) + ge_balance_positive_inverse_zero_construct_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_construct_resultleftright dst_positive_scale_inverse_zero_construct_resultleftright dst_negative_code_inverse_zero_construct_resultleftright dst_negative_scale_inverse_zero_construct_resultleftright. (((G) = (((((dst_positive_code_inverse_zero_construct_resultleftright) + (dst_positive_scale_inverse_zero_construct_resultleftright)) * S ((dst_positive_code_inverse_zero_construct_resultleftright) + (dst_positive_scale_inverse_zero_construct_resultleftright)) + ((dst_positive_scale_inverse_zero_construct_resultleftright) + (dst_positive_scale_inverse_zero_construct_resultleftright))) + (((dst_negative_code_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)) * S ((dst_negative_code_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)) + ((dst_negative_scale_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)))) * S ((((dst_positive_code_inverse_zero_construct_resultleftright) + (dst_positive_scale_inverse_zero_construct_resultleftright)) * S ((dst_positive_code_inverse_zero_construct_resultleftright) + (dst_positive_scale_inverse_zero_construct_resultleftright)) + ((dst_positive_scale_inverse_zero_construct_resultleftright) + (dst_positive_scale_inverse_zero_construct_resultleftright))) + (((dst_negative_code_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)) * S ((dst_negative_code_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)) + ((dst_negative_scale_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)))) + ((((dst_negative_code_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)) * S ((dst_negative_code_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)) + ((dst_negative_scale_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright))) + (((dst_negative_code_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)) * S ((dst_negative_code_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)) + ((dst_negative_scale_inverse_zero_construct_resultleftright) + (dst_negative_scale_inverse_zero_construct_resultleftright)))))) /\ (forall dst_index_inverse_zero_construct_resultleftright. (exists pvs_le_gap_inverse_zero_construct_resultleftrightdomain. pvs_le_gap_inverse_zero_construct_resultleftrightdomain + (dst_index_inverse_zero_construct_resultleftright) = (0)) -> exists dst_positive_inverse_zero_construct_resultleftright dst_negative_inverse_zero_construct_resultleftright dst_value_inverse_zero_construct_resultleftright. ((((exists ff_h_pvs_inverse_zero_construct_resultleftrightentrypositive. ff_h_pvs_inverse_zero_construct_resultleftrightentrypositive + S (dst_positive_inverse_zero_construct_resultleftright) = S ((S (dst_index_inverse_zero_construct_resultleftright)) * dst_positive_scale_inverse_zero_construct_resultleftright)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftrightentrypositive. dst_positive_code_inverse_zero_construct_resultleftright = ff_q_pvs_inverse_zero_construct_resultleftrightentrypositive * S ((S (dst_index_inverse_zero_construct_resultleftright)) * dst_positive_scale_inverse_zero_construct_resultleftright) + (dst_positive_inverse_zero_construct_resultleftright))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftrightentrynegative. ff_h_pvs_inverse_zero_construct_resultleftrightentrynegative + S (dst_negative_inverse_zero_construct_resultleftright) = S ((S (dst_index_inverse_zero_construct_resultleftright)) * dst_negative_scale_inverse_zero_construct_resultleftright)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftrightentrynegative. dst_negative_code_inverse_zero_construct_resultleftright = ff_q_pvs_inverse_zero_construct_resultleftrightentrynegative * S ((S (dst_index_inverse_zero_construct_resultleftright)) * dst_negative_scale_inverse_zero_construct_resultleftright) + (dst_negative_inverse_zero_construct_resultleftright))) /\ (exists ge_balance_positive_inverse_zero_construct_resultleftrightentryvalue ge_balance_negative_inverse_zero_construct_resultleftrightentryvalue. (((((dst_value_inverse_zero_construct_resultleftright) = 2 * (ge_balance_positive_inverse_zero_construct_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftrightentryvaluedecode. (((dst_value_inverse_zero_construct_resultleftright) = 2 * ge_signed_half_inverse_zero_construct_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultleftrightentryvalue) = S ge_signed_half_inverse_zero_construct_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultleftright) + ge_balance_negative_inverse_zero_construct_resultleftrightentryvalue = (dst_negative_inverse_zero_construct_resultleftright) + ge_balance_positive_inverse_zero_construct_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_construct_resultlefttable dst_positive_scale_inverse_zero_construct_resultlefttable dst_negative_code_inverse_zero_construct_resultlefttable dst_negative_scale_inverse_zero_construct_resultlefttable. (((di_delta_inverse_zero_construct_result) = (((((dst_positive_code_inverse_zero_construct_resultlefttable) + (dst_positive_scale_inverse_zero_construct_resultlefttable)) * S ((dst_positive_code_inverse_zero_construct_resultlefttable) + (dst_positive_scale_inverse_zero_construct_resultlefttable)) + ((dst_positive_scale_inverse_zero_construct_resultlefttable) + (dst_positive_scale_inverse_zero_construct_resultlefttable))) + (((dst_negative_code_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)) * S ((dst_negative_code_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)) + ((dst_negative_scale_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)))) * S ((((dst_positive_code_inverse_zero_construct_resultlefttable) + (dst_positive_scale_inverse_zero_construct_resultlefttable)) * S ((dst_positive_code_inverse_zero_construct_resultlefttable) + (dst_positive_scale_inverse_zero_construct_resultlefttable)) + ((dst_positive_scale_inverse_zero_construct_resultlefttable) + (dst_positive_scale_inverse_zero_construct_resultlefttable))) + (((dst_negative_code_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)) * S ((dst_negative_code_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)) + ((dst_negative_scale_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)))) + ((((dst_negative_code_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)) * S ((dst_negative_code_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)) + ((dst_negative_scale_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable))) + (((dst_negative_code_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)) * S ((dst_negative_code_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)) + ((dst_negative_scale_inverse_zero_construct_resultlefttable) + (dst_negative_scale_inverse_zero_construct_resultlefttable)))))) /\ (forall dst_index_inverse_zero_construct_resultlefttable. (exists pvs_le_gap_inverse_zero_construct_resultlefttabledomain. pvs_le_gap_inverse_zero_construct_resultlefttabledomain + (dst_index_inverse_zero_construct_resultlefttable) = (0)) -> exists dst_positive_inverse_zero_construct_resultlefttable dst_negative_inverse_zero_construct_resultlefttable dst_value_inverse_zero_construct_resultlefttable. ((((exists ff_h_pvs_inverse_zero_construct_resultlefttableentrypositive. ff_h_pvs_inverse_zero_construct_resultlefttableentrypositive + S (dst_positive_inverse_zero_construct_resultlefttable) = S ((S (dst_index_inverse_zero_construct_resultlefttable)) * dst_positive_scale_inverse_zero_construct_resultlefttable)) /\ exists ff_q_pvs_inverse_zero_construct_resultlefttableentrypositive. dst_positive_code_inverse_zero_construct_resultlefttable = ff_q_pvs_inverse_zero_construct_resultlefttableentrypositive * S ((S (dst_index_inverse_zero_construct_resultlefttable)) * dst_positive_scale_inverse_zero_construct_resultlefttable) + (dst_positive_inverse_zero_construct_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultlefttableentrynegative. ff_h_pvs_inverse_zero_construct_resultlefttableentrynegative + S (dst_negative_inverse_zero_construct_resultlefttable) = S ((S (dst_index_inverse_zero_construct_resultlefttable)) * dst_negative_scale_inverse_zero_construct_resultlefttable)) /\ exists ff_q_pvs_inverse_zero_construct_resultlefttableentrynegative. dst_negative_code_inverse_zero_construct_resultlefttable = ff_q_pvs_inverse_zero_construct_resultlefttableentrynegative * S ((S (dst_index_inverse_zero_construct_resultlefttable)) * dst_negative_scale_inverse_zero_construct_resultlefttable) + (dst_negative_inverse_zero_construct_resultlefttable))) /\ (exists ge_balance_positive_inverse_zero_construct_resultlefttableentryvalue ge_balance_negative_inverse_zero_construct_resultlefttableentryvalue. (((((dst_value_inverse_zero_construct_resultlefttable) = 2 * (ge_balance_positive_inverse_zero_construct_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultlefttableentryvaluedecode. (((dst_value_inverse_zero_construct_resultlefttable) = 2 * ge_signed_half_inverse_zero_construct_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultlefttableentryvalue) = S ge_signed_half_inverse_zero_construct_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultlefttable) + ge_balance_negative_inverse_zero_construct_resultlefttableentryvalue = (dst_negative_inverse_zero_construct_resultlefttable) + ge_balance_positive_inverse_zero_construct_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_zero_construct_resultleft dc_output_inverse_zero_construct_resultleft. ~(dc_input_inverse_zero_construct_resultleft=0) -> (exists pvs_le_gap_inverse_zero_construct_resultleftdomain. pvs_le_gap_inverse_zero_construct_resultleftdomain + (dc_input_inverse_zero_construct_resultleft) = (0)) -> (exists dst_positive_code_inverse_zero_construct_resultleftlookup dst_positive_scale_inverse_zero_construct_resultleftlookup dst_negative_code_inverse_zero_construct_resultleftlookup dst_negative_scale_inverse_zero_construct_resultleftlookup dst_positive_inverse_zero_construct_resultleftlookup dst_negative_inverse_zero_construct_resultleftlookup. (((di_delta_inverse_zero_construct_result) = (((((dst_positive_code_inverse_zero_construct_resultleftlookup) + (dst_positive_scale_inverse_zero_construct_resultleftlookup)) * S ((dst_positive_code_inverse_zero_construct_resultleftlookup) + (dst_positive_scale_inverse_zero_construct_resultleftlookup)) + ((dst_positive_scale_inverse_zero_construct_resultleftlookup) + (dst_positive_scale_inverse_zero_construct_resultleftlookup))) + (((dst_negative_code_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)) * S ((dst_negative_code_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)) + ((dst_negative_scale_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)))) * S ((((dst_positive_code_inverse_zero_construct_resultleftlookup) + (dst_positive_scale_inverse_zero_construct_resultleftlookup)) * S ((dst_positive_code_inverse_zero_construct_resultleftlookup) + (dst_positive_scale_inverse_zero_construct_resultleftlookup)) + ((dst_positive_scale_inverse_zero_construct_resultleftlookup) + (dst_positive_scale_inverse_zero_construct_resultleftlookup))) + (((dst_negative_code_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)) * S ((dst_negative_code_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)) + ((dst_negative_scale_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)))) + ((((dst_negative_code_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)) * S ((dst_negative_code_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)) + ((dst_negative_scale_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup))) + (((dst_negative_code_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)) * S ((dst_negative_code_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)) + ((dst_negative_scale_inverse_zero_construct_resultleftlookup) + (dst_negative_scale_inverse_zero_construct_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftlookuppositive. ff_h_pvs_inverse_zero_construct_resultleftlookuppositive + S (dst_positive_inverse_zero_construct_resultleftlookup) = S ((S (dc_input_inverse_zero_construct_resultleft)) * dst_positive_scale_inverse_zero_construct_resultleftlookup)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftlookuppositive. dst_positive_code_inverse_zero_construct_resultleftlookup = ff_q_pvs_inverse_zero_construct_resultleftlookuppositive * S ((S (dc_input_inverse_zero_construct_resultleft)) * dst_positive_scale_inverse_zero_construct_resultleftlookup) + (dst_positive_inverse_zero_construct_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftlookupnegative. ff_h_pvs_inverse_zero_construct_resultleftlookupnegative + S (dst_negative_inverse_zero_construct_resultleftlookup) = S ((S (dc_input_inverse_zero_construct_resultleft)) * dst_negative_scale_inverse_zero_construct_resultleftlookup)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftlookupnegative. dst_negative_code_inverse_zero_construct_resultleftlookup = ff_q_pvs_inverse_zero_construct_resultleftlookupnegative * S ((S (dc_input_inverse_zero_construct_resultleft)) * dst_negative_scale_inverse_zero_construct_resultleftlookup) + (dst_negative_inverse_zero_construct_resultleftlookup))) /\ (exists ge_balance_positive_inverse_zero_construct_resultleftlookupvalue ge_balance_negative_inverse_zero_construct_resultleftlookupvalue. (((((dc_output_inverse_zero_construct_resultleft) = 2 * (ge_balance_positive_inverse_zero_construct_resultleftlookupvalue) /\ (ge_balance_negative_inverse_zero_construct_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftlookupvaluedecode. (((dc_output_inverse_zero_construct_resultleft) = 2 * ge_signed_half_inverse_zero_construct_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultleftlookupvalue) = S ge_signed_half_inverse_zero_construct_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultleftlookup) + ge_balance_negative_inverse_zero_construct_resultleftlookupvalue = (dst_negative_inverse_zero_construct_resultleftlookup) + ge_balance_positive_inverse_zero_construct_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_zero_construct_resultleft)=0)) /\ (exists dc_mask_inverse_zero_construct_resultleftvalue. ((((exists dst_positive_code_inverse_zero_construct_resultleftvaluemasktable dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable dst_negative_code_inverse_zero_construct_resultleftvaluemasktable dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable. (((dc_mask_inverse_zero_construct_resultleftvalue) = (((((dst_positive_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_zero_construct_resultleftvaluemasktable. (exists pvs_le_gap_inverse_zero_construct_resultleftvaluemasktabledomain. pvs_le_gap_inverse_zero_construct_resultleftvaluemasktabledomain + (dst_index_inverse_zero_construct_resultleftvaluemasktable) = (dc_input_inverse_zero_construct_resultleft)) -> exists dst_positive_inverse_zero_construct_resultleftvaluemasktable dst_negative_inverse_zero_construct_resultleftvaluemasktable dst_value_inverse_zero_construct_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_zero_construct_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_zero_construct_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_zero_construct_resultleftvaluemasktable) = S ((S (dst_index_inverse_zero_construct_resultleftvaluemasktable)) * dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_zero_construct_resultleftvaluemasktable = ff_q_pvs_inverse_zero_construct_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_zero_construct_resultleftvaluemasktable)) * dst_positive_scale_inverse_zero_construct_resultleftvaluemasktable) + (dst_positive_inverse_zero_construct_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_zero_construct_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_zero_construct_resultleftvaluemasktable) = S ((S (dst_index_inverse_zero_construct_resultleftvaluemasktable)) * dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_zero_construct_resultleftvaluemasktable = ff_q_pvs_inverse_zero_construct_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_zero_construct_resultleftvaluemasktable)) * dst_negative_scale_inverse_zero_construct_resultleftvaluemasktable) + (dst_negative_inverse_zero_construct_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_zero_construct_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_zero_construct_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_zero_construct_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_zero_construct_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_zero_construct_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_zero_construct_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_zero_construct_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultleftvaluemasktable) + ge_balance_negative_inverse_zero_construct_resultleftvaluemasktableentryvalue = (dst_negative_inverse_zero_construct_resultleftvaluemasktable) + ge_balance_positive_inverse_zero_construct_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_zero_construct_resultleftvaluemask dc_value_inverse_zero_construct_resultleftvaluemask. (exists pvs_le_gap_inverse_zero_construct_resultleftvaluemaskdomain. pvs_le_gap_inverse_zero_construct_resultleftvaluemaskdomain + (dc_index_inverse_zero_construct_resultleftvaluemask) = (dc_input_inverse_zero_construct_resultleft)) -> (exists dst_positive_code_inverse_zero_construct_resultleftvaluemasklookup dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup dst_positive_inverse_zero_construct_resultleftvaluemasklookup dst_negative_inverse_zero_construct_resultleftvaluemasklookup. (((dc_mask_inverse_zero_construct_resultleftvalue) = (((((dst_positive_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_zero_construct_resultleftvaluemasklookuppositive + S (dst_positive_inverse_zero_construct_resultleftvaluemasklookup) = S ((S (dc_index_inverse_zero_construct_resultleftvaluemask)) * dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftvaluemasklookuppositive. dst_positive_code_inverse_zero_construct_resultleftvaluemasklookup = ff_q_pvs_inverse_zero_construct_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_zero_construct_resultleftvaluemask)) * dst_positive_scale_inverse_zero_construct_resultleftvaluemasklookup) + (dst_positive_inverse_zero_construct_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_zero_construct_resultleftvaluemasklookupnegative + S (dst_negative_inverse_zero_construct_resultleftvaluemasklookup) = S ((S (dc_index_inverse_zero_construct_resultleftvaluemask)) * dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftvaluemasklookupnegative. dst_negative_code_inverse_zero_construct_resultleftvaluemasklookup = ff_q_pvs_inverse_zero_construct_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_zero_construct_resultleftvaluemask)) * dst_negative_scale_inverse_zero_construct_resultleftvaluemasklookup) + (dst_negative_inverse_zero_construct_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_zero_construct_resultleftvaluemasklookupvalue ge_balance_negative_inverse_zero_construct_resultleftvaluemasklookupvalue. (((((dc_value_inverse_zero_construct_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_zero_construct_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_zero_construct_resultleftvaluemask) = 2 * ge_signed_half_inverse_zero_construct_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_zero_construct_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultleftvaluemasklookup) + ge_balance_negative_inverse_zero_construct_resultleftvaluemasklookupvalue = (dst_negative_inverse_zero_construct_resultleftvaluemasklookup) + ge_balance_positive_inverse_zero_construct_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_zero_construct_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_zero_construct_resultleftvaluemaskentry dc_left_inverse_zero_construct_resultleftvaluemaskentry dc_right_inverse_zero_construct_resultleftvaluemaskentry. (((dc_input_inverse_zero_construct_resultleft)=(dc_index_inverse_zero_construct_resultleftvaluemask)*dc_quotient_inverse_zero_construct_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryleft dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft dst_positive_inverse_zero_construct_resultleftvaluemaskentryleft dst_negative_inverse_zero_construct_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_zero_construct_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_zero_construct_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_zero_construct_resultleftvaluemask)) * dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryleft = ff_q_pvs_inverse_zero_construct_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_zero_construct_resultleftvaluemask)) * dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_positive_inverse_zero_construct_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_zero_construct_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_zero_construct_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_zero_construct_resultleftvaluemask)) * dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryleft = ff_q_pvs_inverse_zero_construct_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_zero_construct_resultleftvaluemask)) * dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryleft) + (dst_negative_inverse_zero_construct_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_zero_construct_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_zero_construct_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_zero_construct_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_construct_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_zero_construct_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_zero_construct_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_zero_construct_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_zero_construct_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryright dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright dst_positive_inverse_zero_construct_resultleftvaluemaskentryright dst_negative_inverse_zero_construct_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_zero_construct_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_zero_construct_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_construct_resultleftvaluemaskentry)) * dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_zero_construct_resultleftvaluemaskentryright = ff_q_pvs_inverse_zero_construct_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_zero_construct_resultleftvaluemaskentry)) * dst_positive_scale_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_positive_inverse_zero_construct_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_zero_construct_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_zero_construct_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_construct_resultleftvaluemaskentry)) * dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_construct_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_zero_construct_resultleftvaluemaskentryright = ff_q_pvs_inverse_zero_construct_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_zero_construct_resultleftvaluemaskentry)) * dst_negative_scale_inverse_zero_construct_resultleftvaluemaskentryright) + (dst_negative_inverse_zero_construct_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_zero_construct_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_zero_construct_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_zero_construct_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_construct_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_zero_construct_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultleftvaluemaskentryright) + ge_balance_negative_inverse_zero_construct_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_zero_construct_resultleftvaluemaskentryright) + ge_balance_positive_inverse_zero_construct_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_zero_construct_resultleftvaluemaskentryproduct sto_an_inverse_zero_construct_resultleftvaluemaskentryproduct sto_bp_inverse_zero_construct_resultleftvaluemaskentryproduct sto_bn_inverse_zero_construct_resultleftvaluemaskentryproduct sto_cp_inverse_zero_construct_resultleftvaluemaskentryproduct sto_cn_inverse_zero_construct_resultleftvaluemaskentryproduct. (((((dc_left_inverse_zero_construct_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_zero_construct_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_zero_construct_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductleft. (((dc_left_inverse_zero_construct_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_zero_construct_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_zero_construct_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_zero_construct_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_zero_construct_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_zero_construct_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductright. (((dc_right_inverse_zero_construct_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_zero_construct_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_zero_construct_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_zero_construct_resultleftvaluemask) = 2 * (sto_cp_inverse_zero_construct_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_zero_construct_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_zero_construct_resultleftvaluemask) = 2 * ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_zero_construct_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_zero_construct_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_construct_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_zero_construct_resultleftvaluemaskentryproduct * sto_bp_inverse_zero_construct_resultleftvaluemaskentryproduct + sto_an_inverse_zero_construct_resultleftvaluemaskentryproduct * sto_bn_inverse_zero_construct_resultleftvaluemaskentryproduct) + sto_cn_inverse_zero_construct_resultleftvaluemaskentryproduct = (sto_ap_inverse_zero_construct_resultleftvaluemaskentryproduct * sto_bn_inverse_zero_construct_resultleftvaluemaskentryproduct + sto_an_inverse_zero_construct_resultleftvaluemaskentryproduct * sto_bp_inverse_zero_construct_resultleftvaluemaskentryproduct) + sto_cp_inverse_zero_construct_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_zero_construct_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_zero_construct_resultleftvaluemaskentrynondivisor. (dc_input_inverse_zero_construct_resultleft) = (dc_index_inverse_zero_construct_resultleftvaluemask) * pvs_factor_inverse_zero_construct_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_zero_construct_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_zero_construct_resultleftvaluefold dst_positive_scale_inverse_zero_construct_resultleftvaluefold dst_negative_code_inverse_zero_construct_resultleftvaluefold dst_negative_scale_inverse_zero_construct_resultleftvaluefold dst_positive_sum_inverse_zero_construct_resultleftvaluefold dst_negative_sum_inverse_zero_construct_resultleftvaluefold. (((dc_mask_inverse_zero_construct_resultleftvalue) = (((((dst_positive_code_inverse_zero_construct_resultleftvaluefold) + (dst_positive_scale_inverse_zero_construct_resultleftvaluefold)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluefold) + (dst_positive_scale_inverse_zero_construct_resultleftvaluefold)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluefold) + (dst_positive_scale_inverse_zero_construct_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_zero_construct_resultleftvaluefold) + (dst_positive_scale_inverse_zero_construct_resultleftvaluefold)) * S ((dst_positive_code_inverse_zero_construct_resultleftvaluefold) + (dst_positive_scale_inverse_zero_construct_resultleftvaluefold)) + ((dst_positive_scale_inverse_zero_construct_resultleftvaluefold) + (dst_positive_scale_inverse_zero_construct_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)))) + ((((dst_negative_code_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_construct_resultleftvaluefold) + (dst_negative_scale_inverse_zero_construct_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_zero_construct_resultleftvaluefoldpositive fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_zero_construct_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_zero_construct_resultleftvaluefold) = S ((S (S (dc_input_inverse_zero_construct_resultleft))) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_zero_construct_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_zero_construct_resultleft))) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_zero_construct_resultleftvaluefold))) /\ forall fs_i_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_zero_construct_resultleft)) -> exists fs_a_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_construct_resultleftvaluefold)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_zero_construct_resultleftvaluefold = fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_construct_resultleftvaluefold) + (fs_a_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_zero_construct_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive) + (fs_r_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_zero_construct_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldpositive) + (fs_s_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_zero_construct_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_zero_construct_resultleftvaluefoldnegative fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_zero_construct_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_zero_construct_resultleftvaluefold) = S ((S (S (dc_input_inverse_zero_construct_resultleft))) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_zero_construct_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_zero_construct_resultleft))) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_zero_construct_resultleftvaluefold))) /\ forall fs_i_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_zero_construct_resultleft)) -> exists fs_a_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_construct_resultleftvaluefold)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_zero_construct_resultleftvaluefold = fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_construct_resultleftvaluefold) + (fs_a_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_zero_construct_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative) + (fs_r_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_zero_construct_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_construct_resultleftvaluefoldnegative) + (fs_s_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_zero_construct_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_zero_construct_resultleftvaluefoldresult ge_balance_negative_inverse_zero_construct_resultleftvaluefoldresult. (((((dc_output_inverse_zero_construct_resultleft) = 2 * (ge_balance_positive_inverse_zero_construct_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultleftvaluefoldresultdecode. (((dc_output_inverse_zero_construct_resultleft) = 2 * ge_signed_half_inverse_zero_construct_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultleftvaluefoldresult) = S ge_signed_half_inverse_zero_construct_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_zero_construct_resultleftvaluefold) + ge_balance_negative_inverse_zero_construct_resultleftvaluefoldresult = (dst_negative_sum_inverse_zero_construct_resultleftvaluefold) + ge_balance_positive_inverse_zero_construct_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_zero_construct_resultrightleft dst_positive_scale_inverse_zero_construct_resultrightleft dst_negative_code_inverse_zero_construct_resultrightleft dst_negative_scale_inverse_zero_construct_resultrightleft. (((G) = (((((dst_positive_code_inverse_zero_construct_resultrightleft) + (dst_positive_scale_inverse_zero_construct_resultrightleft)) * S ((dst_positive_code_inverse_zero_construct_resultrightleft) + (dst_positive_scale_inverse_zero_construct_resultrightleft)) + ((dst_positive_scale_inverse_zero_construct_resultrightleft) + (dst_positive_scale_inverse_zero_construct_resultrightleft))) + (((dst_negative_code_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)) * S ((dst_negative_code_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)) + ((dst_negative_scale_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)))) * S ((((dst_positive_code_inverse_zero_construct_resultrightleft) + (dst_positive_scale_inverse_zero_construct_resultrightleft)) * S ((dst_positive_code_inverse_zero_construct_resultrightleft) + (dst_positive_scale_inverse_zero_construct_resultrightleft)) + ((dst_positive_scale_inverse_zero_construct_resultrightleft) + (dst_positive_scale_inverse_zero_construct_resultrightleft))) + (((dst_negative_code_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)) * S ((dst_negative_code_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)) + ((dst_negative_scale_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)))) + ((((dst_negative_code_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)) * S ((dst_negative_code_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)) + ((dst_negative_scale_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft))) + (((dst_negative_code_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)) * S ((dst_negative_code_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)) + ((dst_negative_scale_inverse_zero_construct_resultrightleft) + (dst_negative_scale_inverse_zero_construct_resultrightleft)))))) /\ (forall dst_index_inverse_zero_construct_resultrightleft. (exists pvs_le_gap_inverse_zero_construct_resultrightleftdomain. pvs_le_gap_inverse_zero_construct_resultrightleftdomain + (dst_index_inverse_zero_construct_resultrightleft) = (0)) -> exists dst_positive_inverse_zero_construct_resultrightleft dst_negative_inverse_zero_construct_resultrightleft dst_value_inverse_zero_construct_resultrightleft. ((((exists ff_h_pvs_inverse_zero_construct_resultrightleftentrypositive. ff_h_pvs_inverse_zero_construct_resultrightleftentrypositive + S (dst_positive_inverse_zero_construct_resultrightleft) = S ((S (dst_index_inverse_zero_construct_resultrightleft)) * dst_positive_scale_inverse_zero_construct_resultrightleft)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightleftentrypositive. dst_positive_code_inverse_zero_construct_resultrightleft = ff_q_pvs_inverse_zero_construct_resultrightleftentrypositive * S ((S (dst_index_inverse_zero_construct_resultrightleft)) * dst_positive_scale_inverse_zero_construct_resultrightleft) + (dst_positive_inverse_zero_construct_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightleftentrynegative. ff_h_pvs_inverse_zero_construct_resultrightleftentrynegative + S (dst_negative_inverse_zero_construct_resultrightleft) = S ((S (dst_index_inverse_zero_construct_resultrightleft)) * dst_negative_scale_inverse_zero_construct_resultrightleft)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightleftentrynegative. dst_negative_code_inverse_zero_construct_resultrightleft = ff_q_pvs_inverse_zero_construct_resultrightleftentrynegative * S ((S (dst_index_inverse_zero_construct_resultrightleft)) * dst_negative_scale_inverse_zero_construct_resultrightleft) + (dst_negative_inverse_zero_construct_resultrightleft))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrightleftentryvalue ge_balance_negative_inverse_zero_construct_resultrightleftentryvalue. (((((dst_value_inverse_zero_construct_resultrightleft) = 2 * (ge_balance_positive_inverse_zero_construct_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightleftentryvaluedecode. (((dst_value_inverse_zero_construct_resultrightleft) = 2 * ge_signed_half_inverse_zero_construct_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrightleftentryvalue) = S ge_signed_half_inverse_zero_construct_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultrightleft) + ge_balance_negative_inverse_zero_construct_resultrightleftentryvalue = (dst_negative_inverse_zero_construct_resultrightleft) + ge_balance_positive_inverse_zero_construct_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_construct_resultrightright dst_positive_scale_inverse_zero_construct_resultrightright dst_negative_code_inverse_zero_construct_resultrightright dst_negative_scale_inverse_zero_construct_resultrightright. (((F) = (((((dst_positive_code_inverse_zero_construct_resultrightright) + (dst_positive_scale_inverse_zero_construct_resultrightright)) * S ((dst_positive_code_inverse_zero_construct_resultrightright) + (dst_positive_scale_inverse_zero_construct_resultrightright)) + ((dst_positive_scale_inverse_zero_construct_resultrightright) + (dst_positive_scale_inverse_zero_construct_resultrightright))) + (((dst_negative_code_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)) * S ((dst_negative_code_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)) + ((dst_negative_scale_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)))) * S ((((dst_positive_code_inverse_zero_construct_resultrightright) + (dst_positive_scale_inverse_zero_construct_resultrightright)) * S ((dst_positive_code_inverse_zero_construct_resultrightright) + (dst_positive_scale_inverse_zero_construct_resultrightright)) + ((dst_positive_scale_inverse_zero_construct_resultrightright) + (dst_positive_scale_inverse_zero_construct_resultrightright))) + (((dst_negative_code_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)) * S ((dst_negative_code_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)) + ((dst_negative_scale_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)))) + ((((dst_negative_code_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)) * S ((dst_negative_code_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)) + ((dst_negative_scale_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright))) + (((dst_negative_code_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)) * S ((dst_negative_code_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)) + ((dst_negative_scale_inverse_zero_construct_resultrightright) + (dst_negative_scale_inverse_zero_construct_resultrightright)))))) /\ (forall dst_index_inverse_zero_construct_resultrightright. (exists pvs_le_gap_inverse_zero_construct_resultrightrightdomain. pvs_le_gap_inverse_zero_construct_resultrightrightdomain + (dst_index_inverse_zero_construct_resultrightright) = (0)) -> exists dst_positive_inverse_zero_construct_resultrightright dst_negative_inverse_zero_construct_resultrightright dst_value_inverse_zero_construct_resultrightright. ((((exists ff_h_pvs_inverse_zero_construct_resultrightrightentrypositive. ff_h_pvs_inverse_zero_construct_resultrightrightentrypositive + S (dst_positive_inverse_zero_construct_resultrightright) = S ((S (dst_index_inverse_zero_construct_resultrightright)) * dst_positive_scale_inverse_zero_construct_resultrightright)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightrightentrypositive. dst_positive_code_inverse_zero_construct_resultrightright = ff_q_pvs_inverse_zero_construct_resultrightrightentrypositive * S ((S (dst_index_inverse_zero_construct_resultrightright)) * dst_positive_scale_inverse_zero_construct_resultrightright) + (dst_positive_inverse_zero_construct_resultrightright))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightrightentrynegative. ff_h_pvs_inverse_zero_construct_resultrightrightentrynegative + S (dst_negative_inverse_zero_construct_resultrightright) = S ((S (dst_index_inverse_zero_construct_resultrightright)) * dst_negative_scale_inverse_zero_construct_resultrightright)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightrightentrynegative. dst_negative_code_inverse_zero_construct_resultrightright = ff_q_pvs_inverse_zero_construct_resultrightrightentrynegative * S ((S (dst_index_inverse_zero_construct_resultrightright)) * dst_negative_scale_inverse_zero_construct_resultrightright) + (dst_negative_inverse_zero_construct_resultrightright))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrightrightentryvalue ge_balance_negative_inverse_zero_construct_resultrightrightentryvalue. (((((dst_value_inverse_zero_construct_resultrightright) = 2 * (ge_balance_positive_inverse_zero_construct_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightrightentryvaluedecode. (((dst_value_inverse_zero_construct_resultrightright) = 2 * ge_signed_half_inverse_zero_construct_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrightrightentryvalue) = S ge_signed_half_inverse_zero_construct_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultrightright) + ge_balance_negative_inverse_zero_construct_resultrightrightentryvalue = (dst_negative_inverse_zero_construct_resultrightright) + ge_balance_positive_inverse_zero_construct_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_construct_resultrighttable dst_positive_scale_inverse_zero_construct_resultrighttable dst_negative_code_inverse_zero_construct_resultrighttable dst_negative_scale_inverse_zero_construct_resultrighttable. (((di_delta_inverse_zero_construct_result) = (((((dst_positive_code_inverse_zero_construct_resultrighttable) + (dst_positive_scale_inverse_zero_construct_resultrighttable)) * S ((dst_positive_code_inverse_zero_construct_resultrighttable) + (dst_positive_scale_inverse_zero_construct_resultrighttable)) + ((dst_positive_scale_inverse_zero_construct_resultrighttable) + (dst_positive_scale_inverse_zero_construct_resultrighttable))) + (((dst_negative_code_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)) * S ((dst_negative_code_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)) + ((dst_negative_scale_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)))) * S ((((dst_positive_code_inverse_zero_construct_resultrighttable) + (dst_positive_scale_inverse_zero_construct_resultrighttable)) * S ((dst_positive_code_inverse_zero_construct_resultrighttable) + (dst_positive_scale_inverse_zero_construct_resultrighttable)) + ((dst_positive_scale_inverse_zero_construct_resultrighttable) + (dst_positive_scale_inverse_zero_construct_resultrighttable))) + (((dst_negative_code_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)) * S ((dst_negative_code_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)) + ((dst_negative_scale_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)))) + ((((dst_negative_code_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)) * S ((dst_negative_code_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)) + ((dst_negative_scale_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable))) + (((dst_negative_code_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)) * S ((dst_negative_code_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)) + ((dst_negative_scale_inverse_zero_construct_resultrighttable) + (dst_negative_scale_inverse_zero_construct_resultrighttable)))))) /\ (forall dst_index_inverse_zero_construct_resultrighttable. (exists pvs_le_gap_inverse_zero_construct_resultrighttabledomain. pvs_le_gap_inverse_zero_construct_resultrighttabledomain + (dst_index_inverse_zero_construct_resultrighttable) = (0)) -> exists dst_positive_inverse_zero_construct_resultrighttable dst_negative_inverse_zero_construct_resultrighttable dst_value_inverse_zero_construct_resultrighttable. ((((exists ff_h_pvs_inverse_zero_construct_resultrighttableentrypositive. ff_h_pvs_inverse_zero_construct_resultrighttableentrypositive + S (dst_positive_inverse_zero_construct_resultrighttable) = S ((S (dst_index_inverse_zero_construct_resultrighttable)) * dst_positive_scale_inverse_zero_construct_resultrighttable)) /\ exists ff_q_pvs_inverse_zero_construct_resultrighttableentrypositive. dst_positive_code_inverse_zero_construct_resultrighttable = ff_q_pvs_inverse_zero_construct_resultrighttableentrypositive * S ((S (dst_index_inverse_zero_construct_resultrighttable)) * dst_positive_scale_inverse_zero_construct_resultrighttable) + (dst_positive_inverse_zero_construct_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrighttableentrynegative. ff_h_pvs_inverse_zero_construct_resultrighttableentrynegative + S (dst_negative_inverse_zero_construct_resultrighttable) = S ((S (dst_index_inverse_zero_construct_resultrighttable)) * dst_negative_scale_inverse_zero_construct_resultrighttable)) /\ exists ff_q_pvs_inverse_zero_construct_resultrighttableentrynegative. dst_negative_code_inverse_zero_construct_resultrighttable = ff_q_pvs_inverse_zero_construct_resultrighttableentrynegative * S ((S (dst_index_inverse_zero_construct_resultrighttable)) * dst_negative_scale_inverse_zero_construct_resultrighttable) + (dst_negative_inverse_zero_construct_resultrighttable))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrighttableentryvalue ge_balance_negative_inverse_zero_construct_resultrighttableentryvalue. (((((dst_value_inverse_zero_construct_resultrighttable) = 2 * (ge_balance_positive_inverse_zero_construct_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrighttableentryvaluedecode. (((dst_value_inverse_zero_construct_resultrighttable) = 2 * ge_signed_half_inverse_zero_construct_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrighttableentryvalue) = S ge_signed_half_inverse_zero_construct_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultrighttable) + ge_balance_negative_inverse_zero_construct_resultrighttableentryvalue = (dst_negative_inverse_zero_construct_resultrighttable) + ge_balance_positive_inverse_zero_construct_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_zero_construct_resultright dc_output_inverse_zero_construct_resultright. ~(dc_input_inverse_zero_construct_resultright=0) -> (exists pvs_le_gap_inverse_zero_construct_resultrightdomain. pvs_le_gap_inverse_zero_construct_resultrightdomain + (dc_input_inverse_zero_construct_resultright) = (0)) -> (exists dst_positive_code_inverse_zero_construct_resultrightlookup dst_positive_scale_inverse_zero_construct_resultrightlookup dst_negative_code_inverse_zero_construct_resultrightlookup dst_negative_scale_inverse_zero_construct_resultrightlookup dst_positive_inverse_zero_construct_resultrightlookup dst_negative_inverse_zero_construct_resultrightlookup. (((di_delta_inverse_zero_construct_result) = (((((dst_positive_code_inverse_zero_construct_resultrightlookup) + (dst_positive_scale_inverse_zero_construct_resultrightlookup)) * S ((dst_positive_code_inverse_zero_construct_resultrightlookup) + (dst_positive_scale_inverse_zero_construct_resultrightlookup)) + ((dst_positive_scale_inverse_zero_construct_resultrightlookup) + (dst_positive_scale_inverse_zero_construct_resultrightlookup))) + (((dst_negative_code_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)) * S ((dst_negative_code_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)) + ((dst_negative_scale_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)))) * S ((((dst_positive_code_inverse_zero_construct_resultrightlookup) + (dst_positive_scale_inverse_zero_construct_resultrightlookup)) * S ((dst_positive_code_inverse_zero_construct_resultrightlookup) + (dst_positive_scale_inverse_zero_construct_resultrightlookup)) + ((dst_positive_scale_inverse_zero_construct_resultrightlookup) + (dst_positive_scale_inverse_zero_construct_resultrightlookup))) + (((dst_negative_code_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)) * S ((dst_negative_code_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)) + ((dst_negative_scale_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)))) + ((((dst_negative_code_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)) * S ((dst_negative_code_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)) + ((dst_negative_scale_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup))) + (((dst_negative_code_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)) * S ((dst_negative_code_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)) + ((dst_negative_scale_inverse_zero_construct_resultrightlookup) + (dst_negative_scale_inverse_zero_construct_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightlookuppositive. ff_h_pvs_inverse_zero_construct_resultrightlookuppositive + S (dst_positive_inverse_zero_construct_resultrightlookup) = S ((S (dc_input_inverse_zero_construct_resultright)) * dst_positive_scale_inverse_zero_construct_resultrightlookup)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightlookuppositive. dst_positive_code_inverse_zero_construct_resultrightlookup = ff_q_pvs_inverse_zero_construct_resultrightlookuppositive * S ((S (dc_input_inverse_zero_construct_resultright)) * dst_positive_scale_inverse_zero_construct_resultrightlookup) + (dst_positive_inverse_zero_construct_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightlookupnegative. ff_h_pvs_inverse_zero_construct_resultrightlookupnegative + S (dst_negative_inverse_zero_construct_resultrightlookup) = S ((S (dc_input_inverse_zero_construct_resultright)) * dst_negative_scale_inverse_zero_construct_resultrightlookup)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightlookupnegative. dst_negative_code_inverse_zero_construct_resultrightlookup = ff_q_pvs_inverse_zero_construct_resultrightlookupnegative * S ((S (dc_input_inverse_zero_construct_resultright)) * dst_negative_scale_inverse_zero_construct_resultrightlookup) + (dst_negative_inverse_zero_construct_resultrightlookup))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrightlookupvalue ge_balance_negative_inverse_zero_construct_resultrightlookupvalue. (((((dc_output_inverse_zero_construct_resultright) = 2 * (ge_balance_positive_inverse_zero_construct_resultrightlookupvalue) /\ (ge_balance_negative_inverse_zero_construct_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightlookupvaluedecode. (((dc_output_inverse_zero_construct_resultright) = 2 * ge_signed_half_inverse_zero_construct_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrightlookupvalue) = S ge_signed_half_inverse_zero_construct_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultrightlookup) + ge_balance_negative_inverse_zero_construct_resultrightlookupvalue = (dst_negative_inverse_zero_construct_resultrightlookup) + ge_balance_positive_inverse_zero_construct_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_zero_construct_resultright)=0)) /\ (exists dc_mask_inverse_zero_construct_resultrightvalue. ((((exists dst_positive_code_inverse_zero_construct_resultrightvaluemasktable dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable dst_negative_code_inverse_zero_construct_resultrightvaluemasktable dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable. (((dc_mask_inverse_zero_construct_resultrightvalue) = (((((dst_positive_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_zero_construct_resultrightvaluemasktable. (exists pvs_le_gap_inverse_zero_construct_resultrightvaluemasktabledomain. pvs_le_gap_inverse_zero_construct_resultrightvaluemasktabledomain + (dst_index_inverse_zero_construct_resultrightvaluemasktable) = (dc_input_inverse_zero_construct_resultright)) -> exists dst_positive_inverse_zero_construct_resultrightvaluemasktable dst_negative_inverse_zero_construct_resultrightvaluemasktable dst_value_inverse_zero_construct_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_zero_construct_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_zero_construct_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_zero_construct_resultrightvaluemasktable) = S ((S (dst_index_inverse_zero_construct_resultrightvaluemasktable)) * dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_zero_construct_resultrightvaluemasktable = ff_q_pvs_inverse_zero_construct_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_zero_construct_resultrightvaluemasktable)) * dst_positive_scale_inverse_zero_construct_resultrightvaluemasktable) + (dst_positive_inverse_zero_construct_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_zero_construct_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_zero_construct_resultrightvaluemasktable) = S ((S (dst_index_inverse_zero_construct_resultrightvaluemasktable)) * dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_zero_construct_resultrightvaluemasktable = ff_q_pvs_inverse_zero_construct_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_zero_construct_resultrightvaluemasktable)) * dst_negative_scale_inverse_zero_construct_resultrightvaluemasktable) + (dst_negative_inverse_zero_construct_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_zero_construct_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_zero_construct_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_zero_construct_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_zero_construct_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_zero_construct_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_zero_construct_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultrightvaluemasktable) + ge_balance_negative_inverse_zero_construct_resultrightvaluemasktableentryvalue = (dst_negative_inverse_zero_construct_resultrightvaluemasktable) + ge_balance_positive_inverse_zero_construct_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_zero_construct_resultrightvaluemask dc_value_inverse_zero_construct_resultrightvaluemask. (exists pvs_le_gap_inverse_zero_construct_resultrightvaluemaskdomain. pvs_le_gap_inverse_zero_construct_resultrightvaluemaskdomain + (dc_index_inverse_zero_construct_resultrightvaluemask) = (dc_input_inverse_zero_construct_resultright)) -> (exists dst_positive_code_inverse_zero_construct_resultrightvaluemasklookup dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup dst_positive_inverse_zero_construct_resultrightvaluemasklookup dst_negative_inverse_zero_construct_resultrightvaluemasklookup. (((dc_mask_inverse_zero_construct_resultrightvalue) = (((((dst_positive_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_zero_construct_resultrightvaluemasklookuppositive + S (dst_positive_inverse_zero_construct_resultrightvaluemasklookup) = S ((S (dc_index_inverse_zero_construct_resultrightvaluemask)) * dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightvaluemasklookuppositive. dst_positive_code_inverse_zero_construct_resultrightvaluemasklookup = ff_q_pvs_inverse_zero_construct_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_zero_construct_resultrightvaluemask)) * dst_positive_scale_inverse_zero_construct_resultrightvaluemasklookup) + (dst_positive_inverse_zero_construct_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_zero_construct_resultrightvaluemasklookupnegative + S (dst_negative_inverse_zero_construct_resultrightvaluemasklookup) = S ((S (dc_index_inverse_zero_construct_resultrightvaluemask)) * dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightvaluemasklookupnegative. dst_negative_code_inverse_zero_construct_resultrightvaluemasklookup = ff_q_pvs_inverse_zero_construct_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_zero_construct_resultrightvaluemask)) * dst_negative_scale_inverse_zero_construct_resultrightvaluemasklookup) + (dst_negative_inverse_zero_construct_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrightvaluemasklookupvalue ge_balance_negative_inverse_zero_construct_resultrightvaluemasklookupvalue. (((((dc_value_inverse_zero_construct_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_zero_construct_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_zero_construct_resultrightvaluemask) = 2 * ge_signed_half_inverse_zero_construct_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_zero_construct_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultrightvaluemasklookup) + ge_balance_negative_inverse_zero_construct_resultrightvaluemasklookupvalue = (dst_negative_inverse_zero_construct_resultrightvaluemasklookup) + ge_balance_positive_inverse_zero_construct_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_zero_construct_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_zero_construct_resultrightvaluemaskentry dc_left_inverse_zero_construct_resultrightvaluemaskentry dc_right_inverse_zero_construct_resultrightvaluemaskentry. (((dc_input_inverse_zero_construct_resultright)=(dc_index_inverse_zero_construct_resultrightvaluemask)*dc_quotient_inverse_zero_construct_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryleft dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft dst_positive_inverse_zero_construct_resultrightvaluemaskentryleft dst_negative_inverse_zero_construct_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_zero_construct_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_zero_construct_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_zero_construct_resultrightvaluemask)) * dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryleft = ff_q_pvs_inverse_zero_construct_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_zero_construct_resultrightvaluemask)) * dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_positive_inverse_zero_construct_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_zero_construct_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_zero_construct_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_zero_construct_resultrightvaluemask)) * dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryleft = ff_q_pvs_inverse_zero_construct_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_zero_construct_resultrightvaluemask)) * dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryleft) + (dst_negative_inverse_zero_construct_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_zero_construct_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_zero_construct_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_construct_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_zero_construct_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_zero_construct_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_zero_construct_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_zero_construct_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryright dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright dst_positive_inverse_zero_construct_resultrightvaluemaskentryright dst_negative_inverse_zero_construct_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_zero_construct_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_zero_construct_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_construct_resultrightvaluemaskentry)) * dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_zero_construct_resultrightvaluemaskentryright = ff_q_pvs_inverse_zero_construct_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_zero_construct_resultrightvaluemaskentry)) * dst_positive_scale_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_positive_inverse_zero_construct_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_zero_construct_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_zero_construct_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_zero_construct_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_construct_resultrightvaluemaskentry)) * dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_construct_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_zero_construct_resultrightvaluemaskentryright = ff_q_pvs_inverse_zero_construct_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_zero_construct_resultrightvaluemaskentry)) * dst_negative_scale_inverse_zero_construct_resultrightvaluemaskentryright) + (dst_negative_inverse_zero_construct_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_zero_construct_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_zero_construct_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_construct_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_zero_construct_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_zero_construct_resultrightvaluemaskentryright) + ge_balance_negative_inverse_zero_construct_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_zero_construct_resultrightvaluemaskentryright) + ge_balance_positive_inverse_zero_construct_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_zero_construct_resultrightvaluemaskentryproduct sto_an_inverse_zero_construct_resultrightvaluemaskentryproduct sto_bp_inverse_zero_construct_resultrightvaluemaskentryproduct sto_bn_inverse_zero_construct_resultrightvaluemaskentryproduct sto_cp_inverse_zero_construct_resultrightvaluemaskentryproduct sto_cn_inverse_zero_construct_resultrightvaluemaskentryproduct. (((((dc_left_inverse_zero_construct_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_zero_construct_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_zero_construct_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductleft. (((dc_left_inverse_zero_construct_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_zero_construct_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_zero_construct_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_zero_construct_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_zero_construct_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_zero_construct_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductright. (((dc_right_inverse_zero_construct_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_zero_construct_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_zero_construct_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_zero_construct_resultrightvaluemask) = 2 * (sto_cp_inverse_zero_construct_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_zero_construct_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_zero_construct_resultrightvaluemask) = 2 * ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_zero_construct_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_zero_construct_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_construct_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_zero_construct_resultrightvaluemaskentryproduct * sto_bp_inverse_zero_construct_resultrightvaluemaskentryproduct + sto_an_inverse_zero_construct_resultrightvaluemaskentryproduct * sto_bn_inverse_zero_construct_resultrightvaluemaskentryproduct) + sto_cn_inverse_zero_construct_resultrightvaluemaskentryproduct = (sto_ap_inverse_zero_construct_resultrightvaluemaskentryproduct * sto_bn_inverse_zero_construct_resultrightvaluemaskentryproduct + sto_an_inverse_zero_construct_resultrightvaluemaskentryproduct * sto_bp_inverse_zero_construct_resultrightvaluemaskentryproduct) + sto_cp_inverse_zero_construct_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_zero_construct_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_zero_construct_resultrightvaluemaskentrynondivisor. (dc_input_inverse_zero_construct_resultright) = (dc_index_inverse_zero_construct_resultrightvaluemask) * pvs_factor_inverse_zero_construct_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_zero_construct_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_zero_construct_resultrightvaluefold dst_positive_scale_inverse_zero_construct_resultrightvaluefold dst_negative_code_inverse_zero_construct_resultrightvaluefold dst_negative_scale_inverse_zero_construct_resultrightvaluefold dst_positive_sum_inverse_zero_construct_resultrightvaluefold dst_negative_sum_inverse_zero_construct_resultrightvaluefold. (((dc_mask_inverse_zero_construct_resultrightvalue) = (((((dst_positive_code_inverse_zero_construct_resultrightvaluefold) + (dst_positive_scale_inverse_zero_construct_resultrightvaluefold)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluefold) + (dst_positive_scale_inverse_zero_construct_resultrightvaluefold)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluefold) + (dst_positive_scale_inverse_zero_construct_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_zero_construct_resultrightvaluefold) + (dst_positive_scale_inverse_zero_construct_resultrightvaluefold)) * S ((dst_positive_code_inverse_zero_construct_resultrightvaluefold) + (dst_positive_scale_inverse_zero_construct_resultrightvaluefold)) + ((dst_positive_scale_inverse_zero_construct_resultrightvaluefold) + (dst_positive_scale_inverse_zero_construct_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)))) + ((((dst_negative_code_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_construct_resultrightvaluefold) + (dst_negative_scale_inverse_zero_construct_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_zero_construct_resultrightvaluefoldpositive fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_zero_construct_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_zero_construct_resultrightvaluefold) = S ((S (S (dc_input_inverse_zero_construct_resultright))) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_zero_construct_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_zero_construct_resultright))) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_zero_construct_resultrightvaluefold))) /\ forall fs_i_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_zero_construct_resultright)) -> exists fs_a_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_construct_resultrightvaluefold)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_zero_construct_resultrightvaluefold = fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_construct_resultrightvaluefold) + (fs_a_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_zero_construct_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive) + (fs_r_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_zero_construct_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldpositive) + (fs_s_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_zero_construct_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_zero_construct_resultrightvaluefoldnegative fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_zero_construct_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_zero_construct_resultrightvaluefold) = S ((S (S (dc_input_inverse_zero_construct_resultright))) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_zero_construct_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_zero_construct_resultright))) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_zero_construct_resultrightvaluefold))) /\ forall fs_i_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_zero_construct_resultright)) -> exists fs_a_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_construct_resultrightvaluefold)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_zero_construct_resultrightvaluefold = fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_construct_resultrightvaluefold) + (fs_a_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_zero_construct_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative) + (fs_r_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_zero_construct_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_construct_resultrightvaluefoldnegative) + (fs_s_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_zero_construct_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_zero_construct_resultrightvaluefoldresult ge_balance_negative_inverse_zero_construct_resultrightvaluefoldresult. (((((dc_output_inverse_zero_construct_resultright) = 2 * (ge_balance_positive_inverse_zero_construct_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_zero_construct_resultrightvaluefoldresultdecode. (((dc_output_inverse_zero_construct_resultright) = 2 * ge_signed_half_inverse_zero_construct_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_zero_construct_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_zero_construct_resultrightvaluefoldresult) = S ge_signed_half_inverse_zero_construct_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_zero_construct_resultrightvaluefold) + ge_balance_negative_inverse_zero_construct_resultrightvaluefoldresult = (dst_negative_sum_inverse_zero_construct_resultrightvaluefold) + ge_balance_positive_inverse_zero_construct_resultrightvaluefoldresult)))))))))))))))))))))))) /\ (exists dst_positive_code_inverse_zero_construct_zero dst_positive_scale_inverse_zero_construct_zero dst_negative_code_inverse_zero_construct_zero dst_negative_scale_inverse_zero_construct_zero dst_positive_inverse_zero_construct_zero dst_negative_inverse_zero_construct_zero. (((G) = (((((dst_positive_code_inverse_zero_construct_zero) + (dst_positive_scale_inverse_zero_construct_zero)) * S ((dst_positive_code_inverse_zero_construct_zero) + (dst_positive_scale_inverse_zero_construct_zero)) + ((dst_positive_scale_inverse_zero_construct_zero) + (dst_positive_scale_inverse_zero_construct_zero))) + (((dst_negative_code_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)) * S ((dst_negative_code_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)) + ((dst_negative_scale_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)))) * S ((((dst_positive_code_inverse_zero_construct_zero) + (dst_positive_scale_inverse_zero_construct_zero)) * S ((dst_positive_code_inverse_zero_construct_zero) + (dst_positive_scale_inverse_zero_construct_zero)) + ((dst_positive_scale_inverse_zero_construct_zero) + (dst_positive_scale_inverse_zero_construct_zero))) + (((dst_negative_code_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)) * S ((dst_negative_code_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)) + ((dst_negative_scale_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)))) + ((((dst_negative_code_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)) * S ((dst_negative_code_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)) + ((dst_negative_scale_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero))) + (((dst_negative_code_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)) * S ((dst_negative_code_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)) + ((dst_negative_scale_inverse_zero_construct_zero) + (dst_negative_scale_inverse_zero_construct_zero)))))) /\ (((((exists ff_h_pvs_inverse_zero_construct_zeropositive. ff_h_pvs_inverse_zero_construct_zeropositive + S (dst_positive_inverse_zero_construct_zero) = S ((S (0)) * dst_positive_scale_inverse_zero_construct_zero)) /\ exists ff_q_pvs_inverse_zero_construct_zeropositive. dst_positive_code_inverse_zero_construct_zero = ff_q_pvs_inverse_zero_construct_zeropositive * S ((S (0)) * dst_positive_scale_inverse_zero_construct_zero) + (dst_positive_inverse_zero_construct_zero))) /\ (((((exists ff_h_pvs_inverse_zero_construct_zeronegative. ff_h_pvs_inverse_zero_construct_zeronegative + S (dst_negative_inverse_zero_construct_zero) = S ((S (0)) * dst_negative_scale_inverse_zero_construct_zero)) /\ exists ff_q_pvs_inverse_zero_construct_zeronegative. dst_negative_code_inverse_zero_construct_zero = ff_q_pvs_inverse_zero_construct_zeronegative * S ((S (0)) * dst_negative_scale_inverse_zero_construct_zero) + (dst_negative_inverse_zero_construct_zero))) /\ (exists ge_balance_positive_inverse_zero_construct_zerovalue ge_balance_negative_inverse_zero_construct_zerovalue. (((((w) = 2 * (ge_balance_positive_inverse_zero_construct_zerovalue) /\ (ge_balance_negative_inverse_zero_construct_zerovalue) = 0) \/ exists ge_signed_half_inverse_zero_construct_zerovaluedecode. (((w) = 2 * ge_signed_half_inverse_zero_construct_zerovaluedecode + 1 /\ (ge_balance_positive_inverse_zero_construct_zerovalue) = 0) /\ (ge_balance_negative_inverse_zero_construct_zerovalue) = S ge_signed_half_inverse_zero_construct_zerovaluedecode))) /\ ((dst_positive_inverse_zero_construct_zero) + ge_balance_negative_inverse_zero_construct_zerovalue = (dst_negative_inverse_zero_construct_zero) + ge_balance_positive_inverse_zero_construct_zerovalue))))))))))Complete tactic proof in conservative notation
All 16 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
16 script commands · 6 reading checkpoints · 1 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–3
02Establish hgL4–6
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table singleton.
- L4
have hg : ∃ G. ArithTable(0,G) ∧ ArithAt(G,0,w)Definitions: ArithTable(0,G)ArithAt(G,0,w)Original native command in the exact edition - L5
specialize arithmetic_signed_table_singleton (w) - L6
apply arithmetic_signed_table_singleton
03Separate the logical casesL7–8
04Construct an explicit witnessL9–9
Supply the displayed value, then prove that it has the required property.
- L9
exists x
05Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
split
Original defined command ledger · 16 lines
- 0001
intro F - 0002
intro w - 0003
intro hF - 0004
have hg : ∃ G. ArithTable(0,G) ∧ ArithAt(G,0,w) - 0005
specialize arithmetic_signed_table_singleton (w) - 0006
apply arithmetic_signed_table_singleton - 0007
cases hg - 0008
cases hg_witness - 0009
exists x - 0010
split - 0011
specialize dirichlet_inverse_zero (F) - 0012
specialize dirichlet_inverse_zero (x) - 0013
apply dirichlet_inverse_zero - 0014
exact hF - 0015
exact hg_witness_left - 0016
exact hg_witness_right