Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
For an actual table an inverse exists exactly when N=0 or F(1) is signed +1 or -1. At a positive window this is the unit-at-one criterion; the empty window imposes no condition at one. Every inverse has actual delta and two-sided convolution witnesses. Its zeroth value is arbitrary, so uniqueness is positive-value equality, not equality of codes or of zeroth values. Multiplicative-function closure and full finite signed G009 are admitted in the separate Alpha-v32 multiplicative-convolution family.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. DirichletInverse(N,F,G) → DirichletInverse(N,G,F)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
none
Original expanded first-order statement
forall N F G. (exists di_delta_inverse_symm_source. ((((exists dst_positive_code_inverse_symm_sourcedeltatable dst_positive_scale_inverse_symm_sourcedeltatable dst_negative_code_inverse_symm_sourcedeltatable dst_negative_scale_inverse_symm_sourcedeltatable. (((di_delta_inverse_symm_source) = (((((dst_positive_code_inverse_symm_sourcedeltatable) + (dst_positive_scale_inverse_symm_sourcedeltatable)) * S ((dst_positive_code_inverse_symm_sourcedeltatable) + (dst_positive_scale_inverse_symm_sourcedeltatable)) + ((dst_positive_scale_inverse_symm_sourcedeltatable) + (dst_positive_scale_inverse_symm_sourcedeltatable))) + (((dst_negative_code_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)) * S ((dst_negative_code_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)) + ((dst_negative_scale_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)))) * S ((((dst_positive_code_inverse_symm_sourcedeltatable) + (dst_positive_scale_inverse_symm_sourcedeltatable)) * S ((dst_positive_code_inverse_symm_sourcedeltatable) + (dst_positive_scale_inverse_symm_sourcedeltatable)) + ((dst_positive_scale_inverse_symm_sourcedeltatable) + (dst_positive_scale_inverse_symm_sourcedeltatable))) + (((dst_negative_code_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)) * S ((dst_negative_code_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)) + ((dst_negative_scale_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)))) + ((((dst_negative_code_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)) * S ((dst_negative_code_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)) + ((dst_negative_scale_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable))) + (((dst_negative_code_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)) * S ((dst_negative_code_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)) + ((dst_negative_scale_inverse_symm_sourcedeltatable) + (dst_negative_scale_inverse_symm_sourcedeltatable)))))) /\ (forall dst_index_inverse_symm_sourcedeltatable. (exists pvs_le_gap_inverse_symm_sourcedeltatabledomain. pvs_le_gap_inverse_symm_sourcedeltatabledomain + (dst_index_inverse_symm_sourcedeltatable) = (N)) -> exists dst_positive_inverse_symm_sourcedeltatable dst_negative_inverse_symm_sourcedeltatable dst_value_inverse_symm_sourcedeltatable. ((((exists ff_h_pvs_inverse_symm_sourcedeltatableentrypositive. ff_h_pvs_inverse_symm_sourcedeltatableentrypositive + S (dst_positive_inverse_symm_sourcedeltatable) = S ((S (dst_index_inverse_symm_sourcedeltatable)) * dst_positive_scale_inverse_symm_sourcedeltatable)) /\ exists ff_q_pvs_inverse_symm_sourcedeltatableentrypositive. dst_positive_code_inverse_symm_sourcedeltatable = ff_q_pvs_inverse_symm_sourcedeltatableentrypositive * S ((S (dst_index_inverse_symm_sourcedeltatable)) * dst_positive_scale_inverse_symm_sourcedeltatable) + (dst_positive_inverse_symm_sourcedeltatable))) /\ (((((exists ff_h_pvs_inverse_symm_sourcedeltatableentrynegative. ff_h_pvs_inverse_symm_sourcedeltatableentrynegative + S (dst_negative_inverse_symm_sourcedeltatable) = S ((S (dst_index_inverse_symm_sourcedeltatable)) * dst_negative_scale_inverse_symm_sourcedeltatable)) /\ exists ff_q_pvs_inverse_symm_sourcedeltatableentrynegative. dst_negative_code_inverse_symm_sourcedeltatable = ff_q_pvs_inverse_symm_sourcedeltatableentrynegative * S ((S (dst_index_inverse_symm_sourcedeltatable)) * dst_negative_scale_inverse_symm_sourcedeltatable) + (dst_negative_inverse_symm_sourcedeltatable))) /\ (exists ge_balance_positive_inverse_symm_sourcedeltatableentryvalue ge_balance_negative_inverse_symm_sourcedeltatableentryvalue. (((((dst_value_inverse_symm_sourcedeltatable) = 2 * (ge_balance_positive_inverse_symm_sourcedeltatableentryvalue) /\ (ge_balance_negative_inverse_symm_sourcedeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcedeltatableentryvaluedecode. (((dst_value_inverse_symm_sourcedeltatable) = 2 * ge_signed_half_inverse_symm_sourcedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcedeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcedeltatableentryvalue) = S ge_signed_half_inverse_symm_sourcedeltatableentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourcedeltatable) + ge_balance_negative_inverse_symm_sourcedeltatableentryvalue = (dst_negative_inverse_symm_sourcedeltatable) + ge_balance_positive_inverse_symm_sourcedeltatableentryvalue))))))))) /\ (forall du_index_inverse_symm_sourcedelta du_value_inverse_symm_sourcedelta. ~(du_index_inverse_symm_sourcedelta=0) -> (exists pvs_le_gap_inverse_symm_sourcedeltabound. pvs_le_gap_inverse_symm_sourcedeltabound + (du_index_inverse_symm_sourcedelta) = (N)) -> (exists dst_positive_code_inverse_symm_sourcedeltaentry dst_positive_scale_inverse_symm_sourcedeltaentry dst_negative_code_inverse_symm_sourcedeltaentry dst_negative_scale_inverse_symm_sourcedeltaentry dst_positive_inverse_symm_sourcedeltaentry dst_negative_inverse_symm_sourcedeltaentry. (((di_delta_inverse_symm_source) = (((((dst_positive_code_inverse_symm_sourcedeltaentry) + (dst_positive_scale_inverse_symm_sourcedeltaentry)) * S ((dst_positive_code_inverse_symm_sourcedeltaentry) + (dst_positive_scale_inverse_symm_sourcedeltaentry)) + ((dst_positive_scale_inverse_symm_sourcedeltaentry) + (dst_positive_scale_inverse_symm_sourcedeltaentry))) + (((dst_negative_code_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)) * S ((dst_negative_code_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)) + ((dst_negative_scale_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)))) * S ((((dst_positive_code_inverse_symm_sourcedeltaentry) + (dst_positive_scale_inverse_symm_sourcedeltaentry)) * S ((dst_positive_code_inverse_symm_sourcedeltaentry) + (dst_positive_scale_inverse_symm_sourcedeltaentry)) + ((dst_positive_scale_inverse_symm_sourcedeltaentry) + (dst_positive_scale_inverse_symm_sourcedeltaentry))) + (((dst_negative_code_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)) * S ((dst_negative_code_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)) + ((dst_negative_scale_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)))) + ((((dst_negative_code_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)) * S ((dst_negative_code_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)) + ((dst_negative_scale_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry))) + (((dst_negative_code_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)) * S ((dst_negative_code_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)) + ((dst_negative_scale_inverse_symm_sourcedeltaentry) + (dst_negative_scale_inverse_symm_sourcedeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourcedeltaentrypositive. ff_h_pvs_inverse_symm_sourcedeltaentrypositive + S (dst_positive_inverse_symm_sourcedeltaentry) = S ((S (du_index_inverse_symm_sourcedelta)) * dst_positive_scale_inverse_symm_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_symm_sourcedeltaentrypositive. dst_positive_code_inverse_symm_sourcedeltaentry = ff_q_pvs_inverse_symm_sourcedeltaentrypositive * S ((S (du_index_inverse_symm_sourcedelta)) * dst_positive_scale_inverse_symm_sourcedeltaentry) + (dst_positive_inverse_symm_sourcedeltaentry))) /\ (((((exists ff_h_pvs_inverse_symm_sourcedeltaentrynegative. ff_h_pvs_inverse_symm_sourcedeltaentrynegative + S (dst_negative_inverse_symm_sourcedeltaentry) = S ((S (du_index_inverse_symm_sourcedelta)) * dst_negative_scale_inverse_symm_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_symm_sourcedeltaentrynegative. dst_negative_code_inverse_symm_sourcedeltaentry = ff_q_pvs_inverse_symm_sourcedeltaentrynegative * S ((S (du_index_inverse_symm_sourcedelta)) * dst_negative_scale_inverse_symm_sourcedeltaentry) + (dst_negative_inverse_symm_sourcedeltaentry))) /\ (exists ge_balance_positive_inverse_symm_sourcedeltaentryvalue ge_balance_negative_inverse_symm_sourcedeltaentryvalue. (((((du_value_inverse_symm_sourcedelta) = 2 * (ge_balance_positive_inverse_symm_sourcedeltaentryvalue) /\ (ge_balance_negative_inverse_symm_sourcedeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcedeltaentryvaluedecode. (((du_value_inverse_symm_sourcedelta) = 2 * ge_signed_half_inverse_symm_sourcedeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcedeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcedeltaentryvalue) = S ge_signed_half_inverse_symm_sourcedeltaentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourcedeltaentry) + ge_balance_negative_inverse_symm_sourcedeltaentryvalue = (dst_negative_inverse_symm_sourcedeltaentry) + ge_balance_positive_inverse_symm_sourcedeltaentryvalue))))))))) -> ((((du_index_inverse_symm_sourcedelta)=1 -> (du_value_inverse_symm_sourcedelta)=2) /\ (~((du_index_inverse_symm_sourcedelta)=1) -> (du_value_inverse_symm_sourcedelta)=0)))))) /\ (((((exists dst_positive_code_inverse_symm_sourceleftleft dst_positive_scale_inverse_symm_sourceleftleft dst_negative_code_inverse_symm_sourceleftleft dst_negative_scale_inverse_symm_sourceleftleft. (((F) = (((((dst_positive_code_inverse_symm_sourceleftleft) + (dst_positive_scale_inverse_symm_sourceleftleft)) * S ((dst_positive_code_inverse_symm_sourceleftleft) + (dst_positive_scale_inverse_symm_sourceleftleft)) + ((dst_positive_scale_inverse_symm_sourceleftleft) + (dst_positive_scale_inverse_symm_sourceleftleft))) + (((dst_negative_code_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)) * S ((dst_negative_code_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)) + ((dst_negative_scale_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)))) * S ((((dst_positive_code_inverse_symm_sourceleftleft) + (dst_positive_scale_inverse_symm_sourceleftleft)) * S ((dst_positive_code_inverse_symm_sourceleftleft) + (dst_positive_scale_inverse_symm_sourceleftleft)) + ((dst_positive_scale_inverse_symm_sourceleftleft) + (dst_positive_scale_inverse_symm_sourceleftleft))) + (((dst_negative_code_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)) * S ((dst_negative_code_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)) + ((dst_negative_scale_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)))) + ((((dst_negative_code_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)) * S ((dst_negative_code_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)) + ((dst_negative_scale_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft))) + (((dst_negative_code_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)) * S ((dst_negative_code_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)) + ((dst_negative_scale_inverse_symm_sourceleftleft) + (dst_negative_scale_inverse_symm_sourceleftleft)))))) /\ (forall dst_index_inverse_symm_sourceleftleft. (exists pvs_le_gap_inverse_symm_sourceleftleftdomain. pvs_le_gap_inverse_symm_sourceleftleftdomain + (dst_index_inverse_symm_sourceleftleft) = (N)) -> exists dst_positive_inverse_symm_sourceleftleft dst_negative_inverse_symm_sourceleftleft dst_value_inverse_symm_sourceleftleft. ((((exists ff_h_pvs_inverse_symm_sourceleftleftentrypositive. ff_h_pvs_inverse_symm_sourceleftleftentrypositive + S (dst_positive_inverse_symm_sourceleftleft) = S ((S (dst_index_inverse_symm_sourceleftleft)) * dst_positive_scale_inverse_symm_sourceleftleft)) /\ exists ff_q_pvs_inverse_symm_sourceleftleftentrypositive. dst_positive_code_inverse_symm_sourceleftleft = ff_q_pvs_inverse_symm_sourceleftleftentrypositive * S ((S (dst_index_inverse_symm_sourceleftleft)) * dst_positive_scale_inverse_symm_sourceleftleft) + (dst_positive_inverse_symm_sourceleftleft))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftleftentrynegative. ff_h_pvs_inverse_symm_sourceleftleftentrynegative + S (dst_negative_inverse_symm_sourceleftleft) = S ((S (dst_index_inverse_symm_sourceleftleft)) * dst_negative_scale_inverse_symm_sourceleftleft)) /\ exists ff_q_pvs_inverse_symm_sourceleftleftentrynegative. dst_negative_code_inverse_symm_sourceleftleft = ff_q_pvs_inverse_symm_sourceleftleftentrynegative * S ((S (dst_index_inverse_symm_sourceleftleft)) * dst_negative_scale_inverse_symm_sourceleftleft) + (dst_negative_inverse_symm_sourceleftleft))) /\ (exists ge_balance_positive_inverse_symm_sourceleftleftentryvalue ge_balance_negative_inverse_symm_sourceleftleftentryvalue. (((((dst_value_inverse_symm_sourceleftleft) = 2 * (ge_balance_positive_inverse_symm_sourceleftleftentryvalue) /\ (ge_balance_negative_inverse_symm_sourceleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftleftentryvaluedecode. (((dst_value_inverse_symm_sourceleftleft) = 2 * ge_signed_half_inverse_symm_sourceleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourceleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourceleftleftentryvalue) = S ge_signed_half_inverse_symm_sourceleftleftentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourceleftleft) + ge_balance_negative_inverse_symm_sourceleftleftentryvalue = (dst_negative_inverse_symm_sourceleftleft) + ge_balance_positive_inverse_symm_sourceleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_sourceleftright dst_positive_scale_inverse_symm_sourceleftright dst_negative_code_inverse_symm_sourceleftright dst_negative_scale_inverse_symm_sourceleftright. (((G) = (((((dst_positive_code_inverse_symm_sourceleftright) + (dst_positive_scale_inverse_symm_sourceleftright)) * S ((dst_positive_code_inverse_symm_sourceleftright) + (dst_positive_scale_inverse_symm_sourceleftright)) + ((dst_positive_scale_inverse_symm_sourceleftright) + (dst_positive_scale_inverse_symm_sourceleftright))) + (((dst_negative_code_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)) * S ((dst_negative_code_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)) + ((dst_negative_scale_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)))) * S ((((dst_positive_code_inverse_symm_sourceleftright) + (dst_positive_scale_inverse_symm_sourceleftright)) * S ((dst_positive_code_inverse_symm_sourceleftright) + (dst_positive_scale_inverse_symm_sourceleftright)) + ((dst_positive_scale_inverse_symm_sourceleftright) + (dst_positive_scale_inverse_symm_sourceleftright))) + (((dst_negative_code_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)) * S ((dst_negative_code_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)) + ((dst_negative_scale_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)))) + ((((dst_negative_code_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)) * S ((dst_negative_code_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)) + ((dst_negative_scale_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright))) + (((dst_negative_code_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)) * S ((dst_negative_code_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)) + ((dst_negative_scale_inverse_symm_sourceleftright) + (dst_negative_scale_inverse_symm_sourceleftright)))))) /\ (forall dst_index_inverse_symm_sourceleftright. (exists pvs_le_gap_inverse_symm_sourceleftrightdomain. pvs_le_gap_inverse_symm_sourceleftrightdomain + (dst_index_inverse_symm_sourceleftright) = (N)) -> exists dst_positive_inverse_symm_sourceleftright dst_negative_inverse_symm_sourceleftright dst_value_inverse_symm_sourceleftright. ((((exists ff_h_pvs_inverse_symm_sourceleftrightentrypositive. ff_h_pvs_inverse_symm_sourceleftrightentrypositive + S (dst_positive_inverse_symm_sourceleftright) = S ((S (dst_index_inverse_symm_sourceleftright)) * dst_positive_scale_inverse_symm_sourceleftright)) /\ exists ff_q_pvs_inverse_symm_sourceleftrightentrypositive. dst_positive_code_inverse_symm_sourceleftright = ff_q_pvs_inverse_symm_sourceleftrightentrypositive * S ((S (dst_index_inverse_symm_sourceleftright)) * dst_positive_scale_inverse_symm_sourceleftright) + (dst_positive_inverse_symm_sourceleftright))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftrightentrynegative. ff_h_pvs_inverse_symm_sourceleftrightentrynegative + S (dst_negative_inverse_symm_sourceleftright) = S ((S (dst_index_inverse_symm_sourceleftright)) * dst_negative_scale_inverse_symm_sourceleftright)) /\ exists ff_q_pvs_inverse_symm_sourceleftrightentrynegative. dst_negative_code_inverse_symm_sourceleftright = ff_q_pvs_inverse_symm_sourceleftrightentrynegative * S ((S (dst_index_inverse_symm_sourceleftright)) * dst_negative_scale_inverse_symm_sourceleftright) + (dst_negative_inverse_symm_sourceleftright))) /\ (exists ge_balance_positive_inverse_symm_sourceleftrightentryvalue ge_balance_negative_inverse_symm_sourceleftrightentryvalue. (((((dst_value_inverse_symm_sourceleftright) = 2 * (ge_balance_positive_inverse_symm_sourceleftrightentryvalue) /\ (ge_balance_negative_inverse_symm_sourceleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftrightentryvaluedecode. (((dst_value_inverse_symm_sourceleftright) = 2 * ge_signed_half_inverse_symm_sourceleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourceleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourceleftrightentryvalue) = S ge_signed_half_inverse_symm_sourceleftrightentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourceleftright) + ge_balance_negative_inverse_symm_sourceleftrightentryvalue = (dst_negative_inverse_symm_sourceleftright) + ge_balance_positive_inverse_symm_sourceleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_sourcelefttable dst_positive_scale_inverse_symm_sourcelefttable dst_negative_code_inverse_symm_sourcelefttable dst_negative_scale_inverse_symm_sourcelefttable. (((di_delta_inverse_symm_source) = (((((dst_positive_code_inverse_symm_sourcelefttable) + (dst_positive_scale_inverse_symm_sourcelefttable)) * S ((dst_positive_code_inverse_symm_sourcelefttable) + (dst_positive_scale_inverse_symm_sourcelefttable)) + ((dst_positive_scale_inverse_symm_sourcelefttable) + (dst_positive_scale_inverse_symm_sourcelefttable))) + (((dst_negative_code_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)) * S ((dst_negative_code_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)) + ((dst_negative_scale_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)))) * S ((((dst_positive_code_inverse_symm_sourcelefttable) + (dst_positive_scale_inverse_symm_sourcelefttable)) * S ((dst_positive_code_inverse_symm_sourcelefttable) + (dst_positive_scale_inverse_symm_sourcelefttable)) + ((dst_positive_scale_inverse_symm_sourcelefttable) + (dst_positive_scale_inverse_symm_sourcelefttable))) + (((dst_negative_code_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)) * S ((dst_negative_code_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)) + ((dst_negative_scale_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)))) + ((((dst_negative_code_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)) * S ((dst_negative_code_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)) + ((dst_negative_scale_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable))) + (((dst_negative_code_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)) * S ((dst_negative_code_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)) + ((dst_negative_scale_inverse_symm_sourcelefttable) + (dst_negative_scale_inverse_symm_sourcelefttable)))))) /\ (forall dst_index_inverse_symm_sourcelefttable. (exists pvs_le_gap_inverse_symm_sourcelefttabledomain. pvs_le_gap_inverse_symm_sourcelefttabledomain + (dst_index_inverse_symm_sourcelefttable) = (N)) -> exists dst_positive_inverse_symm_sourcelefttable dst_negative_inverse_symm_sourcelefttable dst_value_inverse_symm_sourcelefttable. ((((exists ff_h_pvs_inverse_symm_sourcelefttableentrypositive. ff_h_pvs_inverse_symm_sourcelefttableentrypositive + S (dst_positive_inverse_symm_sourcelefttable) = S ((S (dst_index_inverse_symm_sourcelefttable)) * dst_positive_scale_inverse_symm_sourcelefttable)) /\ exists ff_q_pvs_inverse_symm_sourcelefttableentrypositive. dst_positive_code_inverse_symm_sourcelefttable = ff_q_pvs_inverse_symm_sourcelefttableentrypositive * S ((S (dst_index_inverse_symm_sourcelefttable)) * dst_positive_scale_inverse_symm_sourcelefttable) + (dst_positive_inverse_symm_sourcelefttable))) /\ (((((exists ff_h_pvs_inverse_symm_sourcelefttableentrynegative. ff_h_pvs_inverse_symm_sourcelefttableentrynegative + S (dst_negative_inverse_symm_sourcelefttable) = S ((S (dst_index_inverse_symm_sourcelefttable)) * dst_negative_scale_inverse_symm_sourcelefttable)) /\ exists ff_q_pvs_inverse_symm_sourcelefttableentrynegative. dst_negative_code_inverse_symm_sourcelefttable = ff_q_pvs_inverse_symm_sourcelefttableentrynegative * S ((S (dst_index_inverse_symm_sourcelefttable)) * dst_negative_scale_inverse_symm_sourcelefttable) + (dst_negative_inverse_symm_sourcelefttable))) /\ (exists ge_balance_positive_inverse_symm_sourcelefttableentryvalue ge_balance_negative_inverse_symm_sourcelefttableentryvalue. (((((dst_value_inverse_symm_sourcelefttable) = 2 * (ge_balance_positive_inverse_symm_sourcelefttableentryvalue) /\ (ge_balance_negative_inverse_symm_sourcelefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcelefttableentryvaluedecode. (((dst_value_inverse_symm_sourcelefttable) = 2 * ge_signed_half_inverse_symm_sourcelefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcelefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcelefttableentryvalue) = S ge_signed_half_inverse_symm_sourcelefttableentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourcelefttable) + ge_balance_negative_inverse_symm_sourcelefttableentryvalue = (dst_negative_inverse_symm_sourcelefttable) + ge_balance_positive_inverse_symm_sourcelefttableentryvalue))))))))) /\ (forall dc_input_inverse_symm_sourceleft dc_output_inverse_symm_sourceleft. ~(dc_input_inverse_symm_sourceleft=0) -> (exists pvs_le_gap_inverse_symm_sourceleftdomain. pvs_le_gap_inverse_symm_sourceleftdomain + (dc_input_inverse_symm_sourceleft) = (N)) -> (exists dst_positive_code_inverse_symm_sourceleftlookup dst_positive_scale_inverse_symm_sourceleftlookup dst_negative_code_inverse_symm_sourceleftlookup dst_negative_scale_inverse_symm_sourceleftlookup dst_positive_inverse_symm_sourceleftlookup dst_negative_inverse_symm_sourceleftlookup. (((di_delta_inverse_symm_source) = (((((dst_positive_code_inverse_symm_sourceleftlookup) + (dst_positive_scale_inverse_symm_sourceleftlookup)) * S ((dst_positive_code_inverse_symm_sourceleftlookup) + (dst_positive_scale_inverse_symm_sourceleftlookup)) + ((dst_positive_scale_inverse_symm_sourceleftlookup) + (dst_positive_scale_inverse_symm_sourceleftlookup))) + (((dst_negative_code_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)) * S ((dst_negative_code_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)) + ((dst_negative_scale_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)))) * S ((((dst_positive_code_inverse_symm_sourceleftlookup) + (dst_positive_scale_inverse_symm_sourceleftlookup)) * S ((dst_positive_code_inverse_symm_sourceleftlookup) + (dst_positive_scale_inverse_symm_sourceleftlookup)) + ((dst_positive_scale_inverse_symm_sourceleftlookup) + (dst_positive_scale_inverse_symm_sourceleftlookup))) + (((dst_negative_code_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)) * S ((dst_negative_code_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)) + ((dst_negative_scale_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)))) + ((((dst_negative_code_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)) * S ((dst_negative_code_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)) + ((dst_negative_scale_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup))) + (((dst_negative_code_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)) * S ((dst_negative_code_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)) + ((dst_negative_scale_inverse_symm_sourceleftlookup) + (dst_negative_scale_inverse_symm_sourceleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftlookuppositive. ff_h_pvs_inverse_symm_sourceleftlookuppositive + S (dst_positive_inverse_symm_sourceleftlookup) = S ((S (dc_input_inverse_symm_sourceleft)) * dst_positive_scale_inverse_symm_sourceleftlookup)) /\ exists ff_q_pvs_inverse_symm_sourceleftlookuppositive. dst_positive_code_inverse_symm_sourceleftlookup = ff_q_pvs_inverse_symm_sourceleftlookuppositive * S ((S (dc_input_inverse_symm_sourceleft)) * dst_positive_scale_inverse_symm_sourceleftlookup) + (dst_positive_inverse_symm_sourceleftlookup))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftlookupnegative. ff_h_pvs_inverse_symm_sourceleftlookupnegative + S (dst_negative_inverse_symm_sourceleftlookup) = S ((S (dc_input_inverse_symm_sourceleft)) * dst_negative_scale_inverse_symm_sourceleftlookup)) /\ exists ff_q_pvs_inverse_symm_sourceleftlookupnegative. dst_negative_code_inverse_symm_sourceleftlookup = ff_q_pvs_inverse_symm_sourceleftlookupnegative * S ((S (dc_input_inverse_symm_sourceleft)) * dst_negative_scale_inverse_symm_sourceleftlookup) + (dst_negative_inverse_symm_sourceleftlookup))) /\ (exists ge_balance_positive_inverse_symm_sourceleftlookupvalue ge_balance_negative_inverse_symm_sourceleftlookupvalue. (((((dc_output_inverse_symm_sourceleft) = 2 * (ge_balance_positive_inverse_symm_sourceleftlookupvalue) /\ (ge_balance_negative_inverse_symm_sourceleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftlookupvaluedecode. (((dc_output_inverse_symm_sourceleft) = 2 * ge_signed_half_inverse_symm_sourceleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourceleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourceleftlookupvalue) = S ge_signed_half_inverse_symm_sourceleftlookupvaluedecode))) /\ ((dst_positive_inverse_symm_sourceleftlookup) + ge_balance_negative_inverse_symm_sourceleftlookupvalue = (dst_negative_inverse_symm_sourceleftlookup) + ge_balance_positive_inverse_symm_sourceleftlookupvalue))))))))) -> (((~((dc_input_inverse_symm_sourceleft)=0)) /\ (exists dc_mask_inverse_symm_sourceleftvalue. ((((exists dst_positive_code_inverse_symm_sourceleftvaluemasktable dst_positive_scale_inverse_symm_sourceleftvaluemasktable dst_negative_code_inverse_symm_sourceleftvaluemasktable dst_negative_scale_inverse_symm_sourceleftvaluemasktable. (((dc_mask_inverse_symm_sourceleftvalue) = (((((dst_positive_code_inverse_symm_sourceleftvaluemasktable) + (dst_positive_scale_inverse_symm_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_symm_sourceleftvaluemasktable) + (dst_positive_scale_inverse_symm_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_symm_sourceleftvaluemasktable) + (dst_positive_scale_inverse_symm_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)))) * S ((((dst_positive_code_inverse_symm_sourceleftvaluemasktable) + (dst_positive_scale_inverse_symm_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_symm_sourceleftvaluemasktable) + (dst_positive_scale_inverse_symm_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_symm_sourceleftvaluemasktable) + (dst_positive_scale_inverse_symm_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)))) + ((((dst_negative_code_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemasktable) + (dst_negative_scale_inverse_symm_sourceleftvaluemasktable)))))) /\ (forall dst_index_inverse_symm_sourceleftvaluemasktable. (exists pvs_le_gap_inverse_symm_sourceleftvaluemasktabledomain. pvs_le_gap_inverse_symm_sourceleftvaluemasktabledomain + (dst_index_inverse_symm_sourceleftvaluemasktable) = (dc_input_inverse_symm_sourceleft)) -> exists dst_positive_inverse_symm_sourceleftvaluemasktable dst_negative_inverse_symm_sourceleftvaluemasktable dst_value_inverse_symm_sourceleftvaluemasktable. ((((exists ff_h_pvs_inverse_symm_sourceleftvaluemasktableentrypositive. ff_h_pvs_inverse_symm_sourceleftvaluemasktableentrypositive + S (dst_positive_inverse_symm_sourceleftvaluemasktable) = S ((S (dst_index_inverse_symm_sourceleftvaluemasktable)) * dst_positive_scale_inverse_symm_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_symm_sourceleftvaluemasktableentrypositive. dst_positive_code_inverse_symm_sourceleftvaluemasktable = ff_q_pvs_inverse_symm_sourceleftvaluemasktableentrypositive * S ((S (dst_index_inverse_symm_sourceleftvaluemasktable)) * dst_positive_scale_inverse_symm_sourceleftvaluemasktable) + (dst_positive_inverse_symm_sourceleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftvaluemasktableentrynegative. ff_h_pvs_inverse_symm_sourceleftvaluemasktableentrynegative + S (dst_negative_inverse_symm_sourceleftvaluemasktable) = S ((S (dst_index_inverse_symm_sourceleftvaluemasktable)) * dst_negative_scale_inverse_symm_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_symm_sourceleftvaluemasktableentrynegative. dst_negative_code_inverse_symm_sourceleftvaluemasktable = ff_q_pvs_inverse_symm_sourceleftvaluemasktableentrynegative * S ((S (dst_index_inverse_symm_sourceleftvaluemasktable)) * dst_negative_scale_inverse_symm_sourceleftvaluemasktable) + (dst_negative_inverse_symm_sourceleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_symm_sourceleftvaluemasktableentryvalue ge_balance_negative_inverse_symm_sourceleftvaluemasktableentryvalue. (((((dst_value_inverse_symm_sourceleftvaluemasktable) = 2 * (ge_balance_positive_inverse_symm_sourceleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_symm_sourceleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftvaluemasktableentryvaluedecode. (((dst_value_inverse_symm_sourceleftvaluemasktable) = 2 * ge_signed_half_inverse_symm_sourceleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourceleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourceleftvaluemasktableentryvalue) = S ge_signed_half_inverse_symm_sourceleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourceleftvaluemasktable) + ge_balance_negative_inverse_symm_sourceleftvaluemasktableentryvalue = (dst_negative_inverse_symm_sourceleftvaluemasktable) + ge_balance_positive_inverse_symm_sourceleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_symm_sourceleftvaluemask dc_value_inverse_symm_sourceleftvaluemask. (exists pvs_le_gap_inverse_symm_sourceleftvaluemaskdomain. pvs_le_gap_inverse_symm_sourceleftvaluemaskdomain + (dc_index_inverse_symm_sourceleftvaluemask) = (dc_input_inverse_symm_sourceleft)) -> (exists dst_positive_code_inverse_symm_sourceleftvaluemasklookup dst_positive_scale_inverse_symm_sourceleftvaluemasklookup dst_negative_code_inverse_symm_sourceleftvaluemasklookup dst_negative_scale_inverse_symm_sourceleftvaluemasklookup dst_positive_inverse_symm_sourceleftvaluemasklookup dst_negative_inverse_symm_sourceleftvaluemasklookup. (((dc_mask_inverse_symm_sourceleftvalue) = (((((dst_positive_code_inverse_symm_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_symm_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_symm_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_symm_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_symm_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_symm_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_symm_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_symm_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_symm_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_symm_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_symm_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_symm_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)))) + ((((dst_negative_code_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftvaluemasklookuppositive. ff_h_pvs_inverse_symm_sourceleftvaluemasklookuppositive + S (dst_positive_inverse_symm_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_symm_sourceleftvaluemask)) * dst_positive_scale_inverse_symm_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_symm_sourceleftvaluemasklookuppositive. dst_positive_code_inverse_symm_sourceleftvaluemasklookup = ff_q_pvs_inverse_symm_sourceleftvaluemasklookuppositive * S ((S (dc_index_inverse_symm_sourceleftvaluemask)) * dst_positive_scale_inverse_symm_sourceleftvaluemasklookup) + (dst_positive_inverse_symm_sourceleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftvaluemasklookupnegative. ff_h_pvs_inverse_symm_sourceleftvaluemasklookupnegative + S (dst_negative_inverse_symm_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_symm_sourceleftvaluemask)) * dst_negative_scale_inverse_symm_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_symm_sourceleftvaluemasklookupnegative. dst_negative_code_inverse_symm_sourceleftvaluemasklookup = ff_q_pvs_inverse_symm_sourceleftvaluemasklookupnegative * S ((S (dc_index_inverse_symm_sourceleftvaluemask)) * dst_negative_scale_inverse_symm_sourceleftvaluemasklookup) + (dst_negative_inverse_symm_sourceleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_symm_sourceleftvaluemasklookupvalue ge_balance_negative_inverse_symm_sourceleftvaluemasklookupvalue. (((((dc_value_inverse_symm_sourceleftvaluemask) = 2 * (ge_balance_positive_inverse_symm_sourceleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_symm_sourceleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftvaluemasklookupvaluedecode. (((dc_value_inverse_symm_sourceleftvaluemask) = 2 * ge_signed_half_inverse_symm_sourceleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourceleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourceleftvaluemasklookupvalue) = S ge_signed_half_inverse_symm_sourceleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_symm_sourceleftvaluemasklookup) + ge_balance_negative_inverse_symm_sourceleftvaluemasklookupvalue = (dst_negative_inverse_symm_sourceleftvaluemasklookup) + ge_balance_positive_inverse_symm_sourceleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_symm_sourceleftvaluemask)=0)) /\ (exists dc_quotient_inverse_symm_sourceleftvaluemaskentry dc_left_inverse_symm_sourceleftvaluemaskentry dc_right_inverse_symm_sourceleftvaluemaskentry. (((dc_input_inverse_symm_sourceleft)=(dc_index_inverse_symm_sourceleftvaluemask)*dc_quotient_inverse_symm_sourceleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_symm_sourceleftvaluemaskentryleft dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft dst_positive_inverse_symm_sourceleftvaluemaskentryleft dst_negative_inverse_symm_sourceleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftvaluemaskentryleftpositive. ff_h_pvs_inverse_symm_sourceleftvaluemaskentryleftpositive + S (dst_positive_inverse_symm_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_symm_sourceleftvaluemask)) * dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_symm_sourceleftvaluemaskentryleftpositive. dst_positive_code_inverse_symm_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_symm_sourceleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_symm_sourceleftvaluemask)) * dst_positive_scale_inverse_symm_sourceleftvaluemaskentryleft) + (dst_positive_inverse_symm_sourceleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftvaluemaskentryleftnegative. ff_h_pvs_inverse_symm_sourceleftvaluemaskentryleftnegative + S (dst_negative_inverse_symm_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_symm_sourceleftvaluemask)) * dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_symm_sourceleftvaluemaskentryleftnegative. dst_negative_code_inverse_symm_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_symm_sourceleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_symm_sourceleftvaluemask)) * dst_negative_scale_inverse_symm_sourceleftvaluemaskentryleft) + (dst_negative_inverse_symm_sourceleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_symm_sourceleftvaluemaskentryleftvalue ge_balance_negative_inverse_symm_sourceleftvaluemaskentryleftvalue. (((((dc_left_inverse_symm_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_symm_sourceleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_symm_sourceleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_symm_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_symm_sourceleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourceleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourceleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_symm_sourceleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_symm_sourceleftvaluemaskentryleft) + ge_balance_negative_inverse_symm_sourceleftvaluemaskentryleftvalue = (dst_negative_inverse_symm_sourceleftvaluemaskentryleft) + ge_balance_positive_inverse_symm_sourceleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_sourceleftvaluemaskentryright dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright dst_negative_code_inverse_symm_sourceleftvaluemaskentryright dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright dst_positive_inverse_symm_sourceleftvaluemaskentryright dst_negative_inverse_symm_sourceleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftvaluemaskentryrightpositive. ff_h_pvs_inverse_symm_sourceleftvaluemaskentryrightpositive + S (dst_positive_inverse_symm_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_symm_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_symm_sourceleftvaluemaskentryrightpositive. dst_positive_code_inverse_symm_sourceleftvaluemaskentryright = ff_q_pvs_inverse_symm_sourceleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_symm_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_symm_sourceleftvaluemaskentryright) + (dst_positive_inverse_symm_sourceleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_symm_sourceleftvaluemaskentryrightnegative. ff_h_pvs_inverse_symm_sourceleftvaluemaskentryrightnegative + S (dst_negative_inverse_symm_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_symm_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_symm_sourceleftvaluemaskentryrightnegative. dst_negative_code_inverse_symm_sourceleftvaluemaskentryright = ff_q_pvs_inverse_symm_sourceleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_symm_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_symm_sourceleftvaluemaskentryright) + (dst_negative_inverse_symm_sourceleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_symm_sourceleftvaluemaskentryrightvalue ge_balance_negative_inverse_symm_sourceleftvaluemaskentryrightvalue. (((((dc_right_inverse_symm_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_symm_sourceleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_symm_sourceleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_symm_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_symm_sourceleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourceleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourceleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_symm_sourceleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_symm_sourceleftvaluemaskentryright) + ge_balance_negative_inverse_symm_sourceleftvaluemaskentryrightvalue = (dst_negative_inverse_symm_sourceleftvaluemaskentryright) + ge_balance_positive_inverse_symm_sourceleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_symm_sourceleftvaluemaskentryproduct sto_an_inverse_symm_sourceleftvaluemaskentryproduct sto_bp_inverse_symm_sourceleftvaluemaskentryproduct sto_bn_inverse_symm_sourceleftvaluemaskentryproduct sto_cp_inverse_symm_sourceleftvaluemaskentryproduct sto_cn_inverse_symm_sourceleftvaluemaskentryproduct. (((((dc_left_inverse_symm_sourceleftvaluemaskentry) = 2 * (sto_ap_inverse_symm_sourceleftvaluemaskentryproduct) /\ (sto_an_inverse_symm_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductleft. (((dc_left_inverse_symm_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_symm_sourceleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_symm_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_symm_sourceleftvaluemaskentry) = 2 * (sto_bp_inverse_symm_sourceleftvaluemaskentryproduct) /\ (sto_bn_inverse_symm_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductright. (((dc_right_inverse_symm_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_symm_sourceleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_symm_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_symm_sourceleftvaluemask) = 2 * (sto_cp_inverse_symm_sourceleftvaluemaskentryproduct) /\ (sto_cn_inverse_symm_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductoutput. (((dc_value_inverse_symm_sourceleftvaluemask) = 2 * ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_symm_sourceleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_symm_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_symm_sourceleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_symm_sourceleftvaluemaskentryproduct * sto_bp_inverse_symm_sourceleftvaluemaskentryproduct + sto_an_inverse_symm_sourceleftvaluemaskentryproduct * sto_bn_inverse_symm_sourceleftvaluemaskentryproduct) + sto_cn_inverse_symm_sourceleftvaluemaskentryproduct = (sto_ap_inverse_symm_sourceleftvaluemaskentryproduct * sto_bn_inverse_symm_sourceleftvaluemaskentryproduct + sto_an_inverse_symm_sourceleftvaluemaskentryproduct * sto_bp_inverse_symm_sourceleftvaluemaskentryproduct) + sto_cp_inverse_symm_sourceleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_symm_sourceleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_symm_sourceleftvaluemaskentrynondivisor. (dc_input_inverse_symm_sourceleft) = (dc_index_inverse_symm_sourceleftvaluemask) * pvs_factor_inverse_symm_sourceleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_symm_sourceleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_symm_sourceleftvaluefold dst_positive_scale_inverse_symm_sourceleftvaluefold dst_negative_code_inverse_symm_sourceleftvaluefold dst_negative_scale_inverse_symm_sourceleftvaluefold dst_positive_sum_inverse_symm_sourceleftvaluefold dst_negative_sum_inverse_symm_sourceleftvaluefold. (((dc_mask_inverse_symm_sourceleftvalue) = (((((dst_positive_code_inverse_symm_sourceleftvaluefold) + (dst_positive_scale_inverse_symm_sourceleftvaluefold)) * S ((dst_positive_code_inverse_symm_sourceleftvaluefold) + (dst_positive_scale_inverse_symm_sourceleftvaluefold)) + ((dst_positive_scale_inverse_symm_sourceleftvaluefold) + (dst_positive_scale_inverse_symm_sourceleftvaluefold))) + (((dst_negative_code_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)) * S ((dst_negative_code_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)) + ((dst_negative_scale_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)))) * S ((((dst_positive_code_inverse_symm_sourceleftvaluefold) + (dst_positive_scale_inverse_symm_sourceleftvaluefold)) * S ((dst_positive_code_inverse_symm_sourceleftvaluefold) + (dst_positive_scale_inverse_symm_sourceleftvaluefold)) + ((dst_positive_scale_inverse_symm_sourceleftvaluefold) + (dst_positive_scale_inverse_symm_sourceleftvaluefold))) + (((dst_negative_code_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)) * S ((dst_negative_code_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)) + ((dst_negative_scale_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)))) + ((((dst_negative_code_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)) * S ((dst_negative_code_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)) + ((dst_negative_scale_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold))) + (((dst_negative_code_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)) * S ((dst_negative_code_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)) + ((dst_negative_scale_inverse_symm_sourceleftvaluefold) + (dst_negative_scale_inverse_symm_sourceleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_symm_sourceleftvaluefoldpositive fs_v_dst_inverse_symm_sourceleftvaluefoldpositive. ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_start. fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_symm_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_start. fs_u_dst_inverse_symm_sourceleftvaluefoldpositive = fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_symm_sourceleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_symm_sourceleftvaluefold) = S ((S (S (dc_input_inverse_symm_sourceleft))) * fs_v_dst_inverse_symm_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_symm_sourceleftvaluefoldpositive = fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_symm_sourceleft))) * fs_v_dst_inverse_symm_sourceleftvaluefoldpositive) + (dst_positive_sum_inverse_symm_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps = S (dc_input_inverse_symm_sourceleft)) -> exists fs_a_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps fs_r_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps fs_s_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_symm_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_symm_sourceleftvaluefold = fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_symm_sourceleftvaluefold) + (fs_a_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_symm_sourceleftvaluefoldpositive = fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_sourceleftvaluefoldpositive) + (fs_r_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_symm_sourceleftvaluefoldpositive = fs_q_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_sourceleftvaluefoldpositive) + (fs_s_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps = fs_r_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps + fs_a_dst_inverse_symm_sourceleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_symm_sourceleftvaluefoldnegative fs_v_dst_inverse_symm_sourceleftvaluefoldnegative. ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_start. fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_symm_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_start. fs_u_dst_inverse_symm_sourceleftvaluefoldnegative = fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_symm_sourceleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_symm_sourceleftvaluefold) = S ((S (S (dc_input_inverse_symm_sourceleft))) * fs_v_dst_inverse_symm_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_symm_sourceleftvaluefoldnegative = fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_symm_sourceleft))) * fs_v_dst_inverse_symm_sourceleftvaluefoldnegative) + (dst_negative_sum_inverse_symm_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps = S (dc_input_inverse_symm_sourceleft)) -> exists fs_a_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps fs_r_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps fs_s_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_symm_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_symm_sourceleftvaluefold = fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_symm_sourceleftvaluefold) + (fs_a_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_symm_sourceleftvaluefoldnegative = fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_sourceleftvaluefoldnegative) + (fs_r_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_symm_sourceleftvaluefoldnegative = fs_q_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_sourceleftvaluefoldnegative) + (fs_s_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps = fs_r_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps + fs_a_dst_inverse_symm_sourceleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_symm_sourceleftvaluefoldresult ge_balance_negative_inverse_symm_sourceleftvaluefoldresult. (((((dc_output_inverse_symm_sourceleft) = 2 * (ge_balance_positive_inverse_symm_sourceleftvaluefoldresult) /\ (ge_balance_negative_inverse_symm_sourceleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_symm_sourceleftvaluefoldresultdecode. (((dc_output_inverse_symm_sourceleft) = 2 * ge_signed_half_inverse_symm_sourceleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_symm_sourceleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_symm_sourceleftvaluefoldresult) = S ge_signed_half_inverse_symm_sourceleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_symm_sourceleftvaluefold) + ge_balance_negative_inverse_symm_sourceleftvaluefoldresult = (dst_negative_sum_inverse_symm_sourceleftvaluefold) + ge_balance_positive_inverse_symm_sourceleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_symm_sourcerightleft dst_positive_scale_inverse_symm_sourcerightleft dst_negative_code_inverse_symm_sourcerightleft dst_negative_scale_inverse_symm_sourcerightleft. (((G) = (((((dst_positive_code_inverse_symm_sourcerightleft) + (dst_positive_scale_inverse_symm_sourcerightleft)) * S ((dst_positive_code_inverse_symm_sourcerightleft) + (dst_positive_scale_inverse_symm_sourcerightleft)) + ((dst_positive_scale_inverse_symm_sourcerightleft) + (dst_positive_scale_inverse_symm_sourcerightleft))) + (((dst_negative_code_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)) * S ((dst_negative_code_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)) + ((dst_negative_scale_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)))) * S ((((dst_positive_code_inverse_symm_sourcerightleft) + (dst_positive_scale_inverse_symm_sourcerightleft)) * S ((dst_positive_code_inverse_symm_sourcerightleft) + (dst_positive_scale_inverse_symm_sourcerightleft)) + ((dst_positive_scale_inverse_symm_sourcerightleft) + (dst_positive_scale_inverse_symm_sourcerightleft))) + (((dst_negative_code_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)) * S ((dst_negative_code_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)) + ((dst_negative_scale_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)))) + ((((dst_negative_code_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)) * S ((dst_negative_code_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)) + ((dst_negative_scale_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft))) + (((dst_negative_code_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)) * S ((dst_negative_code_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)) + ((dst_negative_scale_inverse_symm_sourcerightleft) + (dst_negative_scale_inverse_symm_sourcerightleft)))))) /\ (forall dst_index_inverse_symm_sourcerightleft. (exists pvs_le_gap_inverse_symm_sourcerightleftdomain. pvs_le_gap_inverse_symm_sourcerightleftdomain + (dst_index_inverse_symm_sourcerightleft) = (N)) -> exists dst_positive_inverse_symm_sourcerightleft dst_negative_inverse_symm_sourcerightleft dst_value_inverse_symm_sourcerightleft. ((((exists ff_h_pvs_inverse_symm_sourcerightleftentrypositive. ff_h_pvs_inverse_symm_sourcerightleftentrypositive + S (dst_positive_inverse_symm_sourcerightleft) = S ((S (dst_index_inverse_symm_sourcerightleft)) * dst_positive_scale_inverse_symm_sourcerightleft)) /\ exists ff_q_pvs_inverse_symm_sourcerightleftentrypositive. dst_positive_code_inverse_symm_sourcerightleft = ff_q_pvs_inverse_symm_sourcerightleftentrypositive * S ((S (dst_index_inverse_symm_sourcerightleft)) * dst_positive_scale_inverse_symm_sourcerightleft) + (dst_positive_inverse_symm_sourcerightleft))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightleftentrynegative. ff_h_pvs_inverse_symm_sourcerightleftentrynegative + S (dst_negative_inverse_symm_sourcerightleft) = S ((S (dst_index_inverse_symm_sourcerightleft)) * dst_negative_scale_inverse_symm_sourcerightleft)) /\ exists ff_q_pvs_inverse_symm_sourcerightleftentrynegative. dst_negative_code_inverse_symm_sourcerightleft = ff_q_pvs_inverse_symm_sourcerightleftentrynegative * S ((S (dst_index_inverse_symm_sourcerightleft)) * dst_negative_scale_inverse_symm_sourcerightleft) + (dst_negative_inverse_symm_sourcerightleft))) /\ (exists ge_balance_positive_inverse_symm_sourcerightleftentryvalue ge_balance_negative_inverse_symm_sourcerightleftentryvalue. (((((dst_value_inverse_symm_sourcerightleft) = 2 * (ge_balance_positive_inverse_symm_sourcerightleftentryvalue) /\ (ge_balance_negative_inverse_symm_sourcerightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightleftentryvaluedecode. (((dst_value_inverse_symm_sourcerightleft) = 2 * ge_signed_half_inverse_symm_sourcerightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcerightleftentryvalue) = S ge_signed_half_inverse_symm_sourcerightleftentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourcerightleft) + ge_balance_negative_inverse_symm_sourcerightleftentryvalue = (dst_negative_inverse_symm_sourcerightleft) + ge_balance_positive_inverse_symm_sourcerightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_sourcerightright dst_positive_scale_inverse_symm_sourcerightright dst_negative_code_inverse_symm_sourcerightright dst_negative_scale_inverse_symm_sourcerightright. (((F) = (((((dst_positive_code_inverse_symm_sourcerightright) + (dst_positive_scale_inverse_symm_sourcerightright)) * S ((dst_positive_code_inverse_symm_sourcerightright) + (dst_positive_scale_inverse_symm_sourcerightright)) + ((dst_positive_scale_inverse_symm_sourcerightright) + (dst_positive_scale_inverse_symm_sourcerightright))) + (((dst_negative_code_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)) * S ((dst_negative_code_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)) + ((dst_negative_scale_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)))) * S ((((dst_positive_code_inverse_symm_sourcerightright) + (dst_positive_scale_inverse_symm_sourcerightright)) * S ((dst_positive_code_inverse_symm_sourcerightright) + (dst_positive_scale_inverse_symm_sourcerightright)) + ((dst_positive_scale_inverse_symm_sourcerightright) + (dst_positive_scale_inverse_symm_sourcerightright))) + (((dst_negative_code_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)) * S ((dst_negative_code_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)) + ((dst_negative_scale_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)))) + ((((dst_negative_code_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)) * S ((dst_negative_code_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)) + ((dst_negative_scale_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright))) + (((dst_negative_code_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)) * S ((dst_negative_code_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)) + ((dst_negative_scale_inverse_symm_sourcerightright) + (dst_negative_scale_inverse_symm_sourcerightright)))))) /\ (forall dst_index_inverse_symm_sourcerightright. (exists pvs_le_gap_inverse_symm_sourcerightrightdomain. pvs_le_gap_inverse_symm_sourcerightrightdomain + (dst_index_inverse_symm_sourcerightright) = (N)) -> exists dst_positive_inverse_symm_sourcerightright dst_negative_inverse_symm_sourcerightright dst_value_inverse_symm_sourcerightright. ((((exists ff_h_pvs_inverse_symm_sourcerightrightentrypositive. ff_h_pvs_inverse_symm_sourcerightrightentrypositive + S (dst_positive_inverse_symm_sourcerightright) = S ((S (dst_index_inverse_symm_sourcerightright)) * dst_positive_scale_inverse_symm_sourcerightright)) /\ exists ff_q_pvs_inverse_symm_sourcerightrightentrypositive. dst_positive_code_inverse_symm_sourcerightright = ff_q_pvs_inverse_symm_sourcerightrightentrypositive * S ((S (dst_index_inverse_symm_sourcerightright)) * dst_positive_scale_inverse_symm_sourcerightright) + (dst_positive_inverse_symm_sourcerightright))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightrightentrynegative. ff_h_pvs_inverse_symm_sourcerightrightentrynegative + S (dst_negative_inverse_symm_sourcerightright) = S ((S (dst_index_inverse_symm_sourcerightright)) * dst_negative_scale_inverse_symm_sourcerightright)) /\ exists ff_q_pvs_inverse_symm_sourcerightrightentrynegative. dst_negative_code_inverse_symm_sourcerightright = ff_q_pvs_inverse_symm_sourcerightrightentrynegative * S ((S (dst_index_inverse_symm_sourcerightright)) * dst_negative_scale_inverse_symm_sourcerightright) + (dst_negative_inverse_symm_sourcerightright))) /\ (exists ge_balance_positive_inverse_symm_sourcerightrightentryvalue ge_balance_negative_inverse_symm_sourcerightrightentryvalue. (((((dst_value_inverse_symm_sourcerightright) = 2 * (ge_balance_positive_inverse_symm_sourcerightrightentryvalue) /\ (ge_balance_negative_inverse_symm_sourcerightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightrightentryvaluedecode. (((dst_value_inverse_symm_sourcerightright) = 2 * ge_signed_half_inverse_symm_sourcerightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcerightrightentryvalue) = S ge_signed_half_inverse_symm_sourcerightrightentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourcerightright) + ge_balance_negative_inverse_symm_sourcerightrightentryvalue = (dst_negative_inverse_symm_sourcerightright) + ge_balance_positive_inverse_symm_sourcerightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_sourcerighttable dst_positive_scale_inverse_symm_sourcerighttable dst_negative_code_inverse_symm_sourcerighttable dst_negative_scale_inverse_symm_sourcerighttable. (((di_delta_inverse_symm_source) = (((((dst_positive_code_inverse_symm_sourcerighttable) + (dst_positive_scale_inverse_symm_sourcerighttable)) * S ((dst_positive_code_inverse_symm_sourcerighttable) + (dst_positive_scale_inverse_symm_sourcerighttable)) + ((dst_positive_scale_inverse_symm_sourcerighttable) + (dst_positive_scale_inverse_symm_sourcerighttable))) + (((dst_negative_code_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)) * S ((dst_negative_code_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)) + ((dst_negative_scale_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)))) * S ((((dst_positive_code_inverse_symm_sourcerighttable) + (dst_positive_scale_inverse_symm_sourcerighttable)) * S ((dst_positive_code_inverse_symm_sourcerighttable) + (dst_positive_scale_inverse_symm_sourcerighttable)) + ((dst_positive_scale_inverse_symm_sourcerighttable) + (dst_positive_scale_inverse_symm_sourcerighttable))) + (((dst_negative_code_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)) * S ((dst_negative_code_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)) + ((dst_negative_scale_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)))) + ((((dst_negative_code_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)) * S ((dst_negative_code_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)) + ((dst_negative_scale_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable))) + (((dst_negative_code_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)) * S ((dst_negative_code_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)) + ((dst_negative_scale_inverse_symm_sourcerighttable) + (dst_negative_scale_inverse_symm_sourcerighttable)))))) /\ (forall dst_index_inverse_symm_sourcerighttable. (exists pvs_le_gap_inverse_symm_sourcerighttabledomain. pvs_le_gap_inverse_symm_sourcerighttabledomain + (dst_index_inverse_symm_sourcerighttable) = (N)) -> exists dst_positive_inverse_symm_sourcerighttable dst_negative_inverse_symm_sourcerighttable dst_value_inverse_symm_sourcerighttable. ((((exists ff_h_pvs_inverse_symm_sourcerighttableentrypositive. ff_h_pvs_inverse_symm_sourcerighttableentrypositive + S (dst_positive_inverse_symm_sourcerighttable) = S ((S (dst_index_inverse_symm_sourcerighttable)) * dst_positive_scale_inverse_symm_sourcerighttable)) /\ exists ff_q_pvs_inverse_symm_sourcerighttableentrypositive. dst_positive_code_inverse_symm_sourcerighttable = ff_q_pvs_inverse_symm_sourcerighttableentrypositive * S ((S (dst_index_inverse_symm_sourcerighttable)) * dst_positive_scale_inverse_symm_sourcerighttable) + (dst_positive_inverse_symm_sourcerighttable))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerighttableentrynegative. ff_h_pvs_inverse_symm_sourcerighttableentrynegative + S (dst_negative_inverse_symm_sourcerighttable) = S ((S (dst_index_inverse_symm_sourcerighttable)) * dst_negative_scale_inverse_symm_sourcerighttable)) /\ exists ff_q_pvs_inverse_symm_sourcerighttableentrynegative. dst_negative_code_inverse_symm_sourcerighttable = ff_q_pvs_inverse_symm_sourcerighttableentrynegative * S ((S (dst_index_inverse_symm_sourcerighttable)) * dst_negative_scale_inverse_symm_sourcerighttable) + (dst_negative_inverse_symm_sourcerighttable))) /\ (exists ge_balance_positive_inverse_symm_sourcerighttableentryvalue ge_balance_negative_inverse_symm_sourcerighttableentryvalue. (((((dst_value_inverse_symm_sourcerighttable) = 2 * (ge_balance_positive_inverse_symm_sourcerighttableentryvalue) /\ (ge_balance_negative_inverse_symm_sourcerighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcerighttableentryvaluedecode. (((dst_value_inverse_symm_sourcerighttable) = 2 * ge_signed_half_inverse_symm_sourcerighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcerighttableentryvalue) = S ge_signed_half_inverse_symm_sourcerighttableentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourcerighttable) + ge_balance_negative_inverse_symm_sourcerighttableentryvalue = (dst_negative_inverse_symm_sourcerighttable) + ge_balance_positive_inverse_symm_sourcerighttableentryvalue))))))))) /\ (forall dc_input_inverse_symm_sourceright dc_output_inverse_symm_sourceright. ~(dc_input_inverse_symm_sourceright=0) -> (exists pvs_le_gap_inverse_symm_sourcerightdomain. pvs_le_gap_inverse_symm_sourcerightdomain + (dc_input_inverse_symm_sourceright) = (N)) -> (exists dst_positive_code_inverse_symm_sourcerightlookup dst_positive_scale_inverse_symm_sourcerightlookup dst_negative_code_inverse_symm_sourcerightlookup dst_negative_scale_inverse_symm_sourcerightlookup dst_positive_inverse_symm_sourcerightlookup dst_negative_inverse_symm_sourcerightlookup. (((di_delta_inverse_symm_source) = (((((dst_positive_code_inverse_symm_sourcerightlookup) + (dst_positive_scale_inverse_symm_sourcerightlookup)) * S ((dst_positive_code_inverse_symm_sourcerightlookup) + (dst_positive_scale_inverse_symm_sourcerightlookup)) + ((dst_positive_scale_inverse_symm_sourcerightlookup) + (dst_positive_scale_inverse_symm_sourcerightlookup))) + (((dst_negative_code_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)) * S ((dst_negative_code_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)) + ((dst_negative_scale_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)))) * S ((((dst_positive_code_inverse_symm_sourcerightlookup) + (dst_positive_scale_inverse_symm_sourcerightlookup)) * S ((dst_positive_code_inverse_symm_sourcerightlookup) + (dst_positive_scale_inverse_symm_sourcerightlookup)) + ((dst_positive_scale_inverse_symm_sourcerightlookup) + (dst_positive_scale_inverse_symm_sourcerightlookup))) + (((dst_negative_code_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)) * S ((dst_negative_code_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)) + ((dst_negative_scale_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)))) + ((((dst_negative_code_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)) * S ((dst_negative_code_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)) + ((dst_negative_scale_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup))) + (((dst_negative_code_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)) * S ((dst_negative_code_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)) + ((dst_negative_scale_inverse_symm_sourcerightlookup) + (dst_negative_scale_inverse_symm_sourcerightlookup)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightlookuppositive. ff_h_pvs_inverse_symm_sourcerightlookuppositive + S (dst_positive_inverse_symm_sourcerightlookup) = S ((S (dc_input_inverse_symm_sourceright)) * dst_positive_scale_inverse_symm_sourcerightlookup)) /\ exists ff_q_pvs_inverse_symm_sourcerightlookuppositive. dst_positive_code_inverse_symm_sourcerightlookup = ff_q_pvs_inverse_symm_sourcerightlookuppositive * S ((S (dc_input_inverse_symm_sourceright)) * dst_positive_scale_inverse_symm_sourcerightlookup) + (dst_positive_inverse_symm_sourcerightlookup))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightlookupnegative. ff_h_pvs_inverse_symm_sourcerightlookupnegative + S (dst_negative_inverse_symm_sourcerightlookup) = S ((S (dc_input_inverse_symm_sourceright)) * dst_negative_scale_inverse_symm_sourcerightlookup)) /\ exists ff_q_pvs_inverse_symm_sourcerightlookupnegative. dst_negative_code_inverse_symm_sourcerightlookup = ff_q_pvs_inverse_symm_sourcerightlookupnegative * S ((S (dc_input_inverse_symm_sourceright)) * dst_negative_scale_inverse_symm_sourcerightlookup) + (dst_negative_inverse_symm_sourcerightlookup))) /\ (exists ge_balance_positive_inverse_symm_sourcerightlookupvalue ge_balance_negative_inverse_symm_sourcerightlookupvalue. (((((dc_output_inverse_symm_sourceright) = 2 * (ge_balance_positive_inverse_symm_sourcerightlookupvalue) /\ (ge_balance_negative_inverse_symm_sourcerightlookupvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightlookupvaluedecode. (((dc_output_inverse_symm_sourceright) = 2 * ge_signed_half_inverse_symm_sourcerightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerightlookupvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcerightlookupvalue) = S ge_signed_half_inverse_symm_sourcerightlookupvaluedecode))) /\ ((dst_positive_inverse_symm_sourcerightlookup) + ge_balance_negative_inverse_symm_sourcerightlookupvalue = (dst_negative_inverse_symm_sourcerightlookup) + ge_balance_positive_inverse_symm_sourcerightlookupvalue))))))))) -> (((~((dc_input_inverse_symm_sourceright)=0)) /\ (exists dc_mask_inverse_symm_sourcerightvalue. ((((exists dst_positive_code_inverse_symm_sourcerightvaluemasktable dst_positive_scale_inverse_symm_sourcerightvaluemasktable dst_negative_code_inverse_symm_sourcerightvaluemasktable dst_negative_scale_inverse_symm_sourcerightvaluemasktable. (((dc_mask_inverse_symm_sourcerightvalue) = (((((dst_positive_code_inverse_symm_sourcerightvaluemasktable) + (dst_positive_scale_inverse_symm_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_symm_sourcerightvaluemasktable) + (dst_positive_scale_inverse_symm_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_symm_sourcerightvaluemasktable) + (dst_positive_scale_inverse_symm_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)))) * S ((((dst_positive_code_inverse_symm_sourcerightvaluemasktable) + (dst_positive_scale_inverse_symm_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_symm_sourcerightvaluemasktable) + (dst_positive_scale_inverse_symm_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_symm_sourcerightvaluemasktable) + (dst_positive_scale_inverse_symm_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)))) + ((((dst_negative_code_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemasktable) + (dst_negative_scale_inverse_symm_sourcerightvaluemasktable)))))) /\ (forall dst_index_inverse_symm_sourcerightvaluemasktable. (exists pvs_le_gap_inverse_symm_sourcerightvaluemasktabledomain. pvs_le_gap_inverse_symm_sourcerightvaluemasktabledomain + (dst_index_inverse_symm_sourcerightvaluemasktable) = (dc_input_inverse_symm_sourceright)) -> exists dst_positive_inverse_symm_sourcerightvaluemasktable dst_negative_inverse_symm_sourcerightvaluemasktable dst_value_inverse_symm_sourcerightvaluemasktable. ((((exists ff_h_pvs_inverse_symm_sourcerightvaluemasktableentrypositive. ff_h_pvs_inverse_symm_sourcerightvaluemasktableentrypositive + S (dst_positive_inverse_symm_sourcerightvaluemasktable) = S ((S (dst_index_inverse_symm_sourcerightvaluemasktable)) * dst_positive_scale_inverse_symm_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_symm_sourcerightvaluemasktableentrypositive. dst_positive_code_inverse_symm_sourcerightvaluemasktable = ff_q_pvs_inverse_symm_sourcerightvaluemasktableentrypositive * S ((S (dst_index_inverse_symm_sourcerightvaluemasktable)) * dst_positive_scale_inverse_symm_sourcerightvaluemasktable) + (dst_positive_inverse_symm_sourcerightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightvaluemasktableentrynegative. ff_h_pvs_inverse_symm_sourcerightvaluemasktableentrynegative + S (dst_negative_inverse_symm_sourcerightvaluemasktable) = S ((S (dst_index_inverse_symm_sourcerightvaluemasktable)) * dst_negative_scale_inverse_symm_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_symm_sourcerightvaluemasktableentrynegative. dst_negative_code_inverse_symm_sourcerightvaluemasktable = ff_q_pvs_inverse_symm_sourcerightvaluemasktableentrynegative * S ((S (dst_index_inverse_symm_sourcerightvaluemasktable)) * dst_negative_scale_inverse_symm_sourcerightvaluemasktable) + (dst_negative_inverse_symm_sourcerightvaluemasktable))) /\ (exists ge_balance_positive_inverse_symm_sourcerightvaluemasktableentryvalue ge_balance_negative_inverse_symm_sourcerightvaluemasktableentryvalue. (((((dst_value_inverse_symm_sourcerightvaluemasktable) = 2 * (ge_balance_positive_inverse_symm_sourcerightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_symm_sourcerightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightvaluemasktableentryvaluedecode. (((dst_value_inverse_symm_sourcerightvaluemasktable) = 2 * ge_signed_half_inverse_symm_sourcerightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcerightvaluemasktableentryvalue) = S ge_signed_half_inverse_symm_sourcerightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_symm_sourcerightvaluemasktable) + ge_balance_negative_inverse_symm_sourcerightvaluemasktableentryvalue = (dst_negative_inverse_symm_sourcerightvaluemasktable) + ge_balance_positive_inverse_symm_sourcerightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_symm_sourcerightvaluemask dc_value_inverse_symm_sourcerightvaluemask. (exists pvs_le_gap_inverse_symm_sourcerightvaluemaskdomain. pvs_le_gap_inverse_symm_sourcerightvaluemaskdomain + (dc_index_inverse_symm_sourcerightvaluemask) = (dc_input_inverse_symm_sourceright)) -> (exists dst_positive_code_inverse_symm_sourcerightvaluemasklookup dst_positive_scale_inverse_symm_sourcerightvaluemasklookup dst_negative_code_inverse_symm_sourcerightvaluemasklookup dst_negative_scale_inverse_symm_sourcerightvaluemasklookup dst_positive_inverse_symm_sourcerightvaluemasklookup dst_negative_inverse_symm_sourcerightvaluemasklookup. (((dc_mask_inverse_symm_sourcerightvalue) = (((((dst_positive_code_inverse_symm_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_symm_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_symm_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_symm_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_symm_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_symm_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)))) * S ((((dst_positive_code_inverse_symm_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_symm_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_symm_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_symm_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_symm_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_symm_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)))) + ((((dst_negative_code_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightvaluemasklookuppositive. ff_h_pvs_inverse_symm_sourcerightvaluemasklookuppositive + S (dst_positive_inverse_symm_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_symm_sourcerightvaluemask)) * dst_positive_scale_inverse_symm_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_symm_sourcerightvaluemasklookuppositive. dst_positive_code_inverse_symm_sourcerightvaluemasklookup = ff_q_pvs_inverse_symm_sourcerightvaluemasklookuppositive * S ((S (dc_index_inverse_symm_sourcerightvaluemask)) * dst_positive_scale_inverse_symm_sourcerightvaluemasklookup) + (dst_positive_inverse_symm_sourcerightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightvaluemasklookupnegative. ff_h_pvs_inverse_symm_sourcerightvaluemasklookupnegative + S (dst_negative_inverse_symm_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_symm_sourcerightvaluemask)) * dst_negative_scale_inverse_symm_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_symm_sourcerightvaluemasklookupnegative. dst_negative_code_inverse_symm_sourcerightvaluemasklookup = ff_q_pvs_inverse_symm_sourcerightvaluemasklookupnegative * S ((S (dc_index_inverse_symm_sourcerightvaluemask)) * dst_negative_scale_inverse_symm_sourcerightvaluemasklookup) + (dst_negative_inverse_symm_sourcerightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_symm_sourcerightvaluemasklookupvalue ge_balance_negative_inverse_symm_sourcerightvaluemasklookupvalue. (((((dc_value_inverse_symm_sourcerightvaluemask) = 2 * (ge_balance_positive_inverse_symm_sourcerightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_symm_sourcerightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightvaluemasklookupvaluedecode. (((dc_value_inverse_symm_sourcerightvaluemask) = 2 * ge_signed_half_inverse_symm_sourcerightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcerightvaluemasklookupvalue) = S ge_signed_half_inverse_symm_sourcerightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_symm_sourcerightvaluemasklookup) + ge_balance_negative_inverse_symm_sourcerightvaluemasklookupvalue = (dst_negative_inverse_symm_sourcerightvaluemasklookup) + ge_balance_positive_inverse_symm_sourcerightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_symm_sourcerightvaluemask)=0)) /\ (exists dc_quotient_inverse_symm_sourcerightvaluemaskentry dc_left_inverse_symm_sourcerightvaluemaskentry dc_right_inverse_symm_sourcerightvaluemaskentry. (((dc_input_inverse_symm_sourceright)=(dc_index_inverse_symm_sourcerightvaluemask)*dc_quotient_inverse_symm_sourcerightvaluemaskentry) /\ (((exists dst_positive_code_inverse_symm_sourcerightvaluemaskentryleft dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft dst_positive_inverse_symm_sourcerightvaluemaskentryleft dst_negative_inverse_symm_sourcerightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightvaluemaskentryleftpositive. ff_h_pvs_inverse_symm_sourcerightvaluemaskentryleftpositive + S (dst_positive_inverse_symm_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_symm_sourcerightvaluemask)) * dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_symm_sourcerightvaluemaskentryleftpositive. dst_positive_code_inverse_symm_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_symm_sourcerightvaluemaskentryleftpositive * S ((S (dc_index_inverse_symm_sourcerightvaluemask)) * dst_positive_scale_inverse_symm_sourcerightvaluemaskentryleft) + (dst_positive_inverse_symm_sourcerightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightvaluemaskentryleftnegative. ff_h_pvs_inverse_symm_sourcerightvaluemaskentryleftnegative + S (dst_negative_inverse_symm_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_symm_sourcerightvaluemask)) * dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_symm_sourcerightvaluemaskentryleftnegative. dst_negative_code_inverse_symm_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_symm_sourcerightvaluemaskentryleftnegative * S ((S (dc_index_inverse_symm_sourcerightvaluemask)) * dst_negative_scale_inverse_symm_sourcerightvaluemaskentryleft) + (dst_negative_inverse_symm_sourcerightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_symm_sourcerightvaluemaskentryleftvalue ge_balance_negative_inverse_symm_sourcerightvaluemaskentryleftvalue. (((((dc_left_inverse_symm_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_symm_sourcerightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_symm_sourcerightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightvaluemaskentryleftvaluedecode. (((dc_left_inverse_symm_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_symm_sourcerightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcerightvaluemaskentryleftvalue) = S ge_signed_half_inverse_symm_sourcerightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_symm_sourcerightvaluemaskentryleft) + ge_balance_negative_inverse_symm_sourcerightvaluemaskentryleftvalue = (dst_negative_inverse_symm_sourcerightvaluemaskentryleft) + ge_balance_positive_inverse_symm_sourcerightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_sourcerightvaluemaskentryright dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright dst_negative_code_inverse_symm_sourcerightvaluemaskentryright dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright dst_positive_inverse_symm_sourcerightvaluemaskentryright dst_negative_inverse_symm_sourcerightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)))) + ((((dst_negative_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightvaluemaskentryrightpositive. ff_h_pvs_inverse_symm_sourcerightvaluemaskentryrightpositive + S (dst_positive_inverse_symm_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_symm_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_symm_sourcerightvaluemaskentryrightpositive. dst_positive_code_inverse_symm_sourcerightvaluemaskentryright = ff_q_pvs_inverse_symm_sourcerightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_symm_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_symm_sourcerightvaluemaskentryright) + (dst_positive_inverse_symm_sourcerightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_symm_sourcerightvaluemaskentryrightnegative. ff_h_pvs_inverse_symm_sourcerightvaluemaskentryrightnegative + S (dst_negative_inverse_symm_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_symm_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_symm_sourcerightvaluemaskentryrightnegative. dst_negative_code_inverse_symm_sourcerightvaluemaskentryright = ff_q_pvs_inverse_symm_sourcerightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_symm_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_symm_sourcerightvaluemaskentryright) + (dst_negative_inverse_symm_sourcerightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_symm_sourcerightvaluemaskentryrightvalue ge_balance_negative_inverse_symm_sourcerightvaluemaskentryrightvalue. (((((dc_right_inverse_symm_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_symm_sourcerightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_symm_sourcerightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightvaluemaskentryrightvaluedecode. (((dc_right_inverse_symm_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_symm_sourcerightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_symm_sourcerightvaluemaskentryrightvalue) = S ge_signed_half_inverse_symm_sourcerightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_symm_sourcerightvaluemaskentryright) + ge_balance_negative_inverse_symm_sourcerightvaluemaskentryrightvalue = (dst_negative_inverse_symm_sourcerightvaluemaskentryright) + ge_balance_positive_inverse_symm_sourcerightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_symm_sourcerightvaluemaskentryproduct sto_an_inverse_symm_sourcerightvaluemaskentryproduct sto_bp_inverse_symm_sourcerightvaluemaskentryproduct sto_bn_inverse_symm_sourcerightvaluemaskentryproduct sto_cp_inverse_symm_sourcerightvaluemaskentryproduct sto_cn_inverse_symm_sourcerightvaluemaskentryproduct. (((((dc_left_inverse_symm_sourcerightvaluemaskentry) = 2 * (sto_ap_inverse_symm_sourcerightvaluemaskentryproduct) /\ (sto_an_inverse_symm_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductleft. (((dc_left_inverse_symm_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_symm_sourcerightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_symm_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_symm_sourcerightvaluemaskentry) = 2 * (sto_bp_inverse_symm_sourcerightvaluemaskentryproduct) /\ (sto_bn_inverse_symm_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductright. (((dc_right_inverse_symm_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_symm_sourcerightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_symm_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_symm_sourcerightvaluemask) = 2 * (sto_cp_inverse_symm_sourcerightvaluemaskentryproduct) /\ (sto_cn_inverse_symm_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductoutput. (((dc_value_inverse_symm_sourcerightvaluemask) = 2 * ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_symm_sourcerightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_symm_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_symm_sourcerightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_symm_sourcerightvaluemaskentryproduct * sto_bp_inverse_symm_sourcerightvaluemaskentryproduct + sto_an_inverse_symm_sourcerightvaluemaskentryproduct * sto_bn_inverse_symm_sourcerightvaluemaskentryproduct) + sto_cn_inverse_symm_sourcerightvaluemaskentryproduct = (sto_ap_inverse_symm_sourcerightvaluemaskentryproduct * sto_bn_inverse_symm_sourcerightvaluemaskentryproduct + sto_an_inverse_symm_sourcerightvaluemaskentryproduct * sto_bp_inverse_symm_sourcerightvaluemaskentryproduct) + sto_cp_inverse_symm_sourcerightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_symm_sourcerightvaluemask)=0 \/ ~(exists pvs_factor_inverse_symm_sourcerightvaluemaskentrynondivisor. (dc_input_inverse_symm_sourceright) = (dc_index_inverse_symm_sourcerightvaluemask) * pvs_factor_inverse_symm_sourcerightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_symm_sourcerightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_symm_sourcerightvaluefold dst_positive_scale_inverse_symm_sourcerightvaluefold dst_negative_code_inverse_symm_sourcerightvaluefold dst_negative_scale_inverse_symm_sourcerightvaluefold dst_positive_sum_inverse_symm_sourcerightvaluefold dst_negative_sum_inverse_symm_sourcerightvaluefold. (((dc_mask_inverse_symm_sourcerightvalue) = (((((dst_positive_code_inverse_symm_sourcerightvaluefold) + (dst_positive_scale_inverse_symm_sourcerightvaluefold)) * S ((dst_positive_code_inverse_symm_sourcerightvaluefold) + (dst_positive_scale_inverse_symm_sourcerightvaluefold)) + ((dst_positive_scale_inverse_symm_sourcerightvaluefold) + (dst_positive_scale_inverse_symm_sourcerightvaluefold))) + (((dst_negative_code_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)) * S ((dst_negative_code_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)) + ((dst_negative_scale_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)))) * S ((((dst_positive_code_inverse_symm_sourcerightvaluefold) + (dst_positive_scale_inverse_symm_sourcerightvaluefold)) * S ((dst_positive_code_inverse_symm_sourcerightvaluefold) + (dst_positive_scale_inverse_symm_sourcerightvaluefold)) + ((dst_positive_scale_inverse_symm_sourcerightvaluefold) + (dst_positive_scale_inverse_symm_sourcerightvaluefold))) + (((dst_negative_code_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)) * S ((dst_negative_code_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)) + ((dst_negative_scale_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)))) + ((((dst_negative_code_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)) * S ((dst_negative_code_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)) + ((dst_negative_scale_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold))) + (((dst_negative_code_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)) * S ((dst_negative_code_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)) + ((dst_negative_scale_inverse_symm_sourcerightvaluefold) + (dst_negative_scale_inverse_symm_sourcerightvaluefold)))))) /\ (((exists fs_u_dst_inverse_symm_sourcerightvaluefoldpositive fs_v_dst_inverse_symm_sourcerightvaluefoldpositive. ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_start. fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_symm_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_start. fs_u_dst_inverse_symm_sourcerightvaluefoldpositive = fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_symm_sourcerightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_terminal. fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_symm_sourcerightvaluefold) = S ((S (S (dc_input_inverse_symm_sourceright))) * fs_v_dst_inverse_symm_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_terminal. fs_u_dst_inverse_symm_sourcerightvaluefoldpositive = fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_symm_sourceright))) * fs_v_dst_inverse_symm_sourcerightvaluefoldpositive) + (dst_positive_sum_inverse_symm_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps = S (dc_input_inverse_symm_sourceright)) -> exists fs_a_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps fs_r_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps fs_s_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_symm_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_symm_sourcerightvaluefold = fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_symm_sourcerightvaluefold) + (fs_a_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_symm_sourcerightvaluefoldpositive = fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_sourcerightvaluefoldpositive) + (fs_r_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_symm_sourcerightvaluefoldpositive = fs_q_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_sourcerightvaluefoldpositive) + (fs_s_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps = fs_r_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps + fs_a_dst_inverse_symm_sourcerightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_symm_sourcerightvaluefoldnegative fs_v_dst_inverse_symm_sourcerightvaluefoldnegative. ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_start. fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_symm_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_start. fs_u_dst_inverse_symm_sourcerightvaluefoldnegative = fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_symm_sourcerightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_terminal. fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_symm_sourcerightvaluefold) = S ((S (S (dc_input_inverse_symm_sourceright))) * fs_v_dst_inverse_symm_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_terminal. fs_u_dst_inverse_symm_sourcerightvaluefoldnegative = fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_symm_sourceright))) * fs_v_dst_inverse_symm_sourcerightvaluefoldnegative) + (dst_negative_sum_inverse_symm_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps = S (dc_input_inverse_symm_sourceright)) -> exists fs_a_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps fs_r_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps fs_s_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_symm_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_symm_sourcerightvaluefold = fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_symm_sourcerightvaluefold) + (fs_a_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_symm_sourcerightvaluefoldnegative = fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_sourcerightvaluefoldnegative) + (fs_r_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_symm_sourcerightvaluefoldnegative = fs_q_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_sourcerightvaluefoldnegative) + (fs_s_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps = fs_r_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps + fs_a_dst_inverse_symm_sourcerightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_symm_sourcerightvaluefoldresult ge_balance_negative_inverse_symm_sourcerightvaluefoldresult. (((((dc_output_inverse_symm_sourceright) = 2 * (ge_balance_positive_inverse_symm_sourcerightvaluefoldresult) /\ (ge_balance_negative_inverse_symm_sourcerightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_symm_sourcerightvaluefoldresultdecode. (((dc_output_inverse_symm_sourceright) = 2 * ge_signed_half_inverse_symm_sourcerightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_symm_sourcerightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_symm_sourcerightvaluefoldresult) = S ge_signed_half_inverse_symm_sourcerightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_symm_sourcerightvaluefold) + ge_balance_negative_inverse_symm_sourcerightvaluefoldresult = (dst_negative_sum_inverse_symm_sourcerightvaluefold) + ge_balance_positive_inverse_symm_sourcerightvaluefoldresult)))))))))))))))))))))))) -> (exists di_delta_inverse_symm_result. ((((exists dst_positive_code_inverse_symm_resultdeltatable dst_positive_scale_inverse_symm_resultdeltatable dst_negative_code_inverse_symm_resultdeltatable dst_negative_scale_inverse_symm_resultdeltatable. (((di_delta_inverse_symm_result) = (((((dst_positive_code_inverse_symm_resultdeltatable) + (dst_positive_scale_inverse_symm_resultdeltatable)) * S ((dst_positive_code_inverse_symm_resultdeltatable) + (dst_positive_scale_inverse_symm_resultdeltatable)) + ((dst_positive_scale_inverse_symm_resultdeltatable) + (dst_positive_scale_inverse_symm_resultdeltatable))) + (((dst_negative_code_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)) * S ((dst_negative_code_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)) + ((dst_negative_scale_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)))) * S ((((dst_positive_code_inverse_symm_resultdeltatable) + (dst_positive_scale_inverse_symm_resultdeltatable)) * S ((dst_positive_code_inverse_symm_resultdeltatable) + (dst_positive_scale_inverse_symm_resultdeltatable)) + ((dst_positive_scale_inverse_symm_resultdeltatable) + (dst_positive_scale_inverse_symm_resultdeltatable))) + (((dst_negative_code_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)) * S ((dst_negative_code_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)) + ((dst_negative_scale_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)))) + ((((dst_negative_code_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)) * S ((dst_negative_code_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)) + ((dst_negative_scale_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable))) + (((dst_negative_code_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)) * S ((dst_negative_code_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)) + ((dst_negative_scale_inverse_symm_resultdeltatable) + (dst_negative_scale_inverse_symm_resultdeltatable)))))) /\ (forall dst_index_inverse_symm_resultdeltatable. (exists pvs_le_gap_inverse_symm_resultdeltatabledomain. pvs_le_gap_inverse_symm_resultdeltatabledomain + (dst_index_inverse_symm_resultdeltatable) = (N)) -> exists dst_positive_inverse_symm_resultdeltatable dst_negative_inverse_symm_resultdeltatable dst_value_inverse_symm_resultdeltatable. ((((exists ff_h_pvs_inverse_symm_resultdeltatableentrypositive. ff_h_pvs_inverse_symm_resultdeltatableentrypositive + S (dst_positive_inverse_symm_resultdeltatable) = S ((S (dst_index_inverse_symm_resultdeltatable)) * dst_positive_scale_inverse_symm_resultdeltatable)) /\ exists ff_q_pvs_inverse_symm_resultdeltatableentrypositive. dst_positive_code_inverse_symm_resultdeltatable = ff_q_pvs_inverse_symm_resultdeltatableentrypositive * S ((S (dst_index_inverse_symm_resultdeltatable)) * dst_positive_scale_inverse_symm_resultdeltatable) + (dst_positive_inverse_symm_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_symm_resultdeltatableentrynegative. ff_h_pvs_inverse_symm_resultdeltatableentrynegative + S (dst_negative_inverse_symm_resultdeltatable) = S ((S (dst_index_inverse_symm_resultdeltatable)) * dst_negative_scale_inverse_symm_resultdeltatable)) /\ exists ff_q_pvs_inverse_symm_resultdeltatableentrynegative. dst_negative_code_inverse_symm_resultdeltatable = ff_q_pvs_inverse_symm_resultdeltatableentrynegative * S ((S (dst_index_inverse_symm_resultdeltatable)) * dst_negative_scale_inverse_symm_resultdeltatable) + (dst_negative_inverse_symm_resultdeltatable))) /\ (exists ge_balance_positive_inverse_symm_resultdeltatableentryvalue ge_balance_negative_inverse_symm_resultdeltatableentryvalue. (((((dst_value_inverse_symm_resultdeltatable) = 2 * (ge_balance_positive_inverse_symm_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_symm_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultdeltatableentryvaluedecode. (((dst_value_inverse_symm_resultdeltatable) = 2 * ge_signed_half_inverse_symm_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultdeltatableentryvalue) = S ge_signed_half_inverse_symm_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultdeltatable) + ge_balance_negative_inverse_symm_resultdeltatableentryvalue = (dst_negative_inverse_symm_resultdeltatable) + ge_balance_positive_inverse_symm_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_symm_resultdelta du_value_inverse_symm_resultdelta. ~(du_index_inverse_symm_resultdelta=0) -> (exists pvs_le_gap_inverse_symm_resultdeltabound. pvs_le_gap_inverse_symm_resultdeltabound + (du_index_inverse_symm_resultdelta) = (N)) -> (exists dst_positive_code_inverse_symm_resultdeltaentry dst_positive_scale_inverse_symm_resultdeltaentry dst_negative_code_inverse_symm_resultdeltaentry dst_negative_scale_inverse_symm_resultdeltaentry dst_positive_inverse_symm_resultdeltaentry dst_negative_inverse_symm_resultdeltaentry. (((di_delta_inverse_symm_result) = (((((dst_positive_code_inverse_symm_resultdeltaentry) + (dst_positive_scale_inverse_symm_resultdeltaentry)) * S ((dst_positive_code_inverse_symm_resultdeltaentry) + (dst_positive_scale_inverse_symm_resultdeltaentry)) + ((dst_positive_scale_inverse_symm_resultdeltaentry) + (dst_positive_scale_inverse_symm_resultdeltaentry))) + (((dst_negative_code_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)) * S ((dst_negative_code_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)) + ((dst_negative_scale_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)))) * S ((((dst_positive_code_inverse_symm_resultdeltaentry) + (dst_positive_scale_inverse_symm_resultdeltaentry)) * S ((dst_positive_code_inverse_symm_resultdeltaentry) + (dst_positive_scale_inverse_symm_resultdeltaentry)) + ((dst_positive_scale_inverse_symm_resultdeltaentry) + (dst_positive_scale_inverse_symm_resultdeltaentry))) + (((dst_negative_code_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)) * S ((dst_negative_code_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)) + ((dst_negative_scale_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)))) + ((((dst_negative_code_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)) * S ((dst_negative_code_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)) + ((dst_negative_scale_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry))) + (((dst_negative_code_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)) * S ((dst_negative_code_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)) + ((dst_negative_scale_inverse_symm_resultdeltaentry) + (dst_negative_scale_inverse_symm_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultdeltaentrypositive. ff_h_pvs_inverse_symm_resultdeltaentrypositive + S (dst_positive_inverse_symm_resultdeltaentry) = S ((S (du_index_inverse_symm_resultdelta)) * dst_positive_scale_inverse_symm_resultdeltaentry)) /\ exists ff_q_pvs_inverse_symm_resultdeltaentrypositive. dst_positive_code_inverse_symm_resultdeltaentry = ff_q_pvs_inverse_symm_resultdeltaentrypositive * S ((S (du_index_inverse_symm_resultdelta)) * dst_positive_scale_inverse_symm_resultdeltaentry) + (dst_positive_inverse_symm_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_symm_resultdeltaentrynegative. ff_h_pvs_inverse_symm_resultdeltaentrynegative + S (dst_negative_inverse_symm_resultdeltaentry) = S ((S (du_index_inverse_symm_resultdelta)) * dst_negative_scale_inverse_symm_resultdeltaentry)) /\ exists ff_q_pvs_inverse_symm_resultdeltaentrynegative. dst_negative_code_inverse_symm_resultdeltaentry = ff_q_pvs_inverse_symm_resultdeltaentrynegative * S ((S (du_index_inverse_symm_resultdelta)) * dst_negative_scale_inverse_symm_resultdeltaentry) + (dst_negative_inverse_symm_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_symm_resultdeltaentryvalue ge_balance_negative_inverse_symm_resultdeltaentryvalue. (((((du_value_inverse_symm_resultdelta) = 2 * (ge_balance_positive_inverse_symm_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_symm_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultdeltaentryvaluedecode. (((du_value_inverse_symm_resultdelta) = 2 * ge_signed_half_inverse_symm_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultdeltaentryvalue) = S ge_signed_half_inverse_symm_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultdeltaentry) + ge_balance_negative_inverse_symm_resultdeltaentryvalue = (dst_negative_inverse_symm_resultdeltaentry) + ge_balance_positive_inverse_symm_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_symm_resultdelta)=1 -> (du_value_inverse_symm_resultdelta)=2) /\ (~((du_index_inverse_symm_resultdelta)=1) -> (du_value_inverse_symm_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_symm_resultleftleft dst_positive_scale_inverse_symm_resultleftleft dst_negative_code_inverse_symm_resultleftleft dst_negative_scale_inverse_symm_resultleftleft. (((G) = (((((dst_positive_code_inverse_symm_resultleftleft) + (dst_positive_scale_inverse_symm_resultleftleft)) * S ((dst_positive_code_inverse_symm_resultleftleft) + (dst_positive_scale_inverse_symm_resultleftleft)) + ((dst_positive_scale_inverse_symm_resultleftleft) + (dst_positive_scale_inverse_symm_resultleftleft))) + (((dst_negative_code_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)) * S ((dst_negative_code_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)) + ((dst_negative_scale_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)))) * S ((((dst_positive_code_inverse_symm_resultleftleft) + (dst_positive_scale_inverse_symm_resultleftleft)) * S ((dst_positive_code_inverse_symm_resultleftleft) + (dst_positive_scale_inverse_symm_resultleftleft)) + ((dst_positive_scale_inverse_symm_resultleftleft) + (dst_positive_scale_inverse_symm_resultleftleft))) + (((dst_negative_code_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)) * S ((dst_negative_code_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)) + ((dst_negative_scale_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)))) + ((((dst_negative_code_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)) * S ((dst_negative_code_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)) + ((dst_negative_scale_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft))) + (((dst_negative_code_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)) * S ((dst_negative_code_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)) + ((dst_negative_scale_inverse_symm_resultleftleft) + (dst_negative_scale_inverse_symm_resultleftleft)))))) /\ (forall dst_index_inverse_symm_resultleftleft. (exists pvs_le_gap_inverse_symm_resultleftleftdomain. pvs_le_gap_inverse_symm_resultleftleftdomain + (dst_index_inverse_symm_resultleftleft) = (N)) -> exists dst_positive_inverse_symm_resultleftleft dst_negative_inverse_symm_resultleftleft dst_value_inverse_symm_resultleftleft. ((((exists ff_h_pvs_inverse_symm_resultleftleftentrypositive. ff_h_pvs_inverse_symm_resultleftleftentrypositive + S (dst_positive_inverse_symm_resultleftleft) = S ((S (dst_index_inverse_symm_resultleftleft)) * dst_positive_scale_inverse_symm_resultleftleft)) /\ exists ff_q_pvs_inverse_symm_resultleftleftentrypositive. dst_positive_code_inverse_symm_resultleftleft = ff_q_pvs_inverse_symm_resultleftleftentrypositive * S ((S (dst_index_inverse_symm_resultleftleft)) * dst_positive_scale_inverse_symm_resultleftleft) + (dst_positive_inverse_symm_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftleftentrynegative. ff_h_pvs_inverse_symm_resultleftleftentrynegative + S (dst_negative_inverse_symm_resultleftleft) = S ((S (dst_index_inverse_symm_resultleftleft)) * dst_negative_scale_inverse_symm_resultleftleft)) /\ exists ff_q_pvs_inverse_symm_resultleftleftentrynegative. dst_negative_code_inverse_symm_resultleftleft = ff_q_pvs_inverse_symm_resultleftleftentrynegative * S ((S (dst_index_inverse_symm_resultleftleft)) * dst_negative_scale_inverse_symm_resultleftleft) + (dst_negative_inverse_symm_resultleftleft))) /\ (exists ge_balance_positive_inverse_symm_resultleftleftentryvalue ge_balance_negative_inverse_symm_resultleftleftentryvalue. (((((dst_value_inverse_symm_resultleftleft) = 2 * (ge_balance_positive_inverse_symm_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_symm_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultleftleftentryvaluedecode. (((dst_value_inverse_symm_resultleftleft) = 2 * ge_signed_half_inverse_symm_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultleftleftentryvalue) = S ge_signed_half_inverse_symm_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultleftleft) + ge_balance_negative_inverse_symm_resultleftleftentryvalue = (dst_negative_inverse_symm_resultleftleft) + ge_balance_positive_inverse_symm_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_resultleftright dst_positive_scale_inverse_symm_resultleftright dst_negative_code_inverse_symm_resultleftright dst_negative_scale_inverse_symm_resultleftright. (((F) = (((((dst_positive_code_inverse_symm_resultleftright) + (dst_positive_scale_inverse_symm_resultleftright)) * S ((dst_positive_code_inverse_symm_resultleftright) + (dst_positive_scale_inverse_symm_resultleftright)) + ((dst_positive_scale_inverse_symm_resultleftright) + (dst_positive_scale_inverse_symm_resultleftright))) + (((dst_negative_code_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)) * S ((dst_negative_code_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)) + ((dst_negative_scale_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)))) * S ((((dst_positive_code_inverse_symm_resultleftright) + (dst_positive_scale_inverse_symm_resultleftright)) * S ((dst_positive_code_inverse_symm_resultleftright) + (dst_positive_scale_inverse_symm_resultleftright)) + ((dst_positive_scale_inverse_symm_resultleftright) + (dst_positive_scale_inverse_symm_resultleftright))) + (((dst_negative_code_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)) * S ((dst_negative_code_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)) + ((dst_negative_scale_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)))) + ((((dst_negative_code_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)) * S ((dst_negative_code_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)) + ((dst_negative_scale_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright))) + (((dst_negative_code_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)) * S ((dst_negative_code_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)) + ((dst_negative_scale_inverse_symm_resultleftright) + (dst_negative_scale_inverse_symm_resultleftright)))))) /\ (forall dst_index_inverse_symm_resultleftright. (exists pvs_le_gap_inverse_symm_resultleftrightdomain. pvs_le_gap_inverse_symm_resultleftrightdomain + (dst_index_inverse_symm_resultleftright) = (N)) -> exists dst_positive_inverse_symm_resultleftright dst_negative_inverse_symm_resultleftright dst_value_inverse_symm_resultleftright. ((((exists ff_h_pvs_inverse_symm_resultleftrightentrypositive. ff_h_pvs_inverse_symm_resultleftrightentrypositive + S (dst_positive_inverse_symm_resultleftright) = S ((S (dst_index_inverse_symm_resultleftright)) * dst_positive_scale_inverse_symm_resultleftright)) /\ exists ff_q_pvs_inverse_symm_resultleftrightentrypositive. dst_positive_code_inverse_symm_resultleftright = ff_q_pvs_inverse_symm_resultleftrightentrypositive * S ((S (dst_index_inverse_symm_resultleftright)) * dst_positive_scale_inverse_symm_resultleftright) + (dst_positive_inverse_symm_resultleftright))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftrightentrynegative. ff_h_pvs_inverse_symm_resultleftrightentrynegative + S (dst_negative_inverse_symm_resultleftright) = S ((S (dst_index_inverse_symm_resultleftright)) * dst_negative_scale_inverse_symm_resultleftright)) /\ exists ff_q_pvs_inverse_symm_resultleftrightentrynegative. dst_negative_code_inverse_symm_resultleftright = ff_q_pvs_inverse_symm_resultleftrightentrynegative * S ((S (dst_index_inverse_symm_resultleftright)) * dst_negative_scale_inverse_symm_resultleftright) + (dst_negative_inverse_symm_resultleftright))) /\ (exists ge_balance_positive_inverse_symm_resultleftrightentryvalue ge_balance_negative_inverse_symm_resultleftrightentryvalue. (((((dst_value_inverse_symm_resultleftright) = 2 * (ge_balance_positive_inverse_symm_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_symm_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultleftrightentryvaluedecode. (((dst_value_inverse_symm_resultleftright) = 2 * ge_signed_half_inverse_symm_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultleftrightentryvalue) = S ge_signed_half_inverse_symm_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultleftright) + ge_balance_negative_inverse_symm_resultleftrightentryvalue = (dst_negative_inverse_symm_resultleftright) + ge_balance_positive_inverse_symm_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_resultlefttable dst_positive_scale_inverse_symm_resultlefttable dst_negative_code_inverse_symm_resultlefttable dst_negative_scale_inverse_symm_resultlefttable. (((di_delta_inverse_symm_result) = (((((dst_positive_code_inverse_symm_resultlefttable) + (dst_positive_scale_inverse_symm_resultlefttable)) * S ((dst_positive_code_inverse_symm_resultlefttable) + (dst_positive_scale_inverse_symm_resultlefttable)) + ((dst_positive_scale_inverse_symm_resultlefttable) + (dst_positive_scale_inverse_symm_resultlefttable))) + (((dst_negative_code_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)) * S ((dst_negative_code_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)) + ((dst_negative_scale_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)))) * S ((((dst_positive_code_inverse_symm_resultlefttable) + (dst_positive_scale_inverse_symm_resultlefttable)) * S ((dst_positive_code_inverse_symm_resultlefttable) + (dst_positive_scale_inverse_symm_resultlefttable)) + ((dst_positive_scale_inverse_symm_resultlefttable) + (dst_positive_scale_inverse_symm_resultlefttable))) + (((dst_negative_code_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)) * S ((dst_negative_code_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)) + ((dst_negative_scale_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)))) + ((((dst_negative_code_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)) * S ((dst_negative_code_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)) + ((dst_negative_scale_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable))) + (((dst_negative_code_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)) * S ((dst_negative_code_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)) + ((dst_negative_scale_inverse_symm_resultlefttable) + (dst_negative_scale_inverse_symm_resultlefttable)))))) /\ (forall dst_index_inverse_symm_resultlefttable. (exists pvs_le_gap_inverse_symm_resultlefttabledomain. pvs_le_gap_inverse_symm_resultlefttabledomain + (dst_index_inverse_symm_resultlefttable) = (N)) -> exists dst_positive_inverse_symm_resultlefttable dst_negative_inverse_symm_resultlefttable dst_value_inverse_symm_resultlefttable. ((((exists ff_h_pvs_inverse_symm_resultlefttableentrypositive. ff_h_pvs_inverse_symm_resultlefttableentrypositive + S (dst_positive_inverse_symm_resultlefttable) = S ((S (dst_index_inverse_symm_resultlefttable)) * dst_positive_scale_inverse_symm_resultlefttable)) /\ exists ff_q_pvs_inverse_symm_resultlefttableentrypositive. dst_positive_code_inverse_symm_resultlefttable = ff_q_pvs_inverse_symm_resultlefttableentrypositive * S ((S (dst_index_inverse_symm_resultlefttable)) * dst_positive_scale_inverse_symm_resultlefttable) + (dst_positive_inverse_symm_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_symm_resultlefttableentrynegative. ff_h_pvs_inverse_symm_resultlefttableentrynegative + S (dst_negative_inverse_symm_resultlefttable) = S ((S (dst_index_inverse_symm_resultlefttable)) * dst_negative_scale_inverse_symm_resultlefttable)) /\ exists ff_q_pvs_inverse_symm_resultlefttableentrynegative. dst_negative_code_inverse_symm_resultlefttable = ff_q_pvs_inverse_symm_resultlefttableentrynegative * S ((S (dst_index_inverse_symm_resultlefttable)) * dst_negative_scale_inverse_symm_resultlefttable) + (dst_negative_inverse_symm_resultlefttable))) /\ (exists ge_balance_positive_inverse_symm_resultlefttableentryvalue ge_balance_negative_inverse_symm_resultlefttableentryvalue. (((((dst_value_inverse_symm_resultlefttable) = 2 * (ge_balance_positive_inverse_symm_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_symm_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultlefttableentryvaluedecode. (((dst_value_inverse_symm_resultlefttable) = 2 * ge_signed_half_inverse_symm_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultlefttableentryvalue) = S ge_signed_half_inverse_symm_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultlefttable) + ge_balance_negative_inverse_symm_resultlefttableentryvalue = (dst_negative_inverse_symm_resultlefttable) + ge_balance_positive_inverse_symm_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_symm_resultleft dc_output_inverse_symm_resultleft. ~(dc_input_inverse_symm_resultleft=0) -> (exists pvs_le_gap_inverse_symm_resultleftdomain. pvs_le_gap_inverse_symm_resultleftdomain + (dc_input_inverse_symm_resultleft) = (N)) -> (exists dst_positive_code_inverse_symm_resultleftlookup dst_positive_scale_inverse_symm_resultleftlookup dst_negative_code_inverse_symm_resultleftlookup dst_negative_scale_inverse_symm_resultleftlookup dst_positive_inverse_symm_resultleftlookup dst_negative_inverse_symm_resultleftlookup. (((di_delta_inverse_symm_result) = (((((dst_positive_code_inverse_symm_resultleftlookup) + (dst_positive_scale_inverse_symm_resultleftlookup)) * S ((dst_positive_code_inverse_symm_resultleftlookup) + (dst_positive_scale_inverse_symm_resultleftlookup)) + ((dst_positive_scale_inverse_symm_resultleftlookup) + (dst_positive_scale_inverse_symm_resultleftlookup))) + (((dst_negative_code_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)) * S ((dst_negative_code_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)) + ((dst_negative_scale_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)))) * S ((((dst_positive_code_inverse_symm_resultleftlookup) + (dst_positive_scale_inverse_symm_resultleftlookup)) * S ((dst_positive_code_inverse_symm_resultleftlookup) + (dst_positive_scale_inverse_symm_resultleftlookup)) + ((dst_positive_scale_inverse_symm_resultleftlookup) + (dst_positive_scale_inverse_symm_resultleftlookup))) + (((dst_negative_code_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)) * S ((dst_negative_code_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)) + ((dst_negative_scale_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)))) + ((((dst_negative_code_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)) * S ((dst_negative_code_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)) + ((dst_negative_scale_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup))) + (((dst_negative_code_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)) * S ((dst_negative_code_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)) + ((dst_negative_scale_inverse_symm_resultleftlookup) + (dst_negative_scale_inverse_symm_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftlookuppositive. ff_h_pvs_inverse_symm_resultleftlookuppositive + S (dst_positive_inverse_symm_resultleftlookup) = S ((S (dc_input_inverse_symm_resultleft)) * dst_positive_scale_inverse_symm_resultleftlookup)) /\ exists ff_q_pvs_inverse_symm_resultleftlookuppositive. dst_positive_code_inverse_symm_resultleftlookup = ff_q_pvs_inverse_symm_resultleftlookuppositive * S ((S (dc_input_inverse_symm_resultleft)) * dst_positive_scale_inverse_symm_resultleftlookup) + (dst_positive_inverse_symm_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftlookupnegative. ff_h_pvs_inverse_symm_resultleftlookupnegative + S (dst_negative_inverse_symm_resultleftlookup) = S ((S (dc_input_inverse_symm_resultleft)) * dst_negative_scale_inverse_symm_resultleftlookup)) /\ exists ff_q_pvs_inverse_symm_resultleftlookupnegative. dst_negative_code_inverse_symm_resultleftlookup = ff_q_pvs_inverse_symm_resultleftlookupnegative * S ((S (dc_input_inverse_symm_resultleft)) * dst_negative_scale_inverse_symm_resultleftlookup) + (dst_negative_inverse_symm_resultleftlookup))) /\ (exists ge_balance_positive_inverse_symm_resultleftlookupvalue ge_balance_negative_inverse_symm_resultleftlookupvalue. (((((dc_output_inverse_symm_resultleft) = 2 * (ge_balance_positive_inverse_symm_resultleftlookupvalue) /\ (ge_balance_negative_inverse_symm_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultleftlookupvaluedecode. (((dc_output_inverse_symm_resultleft) = 2 * ge_signed_half_inverse_symm_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultleftlookupvalue) = S ge_signed_half_inverse_symm_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_symm_resultleftlookup) + ge_balance_negative_inverse_symm_resultleftlookupvalue = (dst_negative_inverse_symm_resultleftlookup) + ge_balance_positive_inverse_symm_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_symm_resultleft)=0)) /\ (exists dc_mask_inverse_symm_resultleftvalue. ((((exists dst_positive_code_inverse_symm_resultleftvaluemasktable dst_positive_scale_inverse_symm_resultleftvaluemasktable dst_negative_code_inverse_symm_resultleftvaluemasktable dst_negative_scale_inverse_symm_resultleftvaluemasktable. (((dc_mask_inverse_symm_resultleftvalue) = (((((dst_positive_code_inverse_symm_resultleftvaluemasktable) + (dst_positive_scale_inverse_symm_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_symm_resultleftvaluemasktable) + (dst_positive_scale_inverse_symm_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_symm_resultleftvaluemasktable) + (dst_positive_scale_inverse_symm_resultleftvaluemasktable))) + (((dst_negative_code_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_symm_resultleftvaluemasktable) + (dst_positive_scale_inverse_symm_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_symm_resultleftvaluemasktable) + (dst_positive_scale_inverse_symm_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_symm_resultleftvaluemasktable) + (dst_positive_scale_inverse_symm_resultleftvaluemasktable))) + (((dst_negative_code_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable))) + (((dst_negative_code_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_symm_resultleftvaluemasktable) + (dst_negative_scale_inverse_symm_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_symm_resultleftvaluemasktable. (exists pvs_le_gap_inverse_symm_resultleftvaluemasktabledomain. pvs_le_gap_inverse_symm_resultleftvaluemasktabledomain + (dst_index_inverse_symm_resultleftvaluemasktable) = (dc_input_inverse_symm_resultleft)) -> exists dst_positive_inverse_symm_resultleftvaluemasktable dst_negative_inverse_symm_resultleftvaluemasktable dst_value_inverse_symm_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_symm_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_symm_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_symm_resultleftvaluemasktable) = S ((S (dst_index_inverse_symm_resultleftvaluemasktable)) * dst_positive_scale_inverse_symm_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_symm_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_symm_resultleftvaluemasktable = ff_q_pvs_inverse_symm_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_symm_resultleftvaluemasktable)) * dst_positive_scale_inverse_symm_resultleftvaluemasktable) + (dst_positive_inverse_symm_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_symm_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_symm_resultleftvaluemasktable) = S ((S (dst_index_inverse_symm_resultleftvaluemasktable)) * dst_negative_scale_inverse_symm_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_symm_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_symm_resultleftvaluemasktable = ff_q_pvs_inverse_symm_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_symm_resultleftvaluemasktable)) * dst_negative_scale_inverse_symm_resultleftvaluemasktable) + (dst_negative_inverse_symm_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_symm_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_symm_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_symm_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_symm_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_symm_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_symm_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_symm_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_symm_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultleftvaluemasktable) + ge_balance_negative_inverse_symm_resultleftvaluemasktableentryvalue = (dst_negative_inverse_symm_resultleftvaluemasktable) + ge_balance_positive_inverse_symm_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_symm_resultleftvaluemask dc_value_inverse_symm_resultleftvaluemask. (exists pvs_le_gap_inverse_symm_resultleftvaluemaskdomain. pvs_le_gap_inverse_symm_resultleftvaluemaskdomain + (dc_index_inverse_symm_resultleftvaluemask) = (dc_input_inverse_symm_resultleft)) -> (exists dst_positive_code_inverse_symm_resultleftvaluemasklookup dst_positive_scale_inverse_symm_resultleftvaluemasklookup dst_negative_code_inverse_symm_resultleftvaluemasklookup dst_negative_scale_inverse_symm_resultleftvaluemasklookup dst_positive_inverse_symm_resultleftvaluemasklookup dst_negative_inverse_symm_resultleftvaluemasklookup. (((dc_mask_inverse_symm_resultleftvalue) = (((((dst_positive_code_inverse_symm_resultleftvaluemasklookup) + (dst_positive_scale_inverse_symm_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_symm_resultleftvaluemasklookup) + (dst_positive_scale_inverse_symm_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_symm_resultleftvaluemasklookup) + (dst_positive_scale_inverse_symm_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_symm_resultleftvaluemasklookup) + (dst_positive_scale_inverse_symm_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_symm_resultleftvaluemasklookup) + (dst_positive_scale_inverse_symm_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_symm_resultleftvaluemasklookup) + (dst_positive_scale_inverse_symm_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_symm_resultleftvaluemasklookup) + (dst_negative_scale_inverse_symm_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_symm_resultleftvaluemasklookuppositive + S (dst_positive_inverse_symm_resultleftvaluemasklookup) = S ((S (dc_index_inverse_symm_resultleftvaluemask)) * dst_positive_scale_inverse_symm_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_symm_resultleftvaluemasklookuppositive. dst_positive_code_inverse_symm_resultleftvaluemasklookup = ff_q_pvs_inverse_symm_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_symm_resultleftvaluemask)) * dst_positive_scale_inverse_symm_resultleftvaluemasklookup) + (dst_positive_inverse_symm_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_symm_resultleftvaluemasklookupnegative + S (dst_negative_inverse_symm_resultleftvaluemasklookup) = S ((S (dc_index_inverse_symm_resultleftvaluemask)) * dst_negative_scale_inverse_symm_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_symm_resultleftvaluemasklookupnegative. dst_negative_code_inverse_symm_resultleftvaluemasklookup = ff_q_pvs_inverse_symm_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_symm_resultleftvaluemask)) * dst_negative_scale_inverse_symm_resultleftvaluemasklookup) + (dst_negative_inverse_symm_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_symm_resultleftvaluemasklookupvalue ge_balance_negative_inverse_symm_resultleftvaluemasklookupvalue. (((((dc_value_inverse_symm_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_symm_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_symm_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_symm_resultleftvaluemask) = 2 * ge_signed_half_inverse_symm_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_symm_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_symm_resultleftvaluemasklookup) + ge_balance_negative_inverse_symm_resultleftvaluemasklookupvalue = (dst_negative_inverse_symm_resultleftvaluemasklookup) + ge_balance_positive_inverse_symm_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_symm_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_symm_resultleftvaluemaskentry dc_left_inverse_symm_resultleftvaluemaskentry dc_right_inverse_symm_resultleftvaluemaskentry. (((dc_input_inverse_symm_resultleft)=(dc_index_inverse_symm_resultleftvaluemask)*dc_quotient_inverse_symm_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_symm_resultleftvaluemaskentryleft dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft dst_negative_code_inverse_symm_resultleftvaluemaskentryleft dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft dst_positive_inverse_symm_resultleftvaluemaskentryleft dst_negative_inverse_symm_resultleftvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_symm_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_symm_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_symm_resultleftvaluemask)) * dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_symm_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_symm_resultleftvaluemaskentryleft = ff_q_pvs_inverse_symm_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_symm_resultleftvaluemask)) * dst_positive_scale_inverse_symm_resultleftvaluemaskentryleft) + (dst_positive_inverse_symm_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_symm_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_symm_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_symm_resultleftvaluemask)) * dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_symm_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_symm_resultleftvaluemaskentryleft = ff_q_pvs_inverse_symm_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_symm_resultleftvaluemask)) * dst_negative_scale_inverse_symm_resultleftvaluemaskentryleft) + (dst_negative_inverse_symm_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_symm_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_symm_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_symm_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_symm_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_symm_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_symm_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_symm_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_symm_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_symm_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_symm_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_symm_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_symm_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_resultleftvaluemaskentryright dst_positive_scale_inverse_symm_resultleftvaluemaskentryright dst_negative_code_inverse_symm_resultleftvaluemaskentryright dst_negative_scale_inverse_symm_resultleftvaluemaskentryright dst_positive_inverse_symm_resultleftvaluemaskentryright dst_negative_inverse_symm_resultleftvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_symm_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_symm_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_symm_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_symm_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_symm_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_symm_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_symm_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_symm_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_symm_resultleftvaluemaskentry)) * dst_positive_scale_inverse_symm_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_symm_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_symm_resultleftvaluemaskentryright = ff_q_pvs_inverse_symm_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_symm_resultleftvaluemaskentry)) * dst_positive_scale_inverse_symm_resultleftvaluemaskentryright) + (dst_positive_inverse_symm_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_symm_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_symm_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_symm_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_symm_resultleftvaluemaskentry)) * dst_negative_scale_inverse_symm_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_symm_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_symm_resultleftvaluemaskentryright = ff_q_pvs_inverse_symm_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_symm_resultleftvaluemaskentry)) * dst_negative_scale_inverse_symm_resultleftvaluemaskentryright) + (dst_negative_inverse_symm_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_symm_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_symm_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_symm_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_symm_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_symm_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_symm_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_symm_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_symm_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_symm_resultleftvaluemaskentryright) + ge_balance_negative_inverse_symm_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_symm_resultleftvaluemaskentryright) + ge_balance_positive_inverse_symm_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_symm_resultleftvaluemaskentryproduct sto_an_inverse_symm_resultleftvaluemaskentryproduct sto_bp_inverse_symm_resultleftvaluemaskentryproduct sto_bn_inverse_symm_resultleftvaluemaskentryproduct sto_cp_inverse_symm_resultleftvaluemaskentryproduct sto_cn_inverse_symm_resultleftvaluemaskentryproduct. (((((dc_left_inverse_symm_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_symm_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_symm_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_resultleftvaluemaskentryproductleft. (((dc_left_inverse_symm_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_symm_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_symm_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_symm_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_symm_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_symm_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_symm_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_symm_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_resultleftvaluemaskentryproductright. (((dc_right_inverse_symm_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_symm_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_symm_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_symm_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_symm_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_symm_resultleftvaluemask) = 2 * (sto_cp_inverse_symm_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_symm_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_symm_resultleftvaluemask) = 2 * ge_signed_half_inverse_symm_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_symm_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_symm_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_symm_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_symm_resultleftvaluemaskentryproduct * sto_bp_inverse_symm_resultleftvaluemaskentryproduct + sto_an_inverse_symm_resultleftvaluemaskentryproduct * sto_bn_inverse_symm_resultleftvaluemaskentryproduct) + sto_cn_inverse_symm_resultleftvaluemaskentryproduct = (sto_ap_inverse_symm_resultleftvaluemaskentryproduct * sto_bn_inverse_symm_resultleftvaluemaskentryproduct + sto_an_inverse_symm_resultleftvaluemaskentryproduct * sto_bp_inverse_symm_resultleftvaluemaskentryproduct) + sto_cp_inverse_symm_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_symm_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_symm_resultleftvaluemaskentrynondivisor. (dc_input_inverse_symm_resultleft) = (dc_index_inverse_symm_resultleftvaluemask) * pvs_factor_inverse_symm_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_symm_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_symm_resultleftvaluefold dst_positive_scale_inverse_symm_resultleftvaluefold dst_negative_code_inverse_symm_resultleftvaluefold dst_negative_scale_inverse_symm_resultleftvaluefold dst_positive_sum_inverse_symm_resultleftvaluefold dst_negative_sum_inverse_symm_resultleftvaluefold. (((dc_mask_inverse_symm_resultleftvalue) = (((((dst_positive_code_inverse_symm_resultleftvaluefold) + (dst_positive_scale_inverse_symm_resultleftvaluefold)) * S ((dst_positive_code_inverse_symm_resultleftvaluefold) + (dst_positive_scale_inverse_symm_resultleftvaluefold)) + ((dst_positive_scale_inverse_symm_resultleftvaluefold) + (dst_positive_scale_inverse_symm_resultleftvaluefold))) + (((dst_negative_code_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)) * S ((dst_negative_code_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)) + ((dst_negative_scale_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_symm_resultleftvaluefold) + (dst_positive_scale_inverse_symm_resultleftvaluefold)) * S ((dst_positive_code_inverse_symm_resultleftvaluefold) + (dst_positive_scale_inverse_symm_resultleftvaluefold)) + ((dst_positive_scale_inverse_symm_resultleftvaluefold) + (dst_positive_scale_inverse_symm_resultleftvaluefold))) + (((dst_negative_code_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)) * S ((dst_negative_code_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)) + ((dst_negative_scale_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)))) + ((((dst_negative_code_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)) * S ((dst_negative_code_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)) + ((dst_negative_scale_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold))) + (((dst_negative_code_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)) * S ((dst_negative_code_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)) + ((dst_negative_scale_inverse_symm_resultleftvaluefold) + (dst_negative_scale_inverse_symm_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_symm_resultleftvaluefoldpositive fs_v_dst_inverse_symm_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_symm_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_symm_resultleftvaluefoldpositive = fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_symm_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_symm_resultleftvaluefold) = S ((S (S (dc_input_inverse_symm_resultleft))) * fs_v_dst_inverse_symm_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_symm_resultleftvaluefoldpositive = fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_symm_resultleft))) * fs_v_dst_inverse_symm_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_symm_resultleftvaluefold))) /\ forall fs_i_dst_inverse_symm_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_symm_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_symm_resultleft)) -> exists fs_a_dst_inverse_symm_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_symm_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_symm_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_symm_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_symm_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_symm_resultleftvaluefold)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_symm_resultleftvaluefold = fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_symm_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_symm_resultleftvaluefold) + (fs_a_dst_inverse_symm_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_symm_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_symm_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_symm_resultleftvaluefoldpositive = fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_symm_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_resultleftvaluefoldpositive) + (fs_r_dst_inverse_symm_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_symm_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_symm_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_symm_resultleftvaluefoldpositive = fs_q_dst_inverse_symm_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_symm_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_resultleftvaluefoldpositive) + (fs_s_dst_inverse_symm_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_symm_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_symm_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_symm_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_symm_resultleftvaluefoldnegative fs_v_dst_inverse_symm_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_symm_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_symm_resultleftvaluefoldnegative = fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_symm_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_symm_resultleftvaluefold) = S ((S (S (dc_input_inverse_symm_resultleft))) * fs_v_dst_inverse_symm_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_symm_resultleftvaluefoldnegative = fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_symm_resultleft))) * fs_v_dst_inverse_symm_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_symm_resultleftvaluefold))) /\ forall fs_i_dst_inverse_symm_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_symm_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_symm_resultleft)) -> exists fs_a_dst_inverse_symm_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_symm_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_symm_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_symm_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_symm_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_symm_resultleftvaluefold)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_symm_resultleftvaluefold = fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_symm_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_symm_resultleftvaluefold) + (fs_a_dst_inverse_symm_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_symm_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_symm_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_symm_resultleftvaluefoldnegative = fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_symm_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_resultleftvaluefoldnegative) + (fs_r_dst_inverse_symm_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_symm_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_symm_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_symm_resultleftvaluefoldnegative = fs_q_dst_inverse_symm_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_symm_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_resultleftvaluefoldnegative) + (fs_s_dst_inverse_symm_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_symm_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_symm_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_symm_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_symm_resultleftvaluefoldresult ge_balance_negative_inverse_symm_resultleftvaluefoldresult. (((((dc_output_inverse_symm_resultleft) = 2 * (ge_balance_positive_inverse_symm_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_symm_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_symm_resultleftvaluefoldresultdecode. (((dc_output_inverse_symm_resultleft) = 2 * ge_signed_half_inverse_symm_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_symm_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_symm_resultleftvaluefoldresult) = S ge_signed_half_inverse_symm_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_symm_resultleftvaluefold) + ge_balance_negative_inverse_symm_resultleftvaluefoldresult = (dst_negative_sum_inverse_symm_resultleftvaluefold) + ge_balance_positive_inverse_symm_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_symm_resultrightleft dst_positive_scale_inverse_symm_resultrightleft dst_negative_code_inverse_symm_resultrightleft dst_negative_scale_inverse_symm_resultrightleft. (((F) = (((((dst_positive_code_inverse_symm_resultrightleft) + (dst_positive_scale_inverse_symm_resultrightleft)) * S ((dst_positive_code_inverse_symm_resultrightleft) + (dst_positive_scale_inverse_symm_resultrightleft)) + ((dst_positive_scale_inverse_symm_resultrightleft) + (dst_positive_scale_inverse_symm_resultrightleft))) + (((dst_negative_code_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)) * S ((dst_negative_code_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)) + ((dst_negative_scale_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)))) * S ((((dst_positive_code_inverse_symm_resultrightleft) + (dst_positive_scale_inverse_symm_resultrightleft)) * S ((dst_positive_code_inverse_symm_resultrightleft) + (dst_positive_scale_inverse_symm_resultrightleft)) + ((dst_positive_scale_inverse_symm_resultrightleft) + (dst_positive_scale_inverse_symm_resultrightleft))) + (((dst_negative_code_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)) * S ((dst_negative_code_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)) + ((dst_negative_scale_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)))) + ((((dst_negative_code_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)) * S ((dst_negative_code_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)) + ((dst_negative_scale_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft))) + (((dst_negative_code_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)) * S ((dst_negative_code_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)) + ((dst_negative_scale_inverse_symm_resultrightleft) + (dst_negative_scale_inverse_symm_resultrightleft)))))) /\ (forall dst_index_inverse_symm_resultrightleft. (exists pvs_le_gap_inverse_symm_resultrightleftdomain. pvs_le_gap_inverse_symm_resultrightleftdomain + (dst_index_inverse_symm_resultrightleft) = (N)) -> exists dst_positive_inverse_symm_resultrightleft dst_negative_inverse_symm_resultrightleft dst_value_inverse_symm_resultrightleft. ((((exists ff_h_pvs_inverse_symm_resultrightleftentrypositive. ff_h_pvs_inverse_symm_resultrightleftentrypositive + S (dst_positive_inverse_symm_resultrightleft) = S ((S (dst_index_inverse_symm_resultrightleft)) * dst_positive_scale_inverse_symm_resultrightleft)) /\ exists ff_q_pvs_inverse_symm_resultrightleftentrypositive. dst_positive_code_inverse_symm_resultrightleft = ff_q_pvs_inverse_symm_resultrightleftentrypositive * S ((S (dst_index_inverse_symm_resultrightleft)) * dst_positive_scale_inverse_symm_resultrightleft) + (dst_positive_inverse_symm_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightleftentrynegative. ff_h_pvs_inverse_symm_resultrightleftentrynegative + S (dst_negative_inverse_symm_resultrightleft) = S ((S (dst_index_inverse_symm_resultrightleft)) * dst_negative_scale_inverse_symm_resultrightleft)) /\ exists ff_q_pvs_inverse_symm_resultrightleftentrynegative. dst_negative_code_inverse_symm_resultrightleft = ff_q_pvs_inverse_symm_resultrightleftentrynegative * S ((S (dst_index_inverse_symm_resultrightleft)) * dst_negative_scale_inverse_symm_resultrightleft) + (dst_negative_inverse_symm_resultrightleft))) /\ (exists ge_balance_positive_inverse_symm_resultrightleftentryvalue ge_balance_negative_inverse_symm_resultrightleftentryvalue. (((((dst_value_inverse_symm_resultrightleft) = 2 * (ge_balance_positive_inverse_symm_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_symm_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultrightleftentryvaluedecode. (((dst_value_inverse_symm_resultrightleft) = 2 * ge_signed_half_inverse_symm_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultrightleftentryvalue) = S ge_signed_half_inverse_symm_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultrightleft) + ge_balance_negative_inverse_symm_resultrightleftentryvalue = (dst_negative_inverse_symm_resultrightleft) + ge_balance_positive_inverse_symm_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_resultrightright dst_positive_scale_inverse_symm_resultrightright dst_negative_code_inverse_symm_resultrightright dst_negative_scale_inverse_symm_resultrightright. (((G) = (((((dst_positive_code_inverse_symm_resultrightright) + (dst_positive_scale_inverse_symm_resultrightright)) * S ((dst_positive_code_inverse_symm_resultrightright) + (dst_positive_scale_inverse_symm_resultrightright)) + ((dst_positive_scale_inverse_symm_resultrightright) + (dst_positive_scale_inverse_symm_resultrightright))) + (((dst_negative_code_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)) * S ((dst_negative_code_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)) + ((dst_negative_scale_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)))) * S ((((dst_positive_code_inverse_symm_resultrightright) + (dst_positive_scale_inverse_symm_resultrightright)) * S ((dst_positive_code_inverse_symm_resultrightright) + (dst_positive_scale_inverse_symm_resultrightright)) + ((dst_positive_scale_inverse_symm_resultrightright) + (dst_positive_scale_inverse_symm_resultrightright))) + (((dst_negative_code_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)) * S ((dst_negative_code_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)) + ((dst_negative_scale_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)))) + ((((dst_negative_code_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)) * S ((dst_negative_code_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)) + ((dst_negative_scale_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright))) + (((dst_negative_code_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)) * S ((dst_negative_code_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)) + ((dst_negative_scale_inverse_symm_resultrightright) + (dst_negative_scale_inverse_symm_resultrightright)))))) /\ (forall dst_index_inverse_symm_resultrightright. (exists pvs_le_gap_inverse_symm_resultrightrightdomain. pvs_le_gap_inverse_symm_resultrightrightdomain + (dst_index_inverse_symm_resultrightright) = (N)) -> exists dst_positive_inverse_symm_resultrightright dst_negative_inverse_symm_resultrightright dst_value_inverse_symm_resultrightright. ((((exists ff_h_pvs_inverse_symm_resultrightrightentrypositive. ff_h_pvs_inverse_symm_resultrightrightentrypositive + S (dst_positive_inverse_symm_resultrightright) = S ((S (dst_index_inverse_symm_resultrightright)) * dst_positive_scale_inverse_symm_resultrightright)) /\ exists ff_q_pvs_inverse_symm_resultrightrightentrypositive. dst_positive_code_inverse_symm_resultrightright = ff_q_pvs_inverse_symm_resultrightrightentrypositive * S ((S (dst_index_inverse_symm_resultrightright)) * dst_positive_scale_inverse_symm_resultrightright) + (dst_positive_inverse_symm_resultrightright))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightrightentrynegative. ff_h_pvs_inverse_symm_resultrightrightentrynegative + S (dst_negative_inverse_symm_resultrightright) = S ((S (dst_index_inverse_symm_resultrightright)) * dst_negative_scale_inverse_symm_resultrightright)) /\ exists ff_q_pvs_inverse_symm_resultrightrightentrynegative. dst_negative_code_inverse_symm_resultrightright = ff_q_pvs_inverse_symm_resultrightrightentrynegative * S ((S (dst_index_inverse_symm_resultrightright)) * dst_negative_scale_inverse_symm_resultrightright) + (dst_negative_inverse_symm_resultrightright))) /\ (exists ge_balance_positive_inverse_symm_resultrightrightentryvalue ge_balance_negative_inverse_symm_resultrightrightentryvalue. (((((dst_value_inverse_symm_resultrightright) = 2 * (ge_balance_positive_inverse_symm_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_symm_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultrightrightentryvaluedecode. (((dst_value_inverse_symm_resultrightright) = 2 * ge_signed_half_inverse_symm_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultrightrightentryvalue) = S ge_signed_half_inverse_symm_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultrightright) + ge_balance_negative_inverse_symm_resultrightrightentryvalue = (dst_negative_inverse_symm_resultrightright) + ge_balance_positive_inverse_symm_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_resultrighttable dst_positive_scale_inverse_symm_resultrighttable dst_negative_code_inverse_symm_resultrighttable dst_negative_scale_inverse_symm_resultrighttable. (((di_delta_inverse_symm_result) = (((((dst_positive_code_inverse_symm_resultrighttable) + (dst_positive_scale_inverse_symm_resultrighttable)) * S ((dst_positive_code_inverse_symm_resultrighttable) + (dst_positive_scale_inverse_symm_resultrighttable)) + ((dst_positive_scale_inverse_symm_resultrighttable) + (dst_positive_scale_inverse_symm_resultrighttable))) + (((dst_negative_code_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)) * S ((dst_negative_code_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)) + ((dst_negative_scale_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)))) * S ((((dst_positive_code_inverse_symm_resultrighttable) + (dst_positive_scale_inverse_symm_resultrighttable)) * S ((dst_positive_code_inverse_symm_resultrighttable) + (dst_positive_scale_inverse_symm_resultrighttable)) + ((dst_positive_scale_inverse_symm_resultrighttable) + (dst_positive_scale_inverse_symm_resultrighttable))) + (((dst_negative_code_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)) * S ((dst_negative_code_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)) + ((dst_negative_scale_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)))) + ((((dst_negative_code_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)) * S ((dst_negative_code_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)) + ((dst_negative_scale_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable))) + (((dst_negative_code_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)) * S ((dst_negative_code_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)) + ((dst_negative_scale_inverse_symm_resultrighttable) + (dst_negative_scale_inverse_symm_resultrighttable)))))) /\ (forall dst_index_inverse_symm_resultrighttable. (exists pvs_le_gap_inverse_symm_resultrighttabledomain. pvs_le_gap_inverse_symm_resultrighttabledomain + (dst_index_inverse_symm_resultrighttable) = (N)) -> exists dst_positive_inverse_symm_resultrighttable dst_negative_inverse_symm_resultrighttable dst_value_inverse_symm_resultrighttable. ((((exists ff_h_pvs_inverse_symm_resultrighttableentrypositive. ff_h_pvs_inverse_symm_resultrighttableentrypositive + S (dst_positive_inverse_symm_resultrighttable) = S ((S (dst_index_inverse_symm_resultrighttable)) * dst_positive_scale_inverse_symm_resultrighttable)) /\ exists ff_q_pvs_inverse_symm_resultrighttableentrypositive. dst_positive_code_inverse_symm_resultrighttable = ff_q_pvs_inverse_symm_resultrighttableentrypositive * S ((S (dst_index_inverse_symm_resultrighttable)) * dst_positive_scale_inverse_symm_resultrighttable) + (dst_positive_inverse_symm_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_symm_resultrighttableentrynegative. ff_h_pvs_inverse_symm_resultrighttableentrynegative + S (dst_negative_inverse_symm_resultrighttable) = S ((S (dst_index_inverse_symm_resultrighttable)) * dst_negative_scale_inverse_symm_resultrighttable)) /\ exists ff_q_pvs_inverse_symm_resultrighttableentrynegative. dst_negative_code_inverse_symm_resultrighttable = ff_q_pvs_inverse_symm_resultrighttableentrynegative * S ((S (dst_index_inverse_symm_resultrighttable)) * dst_negative_scale_inverse_symm_resultrighttable) + (dst_negative_inverse_symm_resultrighttable))) /\ (exists ge_balance_positive_inverse_symm_resultrighttableentryvalue ge_balance_negative_inverse_symm_resultrighttableentryvalue. (((((dst_value_inverse_symm_resultrighttable) = 2 * (ge_balance_positive_inverse_symm_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_symm_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultrighttableentryvaluedecode. (((dst_value_inverse_symm_resultrighttable) = 2 * ge_signed_half_inverse_symm_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultrighttableentryvalue) = S ge_signed_half_inverse_symm_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultrighttable) + ge_balance_negative_inverse_symm_resultrighttableentryvalue = (dst_negative_inverse_symm_resultrighttable) + ge_balance_positive_inverse_symm_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_symm_resultright dc_output_inverse_symm_resultright. ~(dc_input_inverse_symm_resultright=0) -> (exists pvs_le_gap_inverse_symm_resultrightdomain. pvs_le_gap_inverse_symm_resultrightdomain + (dc_input_inverse_symm_resultright) = (N)) -> (exists dst_positive_code_inverse_symm_resultrightlookup dst_positive_scale_inverse_symm_resultrightlookup dst_negative_code_inverse_symm_resultrightlookup dst_negative_scale_inverse_symm_resultrightlookup dst_positive_inverse_symm_resultrightlookup dst_negative_inverse_symm_resultrightlookup. (((di_delta_inverse_symm_result) = (((((dst_positive_code_inverse_symm_resultrightlookup) + (dst_positive_scale_inverse_symm_resultrightlookup)) * S ((dst_positive_code_inverse_symm_resultrightlookup) + (dst_positive_scale_inverse_symm_resultrightlookup)) + ((dst_positive_scale_inverse_symm_resultrightlookup) + (dst_positive_scale_inverse_symm_resultrightlookup))) + (((dst_negative_code_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)) * S ((dst_negative_code_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)) + ((dst_negative_scale_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)))) * S ((((dst_positive_code_inverse_symm_resultrightlookup) + (dst_positive_scale_inverse_symm_resultrightlookup)) * S ((dst_positive_code_inverse_symm_resultrightlookup) + (dst_positive_scale_inverse_symm_resultrightlookup)) + ((dst_positive_scale_inverse_symm_resultrightlookup) + (dst_positive_scale_inverse_symm_resultrightlookup))) + (((dst_negative_code_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)) * S ((dst_negative_code_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)) + ((dst_negative_scale_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)))) + ((((dst_negative_code_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)) * S ((dst_negative_code_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)) + ((dst_negative_scale_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup))) + (((dst_negative_code_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)) * S ((dst_negative_code_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)) + ((dst_negative_scale_inverse_symm_resultrightlookup) + (dst_negative_scale_inverse_symm_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightlookuppositive. ff_h_pvs_inverse_symm_resultrightlookuppositive + S (dst_positive_inverse_symm_resultrightlookup) = S ((S (dc_input_inverse_symm_resultright)) * dst_positive_scale_inverse_symm_resultrightlookup)) /\ exists ff_q_pvs_inverse_symm_resultrightlookuppositive. dst_positive_code_inverse_symm_resultrightlookup = ff_q_pvs_inverse_symm_resultrightlookuppositive * S ((S (dc_input_inverse_symm_resultright)) * dst_positive_scale_inverse_symm_resultrightlookup) + (dst_positive_inverse_symm_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightlookupnegative. ff_h_pvs_inverse_symm_resultrightlookupnegative + S (dst_negative_inverse_symm_resultrightlookup) = S ((S (dc_input_inverse_symm_resultright)) * dst_negative_scale_inverse_symm_resultrightlookup)) /\ exists ff_q_pvs_inverse_symm_resultrightlookupnegative. dst_negative_code_inverse_symm_resultrightlookup = ff_q_pvs_inverse_symm_resultrightlookupnegative * S ((S (dc_input_inverse_symm_resultright)) * dst_negative_scale_inverse_symm_resultrightlookup) + (dst_negative_inverse_symm_resultrightlookup))) /\ (exists ge_balance_positive_inverse_symm_resultrightlookupvalue ge_balance_negative_inverse_symm_resultrightlookupvalue. (((((dc_output_inverse_symm_resultright) = 2 * (ge_balance_positive_inverse_symm_resultrightlookupvalue) /\ (ge_balance_negative_inverse_symm_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultrightlookupvaluedecode. (((dc_output_inverse_symm_resultright) = 2 * ge_signed_half_inverse_symm_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultrightlookupvalue) = S ge_signed_half_inverse_symm_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_symm_resultrightlookup) + ge_balance_negative_inverse_symm_resultrightlookupvalue = (dst_negative_inverse_symm_resultrightlookup) + ge_balance_positive_inverse_symm_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_symm_resultright)=0)) /\ (exists dc_mask_inverse_symm_resultrightvalue. ((((exists dst_positive_code_inverse_symm_resultrightvaluemasktable dst_positive_scale_inverse_symm_resultrightvaluemasktable dst_negative_code_inverse_symm_resultrightvaluemasktable dst_negative_scale_inverse_symm_resultrightvaluemasktable. (((dc_mask_inverse_symm_resultrightvalue) = (((((dst_positive_code_inverse_symm_resultrightvaluemasktable) + (dst_positive_scale_inverse_symm_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_symm_resultrightvaluemasktable) + (dst_positive_scale_inverse_symm_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_symm_resultrightvaluemasktable) + (dst_positive_scale_inverse_symm_resultrightvaluemasktable))) + (((dst_negative_code_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_symm_resultrightvaluemasktable) + (dst_positive_scale_inverse_symm_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_symm_resultrightvaluemasktable) + (dst_positive_scale_inverse_symm_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_symm_resultrightvaluemasktable) + (dst_positive_scale_inverse_symm_resultrightvaluemasktable))) + (((dst_negative_code_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable))) + (((dst_negative_code_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_symm_resultrightvaluemasktable) + (dst_negative_scale_inverse_symm_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_symm_resultrightvaluemasktable. (exists pvs_le_gap_inverse_symm_resultrightvaluemasktabledomain. pvs_le_gap_inverse_symm_resultrightvaluemasktabledomain + (dst_index_inverse_symm_resultrightvaluemasktable) = (dc_input_inverse_symm_resultright)) -> exists dst_positive_inverse_symm_resultrightvaluemasktable dst_negative_inverse_symm_resultrightvaluemasktable dst_value_inverse_symm_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_symm_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_symm_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_symm_resultrightvaluemasktable) = S ((S (dst_index_inverse_symm_resultrightvaluemasktable)) * dst_positive_scale_inverse_symm_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_symm_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_symm_resultrightvaluemasktable = ff_q_pvs_inverse_symm_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_symm_resultrightvaluemasktable)) * dst_positive_scale_inverse_symm_resultrightvaluemasktable) + (dst_positive_inverse_symm_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_symm_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_symm_resultrightvaluemasktable) = S ((S (dst_index_inverse_symm_resultrightvaluemasktable)) * dst_negative_scale_inverse_symm_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_symm_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_symm_resultrightvaluemasktable = ff_q_pvs_inverse_symm_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_symm_resultrightvaluemasktable)) * dst_negative_scale_inverse_symm_resultrightvaluemasktable) + (dst_negative_inverse_symm_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_symm_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_symm_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_symm_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_symm_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_symm_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_symm_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_symm_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_symm_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_symm_resultrightvaluemasktable) + ge_balance_negative_inverse_symm_resultrightvaluemasktableentryvalue = (dst_negative_inverse_symm_resultrightvaluemasktable) + ge_balance_positive_inverse_symm_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_symm_resultrightvaluemask dc_value_inverse_symm_resultrightvaluemask. (exists pvs_le_gap_inverse_symm_resultrightvaluemaskdomain. pvs_le_gap_inverse_symm_resultrightvaluemaskdomain + (dc_index_inverse_symm_resultrightvaluemask) = (dc_input_inverse_symm_resultright)) -> (exists dst_positive_code_inverse_symm_resultrightvaluemasklookup dst_positive_scale_inverse_symm_resultrightvaluemasklookup dst_negative_code_inverse_symm_resultrightvaluemasklookup dst_negative_scale_inverse_symm_resultrightvaluemasklookup dst_positive_inverse_symm_resultrightvaluemasklookup dst_negative_inverse_symm_resultrightvaluemasklookup. (((dc_mask_inverse_symm_resultrightvalue) = (((((dst_positive_code_inverse_symm_resultrightvaluemasklookup) + (dst_positive_scale_inverse_symm_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_symm_resultrightvaluemasklookup) + (dst_positive_scale_inverse_symm_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_symm_resultrightvaluemasklookup) + (dst_positive_scale_inverse_symm_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_symm_resultrightvaluemasklookup) + (dst_positive_scale_inverse_symm_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_symm_resultrightvaluemasklookup) + (dst_positive_scale_inverse_symm_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_symm_resultrightvaluemasklookup) + (dst_positive_scale_inverse_symm_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_symm_resultrightvaluemasklookup) + (dst_negative_scale_inverse_symm_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_symm_resultrightvaluemasklookuppositive + S (dst_positive_inverse_symm_resultrightvaluemasklookup) = S ((S (dc_index_inverse_symm_resultrightvaluemask)) * dst_positive_scale_inverse_symm_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_symm_resultrightvaluemasklookuppositive. dst_positive_code_inverse_symm_resultrightvaluemasklookup = ff_q_pvs_inverse_symm_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_symm_resultrightvaluemask)) * dst_positive_scale_inverse_symm_resultrightvaluemasklookup) + (dst_positive_inverse_symm_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_symm_resultrightvaluemasklookupnegative + S (dst_negative_inverse_symm_resultrightvaluemasklookup) = S ((S (dc_index_inverse_symm_resultrightvaluemask)) * dst_negative_scale_inverse_symm_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_symm_resultrightvaluemasklookupnegative. dst_negative_code_inverse_symm_resultrightvaluemasklookup = ff_q_pvs_inverse_symm_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_symm_resultrightvaluemask)) * dst_negative_scale_inverse_symm_resultrightvaluemasklookup) + (dst_negative_inverse_symm_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_symm_resultrightvaluemasklookupvalue ge_balance_negative_inverse_symm_resultrightvaluemasklookupvalue. (((((dc_value_inverse_symm_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_symm_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_symm_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_symm_resultrightvaluemask) = 2 * ge_signed_half_inverse_symm_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_symm_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_symm_resultrightvaluemasklookup) + ge_balance_negative_inverse_symm_resultrightvaluemasklookupvalue = (dst_negative_inverse_symm_resultrightvaluemasklookup) + ge_balance_positive_inverse_symm_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_symm_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_symm_resultrightvaluemaskentry dc_left_inverse_symm_resultrightvaluemaskentry dc_right_inverse_symm_resultrightvaluemaskentry. (((dc_input_inverse_symm_resultright)=(dc_index_inverse_symm_resultrightvaluemask)*dc_quotient_inverse_symm_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_symm_resultrightvaluemaskentryleft dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft dst_negative_code_inverse_symm_resultrightvaluemaskentryleft dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft dst_positive_inverse_symm_resultrightvaluemaskentryleft dst_negative_inverse_symm_resultrightvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_symm_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_symm_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_symm_resultrightvaluemask)) * dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_symm_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_symm_resultrightvaluemaskentryleft = ff_q_pvs_inverse_symm_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_symm_resultrightvaluemask)) * dst_positive_scale_inverse_symm_resultrightvaluemaskentryleft) + (dst_positive_inverse_symm_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_symm_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_symm_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_symm_resultrightvaluemask)) * dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_symm_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_symm_resultrightvaluemaskentryleft = ff_q_pvs_inverse_symm_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_symm_resultrightvaluemask)) * dst_negative_scale_inverse_symm_resultrightvaluemaskentryleft) + (dst_negative_inverse_symm_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_symm_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_symm_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_symm_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_symm_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_symm_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_symm_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_symm_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_symm_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_symm_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_symm_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_symm_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_symm_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_symm_resultrightvaluemaskentryright dst_positive_scale_inverse_symm_resultrightvaluemaskentryright dst_negative_code_inverse_symm_resultrightvaluemaskentryright dst_negative_scale_inverse_symm_resultrightvaluemaskentryright dst_positive_inverse_symm_resultrightvaluemaskentryright dst_negative_inverse_symm_resultrightvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_symm_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_symm_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_symm_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_symm_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_symm_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_symm_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_symm_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_symm_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_symm_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_symm_resultrightvaluemaskentry)) * dst_positive_scale_inverse_symm_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_symm_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_symm_resultrightvaluemaskentryright = ff_q_pvs_inverse_symm_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_symm_resultrightvaluemaskentry)) * dst_positive_scale_inverse_symm_resultrightvaluemaskentryright) + (dst_positive_inverse_symm_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_symm_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_symm_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_symm_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_symm_resultrightvaluemaskentry)) * dst_negative_scale_inverse_symm_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_symm_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_symm_resultrightvaluemaskentryright = ff_q_pvs_inverse_symm_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_symm_resultrightvaluemaskentry)) * dst_negative_scale_inverse_symm_resultrightvaluemaskentryright) + (dst_negative_inverse_symm_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_symm_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_symm_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_symm_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_symm_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_symm_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_symm_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_symm_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_symm_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_symm_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_symm_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_symm_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_symm_resultrightvaluemaskentryright) + ge_balance_negative_inverse_symm_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_symm_resultrightvaluemaskentryright) + ge_balance_positive_inverse_symm_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_symm_resultrightvaluemaskentryproduct sto_an_inverse_symm_resultrightvaluemaskentryproduct sto_bp_inverse_symm_resultrightvaluemaskentryproduct sto_bn_inverse_symm_resultrightvaluemaskentryproduct sto_cp_inverse_symm_resultrightvaluemaskentryproduct sto_cn_inverse_symm_resultrightvaluemaskentryproduct. (((((dc_left_inverse_symm_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_symm_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_symm_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_resultrightvaluemaskentryproductleft. (((dc_left_inverse_symm_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_symm_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_symm_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_symm_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_symm_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_symm_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_symm_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_symm_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_resultrightvaluemaskentryproductright. (((dc_right_inverse_symm_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_symm_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_symm_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_symm_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_symm_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_symm_resultrightvaluemask) = 2 * (sto_cp_inverse_symm_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_symm_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_symm_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_symm_resultrightvaluemask) = 2 * ge_signed_half_inverse_symm_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_symm_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_symm_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_symm_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_symm_resultrightvaluemaskentryproduct * sto_bp_inverse_symm_resultrightvaluemaskentryproduct + sto_an_inverse_symm_resultrightvaluemaskentryproduct * sto_bn_inverse_symm_resultrightvaluemaskentryproduct) + sto_cn_inverse_symm_resultrightvaluemaskentryproduct = (sto_ap_inverse_symm_resultrightvaluemaskentryproduct * sto_bn_inverse_symm_resultrightvaluemaskentryproduct + sto_an_inverse_symm_resultrightvaluemaskentryproduct * sto_bp_inverse_symm_resultrightvaluemaskentryproduct) + sto_cp_inverse_symm_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_symm_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_symm_resultrightvaluemaskentrynondivisor. (dc_input_inverse_symm_resultright) = (dc_index_inverse_symm_resultrightvaluemask) * pvs_factor_inverse_symm_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_symm_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_symm_resultrightvaluefold dst_positive_scale_inverse_symm_resultrightvaluefold dst_negative_code_inverse_symm_resultrightvaluefold dst_negative_scale_inverse_symm_resultrightvaluefold dst_positive_sum_inverse_symm_resultrightvaluefold dst_negative_sum_inverse_symm_resultrightvaluefold. (((dc_mask_inverse_symm_resultrightvalue) = (((((dst_positive_code_inverse_symm_resultrightvaluefold) + (dst_positive_scale_inverse_symm_resultrightvaluefold)) * S ((dst_positive_code_inverse_symm_resultrightvaluefold) + (dst_positive_scale_inverse_symm_resultrightvaluefold)) + ((dst_positive_scale_inverse_symm_resultrightvaluefold) + (dst_positive_scale_inverse_symm_resultrightvaluefold))) + (((dst_negative_code_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)) * S ((dst_negative_code_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)) + ((dst_negative_scale_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_symm_resultrightvaluefold) + (dst_positive_scale_inverse_symm_resultrightvaluefold)) * S ((dst_positive_code_inverse_symm_resultrightvaluefold) + (dst_positive_scale_inverse_symm_resultrightvaluefold)) + ((dst_positive_scale_inverse_symm_resultrightvaluefold) + (dst_positive_scale_inverse_symm_resultrightvaluefold))) + (((dst_negative_code_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)) * S ((dst_negative_code_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)) + ((dst_negative_scale_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)))) + ((((dst_negative_code_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)) * S ((dst_negative_code_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)) + ((dst_negative_scale_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold))) + (((dst_negative_code_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)) * S ((dst_negative_code_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)) + ((dst_negative_scale_inverse_symm_resultrightvaluefold) + (dst_negative_scale_inverse_symm_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_symm_resultrightvaluefoldpositive fs_v_dst_inverse_symm_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_symm_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_symm_resultrightvaluefoldpositive = fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_symm_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_symm_resultrightvaluefold) = S ((S (S (dc_input_inverse_symm_resultright))) * fs_v_dst_inverse_symm_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_symm_resultrightvaluefoldpositive = fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_symm_resultright))) * fs_v_dst_inverse_symm_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_symm_resultrightvaluefold))) /\ forall fs_i_dst_inverse_symm_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_symm_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_symm_resultright)) -> exists fs_a_dst_inverse_symm_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_symm_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_symm_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_symm_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_symm_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_symm_resultrightvaluefold)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_symm_resultrightvaluefold = fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_symm_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_symm_resultrightvaluefold) + (fs_a_dst_inverse_symm_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_symm_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_symm_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_symm_resultrightvaluefoldpositive = fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_symm_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_resultrightvaluefoldpositive) + (fs_r_dst_inverse_symm_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_symm_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_symm_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_symm_resultrightvaluefoldpositive = fs_q_dst_inverse_symm_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_symm_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_symm_resultrightvaluefoldpositive) + (fs_s_dst_inverse_symm_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_symm_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_symm_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_symm_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_symm_resultrightvaluefoldnegative fs_v_dst_inverse_symm_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_symm_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_symm_resultrightvaluefoldnegative = fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_symm_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_symm_resultrightvaluefold) = S ((S (S (dc_input_inverse_symm_resultright))) * fs_v_dst_inverse_symm_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_symm_resultrightvaluefoldnegative = fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_symm_resultright))) * fs_v_dst_inverse_symm_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_symm_resultrightvaluefold))) /\ forall fs_i_dst_inverse_symm_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_symm_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_symm_resultright)) -> exists fs_a_dst_inverse_symm_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_symm_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_symm_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_symm_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_symm_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_symm_resultrightvaluefold)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_symm_resultrightvaluefold = fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_symm_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_symm_resultrightvaluefold) + (fs_a_dst_inverse_symm_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_symm_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_symm_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_symm_resultrightvaluefoldnegative = fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_symm_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_resultrightvaluefoldnegative) + (fs_r_dst_inverse_symm_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_symm_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_symm_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_symm_resultrightvaluefoldnegative = fs_q_dst_inverse_symm_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_symm_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_symm_resultrightvaluefoldnegative) + (fs_s_dst_inverse_symm_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_symm_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_symm_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_symm_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_symm_resultrightvaluefoldresult ge_balance_negative_inverse_symm_resultrightvaluefoldresult. (((((dc_output_inverse_symm_resultright) = 2 * (ge_balance_positive_inverse_symm_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_symm_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_symm_resultrightvaluefoldresultdecode. (((dc_output_inverse_symm_resultright) = 2 * ge_signed_half_inverse_symm_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_symm_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_symm_resultrightvaluefoldresult) = S ge_signed_half_inverse_symm_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_symm_resultrightvaluefold) + ge_balance_negative_inverse_symm_resultrightvaluefoldresult = (dst_negative_sum_inverse_symm_resultrightvaluefold) + ge_balance_positive_inverse_symm_resultrightvaluefoldresult))))))))))))))))))))))))Complete tactic proof in conservative notation
All 13 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
13 script commands · 7 reading checkpoints · 0 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
01Fix variables and assumptionsL1–4
02Separate the logical casesL5–7
03Construct an explicit witnessL8–8
Supply the displayed value, then prove that it has the required property.
- L8
exists x
04Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
split
05Use earlier factsL10–10
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L10
exact hi_witness_left
06Separate the logical casesL11–11
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L11
split