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. ∀ G. ArithTable(0,F) → ArithTable(0,G) → DirichletInverse(0,F,G)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order statement
forall F G. (exists dst_positive_code_inverse_zero_left dst_positive_scale_inverse_zero_left dst_negative_code_inverse_zero_left dst_negative_scale_inverse_zero_left. (((F) = (((((dst_positive_code_inverse_zero_left) + (dst_positive_scale_inverse_zero_left)) * S ((dst_positive_code_inverse_zero_left) + (dst_positive_scale_inverse_zero_left)) + ((dst_positive_scale_inverse_zero_left) + (dst_positive_scale_inverse_zero_left))) + (((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) * S ((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) + ((dst_negative_scale_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)))) * S ((((dst_positive_code_inverse_zero_left) + (dst_positive_scale_inverse_zero_left)) * S ((dst_positive_code_inverse_zero_left) + (dst_positive_scale_inverse_zero_left)) + ((dst_positive_scale_inverse_zero_left) + (dst_positive_scale_inverse_zero_left))) + (((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) * S ((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) + ((dst_negative_scale_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)))) + ((((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) * S ((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) + ((dst_negative_scale_inverse_zero_left) + (dst_negative_scale_inverse_zero_left))) + (((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) * S ((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) + ((dst_negative_scale_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)))))) /\ (forall dst_index_inverse_zero_left. (exists pvs_le_gap_inverse_zero_leftdomain. pvs_le_gap_inverse_zero_leftdomain + (dst_index_inverse_zero_left) = (0)) -> exists dst_positive_inverse_zero_left dst_negative_inverse_zero_left dst_value_inverse_zero_left. ((((exists ff_h_pvs_inverse_zero_leftentrypositive. ff_h_pvs_inverse_zero_leftentrypositive + S (dst_positive_inverse_zero_left) = S ((S (dst_index_inverse_zero_left)) * dst_positive_scale_inverse_zero_left)) /\ exists ff_q_pvs_inverse_zero_leftentrypositive. dst_positive_code_inverse_zero_left = ff_q_pvs_inverse_zero_leftentrypositive * S ((S (dst_index_inverse_zero_left)) * dst_positive_scale_inverse_zero_left) + (dst_positive_inverse_zero_left))) /\ (((((exists ff_h_pvs_inverse_zero_leftentrynegative. ff_h_pvs_inverse_zero_leftentrynegative + S (dst_negative_inverse_zero_left) = S ((S (dst_index_inverse_zero_left)) * dst_negative_scale_inverse_zero_left)) /\ exists ff_q_pvs_inverse_zero_leftentrynegative. dst_negative_code_inverse_zero_left = ff_q_pvs_inverse_zero_leftentrynegative * S ((S (dst_index_inverse_zero_left)) * dst_negative_scale_inverse_zero_left) + (dst_negative_inverse_zero_left))) /\ (exists ge_balance_positive_inverse_zero_leftentryvalue ge_balance_negative_inverse_zero_leftentryvalue. (((((dst_value_inverse_zero_left) = 2 * (ge_balance_positive_inverse_zero_leftentryvalue) /\ (ge_balance_negative_inverse_zero_leftentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_leftentryvaluedecode. (((dst_value_inverse_zero_left) = 2 * ge_signed_half_inverse_zero_leftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_leftentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_leftentryvalue) = S ge_signed_half_inverse_zero_leftentryvaluedecode))) /\ ((dst_positive_inverse_zero_left) + ge_balance_negative_inverse_zero_leftentryvalue = (dst_negative_inverse_zero_left) + ge_balance_positive_inverse_zero_leftentryvalue))))))))) -> (exists dst_positive_code_inverse_zero_right dst_positive_scale_inverse_zero_right dst_negative_code_inverse_zero_right dst_negative_scale_inverse_zero_right. (((G) = (((((dst_positive_code_inverse_zero_right) + (dst_positive_scale_inverse_zero_right)) * S ((dst_positive_code_inverse_zero_right) + (dst_positive_scale_inverse_zero_right)) + ((dst_positive_scale_inverse_zero_right) + (dst_positive_scale_inverse_zero_right))) + (((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) * S ((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) + ((dst_negative_scale_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)))) * S ((((dst_positive_code_inverse_zero_right) + (dst_positive_scale_inverse_zero_right)) * S ((dst_positive_code_inverse_zero_right) + (dst_positive_scale_inverse_zero_right)) + ((dst_positive_scale_inverse_zero_right) + (dst_positive_scale_inverse_zero_right))) + (((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) * S ((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) + ((dst_negative_scale_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)))) + ((((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) * S ((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) + ((dst_negative_scale_inverse_zero_right) + (dst_negative_scale_inverse_zero_right))) + (((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) * S ((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) + ((dst_negative_scale_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)))))) /\ (forall dst_index_inverse_zero_right. (exists pvs_le_gap_inverse_zero_rightdomain. pvs_le_gap_inverse_zero_rightdomain + (dst_index_inverse_zero_right) = (0)) -> exists dst_positive_inverse_zero_right dst_negative_inverse_zero_right dst_value_inverse_zero_right. ((((exists ff_h_pvs_inverse_zero_rightentrypositive. ff_h_pvs_inverse_zero_rightentrypositive + S (dst_positive_inverse_zero_right) = S ((S (dst_index_inverse_zero_right)) * dst_positive_scale_inverse_zero_right)) /\ exists ff_q_pvs_inverse_zero_rightentrypositive. dst_positive_code_inverse_zero_right = ff_q_pvs_inverse_zero_rightentrypositive * S ((S (dst_index_inverse_zero_right)) * dst_positive_scale_inverse_zero_right) + (dst_positive_inverse_zero_right))) /\ (((((exists ff_h_pvs_inverse_zero_rightentrynegative. ff_h_pvs_inverse_zero_rightentrynegative + S (dst_negative_inverse_zero_right) = S ((S (dst_index_inverse_zero_right)) * dst_negative_scale_inverse_zero_right)) /\ exists ff_q_pvs_inverse_zero_rightentrynegative. dst_negative_code_inverse_zero_right = ff_q_pvs_inverse_zero_rightentrynegative * S ((S (dst_index_inverse_zero_right)) * dst_negative_scale_inverse_zero_right) + (dst_negative_inverse_zero_right))) /\ (exists ge_balance_positive_inverse_zero_rightentryvalue ge_balance_negative_inverse_zero_rightentryvalue. (((((dst_value_inverse_zero_right) = 2 * (ge_balance_positive_inverse_zero_rightentryvalue) /\ (ge_balance_negative_inverse_zero_rightentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_rightentryvaluedecode. (((dst_value_inverse_zero_right) = 2 * ge_signed_half_inverse_zero_rightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_rightentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_rightentryvalue) = S ge_signed_half_inverse_zero_rightentryvaluedecode))) /\ ((dst_positive_inverse_zero_right) + ge_balance_negative_inverse_zero_rightentryvalue = (dst_negative_inverse_zero_right) + ge_balance_positive_inverse_zero_rightentryvalue))))))))) -> (exists di_delta_inverse_zero_result. ((((exists dst_positive_code_inverse_zero_resultdeltatable dst_positive_scale_inverse_zero_resultdeltatable dst_negative_code_inverse_zero_resultdeltatable dst_negative_scale_inverse_zero_resultdeltatable. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable)) * S ((dst_positive_code_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable)) + ((dst_positive_scale_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable))) + (((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) * S ((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) + ((dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)))) * S ((((dst_positive_code_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable)) * S ((dst_positive_code_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable)) + ((dst_positive_scale_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable))) + (((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) * S ((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) + ((dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)))) + ((((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) * S ((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) + ((dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable))) + (((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) * S ((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) + ((dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)))))) /\ (forall dst_index_inverse_zero_resultdeltatable. (exists pvs_le_gap_inverse_zero_resultdeltatabledomain. pvs_le_gap_inverse_zero_resultdeltatabledomain + (dst_index_inverse_zero_resultdeltatable) = (0)) -> exists dst_positive_inverse_zero_resultdeltatable dst_negative_inverse_zero_resultdeltatable dst_value_inverse_zero_resultdeltatable. ((((exists ff_h_pvs_inverse_zero_resultdeltatableentrypositive. ff_h_pvs_inverse_zero_resultdeltatableentrypositive + S (dst_positive_inverse_zero_resultdeltatable) = S ((S (dst_index_inverse_zero_resultdeltatable)) * dst_positive_scale_inverse_zero_resultdeltatable)) /\ exists ff_q_pvs_inverse_zero_resultdeltatableentrypositive. dst_positive_code_inverse_zero_resultdeltatable = ff_q_pvs_inverse_zero_resultdeltatableentrypositive * S ((S (dst_index_inverse_zero_resultdeltatable)) * dst_positive_scale_inverse_zero_resultdeltatable) + (dst_positive_inverse_zero_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_zero_resultdeltatableentrynegative. ff_h_pvs_inverse_zero_resultdeltatableentrynegative + S (dst_negative_inverse_zero_resultdeltatable) = S ((S (dst_index_inverse_zero_resultdeltatable)) * dst_negative_scale_inverse_zero_resultdeltatable)) /\ exists ff_q_pvs_inverse_zero_resultdeltatableentrynegative. dst_negative_code_inverse_zero_resultdeltatable = ff_q_pvs_inverse_zero_resultdeltatableentrynegative * S ((S (dst_index_inverse_zero_resultdeltatable)) * dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_inverse_zero_resultdeltatable))) /\ (exists ge_balance_positive_inverse_zero_resultdeltatableentryvalue ge_balance_negative_inverse_zero_resultdeltatableentryvalue. (((((dst_value_inverse_zero_resultdeltatable) = 2 * (ge_balance_positive_inverse_zero_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_zero_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultdeltatableentryvaluedecode. (((dst_value_inverse_zero_resultdeltatable) = 2 * ge_signed_half_inverse_zero_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultdeltatableentryvalue) = S ge_signed_half_inverse_zero_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultdeltatable) + ge_balance_negative_inverse_zero_resultdeltatableentryvalue = (dst_negative_inverse_zero_resultdeltatable) + ge_balance_positive_inverse_zero_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_zero_resultdelta du_value_inverse_zero_resultdelta. ~(du_index_inverse_zero_resultdelta=0) -> (exists pvs_le_gap_inverse_zero_resultdeltabound. pvs_le_gap_inverse_zero_resultdeltabound + (du_index_inverse_zero_resultdelta) = (0)) -> (exists dst_positive_code_inverse_zero_resultdeltaentry dst_positive_scale_inverse_zero_resultdeltaentry dst_negative_code_inverse_zero_resultdeltaentry dst_negative_scale_inverse_zero_resultdeltaentry dst_positive_inverse_zero_resultdeltaentry dst_negative_inverse_zero_resultdeltaentry. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry)) * S ((dst_positive_code_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry)) + ((dst_positive_scale_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry))) + (((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)))) * S ((((dst_positive_code_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry)) * S ((dst_positive_code_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry)) + ((dst_positive_scale_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry))) + (((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)))) + ((((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry))) + (((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultdeltaentrypositive. ff_h_pvs_inverse_zero_resultdeltaentrypositive + S (dst_positive_inverse_zero_resultdeltaentry) = S ((S (du_index_inverse_zero_resultdelta)) * dst_positive_scale_inverse_zero_resultdeltaentry)) /\ exists ff_q_pvs_inverse_zero_resultdeltaentrypositive. dst_positive_code_inverse_zero_resultdeltaentry = ff_q_pvs_inverse_zero_resultdeltaentrypositive * S ((S (du_index_inverse_zero_resultdelta)) * dst_positive_scale_inverse_zero_resultdeltaentry) + (dst_positive_inverse_zero_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_zero_resultdeltaentrynegative. ff_h_pvs_inverse_zero_resultdeltaentrynegative + S (dst_negative_inverse_zero_resultdeltaentry) = S ((S (du_index_inverse_zero_resultdelta)) * dst_negative_scale_inverse_zero_resultdeltaentry)) /\ exists ff_q_pvs_inverse_zero_resultdeltaentrynegative. dst_negative_code_inverse_zero_resultdeltaentry = ff_q_pvs_inverse_zero_resultdeltaentrynegative * S ((S (du_index_inverse_zero_resultdelta)) * dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_inverse_zero_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_zero_resultdeltaentryvalue ge_balance_negative_inverse_zero_resultdeltaentryvalue. (((((du_value_inverse_zero_resultdelta) = 2 * (ge_balance_positive_inverse_zero_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_zero_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultdeltaentryvaluedecode. (((du_value_inverse_zero_resultdelta) = 2 * ge_signed_half_inverse_zero_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultdeltaentryvalue) = S ge_signed_half_inverse_zero_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultdeltaentry) + ge_balance_negative_inverse_zero_resultdeltaentryvalue = (dst_negative_inverse_zero_resultdeltaentry) + ge_balance_positive_inverse_zero_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_zero_resultdelta)=1 -> (du_value_inverse_zero_resultdelta)=2) /\ (~((du_index_inverse_zero_resultdelta)=1) -> (du_value_inverse_zero_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_zero_resultleftleft dst_positive_scale_inverse_zero_resultleftleft dst_negative_code_inverse_zero_resultleftleft dst_negative_scale_inverse_zero_resultleftleft. (((F) = (((((dst_positive_code_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft)) * S ((dst_positive_code_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft)) + ((dst_positive_scale_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft))) + (((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) * S ((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) + ((dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)))) * S ((((dst_positive_code_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft)) * S ((dst_positive_code_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft)) + ((dst_positive_scale_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft))) + (((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) * S ((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) + ((dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)))) + ((((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) * S ((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) + ((dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft))) + (((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) * S ((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) + ((dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)))))) /\ (forall dst_index_inverse_zero_resultleftleft. (exists pvs_le_gap_inverse_zero_resultleftleftdomain. pvs_le_gap_inverse_zero_resultleftleftdomain + (dst_index_inverse_zero_resultleftleft) = (0)) -> exists dst_positive_inverse_zero_resultleftleft dst_negative_inverse_zero_resultleftleft dst_value_inverse_zero_resultleftleft. ((((exists ff_h_pvs_inverse_zero_resultleftleftentrypositive. ff_h_pvs_inverse_zero_resultleftleftentrypositive + S (dst_positive_inverse_zero_resultleftleft) = S ((S (dst_index_inverse_zero_resultleftleft)) * dst_positive_scale_inverse_zero_resultleftleft)) /\ exists ff_q_pvs_inverse_zero_resultleftleftentrypositive. dst_positive_code_inverse_zero_resultleftleft = ff_q_pvs_inverse_zero_resultleftleftentrypositive * S ((S (dst_index_inverse_zero_resultleftleft)) * dst_positive_scale_inverse_zero_resultleftleft) + (dst_positive_inverse_zero_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftleftentrynegative. ff_h_pvs_inverse_zero_resultleftleftentrynegative + S (dst_negative_inverse_zero_resultleftleft) = S ((S (dst_index_inverse_zero_resultleftleft)) * dst_negative_scale_inverse_zero_resultleftleft)) /\ exists ff_q_pvs_inverse_zero_resultleftleftentrynegative. dst_negative_code_inverse_zero_resultleftleft = ff_q_pvs_inverse_zero_resultleftleftentrynegative * S ((S (dst_index_inverse_zero_resultleftleft)) * dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_inverse_zero_resultleftleft))) /\ (exists ge_balance_positive_inverse_zero_resultleftleftentryvalue ge_balance_negative_inverse_zero_resultleftleftentryvalue. (((((dst_value_inverse_zero_resultleftleft) = 2 * (ge_balance_positive_inverse_zero_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_zero_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftleftentryvaluedecode. (((dst_value_inverse_zero_resultleftleft) = 2 * ge_signed_half_inverse_zero_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftleftentryvalue) = S ge_signed_half_inverse_zero_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftleft) + ge_balance_negative_inverse_zero_resultleftleftentryvalue = (dst_negative_inverse_zero_resultleftleft) + ge_balance_positive_inverse_zero_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultleftright dst_positive_scale_inverse_zero_resultleftright dst_negative_code_inverse_zero_resultleftright dst_negative_scale_inverse_zero_resultleftright. (((G) = (((((dst_positive_code_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright)) * S ((dst_positive_code_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright)) + ((dst_positive_scale_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright))) + (((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) * S ((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) + ((dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)))) * S ((((dst_positive_code_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright)) * S ((dst_positive_code_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright)) + ((dst_positive_scale_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright))) + (((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) * S ((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) + ((dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)))) + ((((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) * S ((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) + ((dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright))) + (((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) * S ((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) + ((dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)))))) /\ (forall dst_index_inverse_zero_resultleftright. (exists pvs_le_gap_inverse_zero_resultleftrightdomain. pvs_le_gap_inverse_zero_resultleftrightdomain + (dst_index_inverse_zero_resultleftright) = (0)) -> exists dst_positive_inverse_zero_resultleftright dst_negative_inverse_zero_resultleftright dst_value_inverse_zero_resultleftright. ((((exists ff_h_pvs_inverse_zero_resultleftrightentrypositive. ff_h_pvs_inverse_zero_resultleftrightentrypositive + S (dst_positive_inverse_zero_resultleftright) = S ((S (dst_index_inverse_zero_resultleftright)) * dst_positive_scale_inverse_zero_resultleftright)) /\ exists ff_q_pvs_inverse_zero_resultleftrightentrypositive. dst_positive_code_inverse_zero_resultleftright = ff_q_pvs_inverse_zero_resultleftrightentrypositive * S ((S (dst_index_inverse_zero_resultleftright)) * dst_positive_scale_inverse_zero_resultleftright) + (dst_positive_inverse_zero_resultleftright))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftrightentrynegative. ff_h_pvs_inverse_zero_resultleftrightentrynegative + S (dst_negative_inverse_zero_resultleftright) = S ((S (dst_index_inverse_zero_resultleftright)) * dst_negative_scale_inverse_zero_resultleftright)) /\ exists ff_q_pvs_inverse_zero_resultleftrightentrynegative. dst_negative_code_inverse_zero_resultleftright = ff_q_pvs_inverse_zero_resultleftrightentrynegative * S ((S (dst_index_inverse_zero_resultleftright)) * dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_inverse_zero_resultleftright))) /\ (exists ge_balance_positive_inverse_zero_resultleftrightentryvalue ge_balance_negative_inverse_zero_resultleftrightentryvalue. (((((dst_value_inverse_zero_resultleftright) = 2 * (ge_balance_positive_inverse_zero_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_zero_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftrightentryvaluedecode. (((dst_value_inverse_zero_resultleftright) = 2 * ge_signed_half_inverse_zero_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftrightentryvalue) = S ge_signed_half_inverse_zero_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftright) + ge_balance_negative_inverse_zero_resultleftrightentryvalue = (dst_negative_inverse_zero_resultleftright) + ge_balance_positive_inverse_zero_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultlefttable dst_positive_scale_inverse_zero_resultlefttable dst_negative_code_inverse_zero_resultlefttable dst_negative_scale_inverse_zero_resultlefttable. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable)) * S ((dst_positive_code_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable)) + ((dst_positive_scale_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable))) + (((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) * S ((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) + ((dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)))) * S ((((dst_positive_code_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable)) * S ((dst_positive_code_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable)) + ((dst_positive_scale_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable))) + (((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) * S ((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) + ((dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)))) + ((((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) * S ((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) + ((dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable))) + (((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) * S ((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) + ((dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)))))) /\ (forall dst_index_inverse_zero_resultlefttable. (exists pvs_le_gap_inverse_zero_resultlefttabledomain. pvs_le_gap_inverse_zero_resultlefttabledomain + (dst_index_inverse_zero_resultlefttable) = (0)) -> exists dst_positive_inverse_zero_resultlefttable dst_negative_inverse_zero_resultlefttable dst_value_inverse_zero_resultlefttable. ((((exists ff_h_pvs_inverse_zero_resultlefttableentrypositive. ff_h_pvs_inverse_zero_resultlefttableentrypositive + S (dst_positive_inverse_zero_resultlefttable) = S ((S (dst_index_inverse_zero_resultlefttable)) * dst_positive_scale_inverse_zero_resultlefttable)) /\ exists ff_q_pvs_inverse_zero_resultlefttableentrypositive. dst_positive_code_inverse_zero_resultlefttable = ff_q_pvs_inverse_zero_resultlefttableentrypositive * S ((S (dst_index_inverse_zero_resultlefttable)) * dst_positive_scale_inverse_zero_resultlefttable) + (dst_positive_inverse_zero_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_zero_resultlefttableentrynegative. ff_h_pvs_inverse_zero_resultlefttableentrynegative + S (dst_negative_inverse_zero_resultlefttable) = S ((S (dst_index_inverse_zero_resultlefttable)) * dst_negative_scale_inverse_zero_resultlefttable)) /\ exists ff_q_pvs_inverse_zero_resultlefttableentrynegative. dst_negative_code_inverse_zero_resultlefttable = ff_q_pvs_inverse_zero_resultlefttableentrynegative * S ((S (dst_index_inverse_zero_resultlefttable)) * dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_inverse_zero_resultlefttable))) /\ (exists ge_balance_positive_inverse_zero_resultlefttableentryvalue ge_balance_negative_inverse_zero_resultlefttableentryvalue. (((((dst_value_inverse_zero_resultlefttable) = 2 * (ge_balance_positive_inverse_zero_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_zero_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultlefttableentryvaluedecode. (((dst_value_inverse_zero_resultlefttable) = 2 * ge_signed_half_inverse_zero_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultlefttableentryvalue) = S ge_signed_half_inverse_zero_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultlefttable) + ge_balance_negative_inverse_zero_resultlefttableentryvalue = (dst_negative_inverse_zero_resultlefttable) + ge_balance_positive_inverse_zero_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_zero_resultleft dc_output_inverse_zero_resultleft. ~(dc_input_inverse_zero_resultleft=0) -> (exists pvs_le_gap_inverse_zero_resultleftdomain. pvs_le_gap_inverse_zero_resultleftdomain + (dc_input_inverse_zero_resultleft) = (0)) -> (exists dst_positive_code_inverse_zero_resultleftlookup dst_positive_scale_inverse_zero_resultleftlookup dst_negative_code_inverse_zero_resultleftlookup dst_negative_scale_inverse_zero_resultleftlookup dst_positive_inverse_zero_resultleftlookup dst_negative_inverse_zero_resultleftlookup. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup)) * S ((dst_positive_code_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup)) + ((dst_positive_scale_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup))) + (((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) * S ((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) + ((dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)))) * S ((((dst_positive_code_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup)) * S ((dst_positive_code_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup)) + ((dst_positive_scale_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup))) + (((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) * S ((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) + ((dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)))) + ((((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) * S ((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) + ((dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup))) + (((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) * S ((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) + ((dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftlookuppositive. ff_h_pvs_inverse_zero_resultleftlookuppositive + S (dst_positive_inverse_zero_resultleftlookup) = S ((S (dc_input_inverse_zero_resultleft)) * dst_positive_scale_inverse_zero_resultleftlookup)) /\ exists ff_q_pvs_inverse_zero_resultleftlookuppositive. dst_positive_code_inverse_zero_resultleftlookup = ff_q_pvs_inverse_zero_resultleftlookuppositive * S ((S (dc_input_inverse_zero_resultleft)) * dst_positive_scale_inverse_zero_resultleftlookup) + (dst_positive_inverse_zero_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftlookupnegative. ff_h_pvs_inverse_zero_resultleftlookupnegative + S (dst_negative_inverse_zero_resultleftlookup) = S ((S (dc_input_inverse_zero_resultleft)) * dst_negative_scale_inverse_zero_resultleftlookup)) /\ exists ff_q_pvs_inverse_zero_resultleftlookupnegative. dst_negative_code_inverse_zero_resultleftlookup = ff_q_pvs_inverse_zero_resultleftlookupnegative * S ((S (dc_input_inverse_zero_resultleft)) * dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_inverse_zero_resultleftlookup))) /\ (exists ge_balance_positive_inverse_zero_resultleftlookupvalue ge_balance_negative_inverse_zero_resultleftlookupvalue. (((((dc_output_inverse_zero_resultleft) = 2 * (ge_balance_positive_inverse_zero_resultleftlookupvalue) /\ (ge_balance_negative_inverse_zero_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftlookupvaluedecode. (((dc_output_inverse_zero_resultleft) = 2 * ge_signed_half_inverse_zero_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftlookupvalue) = S ge_signed_half_inverse_zero_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftlookup) + ge_balance_negative_inverse_zero_resultleftlookupvalue = (dst_negative_inverse_zero_resultleftlookup) + ge_balance_positive_inverse_zero_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_zero_resultleft)=0)) /\ (exists dc_mask_inverse_zero_resultleftvalue. ((((exists dst_positive_code_inverse_zero_resultleftvaluemasktable dst_positive_scale_inverse_zero_resultleftvaluemasktable dst_negative_code_inverse_zero_resultleftvaluemasktable dst_negative_scale_inverse_zero_resultleftvaluemasktable. (((dc_mask_inverse_zero_resultleftvalue) = (((((dst_positive_code_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_zero_resultleftvaluemasktable. (exists pvs_le_gap_inverse_zero_resultleftvaluemasktabledomain. pvs_le_gap_inverse_zero_resultleftvaluemasktabledomain + (dst_index_inverse_zero_resultleftvaluemasktable) = (dc_input_inverse_zero_resultleft)) -> exists dst_positive_inverse_zero_resultleftvaluemasktable dst_negative_inverse_zero_resultleftvaluemasktable dst_value_inverse_zero_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_zero_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_zero_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_zero_resultleftvaluemasktable) = S ((S (dst_index_inverse_zero_resultleftvaluemasktable)) * dst_positive_scale_inverse_zero_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_zero_resultleftvaluemasktable = ff_q_pvs_inverse_zero_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_zero_resultleftvaluemasktable)) * dst_positive_scale_inverse_zero_resultleftvaluemasktable) + (dst_positive_inverse_zero_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_zero_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_zero_resultleftvaluemasktable) = S ((S (dst_index_inverse_zero_resultleftvaluemasktable)) * dst_negative_scale_inverse_zero_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_zero_resultleftvaluemasktable = ff_q_pvs_inverse_zero_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_zero_resultleftvaluemasktable)) * dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_inverse_zero_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_zero_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_zero_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_zero_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_zero_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_zero_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_zero_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftvaluemasktable) + ge_balance_negative_inverse_zero_resultleftvaluemasktableentryvalue = (dst_negative_inverse_zero_resultleftvaluemasktable) + ge_balance_positive_inverse_zero_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_zero_resultleftvaluemask dc_value_inverse_zero_resultleftvaluemask. (exists pvs_le_gap_inverse_zero_resultleftvaluemaskdomain. pvs_le_gap_inverse_zero_resultleftvaluemaskdomain + (dc_index_inverse_zero_resultleftvaluemask) = (dc_input_inverse_zero_resultleft)) -> (exists dst_positive_code_inverse_zero_resultleftvaluemasklookup dst_positive_scale_inverse_zero_resultleftvaluemasklookup dst_negative_code_inverse_zero_resultleftvaluemasklookup dst_negative_scale_inverse_zero_resultleftvaluemasklookup dst_positive_inverse_zero_resultleftvaluemasklookup dst_negative_inverse_zero_resultleftvaluemasklookup. (((dc_mask_inverse_zero_resultleftvalue) = (((((dst_positive_code_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_zero_resultleftvaluemasklookuppositive + S (dst_positive_inverse_zero_resultleftvaluemasklookup) = S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemasklookuppositive. dst_positive_code_inverse_zero_resultleftvaluemasklookup = ff_q_pvs_inverse_zero_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_positive_scale_inverse_zero_resultleftvaluemasklookup) + (dst_positive_inverse_zero_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_zero_resultleftvaluemasklookupnegative + S (dst_negative_inverse_zero_resultleftvaluemasklookup) = S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemasklookupnegative. dst_negative_code_inverse_zero_resultleftvaluemasklookup = ff_q_pvs_inverse_zero_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_inverse_zero_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluemasklookupvalue ge_balance_negative_inverse_zero_resultleftvaluemasklookupvalue. (((((dc_value_inverse_zero_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_zero_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_zero_resultleftvaluemask) = 2 * ge_signed_half_inverse_zero_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_zero_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftvaluemasklookup) + ge_balance_negative_inverse_zero_resultleftvaluemasklookupvalue = (dst_negative_inverse_zero_resultleftvaluemasklookup) + ge_balance_positive_inverse_zero_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_zero_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_zero_resultleftvaluemaskentry dc_left_inverse_zero_resultleftvaluemaskentry dc_right_inverse_zero_resultleftvaluemaskentry. (((dc_input_inverse_zero_resultleft)=(dc_index_inverse_zero_resultleftvaluemask)*dc_quotient_inverse_zero_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_zero_resultleftvaluemaskentryleft dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft dst_negative_code_inverse_zero_resultleftvaluemaskentryleft dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft dst_positive_inverse_zero_resultleftvaluemaskentryleft dst_negative_inverse_zero_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_zero_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_zero_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_zero_resultleftvaluemaskentryleft = ff_q_pvs_inverse_zero_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_inverse_zero_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_zero_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_zero_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_zero_resultleftvaluemaskentryleft = ff_q_pvs_inverse_zero_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_inverse_zero_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_zero_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_zero_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_zero_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_zero_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_zero_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_zero_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_zero_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultleftvaluemaskentryright dst_positive_scale_inverse_zero_resultleftvaluemaskentryright dst_negative_code_inverse_zero_resultleftvaluemaskentryright dst_negative_scale_inverse_zero_resultleftvaluemaskentryright dst_positive_inverse_zero_resultleftvaluemaskentryright dst_negative_inverse_zero_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_zero_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_zero_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_resultleftvaluemaskentry)) * dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_zero_resultleftvaluemaskentryright = ff_q_pvs_inverse_zero_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_zero_resultleftvaluemaskentry)) * dst_positive_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_inverse_zero_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_zero_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_zero_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_resultleftvaluemaskentry)) * dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_zero_resultleftvaluemaskentryright = ff_q_pvs_inverse_zero_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_zero_resultleftvaluemaskentry)) * dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_inverse_zero_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_zero_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_zero_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_zero_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_zero_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftvaluemaskentryright) + ge_balance_negative_inverse_zero_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_zero_resultleftvaluemaskentryright) + ge_balance_positive_inverse_zero_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_zero_resultleftvaluemaskentryproduct sto_an_inverse_zero_resultleftvaluemaskentryproduct sto_bp_inverse_zero_resultleftvaluemaskentryproduct sto_bn_inverse_zero_resultleftvaluemaskentryproduct sto_cp_inverse_zero_resultleftvaluemaskentryproduct sto_cn_inverse_zero_resultleftvaluemaskentryproduct. (((((dc_left_inverse_zero_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_zero_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_zero_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryproductleft. (((dc_left_inverse_zero_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_zero_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_zero_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_zero_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_zero_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_zero_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryproductright. (((dc_right_inverse_zero_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_zero_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_zero_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_zero_resultleftvaluemask) = 2 * (sto_cp_inverse_zero_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_zero_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_zero_resultleftvaluemask) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_zero_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_zero_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_zero_resultleftvaluemaskentryproduct * sto_bp_inverse_zero_resultleftvaluemaskentryproduct + sto_an_inverse_zero_resultleftvaluemaskentryproduct * sto_bn_inverse_zero_resultleftvaluemaskentryproduct) + sto_cn_inverse_zero_resultleftvaluemaskentryproduct = (sto_ap_inverse_zero_resultleftvaluemaskentryproduct * sto_bn_inverse_zero_resultleftvaluemaskentryproduct + sto_an_inverse_zero_resultleftvaluemaskentryproduct * sto_bp_inverse_zero_resultleftvaluemaskentryproduct) + sto_cp_inverse_zero_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_zero_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_zero_resultleftvaluemaskentrynondivisor. (dc_input_inverse_zero_resultleft) = (dc_index_inverse_zero_resultleftvaluemask) * pvs_factor_inverse_zero_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_zero_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_zero_resultleftvaluefold dst_positive_scale_inverse_zero_resultleftvaluefold dst_negative_code_inverse_zero_resultleftvaluefold dst_negative_scale_inverse_zero_resultleftvaluefold dst_positive_sum_inverse_zero_resultleftvaluefold dst_negative_sum_inverse_zero_resultleftvaluefold. (((dc_mask_inverse_zero_resultleftvalue) = (((((dst_positive_code_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold)) * S ((dst_positive_code_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold)) + ((dst_positive_scale_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold)) * S ((dst_positive_code_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold)) + ((dst_positive_scale_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)))) + ((((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_zero_resultleftvaluefoldpositive fs_v_dst_inverse_zero_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_zero_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_zero_resultleftvaluefold) = S ((S (S (dc_input_inverse_zero_resultleft))) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_zero_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_zero_resultleft))) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_zero_resultleftvaluefold))) /\ forall fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_zero_resultleft)) -> exists fs_a_dst_inverse_zero_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_zero_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_zero_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_zero_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_resultleftvaluefold)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_zero_resultleftvaluefold = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_resultleftvaluefold) + (fs_a_dst_inverse_zero_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_zero_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_zero_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive) + (fs_r_dst_inverse_zero_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_zero_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_zero_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive) + (fs_s_dst_inverse_zero_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_zero_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_zero_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_zero_resultleftvaluefoldnegative fs_v_dst_inverse_zero_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_zero_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_zero_resultleftvaluefold) = S ((S (S (dc_input_inverse_zero_resultleft))) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_zero_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_zero_resultleft))) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_zero_resultleftvaluefold))) /\ forall fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_zero_resultleft)) -> exists fs_a_dst_inverse_zero_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_zero_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_zero_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_zero_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_resultleftvaluefold)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_zero_resultleftvaluefold = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_resultleftvaluefold) + (fs_a_dst_inverse_zero_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_zero_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_zero_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative) + (fs_r_dst_inverse_zero_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_zero_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_zero_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative) + (fs_s_dst_inverse_zero_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_zero_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_zero_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluefoldresult ge_balance_negative_inverse_zero_resultleftvaluefoldresult. (((((dc_output_inverse_zero_resultleft) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_zero_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluefoldresultdecode. (((dc_output_inverse_zero_resultleft) = 2 * ge_signed_half_inverse_zero_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluefoldresult) = S ge_signed_half_inverse_zero_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_zero_resultleftvaluefold) + ge_balance_negative_inverse_zero_resultleftvaluefoldresult = (dst_negative_sum_inverse_zero_resultleftvaluefold) + ge_balance_positive_inverse_zero_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_zero_resultrightleft dst_positive_scale_inverse_zero_resultrightleft dst_negative_code_inverse_zero_resultrightleft dst_negative_scale_inverse_zero_resultrightleft. (((G) = (((((dst_positive_code_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft)) * S ((dst_positive_code_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft)) + ((dst_positive_scale_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft))) + (((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) * S ((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) + ((dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)))) * S ((((dst_positive_code_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft)) * S ((dst_positive_code_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft)) + ((dst_positive_scale_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft))) + (((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) * S ((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) + ((dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)))) + ((((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) * S ((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) + ((dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft))) + (((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) * S ((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) + ((dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)))))) /\ (forall dst_index_inverse_zero_resultrightleft. (exists pvs_le_gap_inverse_zero_resultrightleftdomain. pvs_le_gap_inverse_zero_resultrightleftdomain + (dst_index_inverse_zero_resultrightleft) = (0)) -> exists dst_positive_inverse_zero_resultrightleft dst_negative_inverse_zero_resultrightleft dst_value_inverse_zero_resultrightleft. ((((exists ff_h_pvs_inverse_zero_resultrightleftentrypositive. ff_h_pvs_inverse_zero_resultrightleftentrypositive + S (dst_positive_inverse_zero_resultrightleft) = S ((S (dst_index_inverse_zero_resultrightleft)) * dst_positive_scale_inverse_zero_resultrightleft)) /\ exists ff_q_pvs_inverse_zero_resultrightleftentrypositive. dst_positive_code_inverse_zero_resultrightleft = ff_q_pvs_inverse_zero_resultrightleftentrypositive * S ((S (dst_index_inverse_zero_resultrightleft)) * dst_positive_scale_inverse_zero_resultrightleft) + (dst_positive_inverse_zero_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightleftentrynegative. ff_h_pvs_inverse_zero_resultrightleftentrynegative + S (dst_negative_inverse_zero_resultrightleft) = S ((S (dst_index_inverse_zero_resultrightleft)) * dst_negative_scale_inverse_zero_resultrightleft)) /\ exists ff_q_pvs_inverse_zero_resultrightleftentrynegative. dst_negative_code_inverse_zero_resultrightleft = ff_q_pvs_inverse_zero_resultrightleftentrynegative * S ((S (dst_index_inverse_zero_resultrightleft)) * dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_inverse_zero_resultrightleft))) /\ (exists ge_balance_positive_inverse_zero_resultrightleftentryvalue ge_balance_negative_inverse_zero_resultrightleftentryvalue. (((((dst_value_inverse_zero_resultrightleft) = 2 * (ge_balance_positive_inverse_zero_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_zero_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightleftentryvaluedecode. (((dst_value_inverse_zero_resultrightleft) = 2 * ge_signed_half_inverse_zero_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightleftentryvalue) = S ge_signed_half_inverse_zero_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightleft) + ge_balance_negative_inverse_zero_resultrightleftentryvalue = (dst_negative_inverse_zero_resultrightleft) + ge_balance_positive_inverse_zero_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultrightright dst_positive_scale_inverse_zero_resultrightright dst_negative_code_inverse_zero_resultrightright dst_negative_scale_inverse_zero_resultrightright. (((F) = (((((dst_positive_code_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright)) * S ((dst_positive_code_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright)) + ((dst_positive_scale_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright))) + (((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) * S ((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) + ((dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)))) * S ((((dst_positive_code_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright)) * S ((dst_positive_code_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright)) + ((dst_positive_scale_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright))) + (((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) * S ((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) + ((dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)))) + ((((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) * S ((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) + ((dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright))) + (((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) * S ((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) + ((dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)))))) /\ (forall dst_index_inverse_zero_resultrightright. (exists pvs_le_gap_inverse_zero_resultrightrightdomain. pvs_le_gap_inverse_zero_resultrightrightdomain + (dst_index_inverse_zero_resultrightright) = (0)) -> exists dst_positive_inverse_zero_resultrightright dst_negative_inverse_zero_resultrightright dst_value_inverse_zero_resultrightright. ((((exists ff_h_pvs_inverse_zero_resultrightrightentrypositive. ff_h_pvs_inverse_zero_resultrightrightentrypositive + S (dst_positive_inverse_zero_resultrightright) = S ((S (dst_index_inverse_zero_resultrightright)) * dst_positive_scale_inverse_zero_resultrightright)) /\ exists ff_q_pvs_inverse_zero_resultrightrightentrypositive. dst_positive_code_inverse_zero_resultrightright = ff_q_pvs_inverse_zero_resultrightrightentrypositive * S ((S (dst_index_inverse_zero_resultrightright)) * dst_positive_scale_inverse_zero_resultrightright) + (dst_positive_inverse_zero_resultrightright))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightrightentrynegative. ff_h_pvs_inverse_zero_resultrightrightentrynegative + S (dst_negative_inverse_zero_resultrightright) = S ((S (dst_index_inverse_zero_resultrightright)) * dst_negative_scale_inverse_zero_resultrightright)) /\ exists ff_q_pvs_inverse_zero_resultrightrightentrynegative. dst_negative_code_inverse_zero_resultrightright = ff_q_pvs_inverse_zero_resultrightrightentrynegative * S ((S (dst_index_inverse_zero_resultrightright)) * dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_inverse_zero_resultrightright))) /\ (exists ge_balance_positive_inverse_zero_resultrightrightentryvalue ge_balance_negative_inverse_zero_resultrightrightentryvalue. (((((dst_value_inverse_zero_resultrightright) = 2 * (ge_balance_positive_inverse_zero_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_zero_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightrightentryvaluedecode. (((dst_value_inverse_zero_resultrightright) = 2 * ge_signed_half_inverse_zero_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightrightentryvalue) = S ge_signed_half_inverse_zero_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightright) + ge_balance_negative_inverse_zero_resultrightrightentryvalue = (dst_negative_inverse_zero_resultrightright) + ge_balance_positive_inverse_zero_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultrighttable dst_positive_scale_inverse_zero_resultrighttable dst_negative_code_inverse_zero_resultrighttable dst_negative_scale_inverse_zero_resultrighttable. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable)) * S ((dst_positive_code_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable)) + ((dst_positive_scale_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable))) + (((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) * S ((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) + ((dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)))) * S ((((dst_positive_code_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable)) * S ((dst_positive_code_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable)) + ((dst_positive_scale_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable))) + (((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) * S ((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) + ((dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)))) + ((((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) * S ((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) + ((dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable))) + (((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) * S ((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) + ((dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)))))) /\ (forall dst_index_inverse_zero_resultrighttable. (exists pvs_le_gap_inverse_zero_resultrighttabledomain. pvs_le_gap_inverse_zero_resultrighttabledomain + (dst_index_inverse_zero_resultrighttable) = (0)) -> exists dst_positive_inverse_zero_resultrighttable dst_negative_inverse_zero_resultrighttable dst_value_inverse_zero_resultrighttable. ((((exists ff_h_pvs_inverse_zero_resultrighttableentrypositive. ff_h_pvs_inverse_zero_resultrighttableentrypositive + S (dst_positive_inverse_zero_resultrighttable) = S ((S (dst_index_inverse_zero_resultrighttable)) * dst_positive_scale_inverse_zero_resultrighttable)) /\ exists ff_q_pvs_inverse_zero_resultrighttableentrypositive. dst_positive_code_inverse_zero_resultrighttable = ff_q_pvs_inverse_zero_resultrighttableentrypositive * S ((S (dst_index_inverse_zero_resultrighttable)) * dst_positive_scale_inverse_zero_resultrighttable) + (dst_positive_inverse_zero_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_zero_resultrighttableentrynegative. ff_h_pvs_inverse_zero_resultrighttableentrynegative + S (dst_negative_inverse_zero_resultrighttable) = S ((S (dst_index_inverse_zero_resultrighttable)) * dst_negative_scale_inverse_zero_resultrighttable)) /\ exists ff_q_pvs_inverse_zero_resultrighttableentrynegative. dst_negative_code_inverse_zero_resultrighttable = ff_q_pvs_inverse_zero_resultrighttableentrynegative * S ((S (dst_index_inverse_zero_resultrighttable)) * dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_inverse_zero_resultrighttable))) /\ (exists ge_balance_positive_inverse_zero_resultrighttableentryvalue ge_balance_negative_inverse_zero_resultrighttableentryvalue. (((((dst_value_inverse_zero_resultrighttable) = 2 * (ge_balance_positive_inverse_zero_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_zero_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrighttableentryvaluedecode. (((dst_value_inverse_zero_resultrighttable) = 2 * ge_signed_half_inverse_zero_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrighttableentryvalue) = S ge_signed_half_inverse_zero_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultrighttable) + ge_balance_negative_inverse_zero_resultrighttableentryvalue = (dst_negative_inverse_zero_resultrighttable) + ge_balance_positive_inverse_zero_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_zero_resultright dc_output_inverse_zero_resultright. ~(dc_input_inverse_zero_resultright=0) -> (exists pvs_le_gap_inverse_zero_resultrightdomain. pvs_le_gap_inverse_zero_resultrightdomain + (dc_input_inverse_zero_resultright) = (0)) -> (exists dst_positive_code_inverse_zero_resultrightlookup dst_positive_scale_inverse_zero_resultrightlookup dst_negative_code_inverse_zero_resultrightlookup dst_negative_scale_inverse_zero_resultrightlookup dst_positive_inverse_zero_resultrightlookup dst_negative_inverse_zero_resultrightlookup. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup)) * S ((dst_positive_code_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup)) + ((dst_positive_scale_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup))) + (((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) * S ((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) + ((dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)))) * S ((((dst_positive_code_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup)) * S ((dst_positive_code_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup)) + ((dst_positive_scale_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup))) + (((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) * S ((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) + ((dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)))) + ((((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) * S ((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) + ((dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup))) + (((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) * S ((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) + ((dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightlookuppositive. ff_h_pvs_inverse_zero_resultrightlookuppositive + S (dst_positive_inverse_zero_resultrightlookup) = S ((S (dc_input_inverse_zero_resultright)) * dst_positive_scale_inverse_zero_resultrightlookup)) /\ exists ff_q_pvs_inverse_zero_resultrightlookuppositive. dst_positive_code_inverse_zero_resultrightlookup = ff_q_pvs_inverse_zero_resultrightlookuppositive * S ((S (dc_input_inverse_zero_resultright)) * dst_positive_scale_inverse_zero_resultrightlookup) + (dst_positive_inverse_zero_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightlookupnegative. ff_h_pvs_inverse_zero_resultrightlookupnegative + S (dst_negative_inverse_zero_resultrightlookup) = S ((S (dc_input_inverse_zero_resultright)) * dst_negative_scale_inverse_zero_resultrightlookup)) /\ exists ff_q_pvs_inverse_zero_resultrightlookupnegative. dst_negative_code_inverse_zero_resultrightlookup = ff_q_pvs_inverse_zero_resultrightlookupnegative * S ((S (dc_input_inverse_zero_resultright)) * dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_inverse_zero_resultrightlookup))) /\ (exists ge_balance_positive_inverse_zero_resultrightlookupvalue ge_balance_negative_inverse_zero_resultrightlookupvalue. (((((dc_output_inverse_zero_resultright) = 2 * (ge_balance_positive_inverse_zero_resultrightlookupvalue) /\ (ge_balance_negative_inverse_zero_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightlookupvaluedecode. (((dc_output_inverse_zero_resultright) = 2 * ge_signed_half_inverse_zero_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightlookupvalue) = S ge_signed_half_inverse_zero_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightlookup) + ge_balance_negative_inverse_zero_resultrightlookupvalue = (dst_negative_inverse_zero_resultrightlookup) + ge_balance_positive_inverse_zero_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_zero_resultright)=0)) /\ (exists dc_mask_inverse_zero_resultrightvalue. ((((exists dst_positive_code_inverse_zero_resultrightvaluemasktable dst_positive_scale_inverse_zero_resultrightvaluemasktable dst_negative_code_inverse_zero_resultrightvaluemasktable dst_negative_scale_inverse_zero_resultrightvaluemasktable. (((dc_mask_inverse_zero_resultrightvalue) = (((((dst_positive_code_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_zero_resultrightvaluemasktable. (exists pvs_le_gap_inverse_zero_resultrightvaluemasktabledomain. pvs_le_gap_inverse_zero_resultrightvaluemasktabledomain + (dst_index_inverse_zero_resultrightvaluemasktable) = (dc_input_inverse_zero_resultright)) -> exists dst_positive_inverse_zero_resultrightvaluemasktable dst_negative_inverse_zero_resultrightvaluemasktable dst_value_inverse_zero_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_zero_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_zero_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_zero_resultrightvaluemasktable) = S ((S (dst_index_inverse_zero_resultrightvaluemasktable)) * dst_positive_scale_inverse_zero_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_zero_resultrightvaluemasktable = ff_q_pvs_inverse_zero_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_zero_resultrightvaluemasktable)) * dst_positive_scale_inverse_zero_resultrightvaluemasktable) + (dst_positive_inverse_zero_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_zero_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_zero_resultrightvaluemasktable) = S ((S (dst_index_inverse_zero_resultrightvaluemasktable)) * dst_negative_scale_inverse_zero_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_zero_resultrightvaluemasktable = ff_q_pvs_inverse_zero_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_zero_resultrightvaluemasktable)) * dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_inverse_zero_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_zero_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_zero_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_zero_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_zero_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_zero_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_zero_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightvaluemasktable) + ge_balance_negative_inverse_zero_resultrightvaluemasktableentryvalue = (dst_negative_inverse_zero_resultrightvaluemasktable) + ge_balance_positive_inverse_zero_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_zero_resultrightvaluemask dc_value_inverse_zero_resultrightvaluemask. (exists pvs_le_gap_inverse_zero_resultrightvaluemaskdomain. pvs_le_gap_inverse_zero_resultrightvaluemaskdomain + (dc_index_inverse_zero_resultrightvaluemask) = (dc_input_inverse_zero_resultright)) -> (exists dst_positive_code_inverse_zero_resultrightvaluemasklookup dst_positive_scale_inverse_zero_resultrightvaluemasklookup dst_negative_code_inverse_zero_resultrightvaluemasklookup dst_negative_scale_inverse_zero_resultrightvaluemasklookup dst_positive_inverse_zero_resultrightvaluemasklookup dst_negative_inverse_zero_resultrightvaluemasklookup. (((dc_mask_inverse_zero_resultrightvalue) = (((((dst_positive_code_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_zero_resultrightvaluemasklookuppositive + S (dst_positive_inverse_zero_resultrightvaluemasklookup) = S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemasklookuppositive. dst_positive_code_inverse_zero_resultrightvaluemasklookup = ff_q_pvs_inverse_zero_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_positive_scale_inverse_zero_resultrightvaluemasklookup) + (dst_positive_inverse_zero_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_zero_resultrightvaluemasklookupnegative + S (dst_negative_inverse_zero_resultrightvaluemasklookup) = S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemasklookupnegative. dst_negative_code_inverse_zero_resultrightvaluemasklookup = ff_q_pvs_inverse_zero_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_inverse_zero_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluemasklookupvalue ge_balance_negative_inverse_zero_resultrightvaluemasklookupvalue. (((((dc_value_inverse_zero_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_zero_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_zero_resultrightvaluemask) = 2 * ge_signed_half_inverse_zero_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_zero_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightvaluemasklookup) + ge_balance_negative_inverse_zero_resultrightvaluemasklookupvalue = (dst_negative_inverse_zero_resultrightvaluemasklookup) + ge_balance_positive_inverse_zero_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_zero_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_zero_resultrightvaluemaskentry dc_left_inverse_zero_resultrightvaluemaskentry dc_right_inverse_zero_resultrightvaluemaskentry. (((dc_input_inverse_zero_resultright)=(dc_index_inverse_zero_resultrightvaluemask)*dc_quotient_inverse_zero_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_zero_resultrightvaluemaskentryleft dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft dst_negative_code_inverse_zero_resultrightvaluemaskentryleft dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft dst_positive_inverse_zero_resultrightvaluemaskentryleft dst_negative_inverse_zero_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_zero_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_zero_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_zero_resultrightvaluemaskentryleft = ff_q_pvs_inverse_zero_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_inverse_zero_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_zero_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_zero_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_zero_resultrightvaluemaskentryleft = ff_q_pvs_inverse_zero_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_inverse_zero_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_zero_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_zero_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_zero_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_zero_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_zero_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_zero_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_zero_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultrightvaluemaskentryright dst_positive_scale_inverse_zero_resultrightvaluemaskentryright dst_negative_code_inverse_zero_resultrightvaluemaskentryright dst_negative_scale_inverse_zero_resultrightvaluemaskentryright dst_positive_inverse_zero_resultrightvaluemaskentryright dst_negative_inverse_zero_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_zero_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_zero_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_resultrightvaluemaskentry)) * dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_zero_resultrightvaluemaskentryright = ff_q_pvs_inverse_zero_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_zero_resultrightvaluemaskentry)) * dst_positive_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_inverse_zero_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_zero_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_zero_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_resultrightvaluemaskentry)) * dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_zero_resultrightvaluemaskentryright = ff_q_pvs_inverse_zero_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_zero_resultrightvaluemaskentry)) * dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_inverse_zero_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_zero_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_zero_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_zero_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_zero_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightvaluemaskentryright) + ge_balance_negative_inverse_zero_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_zero_resultrightvaluemaskentryright) + ge_balance_positive_inverse_zero_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_zero_resultrightvaluemaskentryproduct sto_an_inverse_zero_resultrightvaluemaskentryproduct sto_bp_inverse_zero_resultrightvaluemaskentryproduct sto_bn_inverse_zero_resultrightvaluemaskentryproduct sto_cp_inverse_zero_resultrightvaluemaskentryproduct sto_cn_inverse_zero_resultrightvaluemaskentryproduct. (((((dc_left_inverse_zero_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_zero_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_zero_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryproductleft. (((dc_left_inverse_zero_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_zero_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_zero_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_zero_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_zero_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_zero_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryproductright. (((dc_right_inverse_zero_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_zero_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_zero_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_zero_resultrightvaluemask) = 2 * (sto_cp_inverse_zero_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_zero_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_zero_resultrightvaluemask) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_zero_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_zero_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_zero_resultrightvaluemaskentryproduct * sto_bp_inverse_zero_resultrightvaluemaskentryproduct + sto_an_inverse_zero_resultrightvaluemaskentryproduct * sto_bn_inverse_zero_resultrightvaluemaskentryproduct) + sto_cn_inverse_zero_resultrightvaluemaskentryproduct = (sto_ap_inverse_zero_resultrightvaluemaskentryproduct * sto_bn_inverse_zero_resultrightvaluemaskentryproduct + sto_an_inverse_zero_resultrightvaluemaskentryproduct * sto_bp_inverse_zero_resultrightvaluemaskentryproduct) + sto_cp_inverse_zero_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_zero_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_zero_resultrightvaluemaskentrynondivisor. (dc_input_inverse_zero_resultright) = (dc_index_inverse_zero_resultrightvaluemask) * pvs_factor_inverse_zero_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_zero_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_zero_resultrightvaluefold dst_positive_scale_inverse_zero_resultrightvaluefold dst_negative_code_inverse_zero_resultrightvaluefold dst_negative_scale_inverse_zero_resultrightvaluefold dst_positive_sum_inverse_zero_resultrightvaluefold dst_negative_sum_inverse_zero_resultrightvaluefold. (((dc_mask_inverse_zero_resultrightvalue) = (((((dst_positive_code_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold)) * S ((dst_positive_code_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold)) + ((dst_positive_scale_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold)) * S ((dst_positive_code_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold)) + ((dst_positive_scale_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)))) + ((((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_zero_resultrightvaluefoldpositive fs_v_dst_inverse_zero_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_zero_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_zero_resultrightvaluefold) = S ((S (S (dc_input_inverse_zero_resultright))) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_zero_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_zero_resultright))) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_zero_resultrightvaluefold))) /\ forall fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_zero_resultright)) -> exists fs_a_dst_inverse_zero_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_zero_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_zero_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_zero_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_resultrightvaluefold)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_zero_resultrightvaluefold = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_resultrightvaluefold) + (fs_a_dst_inverse_zero_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_zero_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_zero_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive) + (fs_r_dst_inverse_zero_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_zero_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_zero_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive) + (fs_s_dst_inverse_zero_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_zero_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_zero_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_zero_resultrightvaluefoldnegative fs_v_dst_inverse_zero_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_zero_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_zero_resultrightvaluefold) = S ((S (S (dc_input_inverse_zero_resultright))) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_zero_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_zero_resultright))) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_zero_resultrightvaluefold))) /\ forall fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_zero_resultright)) -> exists fs_a_dst_inverse_zero_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_zero_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_zero_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_zero_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_resultrightvaluefold)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_zero_resultrightvaluefold = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_resultrightvaluefold) + (fs_a_dst_inverse_zero_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_zero_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_zero_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative) + (fs_r_dst_inverse_zero_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_zero_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_zero_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative) + (fs_s_dst_inverse_zero_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_zero_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_zero_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluefoldresult ge_balance_negative_inverse_zero_resultrightvaluefoldresult. (((((dc_output_inverse_zero_resultright) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_zero_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluefoldresultdecode. (((dc_output_inverse_zero_resultright) = 2 * ge_signed_half_inverse_zero_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluefoldresult) = S ge_signed_half_inverse_zero_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_zero_resultrightvaluefold) + ge_balance_negative_inverse_zero_resultrightvaluefoldresult = (dst_negative_sum_inverse_zero_resultrightvaluefold) + ge_balance_positive_inverse_zero_resultrightvaluefoldresult))))))))))))))))))))))))Complete tactic proof in conservative notation
All 29 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
29 script commands · 9 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.
01Fix variables and assumptionsL1–4
02Establish hdL5–8
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet kronecker delta table exists.
- L5
have hd : ∃ E. KroneckerDeltaTable(0,E) ∧ ArithAt(E,0,0)Definitions: KroneckerDeltaTable(0,E)ArithAt(E,0,0)Original native command in the exact edition - L6
specialize dirichlet_kronecker_delta_table_exists (0) - L7
specialize dirichlet_kronecker_delta_table_exists (0) - L8
apply dirichlet_kronecker_delta_table_exists
03Separate the logical casesL9–11
04Construct an explicit witnessL12–12
Supply the displayed value, then prove that it has the required property.
- L12
exists x
05Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
split
06Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact hd_witness_left
07Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
split
08Use earlier factsL16–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
specialize dirichlet_convolution_table_zero_constructor (F) - L17
specialize dirichlet_convolution_table_zero_constructor (G) - L18
specialize dirichlet_convolution_table_zero_constructor (x) - L19
apply dirichlet_convolution_table_zero_constructor - L20
exact hF - L21
exact hG - L22
exact hd_witness_left_left - L23
specialize dirichlet_convolution_table_zero_constructor (G) - L24
specialize dirichlet_convolution_table_zero_constructor (F) - L25
specialize dirichlet_convolution_table_zero_constructor (x)
Original defined command ledger · 29 lines
- 0001
intro F - 0002
intro G - 0003
intro hF - 0004
intro hG - 0005
have hd : ∃ E. KroneckerDeltaTable(0,E) ∧ ArithAt(E,0,0) - 0006
specialize dirichlet_kronecker_delta_table_exists (0) - 0007
specialize dirichlet_kronecker_delta_table_exists (0) - 0008
apply dirichlet_kronecker_delta_table_exists - 0009
cases hd - 0010
cases hd_witness - 0011
cases hd_witness_left - 0012
exists x - 0013
split - 0014
exact hd_witness_left - 0015
split - 0016
specialize dirichlet_convolution_table_zero_constructor (F) - 0017
specialize dirichlet_convolution_table_zero_constructor (G) - 0018
specialize dirichlet_convolution_table_zero_constructor (x) - 0019
apply dirichlet_convolution_table_zero_constructor - 0020
exact hF - 0021
exact hG - 0022
exact hd_witness_left_left - 0023
specialize dirichlet_convolution_table_zero_constructor (G) - 0024
specialize dirichlet_convolution_table_zero_constructor (F) - 0025
specialize dirichlet_convolution_table_zero_constructor (x) - 0026
apply dirichlet_convolution_table_zero_constructor - 0027
exact hG - 0028
exact hF - 0029
exact hd_witness_left_left