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) → ¬N = 0 → DirichletUnitAtOne(F)Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
one_le_of_ne_zero · checked external prerequisitedivisor_signed_table_lookup · checked external prerequisitedirichlet_kronecker_delta_table_one_value · checked external prerequisitedirichlet_convolution_at_one_iff · checked external prerequisitedirichlet_signed_unit_product_classification · checked external prerequisitedirichlet_unit_at_one_from_value
Original expanded first-order statement
forall N F G. (exists di_delta_inverse_necessary_source. ((((exists dst_positive_code_inverse_necessary_sourcedeltatable dst_positive_scale_inverse_necessary_sourcedeltatable dst_negative_code_inverse_necessary_sourcedeltatable dst_negative_scale_inverse_necessary_sourcedeltatable. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable)) * S ((dst_positive_code_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable)) + ((dst_positive_scale_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable))) + (((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) * S ((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) + ((dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)))) * S ((((dst_positive_code_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable)) * S ((dst_positive_code_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable)) + ((dst_positive_scale_inverse_necessary_sourcedeltatable) + (dst_positive_scale_inverse_necessary_sourcedeltatable))) + (((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) * S ((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) + ((dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)))) + ((((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) * S ((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) + ((dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable))) + (((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) * S ((dst_negative_code_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)) + ((dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_scale_inverse_necessary_sourcedeltatable)))))) /\ (forall dst_index_inverse_necessary_sourcedeltatable. (exists pvs_le_gap_inverse_necessary_sourcedeltatabledomain. pvs_le_gap_inverse_necessary_sourcedeltatabledomain + (dst_index_inverse_necessary_sourcedeltatable) = (N)) -> exists dst_positive_inverse_necessary_sourcedeltatable dst_negative_inverse_necessary_sourcedeltatable dst_value_inverse_necessary_sourcedeltatable. ((((exists ff_h_pvs_inverse_necessary_sourcedeltatableentrypositive. ff_h_pvs_inverse_necessary_sourcedeltatableentrypositive + S (dst_positive_inverse_necessary_sourcedeltatable) = S ((S (dst_index_inverse_necessary_sourcedeltatable)) * dst_positive_scale_inverse_necessary_sourcedeltatable)) /\ exists ff_q_pvs_inverse_necessary_sourcedeltatableentrypositive. dst_positive_code_inverse_necessary_sourcedeltatable = ff_q_pvs_inverse_necessary_sourcedeltatableentrypositive * S ((S (dst_index_inverse_necessary_sourcedeltatable)) * dst_positive_scale_inverse_necessary_sourcedeltatable) + (dst_positive_inverse_necessary_sourcedeltatable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcedeltatableentrynegative. ff_h_pvs_inverse_necessary_sourcedeltatableentrynegative + S (dst_negative_inverse_necessary_sourcedeltatable) = S ((S (dst_index_inverse_necessary_sourcedeltatable)) * dst_negative_scale_inverse_necessary_sourcedeltatable)) /\ exists ff_q_pvs_inverse_necessary_sourcedeltatableentrynegative. dst_negative_code_inverse_necessary_sourcedeltatable = ff_q_pvs_inverse_necessary_sourcedeltatableentrynegative * S ((S (dst_index_inverse_necessary_sourcedeltatable)) * dst_negative_scale_inverse_necessary_sourcedeltatable) + (dst_negative_inverse_necessary_sourcedeltatable))) /\ (exists ge_balance_positive_inverse_necessary_sourcedeltatableentryvalue ge_balance_negative_inverse_necessary_sourcedeltatableentryvalue. (((((dst_value_inverse_necessary_sourcedeltatable) = 2 * (ge_balance_positive_inverse_necessary_sourcedeltatableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcedeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcedeltatableentryvaluedecode. (((dst_value_inverse_necessary_sourcedeltatable) = 2 * ge_signed_half_inverse_necessary_sourcedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcedeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcedeltatableentryvalue) = S ge_signed_half_inverse_necessary_sourcedeltatableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcedeltatable) + ge_balance_negative_inverse_necessary_sourcedeltatableentryvalue = (dst_negative_inverse_necessary_sourcedeltatable) + ge_balance_positive_inverse_necessary_sourcedeltatableentryvalue))))))))) /\ (forall du_index_inverse_necessary_sourcedelta du_value_inverse_necessary_sourcedelta. ~(du_index_inverse_necessary_sourcedelta=0) -> (exists pvs_le_gap_inverse_necessary_sourcedeltabound. pvs_le_gap_inverse_necessary_sourcedeltabound + (du_index_inverse_necessary_sourcedelta) = (N)) -> (exists dst_positive_code_inverse_necessary_sourcedeltaentry dst_positive_scale_inverse_necessary_sourcedeltaentry dst_negative_code_inverse_necessary_sourcedeltaentry dst_negative_scale_inverse_necessary_sourcedeltaentry dst_positive_inverse_necessary_sourcedeltaentry dst_negative_inverse_necessary_sourcedeltaentry. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_positive_code_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry)) + ((dst_positive_scale_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry))) + (((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) + ((dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)))) * S ((((dst_positive_code_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_positive_code_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry)) + ((dst_positive_scale_inverse_necessary_sourcedeltaentry) + (dst_positive_scale_inverse_necessary_sourcedeltaentry))) + (((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) + ((dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)))) + ((((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) + ((dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry))) + (((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) * S ((dst_negative_code_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)) + ((dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_scale_inverse_necessary_sourcedeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcedeltaentrypositive. ff_h_pvs_inverse_necessary_sourcedeltaentrypositive + S (dst_positive_inverse_necessary_sourcedeltaentry) = S ((S (du_index_inverse_necessary_sourcedelta)) * dst_positive_scale_inverse_necessary_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_necessary_sourcedeltaentrypositive. dst_positive_code_inverse_necessary_sourcedeltaentry = ff_q_pvs_inverse_necessary_sourcedeltaentrypositive * S ((S (du_index_inverse_necessary_sourcedelta)) * dst_positive_scale_inverse_necessary_sourcedeltaentry) + (dst_positive_inverse_necessary_sourcedeltaentry))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcedeltaentrynegative. ff_h_pvs_inverse_necessary_sourcedeltaentrynegative + S (dst_negative_inverse_necessary_sourcedeltaentry) = S ((S (du_index_inverse_necessary_sourcedelta)) * dst_negative_scale_inverse_necessary_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_necessary_sourcedeltaentrynegative. dst_negative_code_inverse_necessary_sourcedeltaentry = ff_q_pvs_inverse_necessary_sourcedeltaentrynegative * S ((S (du_index_inverse_necessary_sourcedelta)) * dst_negative_scale_inverse_necessary_sourcedeltaentry) + (dst_negative_inverse_necessary_sourcedeltaentry))) /\ (exists ge_balance_positive_inverse_necessary_sourcedeltaentryvalue ge_balance_negative_inverse_necessary_sourcedeltaentryvalue. (((((du_value_inverse_necessary_sourcedelta) = 2 * (ge_balance_positive_inverse_necessary_sourcedeltaentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcedeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcedeltaentryvaluedecode. (((du_value_inverse_necessary_sourcedelta) = 2 * ge_signed_half_inverse_necessary_sourcedeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcedeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcedeltaentryvalue) = S ge_signed_half_inverse_necessary_sourcedeltaentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcedeltaentry) + ge_balance_negative_inverse_necessary_sourcedeltaentryvalue = (dst_negative_inverse_necessary_sourcedeltaentry) + ge_balance_positive_inverse_necessary_sourcedeltaentryvalue))))))))) -> ((((du_index_inverse_necessary_sourcedelta)=1 -> (du_value_inverse_necessary_sourcedelta)=2) /\ (~((du_index_inverse_necessary_sourcedelta)=1) -> (du_value_inverse_necessary_sourcedelta)=0)))))) /\ (((((exists dst_positive_code_inverse_necessary_sourceleftleft dst_positive_scale_inverse_necessary_sourceleftleft dst_negative_code_inverse_necessary_sourceleftleft dst_negative_scale_inverse_necessary_sourceleftleft. (((F) = (((((dst_positive_code_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft)) * S ((dst_positive_code_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft)) + ((dst_positive_scale_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft))) + (((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) * S ((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) + ((dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)))) * S ((((dst_positive_code_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft)) * S ((dst_positive_code_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft)) + ((dst_positive_scale_inverse_necessary_sourceleftleft) + (dst_positive_scale_inverse_necessary_sourceleftleft))) + (((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) * S ((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) + ((dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)))) + ((((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) * S ((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) + ((dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft))) + (((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) * S ((dst_negative_code_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)) + ((dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_scale_inverse_necessary_sourceleftleft)))))) /\ (forall dst_index_inverse_necessary_sourceleftleft. (exists pvs_le_gap_inverse_necessary_sourceleftleftdomain. pvs_le_gap_inverse_necessary_sourceleftleftdomain + (dst_index_inverse_necessary_sourceleftleft) = (N)) -> exists dst_positive_inverse_necessary_sourceleftleft dst_negative_inverse_necessary_sourceleftleft dst_value_inverse_necessary_sourceleftleft. ((((exists ff_h_pvs_inverse_necessary_sourceleftleftentrypositive. ff_h_pvs_inverse_necessary_sourceleftleftentrypositive + S (dst_positive_inverse_necessary_sourceleftleft) = S ((S (dst_index_inverse_necessary_sourceleftleft)) * dst_positive_scale_inverse_necessary_sourceleftleft)) /\ exists ff_q_pvs_inverse_necessary_sourceleftleftentrypositive. dst_positive_code_inverse_necessary_sourceleftleft = ff_q_pvs_inverse_necessary_sourceleftleftentrypositive * S ((S (dst_index_inverse_necessary_sourceleftleft)) * dst_positive_scale_inverse_necessary_sourceleftleft) + (dst_positive_inverse_necessary_sourceleftleft))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftleftentrynegative. ff_h_pvs_inverse_necessary_sourceleftleftentrynegative + S (dst_negative_inverse_necessary_sourceleftleft) = S ((S (dst_index_inverse_necessary_sourceleftleft)) * dst_negative_scale_inverse_necessary_sourceleftleft)) /\ exists ff_q_pvs_inverse_necessary_sourceleftleftentrynegative. dst_negative_code_inverse_necessary_sourceleftleft = ff_q_pvs_inverse_necessary_sourceleftleftentrynegative * S ((S (dst_index_inverse_necessary_sourceleftleft)) * dst_negative_scale_inverse_necessary_sourceleftleft) + (dst_negative_inverse_necessary_sourceleftleft))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftleftentryvalue ge_balance_negative_inverse_necessary_sourceleftleftentryvalue. (((((dst_value_inverse_necessary_sourceleftleft) = 2 * (ge_balance_positive_inverse_necessary_sourceleftleftentryvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftleftentryvaluedecode. (((dst_value_inverse_necessary_sourceleftleft) = 2 * ge_signed_half_inverse_necessary_sourceleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftleftentryvalue) = S ge_signed_half_inverse_necessary_sourceleftleftentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftleft) + ge_balance_negative_inverse_necessary_sourceleftleftentryvalue = (dst_negative_inverse_necessary_sourceleftleft) + ge_balance_positive_inverse_necessary_sourceleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourceleftright dst_positive_scale_inverse_necessary_sourceleftright dst_negative_code_inverse_necessary_sourceleftright dst_negative_scale_inverse_necessary_sourceleftright. (((G) = (((((dst_positive_code_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright)) * S ((dst_positive_code_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright)) + ((dst_positive_scale_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright))) + (((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) * S ((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) + ((dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)))) * S ((((dst_positive_code_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright)) * S ((dst_positive_code_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright)) + ((dst_positive_scale_inverse_necessary_sourceleftright) + (dst_positive_scale_inverse_necessary_sourceleftright))) + (((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) * S ((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) + ((dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)))) + ((((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) * S ((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) + ((dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright))) + (((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) * S ((dst_negative_code_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)) + ((dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_scale_inverse_necessary_sourceleftright)))))) /\ (forall dst_index_inverse_necessary_sourceleftright. (exists pvs_le_gap_inverse_necessary_sourceleftrightdomain. pvs_le_gap_inverse_necessary_sourceleftrightdomain + (dst_index_inverse_necessary_sourceleftright) = (N)) -> exists dst_positive_inverse_necessary_sourceleftright dst_negative_inverse_necessary_sourceleftright dst_value_inverse_necessary_sourceleftright. ((((exists ff_h_pvs_inverse_necessary_sourceleftrightentrypositive. ff_h_pvs_inverse_necessary_sourceleftrightentrypositive + S (dst_positive_inverse_necessary_sourceleftright) = S ((S (dst_index_inverse_necessary_sourceleftright)) * dst_positive_scale_inverse_necessary_sourceleftright)) /\ exists ff_q_pvs_inverse_necessary_sourceleftrightentrypositive. dst_positive_code_inverse_necessary_sourceleftright = ff_q_pvs_inverse_necessary_sourceleftrightentrypositive * S ((S (dst_index_inverse_necessary_sourceleftright)) * dst_positive_scale_inverse_necessary_sourceleftright) + (dst_positive_inverse_necessary_sourceleftright))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftrightentrynegative. ff_h_pvs_inverse_necessary_sourceleftrightentrynegative + S (dst_negative_inverse_necessary_sourceleftright) = S ((S (dst_index_inverse_necessary_sourceleftright)) * dst_negative_scale_inverse_necessary_sourceleftright)) /\ exists ff_q_pvs_inverse_necessary_sourceleftrightentrynegative. dst_negative_code_inverse_necessary_sourceleftright = ff_q_pvs_inverse_necessary_sourceleftrightentrynegative * S ((S (dst_index_inverse_necessary_sourceleftright)) * dst_negative_scale_inverse_necessary_sourceleftright) + (dst_negative_inverse_necessary_sourceleftright))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftrightentryvalue ge_balance_negative_inverse_necessary_sourceleftrightentryvalue. (((((dst_value_inverse_necessary_sourceleftright) = 2 * (ge_balance_positive_inverse_necessary_sourceleftrightentryvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftrightentryvaluedecode. (((dst_value_inverse_necessary_sourceleftright) = 2 * ge_signed_half_inverse_necessary_sourceleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftrightentryvalue) = S ge_signed_half_inverse_necessary_sourceleftrightentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftright) + ge_balance_negative_inverse_necessary_sourceleftrightentryvalue = (dst_negative_inverse_necessary_sourceleftright) + ge_balance_positive_inverse_necessary_sourceleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcelefttable dst_positive_scale_inverse_necessary_sourcelefttable dst_negative_code_inverse_necessary_sourcelefttable dst_negative_scale_inverse_necessary_sourcelefttable. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable)) * S ((dst_positive_code_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable)) + ((dst_positive_scale_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable))) + (((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) * S ((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) + ((dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)))) * S ((((dst_positive_code_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable)) * S ((dst_positive_code_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable)) + ((dst_positive_scale_inverse_necessary_sourcelefttable) + (dst_positive_scale_inverse_necessary_sourcelefttable))) + (((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) * S ((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) + ((dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)))) + ((((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) * S ((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) + ((dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable))) + (((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) * S ((dst_negative_code_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)) + ((dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_scale_inverse_necessary_sourcelefttable)))))) /\ (forall dst_index_inverse_necessary_sourcelefttable. (exists pvs_le_gap_inverse_necessary_sourcelefttabledomain. pvs_le_gap_inverse_necessary_sourcelefttabledomain + (dst_index_inverse_necessary_sourcelefttable) = (N)) -> exists dst_positive_inverse_necessary_sourcelefttable dst_negative_inverse_necessary_sourcelefttable dst_value_inverse_necessary_sourcelefttable. ((((exists ff_h_pvs_inverse_necessary_sourcelefttableentrypositive. ff_h_pvs_inverse_necessary_sourcelefttableentrypositive + S (dst_positive_inverse_necessary_sourcelefttable) = S ((S (dst_index_inverse_necessary_sourcelefttable)) * dst_positive_scale_inverse_necessary_sourcelefttable)) /\ exists ff_q_pvs_inverse_necessary_sourcelefttableentrypositive. dst_positive_code_inverse_necessary_sourcelefttable = ff_q_pvs_inverse_necessary_sourcelefttableentrypositive * S ((S (dst_index_inverse_necessary_sourcelefttable)) * dst_positive_scale_inverse_necessary_sourcelefttable) + (dst_positive_inverse_necessary_sourcelefttable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcelefttableentrynegative. ff_h_pvs_inverse_necessary_sourcelefttableentrynegative + S (dst_negative_inverse_necessary_sourcelefttable) = S ((S (dst_index_inverse_necessary_sourcelefttable)) * dst_negative_scale_inverse_necessary_sourcelefttable)) /\ exists ff_q_pvs_inverse_necessary_sourcelefttableentrynegative. dst_negative_code_inverse_necessary_sourcelefttable = ff_q_pvs_inverse_necessary_sourcelefttableentrynegative * S ((S (dst_index_inverse_necessary_sourcelefttable)) * dst_negative_scale_inverse_necessary_sourcelefttable) + (dst_negative_inverse_necessary_sourcelefttable))) /\ (exists ge_balance_positive_inverse_necessary_sourcelefttableentryvalue ge_balance_negative_inverse_necessary_sourcelefttableentryvalue. (((((dst_value_inverse_necessary_sourcelefttable) = 2 * (ge_balance_positive_inverse_necessary_sourcelefttableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcelefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcelefttableentryvaluedecode. (((dst_value_inverse_necessary_sourcelefttable) = 2 * ge_signed_half_inverse_necessary_sourcelefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcelefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcelefttableentryvalue) = S ge_signed_half_inverse_necessary_sourcelefttableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcelefttable) + ge_balance_negative_inverse_necessary_sourcelefttableentryvalue = (dst_negative_inverse_necessary_sourcelefttable) + ge_balance_positive_inverse_necessary_sourcelefttableentryvalue))))))))) /\ (forall dc_input_inverse_necessary_sourceleft dc_output_inverse_necessary_sourceleft. ~(dc_input_inverse_necessary_sourceleft=0) -> (exists pvs_le_gap_inverse_necessary_sourceleftdomain. pvs_le_gap_inverse_necessary_sourceleftdomain + (dc_input_inverse_necessary_sourceleft) = (N)) -> (exists dst_positive_code_inverse_necessary_sourceleftlookup dst_positive_scale_inverse_necessary_sourceleftlookup dst_negative_code_inverse_necessary_sourceleftlookup dst_negative_scale_inverse_necessary_sourceleftlookup dst_positive_inverse_necessary_sourceleftlookup dst_negative_inverse_necessary_sourceleftlookup. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup)) * S ((dst_positive_code_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup)) + ((dst_positive_scale_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup))) + (((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) * S ((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) + ((dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)))) * S ((((dst_positive_code_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup)) * S ((dst_positive_code_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup)) + ((dst_positive_scale_inverse_necessary_sourceleftlookup) + (dst_positive_scale_inverse_necessary_sourceleftlookup))) + (((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) * S ((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) + ((dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)))) + ((((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) * S ((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) + ((dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup))) + (((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) * S ((dst_negative_code_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)) + ((dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_scale_inverse_necessary_sourceleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftlookuppositive. ff_h_pvs_inverse_necessary_sourceleftlookuppositive + S (dst_positive_inverse_necessary_sourceleftlookup) = S ((S (dc_input_inverse_necessary_sourceleft)) * dst_positive_scale_inverse_necessary_sourceleftlookup)) /\ exists ff_q_pvs_inverse_necessary_sourceleftlookuppositive. dst_positive_code_inverse_necessary_sourceleftlookup = ff_q_pvs_inverse_necessary_sourceleftlookuppositive * S ((S (dc_input_inverse_necessary_sourceleft)) * dst_positive_scale_inverse_necessary_sourceleftlookup) + (dst_positive_inverse_necessary_sourceleftlookup))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftlookupnegative. ff_h_pvs_inverse_necessary_sourceleftlookupnegative + S (dst_negative_inverse_necessary_sourceleftlookup) = S ((S (dc_input_inverse_necessary_sourceleft)) * dst_negative_scale_inverse_necessary_sourceleftlookup)) /\ exists ff_q_pvs_inverse_necessary_sourceleftlookupnegative. dst_negative_code_inverse_necessary_sourceleftlookup = ff_q_pvs_inverse_necessary_sourceleftlookupnegative * S ((S (dc_input_inverse_necessary_sourceleft)) * dst_negative_scale_inverse_necessary_sourceleftlookup) + (dst_negative_inverse_necessary_sourceleftlookup))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftlookupvalue ge_balance_negative_inverse_necessary_sourceleftlookupvalue. (((((dc_output_inverse_necessary_sourceleft) = 2 * (ge_balance_positive_inverse_necessary_sourceleftlookupvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftlookupvaluedecode. (((dc_output_inverse_necessary_sourceleft) = 2 * ge_signed_half_inverse_necessary_sourceleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftlookupvalue) = S ge_signed_half_inverse_necessary_sourceleftlookupvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftlookup) + ge_balance_negative_inverse_necessary_sourceleftlookupvalue = (dst_negative_inverse_necessary_sourceleftlookup) + ge_balance_positive_inverse_necessary_sourceleftlookupvalue))))))))) -> (((~((dc_input_inverse_necessary_sourceleft)=0)) /\ (exists dc_mask_inverse_necessary_sourceleftvalue. ((((exists dst_positive_code_inverse_necessary_sourceleftvaluemasktable dst_positive_scale_inverse_necessary_sourceleftvaluemasktable dst_negative_code_inverse_necessary_sourceleftvaluemasktable dst_negative_scale_inverse_necessary_sourceleftvaluemasktable. (((dc_mask_inverse_necessary_sourceleftvalue) = (((((dst_positive_code_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)))))) /\ (forall dst_index_inverse_necessary_sourceleftvaluemasktable. (exists pvs_le_gap_inverse_necessary_sourceleftvaluemasktabledomain. pvs_le_gap_inverse_necessary_sourceleftvaluemasktabledomain + (dst_index_inverse_necessary_sourceleftvaluemasktable) = (dc_input_inverse_necessary_sourceleft)) -> exists dst_positive_inverse_necessary_sourceleftvaluemasktable dst_negative_inverse_necessary_sourceleftvaluemasktable dst_value_inverse_necessary_sourceleftvaluemasktable. ((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemasktableentrypositive. ff_h_pvs_inverse_necessary_sourceleftvaluemasktableentrypositive + S (dst_positive_inverse_necessary_sourceleftvaluemasktable) = S ((S (dst_index_inverse_necessary_sourceleftvaluemasktable)) * dst_positive_scale_inverse_necessary_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemasktableentrypositive. dst_positive_code_inverse_necessary_sourceleftvaluemasktable = ff_q_pvs_inverse_necessary_sourceleftvaluemasktableentrypositive * S ((S (dst_index_inverse_necessary_sourceleftvaluemasktable)) * dst_positive_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_positive_inverse_necessary_sourceleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemasktableentrynegative. ff_h_pvs_inverse_necessary_sourceleftvaluemasktableentrynegative + S (dst_negative_inverse_necessary_sourceleftvaluemasktable) = S ((S (dst_index_inverse_necessary_sourceleftvaluemasktable)) * dst_negative_scale_inverse_necessary_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemasktableentrynegative. dst_negative_code_inverse_necessary_sourceleftvaluemasktable = ff_q_pvs_inverse_necessary_sourceleftvaluemasktableentrynegative * S ((S (dst_index_inverse_necessary_sourceleftvaluemasktable)) * dst_negative_scale_inverse_necessary_sourceleftvaluemasktable) + (dst_negative_inverse_necessary_sourceleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluemasktableentryvalue ge_balance_negative_inverse_necessary_sourceleftvaluemasktableentryvalue. (((((dst_value_inverse_necessary_sourceleftvaluemasktable) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemasktableentryvaluedecode. (((dst_value_inverse_necessary_sourceleftvaluemasktable) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemasktableentryvalue) = S ge_signed_half_inverse_necessary_sourceleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftvaluemasktable) + ge_balance_negative_inverse_necessary_sourceleftvaluemasktableentryvalue = (dst_negative_inverse_necessary_sourceleftvaluemasktable) + ge_balance_positive_inverse_necessary_sourceleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_necessary_sourceleftvaluemask dc_value_inverse_necessary_sourceleftvaluemask. (exists pvs_le_gap_inverse_necessary_sourceleftvaluemaskdomain. pvs_le_gap_inverse_necessary_sourceleftvaluemaskdomain + (dc_index_inverse_necessary_sourceleftvaluemask) = (dc_input_inverse_necessary_sourceleft)) -> (exists dst_positive_code_inverse_necessary_sourceleftvaluemasklookup dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup dst_negative_code_inverse_necessary_sourceleftvaluemasklookup dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup dst_positive_inverse_necessary_sourceleftvaluemasklookup dst_negative_inverse_necessary_sourceleftvaluemasklookup. (((dc_mask_inverse_necessary_sourceleftvalue) = (((((dst_positive_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemasklookuppositive. ff_h_pvs_inverse_necessary_sourceleftvaluemasklookuppositive + S (dst_positive_inverse_necessary_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemasklookuppositive. dst_positive_code_inverse_necessary_sourceleftvaluemasklookup = ff_q_pvs_inverse_necessary_sourceleftvaluemasklookuppositive * S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_positive_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_positive_inverse_necessary_sourceleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemasklookupnegative. ff_h_pvs_inverse_necessary_sourceleftvaluemasklookupnegative + S (dst_negative_inverse_necessary_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemasklookupnegative. dst_negative_code_inverse_necessary_sourceleftvaluemasklookup = ff_q_pvs_inverse_necessary_sourceleftvaluemasklookupnegative * S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_negative_scale_inverse_necessary_sourceleftvaluemasklookup) + (dst_negative_inverse_necessary_sourceleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluemasklookupvalue ge_balance_negative_inverse_necessary_sourceleftvaluemasklookupvalue. (((((dc_value_inverse_necessary_sourceleftvaluemask) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemasklookupvaluedecode. (((dc_value_inverse_necessary_sourceleftvaluemask) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemasklookupvalue) = S ge_signed_half_inverse_necessary_sourceleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftvaluemasklookup) + ge_balance_negative_inverse_necessary_sourceleftvaluemasklookupvalue = (dst_negative_inverse_necessary_sourceleftvaluemasklookup) + ge_balance_positive_inverse_necessary_sourceleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_necessary_sourceleftvaluemask)=0)) /\ (exists dc_quotient_inverse_necessary_sourceleftvaluemaskentry dc_left_inverse_necessary_sourceleftvaluemaskentry dc_right_inverse_necessary_sourceleftvaluemaskentry. (((dc_input_inverse_necessary_sourceleft)=(dc_index_inverse_necessary_sourceleftvaluemask)*dc_quotient_inverse_necessary_sourceleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft dst_positive_inverse_necessary_sourceleftvaluemaskentryleft dst_negative_inverse_necessary_sourceleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryleftpositive. ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryleftpositive + S (dst_positive_inverse_necessary_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryleftpositive. dst_positive_code_inverse_necessary_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_positive_inverse_necessary_sourceleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryleftnegative. ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryleftnegative + S (dst_negative_inverse_necessary_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryleftnegative. dst_negative_code_inverse_necessary_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_necessary_sourceleftvaluemask)) * dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryleft) + (dst_negative_inverse_necessary_sourceleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryleftvalue ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryleftvalue. (((((dc_left_inverse_necessary_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_necessary_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftvaluemaskentryleft) + ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryleftvalue = (dst_negative_inverse_necessary_sourceleftvaluemaskentryleft) + ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright dst_positive_inverse_necessary_sourceleftvaluemaskentryright dst_negative_inverse_necessary_sourceleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryrightpositive. ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryrightpositive + S (dst_positive_inverse_necessary_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_necessary_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryrightpositive. dst_positive_code_inverse_necessary_sourceleftvaluemaskentryright = ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_necessary_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_positive_inverse_necessary_sourceleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryrightnegative. ff_h_pvs_inverse_necessary_sourceleftvaluemaskentryrightnegative + S (dst_negative_inverse_necessary_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_necessary_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryrightnegative. dst_negative_code_inverse_necessary_sourceleftvaluemaskentryright = ff_q_pvs_inverse_necessary_sourceleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_necessary_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_necessary_sourceleftvaluemaskentryright) + (dst_negative_inverse_necessary_sourceleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryrightvalue ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryrightvalue. (((((dc_right_inverse_necessary_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_necessary_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_necessary_sourceleftvaluemaskentryright) + ge_balance_negative_inverse_necessary_sourceleftvaluemaskentryrightvalue = (dst_negative_inverse_necessary_sourceleftvaluemaskentryright) + ge_balance_positive_inverse_necessary_sourceleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct sto_an_inverse_necessary_sourceleftvaluemaskentryproduct sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct sto_cp_inverse_necessary_sourceleftvaluemaskentryproduct sto_cn_inverse_necessary_sourceleftvaluemaskentryproduct. (((((dc_left_inverse_necessary_sourceleftvaluemaskentry) = 2 * (sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct) /\ (sto_an_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductleft. (((dc_left_inverse_necessary_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_necessary_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_necessary_sourceleftvaluemaskentry) = 2 * (sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct) /\ (sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductright. (((dc_right_inverse_necessary_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_necessary_sourceleftvaluemask) = 2 * (sto_cp_inverse_necessary_sourceleftvaluemaskentryproduct) /\ (sto_cn_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductoutput. (((dc_value_inverse_necessary_sourceleftvaluemask) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_necessary_sourceleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_necessary_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourceleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct * sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct + sto_an_inverse_necessary_sourceleftvaluemaskentryproduct * sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct) + sto_cn_inverse_necessary_sourceleftvaluemaskentryproduct = (sto_ap_inverse_necessary_sourceleftvaluemaskentryproduct * sto_bn_inverse_necessary_sourceleftvaluemaskentryproduct + sto_an_inverse_necessary_sourceleftvaluemaskentryproduct * sto_bp_inverse_necessary_sourceleftvaluemaskentryproduct) + sto_cp_inverse_necessary_sourceleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_necessary_sourceleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_necessary_sourceleftvaluemaskentrynondivisor. (dc_input_inverse_necessary_sourceleft) = (dc_index_inverse_necessary_sourceleftvaluemask) * pvs_factor_inverse_necessary_sourceleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_necessary_sourceleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_necessary_sourceleftvaluefold dst_positive_scale_inverse_necessary_sourceleftvaluefold dst_negative_code_inverse_necessary_sourceleftvaluefold dst_negative_scale_inverse_necessary_sourceleftvaluefold dst_positive_sum_inverse_necessary_sourceleftvaluefold dst_negative_sum_inverse_necessary_sourceleftvaluefold. (((dc_mask_inverse_necessary_sourceleftvalue) = (((((dst_positive_code_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold))) + (((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)))) * S ((((dst_positive_code_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_positive_code_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_positive_scale_inverse_necessary_sourceleftvaluefold) + (dst_positive_scale_inverse_necessary_sourceleftvaluefold))) + (((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)))) + ((((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold))) + (((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) * S ((dst_negative_code_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)) + ((dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (dst_negative_scale_inverse_necessary_sourceleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive. ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_start. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_start. fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_necessary_sourceleftvaluefold) = S ((S (S (dc_input_inverse_necessary_sourceleft))) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_necessary_sourceleft))) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive) + (dst_positive_sum_inverse_necessary_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps = S (dc_input_inverse_necessary_sourceleft)) -> exists fs_a_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps fs_r_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps fs_s_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_necessary_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_necessary_sourceleftvaluefold = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_necessary_sourceleftvaluefold) + (fs_a_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive) + (fs_r_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_necessary_sourceleftvaluefoldpositive = fs_q_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldpositive) + (fs_s_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps = fs_r_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps + fs_a_dst_inverse_necessary_sourceleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative. ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_start. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_start. fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_necessary_sourceleftvaluefold) = S ((S (S (dc_input_inverse_necessary_sourceleft))) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_necessary_sourceleft))) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative) + (dst_negative_sum_inverse_necessary_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps = S (dc_input_inverse_necessary_sourceleft)) -> exists fs_a_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps fs_r_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps fs_s_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_necessary_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_necessary_sourceleftvaluefold = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_necessary_sourceleftvaluefold) + (fs_a_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative) + (fs_r_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_necessary_sourceleftvaluefoldnegative = fs_q_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourceleftvaluefoldnegative) + (fs_s_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps = fs_r_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps + fs_a_dst_inverse_necessary_sourceleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_necessary_sourceleftvaluefoldresult ge_balance_negative_inverse_necessary_sourceleftvaluefoldresult. (((((dc_output_inverse_necessary_sourceleft) = 2 * (ge_balance_positive_inverse_necessary_sourceleftvaluefoldresult) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_necessary_sourceleftvaluefoldresultdecode. (((dc_output_inverse_necessary_sourceleft) = 2 * ge_signed_half_inverse_necessary_sourceleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_necessary_sourceleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_necessary_sourceleftvaluefoldresult) = S ge_signed_half_inverse_necessary_sourceleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_necessary_sourceleftvaluefold) + ge_balance_negative_inverse_necessary_sourceleftvaluefoldresult = (dst_negative_sum_inverse_necessary_sourceleftvaluefold) + ge_balance_positive_inverse_necessary_sourceleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcerightleft dst_positive_scale_inverse_necessary_sourcerightleft dst_negative_code_inverse_necessary_sourcerightleft dst_negative_scale_inverse_necessary_sourcerightleft. (((G) = (((((dst_positive_code_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft)) * S ((dst_positive_code_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft)) + ((dst_positive_scale_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft))) + (((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) * S ((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) + ((dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)))) * S ((((dst_positive_code_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft)) * S ((dst_positive_code_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft)) + ((dst_positive_scale_inverse_necessary_sourcerightleft) + (dst_positive_scale_inverse_necessary_sourcerightleft))) + (((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) * S ((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) + ((dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)))) + ((((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) * S ((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) + ((dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft))) + (((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) * S ((dst_negative_code_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)) + ((dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_scale_inverse_necessary_sourcerightleft)))))) /\ (forall dst_index_inverse_necessary_sourcerightleft. (exists pvs_le_gap_inverse_necessary_sourcerightleftdomain. pvs_le_gap_inverse_necessary_sourcerightleftdomain + (dst_index_inverse_necessary_sourcerightleft) = (N)) -> exists dst_positive_inverse_necessary_sourcerightleft dst_negative_inverse_necessary_sourcerightleft dst_value_inverse_necessary_sourcerightleft. ((((exists ff_h_pvs_inverse_necessary_sourcerightleftentrypositive. ff_h_pvs_inverse_necessary_sourcerightleftentrypositive + S (dst_positive_inverse_necessary_sourcerightleft) = S ((S (dst_index_inverse_necessary_sourcerightleft)) * dst_positive_scale_inverse_necessary_sourcerightleft)) /\ exists ff_q_pvs_inverse_necessary_sourcerightleftentrypositive. dst_positive_code_inverse_necessary_sourcerightleft = ff_q_pvs_inverse_necessary_sourcerightleftentrypositive * S ((S (dst_index_inverse_necessary_sourcerightleft)) * dst_positive_scale_inverse_necessary_sourcerightleft) + (dst_positive_inverse_necessary_sourcerightleft))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightleftentrynegative. ff_h_pvs_inverse_necessary_sourcerightleftentrynegative + S (dst_negative_inverse_necessary_sourcerightleft) = S ((S (dst_index_inverse_necessary_sourcerightleft)) * dst_negative_scale_inverse_necessary_sourcerightleft)) /\ exists ff_q_pvs_inverse_necessary_sourcerightleftentrynegative. dst_negative_code_inverse_necessary_sourcerightleft = ff_q_pvs_inverse_necessary_sourcerightleftentrynegative * S ((S (dst_index_inverse_necessary_sourcerightleft)) * dst_negative_scale_inverse_necessary_sourcerightleft) + (dst_negative_inverse_necessary_sourcerightleft))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightleftentryvalue ge_balance_negative_inverse_necessary_sourcerightleftentryvalue. (((((dst_value_inverse_necessary_sourcerightleft) = 2 * (ge_balance_positive_inverse_necessary_sourcerightleftentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightleftentryvaluedecode. (((dst_value_inverse_necessary_sourcerightleft) = 2 * ge_signed_half_inverse_necessary_sourcerightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightleftentryvalue) = S ge_signed_half_inverse_necessary_sourcerightleftentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightleft) + ge_balance_negative_inverse_necessary_sourcerightleftentryvalue = (dst_negative_inverse_necessary_sourcerightleft) + ge_balance_positive_inverse_necessary_sourcerightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcerightright dst_positive_scale_inverse_necessary_sourcerightright dst_negative_code_inverse_necessary_sourcerightright dst_negative_scale_inverse_necessary_sourcerightright. (((F) = (((((dst_positive_code_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright)) * S ((dst_positive_code_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright)) + ((dst_positive_scale_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright))) + (((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) * S ((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) + ((dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)))) * S ((((dst_positive_code_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright)) * S ((dst_positive_code_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright)) + ((dst_positive_scale_inverse_necessary_sourcerightright) + (dst_positive_scale_inverse_necessary_sourcerightright))) + (((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) * S ((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) + ((dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)))) + ((((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) * S ((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) + ((dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright))) + (((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) * S ((dst_negative_code_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)) + ((dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_scale_inverse_necessary_sourcerightright)))))) /\ (forall dst_index_inverse_necessary_sourcerightright. (exists pvs_le_gap_inverse_necessary_sourcerightrightdomain. pvs_le_gap_inverse_necessary_sourcerightrightdomain + (dst_index_inverse_necessary_sourcerightright) = (N)) -> exists dst_positive_inverse_necessary_sourcerightright dst_negative_inverse_necessary_sourcerightright dst_value_inverse_necessary_sourcerightright. ((((exists ff_h_pvs_inverse_necessary_sourcerightrightentrypositive. ff_h_pvs_inverse_necessary_sourcerightrightentrypositive + S (dst_positive_inverse_necessary_sourcerightright) = S ((S (dst_index_inverse_necessary_sourcerightright)) * dst_positive_scale_inverse_necessary_sourcerightright)) /\ exists ff_q_pvs_inverse_necessary_sourcerightrightentrypositive. dst_positive_code_inverse_necessary_sourcerightright = ff_q_pvs_inverse_necessary_sourcerightrightentrypositive * S ((S (dst_index_inverse_necessary_sourcerightright)) * dst_positive_scale_inverse_necessary_sourcerightright) + (dst_positive_inverse_necessary_sourcerightright))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightrightentrynegative. ff_h_pvs_inverse_necessary_sourcerightrightentrynegative + S (dst_negative_inverse_necessary_sourcerightright) = S ((S (dst_index_inverse_necessary_sourcerightright)) * dst_negative_scale_inverse_necessary_sourcerightright)) /\ exists ff_q_pvs_inverse_necessary_sourcerightrightentrynegative. dst_negative_code_inverse_necessary_sourcerightright = ff_q_pvs_inverse_necessary_sourcerightrightentrynegative * S ((S (dst_index_inverse_necessary_sourcerightright)) * dst_negative_scale_inverse_necessary_sourcerightright) + (dst_negative_inverse_necessary_sourcerightright))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightrightentryvalue ge_balance_negative_inverse_necessary_sourcerightrightentryvalue. (((((dst_value_inverse_necessary_sourcerightright) = 2 * (ge_balance_positive_inverse_necessary_sourcerightrightentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightrightentryvaluedecode. (((dst_value_inverse_necessary_sourcerightright) = 2 * ge_signed_half_inverse_necessary_sourcerightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightrightentryvalue) = S ge_signed_half_inverse_necessary_sourcerightrightentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightright) + ge_balance_negative_inverse_necessary_sourcerightrightentryvalue = (dst_negative_inverse_necessary_sourcerightright) + ge_balance_positive_inverse_necessary_sourcerightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcerighttable dst_positive_scale_inverse_necessary_sourcerighttable dst_negative_code_inverse_necessary_sourcerighttable dst_negative_scale_inverse_necessary_sourcerighttable. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable)) * S ((dst_positive_code_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable)) + ((dst_positive_scale_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable))) + (((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) * S ((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) + ((dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)))) * S ((((dst_positive_code_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable)) * S ((dst_positive_code_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable)) + ((dst_positive_scale_inverse_necessary_sourcerighttable) + (dst_positive_scale_inverse_necessary_sourcerighttable))) + (((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) * S ((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) + ((dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)))) + ((((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) * S ((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) + ((dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable))) + (((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) * S ((dst_negative_code_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)) + ((dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_scale_inverse_necessary_sourcerighttable)))))) /\ (forall dst_index_inverse_necessary_sourcerighttable. (exists pvs_le_gap_inverse_necessary_sourcerighttabledomain. pvs_le_gap_inverse_necessary_sourcerighttabledomain + (dst_index_inverse_necessary_sourcerighttable) = (N)) -> exists dst_positive_inverse_necessary_sourcerighttable dst_negative_inverse_necessary_sourcerighttable dst_value_inverse_necessary_sourcerighttable. ((((exists ff_h_pvs_inverse_necessary_sourcerighttableentrypositive. ff_h_pvs_inverse_necessary_sourcerighttableentrypositive + S (dst_positive_inverse_necessary_sourcerighttable) = S ((S (dst_index_inverse_necessary_sourcerighttable)) * dst_positive_scale_inverse_necessary_sourcerighttable)) /\ exists ff_q_pvs_inverse_necessary_sourcerighttableentrypositive. dst_positive_code_inverse_necessary_sourcerighttable = ff_q_pvs_inverse_necessary_sourcerighttableentrypositive * S ((S (dst_index_inverse_necessary_sourcerighttable)) * dst_positive_scale_inverse_necessary_sourcerighttable) + (dst_positive_inverse_necessary_sourcerighttable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerighttableentrynegative. ff_h_pvs_inverse_necessary_sourcerighttableentrynegative + S (dst_negative_inverse_necessary_sourcerighttable) = S ((S (dst_index_inverse_necessary_sourcerighttable)) * dst_negative_scale_inverse_necessary_sourcerighttable)) /\ exists ff_q_pvs_inverse_necessary_sourcerighttableentrynegative. dst_negative_code_inverse_necessary_sourcerighttable = ff_q_pvs_inverse_necessary_sourcerighttableentrynegative * S ((S (dst_index_inverse_necessary_sourcerighttable)) * dst_negative_scale_inverse_necessary_sourcerighttable) + (dst_negative_inverse_necessary_sourcerighttable))) /\ (exists ge_balance_positive_inverse_necessary_sourcerighttableentryvalue ge_balance_negative_inverse_necessary_sourcerighttableentryvalue. (((((dst_value_inverse_necessary_sourcerighttable) = 2 * (ge_balance_positive_inverse_necessary_sourcerighttableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcerighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerighttableentryvaluedecode. (((dst_value_inverse_necessary_sourcerighttable) = 2 * ge_signed_half_inverse_necessary_sourcerighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerighttableentryvalue) = S ge_signed_half_inverse_necessary_sourcerighttableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerighttable) + ge_balance_negative_inverse_necessary_sourcerighttableentryvalue = (dst_negative_inverse_necessary_sourcerighttable) + ge_balance_positive_inverse_necessary_sourcerighttableentryvalue))))))))) /\ (forall dc_input_inverse_necessary_sourceright dc_output_inverse_necessary_sourceright. ~(dc_input_inverse_necessary_sourceright=0) -> (exists pvs_le_gap_inverse_necessary_sourcerightdomain. pvs_le_gap_inverse_necessary_sourcerightdomain + (dc_input_inverse_necessary_sourceright) = (N)) -> (exists dst_positive_code_inverse_necessary_sourcerightlookup dst_positive_scale_inverse_necessary_sourcerightlookup dst_negative_code_inverse_necessary_sourcerightlookup dst_negative_scale_inverse_necessary_sourcerightlookup dst_positive_inverse_necessary_sourcerightlookup dst_negative_inverse_necessary_sourcerightlookup. (((di_delta_inverse_necessary_source) = (((((dst_positive_code_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup)) * S ((dst_positive_code_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup)) + ((dst_positive_scale_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup))) + (((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) * S ((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) + ((dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)))) * S ((((dst_positive_code_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup)) * S ((dst_positive_code_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup)) + ((dst_positive_scale_inverse_necessary_sourcerightlookup) + (dst_positive_scale_inverse_necessary_sourcerightlookup))) + (((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) * S ((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) + ((dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)))) + ((((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) * S ((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) + ((dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup))) + (((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) * S ((dst_negative_code_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)) + ((dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_scale_inverse_necessary_sourcerightlookup)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightlookuppositive. ff_h_pvs_inverse_necessary_sourcerightlookuppositive + S (dst_positive_inverse_necessary_sourcerightlookup) = S ((S (dc_input_inverse_necessary_sourceright)) * dst_positive_scale_inverse_necessary_sourcerightlookup)) /\ exists ff_q_pvs_inverse_necessary_sourcerightlookuppositive. dst_positive_code_inverse_necessary_sourcerightlookup = ff_q_pvs_inverse_necessary_sourcerightlookuppositive * S ((S (dc_input_inverse_necessary_sourceright)) * dst_positive_scale_inverse_necessary_sourcerightlookup) + (dst_positive_inverse_necessary_sourcerightlookup))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightlookupnegative. ff_h_pvs_inverse_necessary_sourcerightlookupnegative + S (dst_negative_inverse_necessary_sourcerightlookup) = S ((S (dc_input_inverse_necessary_sourceright)) * dst_negative_scale_inverse_necessary_sourcerightlookup)) /\ exists ff_q_pvs_inverse_necessary_sourcerightlookupnegative. dst_negative_code_inverse_necessary_sourcerightlookup = ff_q_pvs_inverse_necessary_sourcerightlookupnegative * S ((S (dc_input_inverse_necessary_sourceright)) * dst_negative_scale_inverse_necessary_sourcerightlookup) + (dst_negative_inverse_necessary_sourcerightlookup))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightlookupvalue ge_balance_negative_inverse_necessary_sourcerightlookupvalue. (((((dc_output_inverse_necessary_sourceright) = 2 * (ge_balance_positive_inverse_necessary_sourcerightlookupvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightlookupvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightlookupvaluedecode. (((dc_output_inverse_necessary_sourceright) = 2 * ge_signed_half_inverse_necessary_sourcerightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightlookupvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightlookupvalue) = S ge_signed_half_inverse_necessary_sourcerightlookupvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightlookup) + ge_balance_negative_inverse_necessary_sourcerightlookupvalue = (dst_negative_inverse_necessary_sourcerightlookup) + ge_balance_positive_inverse_necessary_sourcerightlookupvalue))))))))) -> (((~((dc_input_inverse_necessary_sourceright)=0)) /\ (exists dc_mask_inverse_necessary_sourcerightvalue. ((((exists dst_positive_code_inverse_necessary_sourcerightvaluemasktable dst_positive_scale_inverse_necessary_sourcerightvaluemasktable dst_negative_code_inverse_necessary_sourcerightvaluemasktable dst_negative_scale_inverse_necessary_sourcerightvaluemasktable. (((dc_mask_inverse_necessary_sourcerightvalue) = (((((dst_positive_code_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)))))) /\ (forall dst_index_inverse_necessary_sourcerightvaluemasktable. (exists pvs_le_gap_inverse_necessary_sourcerightvaluemasktabledomain. pvs_le_gap_inverse_necessary_sourcerightvaluemasktabledomain + (dst_index_inverse_necessary_sourcerightvaluemasktable) = (dc_input_inverse_necessary_sourceright)) -> exists dst_positive_inverse_necessary_sourcerightvaluemasktable dst_negative_inverse_necessary_sourcerightvaluemasktable dst_value_inverse_necessary_sourcerightvaluemasktable. ((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemasktableentrypositive. ff_h_pvs_inverse_necessary_sourcerightvaluemasktableentrypositive + S (dst_positive_inverse_necessary_sourcerightvaluemasktable) = S ((S (dst_index_inverse_necessary_sourcerightvaluemasktable)) * dst_positive_scale_inverse_necessary_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemasktableentrypositive. dst_positive_code_inverse_necessary_sourcerightvaluemasktable = ff_q_pvs_inverse_necessary_sourcerightvaluemasktableentrypositive * S ((S (dst_index_inverse_necessary_sourcerightvaluemasktable)) * dst_positive_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_positive_inverse_necessary_sourcerightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemasktableentrynegative. ff_h_pvs_inverse_necessary_sourcerightvaluemasktableentrynegative + S (dst_negative_inverse_necessary_sourcerightvaluemasktable) = S ((S (dst_index_inverse_necessary_sourcerightvaluemasktable)) * dst_negative_scale_inverse_necessary_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemasktableentrynegative. dst_negative_code_inverse_necessary_sourcerightvaluemasktable = ff_q_pvs_inverse_necessary_sourcerightvaluemasktableentrynegative * S ((S (dst_index_inverse_necessary_sourcerightvaluemasktable)) * dst_negative_scale_inverse_necessary_sourcerightvaluemasktable) + (dst_negative_inverse_necessary_sourcerightvaluemasktable))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluemasktableentryvalue ge_balance_negative_inverse_necessary_sourcerightvaluemasktableentryvalue. (((((dst_value_inverse_necessary_sourcerightvaluemasktable) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemasktableentryvaluedecode. (((dst_value_inverse_necessary_sourcerightvaluemasktable) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemasktableentryvalue) = S ge_signed_half_inverse_necessary_sourcerightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightvaluemasktable) + ge_balance_negative_inverse_necessary_sourcerightvaluemasktableentryvalue = (dst_negative_inverse_necessary_sourcerightvaluemasktable) + ge_balance_positive_inverse_necessary_sourcerightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_necessary_sourcerightvaluemask dc_value_inverse_necessary_sourcerightvaluemask. (exists pvs_le_gap_inverse_necessary_sourcerightvaluemaskdomain. pvs_le_gap_inverse_necessary_sourcerightvaluemaskdomain + (dc_index_inverse_necessary_sourcerightvaluemask) = (dc_input_inverse_necessary_sourceright)) -> (exists dst_positive_code_inverse_necessary_sourcerightvaluemasklookup dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup dst_negative_code_inverse_necessary_sourcerightvaluemasklookup dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup dst_positive_inverse_necessary_sourcerightvaluemasklookup dst_negative_inverse_necessary_sourcerightvaluemasklookup. (((dc_mask_inverse_necessary_sourcerightvalue) = (((((dst_positive_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemasklookuppositive. ff_h_pvs_inverse_necessary_sourcerightvaluemasklookuppositive + S (dst_positive_inverse_necessary_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemasklookuppositive. dst_positive_code_inverse_necessary_sourcerightvaluemasklookup = ff_q_pvs_inverse_necessary_sourcerightvaluemasklookuppositive * S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_positive_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_positive_inverse_necessary_sourcerightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemasklookupnegative. ff_h_pvs_inverse_necessary_sourcerightvaluemasklookupnegative + S (dst_negative_inverse_necessary_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemasklookupnegative. dst_negative_code_inverse_necessary_sourcerightvaluemasklookup = ff_q_pvs_inverse_necessary_sourcerightvaluemasklookupnegative * S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_negative_scale_inverse_necessary_sourcerightvaluemasklookup) + (dst_negative_inverse_necessary_sourcerightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluemasklookupvalue ge_balance_negative_inverse_necessary_sourcerightvaluemasklookupvalue. (((((dc_value_inverse_necessary_sourcerightvaluemask) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemasklookupvaluedecode. (((dc_value_inverse_necessary_sourcerightvaluemask) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemasklookupvalue) = S ge_signed_half_inverse_necessary_sourcerightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightvaluemasklookup) + ge_balance_negative_inverse_necessary_sourcerightvaluemasklookupvalue = (dst_negative_inverse_necessary_sourcerightvaluemasklookup) + ge_balance_positive_inverse_necessary_sourcerightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_necessary_sourcerightvaluemask)=0)) /\ (exists dc_quotient_inverse_necessary_sourcerightvaluemaskentry dc_left_inverse_necessary_sourcerightvaluemaskentry dc_right_inverse_necessary_sourcerightvaluemaskentry. (((dc_input_inverse_necessary_sourceright)=(dc_index_inverse_necessary_sourcerightvaluemask)*dc_quotient_inverse_necessary_sourcerightvaluemaskentry) /\ (((exists dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft dst_positive_inverse_necessary_sourcerightvaluemaskentryleft dst_negative_inverse_necessary_sourcerightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryleftpositive. ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryleftpositive + S (dst_positive_inverse_necessary_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryleftpositive. dst_positive_code_inverse_necessary_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryleftpositive * S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_positive_inverse_necessary_sourcerightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryleftnegative. ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryleftnegative + S (dst_negative_inverse_necessary_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryleftnegative. dst_negative_code_inverse_necessary_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryleftnegative * S ((S (dc_index_inverse_necessary_sourcerightvaluemask)) * dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryleft) + (dst_negative_inverse_necessary_sourcerightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryleftvalue ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryleftvalue. (((((dc_left_inverse_necessary_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryleftvaluedecode. (((dc_left_inverse_necessary_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryleftvalue) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightvaluemaskentryleft) + ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryleftvalue = (dst_negative_inverse_necessary_sourcerightvaluemaskentryleft) + ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright dst_positive_inverse_necessary_sourcerightvaluemaskentryright dst_negative_inverse_necessary_sourcerightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryrightpositive. ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryrightpositive + S (dst_positive_inverse_necessary_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_necessary_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryrightpositive. dst_positive_code_inverse_necessary_sourcerightvaluemaskentryright = ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_necessary_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_positive_inverse_necessary_sourcerightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryrightnegative. ff_h_pvs_inverse_necessary_sourcerightvaluemaskentryrightnegative + S (dst_negative_inverse_necessary_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_necessary_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryrightnegative. dst_negative_code_inverse_necessary_sourcerightvaluemaskentryright = ff_q_pvs_inverse_necessary_sourcerightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_necessary_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_necessary_sourcerightvaluemaskentryright) + (dst_negative_inverse_necessary_sourcerightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryrightvalue ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryrightvalue. (((((dc_right_inverse_necessary_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryrightvaluedecode. (((dc_right_inverse_necessary_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryrightvalue) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_necessary_sourcerightvaluemaskentryright) + ge_balance_negative_inverse_necessary_sourcerightvaluemaskentryrightvalue = (dst_negative_inverse_necessary_sourcerightvaluemaskentryright) + ge_balance_positive_inverse_necessary_sourcerightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct sto_an_inverse_necessary_sourcerightvaluemaskentryproduct sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct sto_cp_inverse_necessary_sourcerightvaluemaskentryproduct sto_cn_inverse_necessary_sourcerightvaluemaskentryproduct. (((((dc_left_inverse_necessary_sourcerightvaluemaskentry) = 2 * (sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct) /\ (sto_an_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductleft. (((dc_left_inverse_necessary_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_necessary_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_necessary_sourcerightvaluemaskentry) = 2 * (sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct) /\ (sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductright. (((dc_right_inverse_necessary_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_necessary_sourcerightvaluemask) = 2 * (sto_cp_inverse_necessary_sourcerightvaluemaskentryproduct) /\ (sto_cn_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductoutput. (((dc_value_inverse_necessary_sourcerightvaluemask) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_necessary_sourcerightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_necessary_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_necessary_sourcerightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct * sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct + sto_an_inverse_necessary_sourcerightvaluemaskentryproduct * sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct) + sto_cn_inverse_necessary_sourcerightvaluemaskentryproduct = (sto_ap_inverse_necessary_sourcerightvaluemaskentryproduct * sto_bn_inverse_necessary_sourcerightvaluemaskentryproduct + sto_an_inverse_necessary_sourcerightvaluemaskentryproduct * sto_bp_inverse_necessary_sourcerightvaluemaskentryproduct) + sto_cp_inverse_necessary_sourcerightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_necessary_sourcerightvaluemask)=0 \/ ~(exists pvs_factor_inverse_necessary_sourcerightvaluemaskentrynondivisor. (dc_input_inverse_necessary_sourceright) = (dc_index_inverse_necessary_sourcerightvaluemask) * pvs_factor_inverse_necessary_sourcerightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_necessary_sourcerightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_necessary_sourcerightvaluefold dst_positive_scale_inverse_necessary_sourcerightvaluefold dst_negative_code_inverse_necessary_sourcerightvaluefold dst_negative_scale_inverse_necessary_sourcerightvaluefold dst_positive_sum_inverse_necessary_sourcerightvaluefold dst_negative_sum_inverse_necessary_sourcerightvaluefold. (((dc_mask_inverse_necessary_sourcerightvalue) = (((((dst_positive_code_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold))) + (((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)))) * S ((((dst_positive_code_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_positive_code_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_positive_scale_inverse_necessary_sourcerightvaluefold) + (dst_positive_scale_inverse_necessary_sourcerightvaluefold))) + (((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)))) + ((((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold))) + (((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) * S ((dst_negative_code_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)) + ((dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (dst_negative_scale_inverse_necessary_sourcerightvaluefold)))))) /\ (((exists fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive. ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_start. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_start. fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_terminal. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_necessary_sourcerightvaluefold) = S ((S (S (dc_input_inverse_necessary_sourceright))) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_terminal. fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_necessary_sourceright))) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive) + (dst_positive_sum_inverse_necessary_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps = S (dc_input_inverse_necessary_sourceright)) -> exists fs_a_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps fs_r_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps fs_s_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_necessary_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_necessary_sourcerightvaluefold = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_necessary_sourcerightvaluefold) + (fs_a_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive) + (fs_r_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_necessary_sourcerightvaluefoldpositive = fs_q_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldpositive) + (fs_s_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps = fs_r_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps + fs_a_dst_inverse_necessary_sourcerightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative. ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_start. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_start. fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_terminal. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_necessary_sourcerightvaluefold) = S ((S (S (dc_input_inverse_necessary_sourceright))) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_terminal. fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_necessary_sourceright))) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative) + (dst_negative_sum_inverse_necessary_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps = S (dc_input_inverse_necessary_sourceright)) -> exists fs_a_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps fs_r_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps fs_s_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_necessary_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_necessary_sourcerightvaluefold = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_necessary_sourcerightvaluefold) + (fs_a_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative) + (fs_r_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_necessary_sourcerightvaluefoldnegative = fs_q_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_necessary_sourcerightvaluefoldnegative) + (fs_s_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps = fs_r_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps + fs_a_dst_inverse_necessary_sourcerightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_necessary_sourcerightvaluefoldresult ge_balance_negative_inverse_necessary_sourcerightvaluefoldresult. (((((dc_output_inverse_necessary_sourceright) = 2 * (ge_balance_positive_inverse_necessary_sourcerightvaluefoldresult) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_necessary_sourcerightvaluefoldresultdecode. (((dc_output_inverse_necessary_sourceright) = 2 * ge_signed_half_inverse_necessary_sourcerightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_necessary_sourcerightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_necessary_sourcerightvaluefoldresult) = S ge_signed_half_inverse_necessary_sourcerightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_necessary_sourcerightvaluefold) + ge_balance_negative_inverse_necessary_sourcerightvaluefoldresult = (dst_negative_sum_inverse_necessary_sourcerightvaluefold) + ge_balance_positive_inverse_necessary_sourcerightvaluefoldresult)))))))))))))))))))))))) -> ~(N=0) -> ((exists dst_positive_code_inverse_necessary_resultpositive dst_positive_scale_inverse_necessary_resultpositive dst_negative_code_inverse_necessary_resultpositive dst_negative_scale_inverse_necessary_resultpositive dst_positive_inverse_necessary_resultpositive dst_negative_inverse_necessary_resultpositive. (((F) = (((((dst_positive_code_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive)) * S ((dst_positive_code_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive)) + ((dst_positive_scale_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive))) + (((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) * S ((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) + ((dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)))) * S ((((dst_positive_code_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive)) * S ((dst_positive_code_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive)) + ((dst_positive_scale_inverse_necessary_resultpositive) + (dst_positive_scale_inverse_necessary_resultpositive))) + (((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) * S ((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) + ((dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)))) + ((((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) * S ((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) + ((dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive))) + (((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) * S ((dst_negative_code_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)) + ((dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_scale_inverse_necessary_resultpositive)))))) /\ (((((exists ff_h_pvs_inverse_necessary_resultpositivepositive. ff_h_pvs_inverse_necessary_resultpositivepositive + S (dst_positive_inverse_necessary_resultpositive) = S ((S (1)) * dst_positive_scale_inverse_necessary_resultpositive)) /\ exists ff_q_pvs_inverse_necessary_resultpositivepositive. dst_positive_code_inverse_necessary_resultpositive = ff_q_pvs_inverse_necessary_resultpositivepositive * S ((S (1)) * dst_positive_scale_inverse_necessary_resultpositive) + (dst_positive_inverse_necessary_resultpositive))) /\ (((((exists ff_h_pvs_inverse_necessary_resultpositivenegative. ff_h_pvs_inverse_necessary_resultpositivenegative + S (dst_negative_inverse_necessary_resultpositive) = S ((S (1)) * dst_negative_scale_inverse_necessary_resultpositive)) /\ exists ff_q_pvs_inverse_necessary_resultpositivenegative. dst_negative_code_inverse_necessary_resultpositive = ff_q_pvs_inverse_necessary_resultpositivenegative * S ((S (1)) * dst_negative_scale_inverse_necessary_resultpositive) + (dst_negative_inverse_necessary_resultpositive))) /\ (exists ge_balance_positive_inverse_necessary_resultpositivevalue ge_balance_negative_inverse_necessary_resultpositivevalue. (((((2) = 2 * (ge_balance_positive_inverse_necessary_resultpositivevalue) /\ (ge_balance_negative_inverse_necessary_resultpositivevalue) = 0) \/ exists ge_signed_half_inverse_necessary_resultpositivevaluedecode. (((2) = 2 * ge_signed_half_inverse_necessary_resultpositivevaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_resultpositivevalue) = 0) /\ (ge_balance_negative_inverse_necessary_resultpositivevalue) = S ge_signed_half_inverse_necessary_resultpositivevaluedecode))) /\ ((dst_positive_inverse_necessary_resultpositive) + ge_balance_negative_inverse_necessary_resultpositivevalue = (dst_negative_inverse_necessary_resultpositive) + ge_balance_positive_inverse_necessary_resultpositivevalue))))))))) \/ (exists dst_positive_code_inverse_necessary_resultnegative dst_positive_scale_inverse_necessary_resultnegative dst_negative_code_inverse_necessary_resultnegative dst_negative_scale_inverse_necessary_resultnegative dst_positive_inverse_necessary_resultnegative dst_negative_inverse_necessary_resultnegative. (((F) = (((((dst_positive_code_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative)) * S ((dst_positive_code_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative)) + ((dst_positive_scale_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative))) + (((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) * S ((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) + ((dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)))) * S ((((dst_positive_code_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative)) * S ((dst_positive_code_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative)) + ((dst_positive_scale_inverse_necessary_resultnegative) + (dst_positive_scale_inverse_necessary_resultnegative))) + (((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) * S ((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) + ((dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)))) + ((((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) * S ((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) + ((dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative))) + (((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) * S ((dst_negative_code_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)) + ((dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_scale_inverse_necessary_resultnegative)))))) /\ (((((exists ff_h_pvs_inverse_necessary_resultnegativepositive. ff_h_pvs_inverse_necessary_resultnegativepositive + S (dst_positive_inverse_necessary_resultnegative) = S ((S (1)) * dst_positive_scale_inverse_necessary_resultnegative)) /\ exists ff_q_pvs_inverse_necessary_resultnegativepositive. dst_positive_code_inverse_necessary_resultnegative = ff_q_pvs_inverse_necessary_resultnegativepositive * S ((S (1)) * dst_positive_scale_inverse_necessary_resultnegative) + (dst_positive_inverse_necessary_resultnegative))) /\ (((((exists ff_h_pvs_inverse_necessary_resultnegativenegative. ff_h_pvs_inverse_necessary_resultnegativenegative + S (dst_negative_inverse_necessary_resultnegative) = S ((S (1)) * dst_negative_scale_inverse_necessary_resultnegative)) /\ exists ff_q_pvs_inverse_necessary_resultnegativenegative. dst_negative_code_inverse_necessary_resultnegative = ff_q_pvs_inverse_necessary_resultnegativenegative * S ((S (1)) * dst_negative_scale_inverse_necessary_resultnegative) + (dst_negative_inverse_necessary_resultnegative))) /\ (exists ge_balance_positive_inverse_necessary_resultnegativevalue ge_balance_negative_inverse_necessary_resultnegativevalue. (((((1) = 2 * (ge_balance_positive_inverse_necessary_resultnegativevalue) /\ (ge_balance_negative_inverse_necessary_resultnegativevalue) = 0) \/ exists ge_signed_half_inverse_necessary_resultnegativevaluedecode. (((1) = 2 * ge_signed_half_inverse_necessary_resultnegativevaluedecode + 1 /\ (ge_balance_positive_inverse_necessary_resultnegativevalue) = 0) /\ (ge_balance_negative_inverse_necessary_resultnegativevalue) = S ge_signed_half_inverse_necessary_resultnegativevaluedecode))) /\ ((dst_positive_inverse_necessary_resultnegative) + ge_balance_negative_inverse_necessary_resultnegativevalue = (dst_negative_inverse_necessary_resultnegative) + ge_balance_positive_inverse_necessary_resultnegativevalue))))))))))Complete tactic proof in conservative notation
All 87 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
87 script commands · 19 reading checkpoints · 9 local claims
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
Named ingredients (1)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–11
03Establish hboundL12–15
04Establish haL16–22
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
- L16
have ha : ∃ a. ArithAt(F,1,a)Definitions: ArithAt(F,1,a)Original native command in the exact edition - L17
specialize divisor_signed_table_lookup (N) - L18
specialize divisor_signed_table_lookup (F) - L19
specialize divisor_signed_table_lookup (1) - L20
apply divisor_signed_table_lookup - L21
exact hi_witness_right_left_left - L22
exact hbound
05Separate the logical casesL23–23
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L23
cases ha
06Establish hbL24–30
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
- L24
have hb : ∃ a. ArithAt(G,1,a)Definitions: ArithAt(G,1,a)Original native command in the exact edition - L25
specialize divisor_signed_table_lookup (N) - L26
specialize divisor_signed_table_lookup (G) - L27
specialize divisor_signed_table_lookup (1) - L28
apply divisor_signed_table_lookup - L29
exact hi_witness_right_left_right_left - L30
exact hbound
07Separate the logical casesL31–31
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L31
cases hb
08Establish heL32–38
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor signed table lookup.
- L32
have he : ∃ a. ArithAt(x,1,a)Definitions: ArithAt(x,1,a)Original native command in the exact edition - L33
specialize divisor_signed_table_lookup (N) - L34
specialize divisor_signed_table_lookup (x) - L35
specialize divisor_signed_table_lookup (1) - L36
apply divisor_signed_table_lookup - L37
exact hi_witness_right_left_right_right_left - L38
exact hbound
09Separate the logical casesL39–39
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L39
cases he
10Establish heqL40–49
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet kronecker delta table one value.
- L40
have heq : x3=2 - L41
specialize dirichlet_kronecker_delta_table_one_value (N) - L42
specialize dirichlet_kronecker_delta_table_one_value (x) - L43
specialize dirichlet_kronecker_delta_table_one_value (x3) - L44
apply dirichlet_kronecker_delta_table_one_value - L45
exact hi_witness_left - L46
exact hbound - L47
exact he_witness - L48
rewrite heq at he_witness - L49
rewrite heq at he_witness
11Establish hcL50–58
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hi witness right left right right right.
- L50
have hc : DirichletSum(F,G,1,2)Definitions: DirichletSum(F,G,1,2)Original native command in the exact edition - L51
specialize hi_witness_right_left_right_right_right (1) - L52
specialize hi_witness_right_left_right_right_right (2) - L53
apply hi_witness_right_left_right_right_right - L54
intro hz - L55
apply PA1 - L56
exact hz - L57
exact hbound - L58
exact he_witness
12Establish hiffL59–67
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet convolution at one iff.
- L59
have hiff : (DirichletSum(F,G,1,2) → SignedMul(x1,x2,2)) ∧ (SignedMul(x1,x2,2) → DirichletSum(F,G,1,2))Definitions: DirichletSum(F,G,1,2)SignedMul(x1,x2,2)Original native command in the exact edition - L60
specialize dirichlet_convolution_at_one_iff (F) - L61
specialize dirichlet_convolution_at_one_iff (G) - L62
specialize dirichlet_convolution_at_one_iff (x1) - L63
specialize dirichlet_convolution_at_one_iff (x2) - L64
specialize dirichlet_convolution_at_one_iff (2) - L65
apply dirichlet_convolution_at_one_iff - L66
exact ha_witness - L67
exact hb_witness
13Separate the logical casesL68–68
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L68
cases hiff
14Establish hpL69–71
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hiff left.
- L69
have hp : SignedMul(x1,x2,2)Definitions: SignedMul(x1,x2,2)Original native command in the exact edition - L70
apply hiff_left - L71
exact hc
15Establish huL72–80
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet signed unit product classification.
- L72
have hu : (x1=2 /\ x2=2) \/ (x1=1 /\ x2=1) - L73
specialize dirichlet_signed_unit_product_classification (x1) - L74
specialize dirichlet_signed_unit_product_classification (x2) - L75
apply dirichlet_signed_unit_product_classification - L76
exact hp - L77
specialize dirichlet_unit_at_one_from_value (F) - L78
specialize dirichlet_unit_at_one_from_value (x1) - L79
apply dirichlet_unit_at_one_from_value - L80
exact ha_witness
16Separate the logical casesL81–83
17Use earlier factsL84–84
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L84
exact hu_left_left
18Separate the logical casesL85–86
19Use earlier factsL87–87
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L87
exact hu_right_left
Original defined command ledger · 87 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro hi - 0005
intro hn - 0006
cases hi - 0007
cases hi_witness - 0008
cases hi_witness_right - 0009
cases hi_witness_right_left - 0010
cases hi_witness_right_left_right - 0011
cases hi_witness_right_left_right_right - 0012
have hbound : Lt(0,N) - 0013
specialize one_le_of_ne_zero (N) - 0014
apply one_le_of_ne_zero - 0015
exact hn - 0016
have ha : ∃ a. ArithAt(F,1,a) - 0017
specialize divisor_signed_table_lookup (N) - 0018
specialize divisor_signed_table_lookup (F) - 0019
specialize divisor_signed_table_lookup (1) - 0020
apply divisor_signed_table_lookup - 0021
exact hi_witness_right_left_left - 0022
exact hbound - 0023
cases ha - 0024
have hb : ∃ a. ArithAt(G,1,a) - 0025
specialize divisor_signed_table_lookup (N) - 0026
specialize divisor_signed_table_lookup (G) - 0027
specialize divisor_signed_table_lookup (1) - 0028
apply divisor_signed_table_lookup - 0029
exact hi_witness_right_left_right_left - 0030
exact hbound - 0031
cases hb - 0032
have he : ∃ a. ArithAt(x,1,a) - 0033
specialize divisor_signed_table_lookup (N) - 0034
specialize divisor_signed_table_lookup (x) - 0035
specialize divisor_signed_table_lookup (1) - 0036
apply divisor_signed_table_lookup - 0037
exact hi_witness_right_left_right_right_left - 0038
exact hbound - 0039
cases he - 0040
have heq : x3=2 - 0041
specialize dirichlet_kronecker_delta_table_one_value (N) - 0042
specialize dirichlet_kronecker_delta_table_one_value (x) - 0043
specialize dirichlet_kronecker_delta_table_one_value (x3) - 0044
apply dirichlet_kronecker_delta_table_one_value - 0045
exact hi_witness_left - 0046
exact hbound - 0047
exact he_witness - 0048
rewrite heq at he_witness - 0049
rewrite heq at he_witness - 0050
have hc : DirichletSum(F,G,1,2) - 0051
specialize hi_witness_right_left_right_right_right (1) - 0052
specialize hi_witness_right_left_right_right_right (2) - 0053
apply hi_witness_right_left_right_right_right - 0054
intro hz - 0055
apply PA1 - 0056
exact hz - 0057
exact hbound - 0058
exact he_witness - 0059
have hiff : (DirichletSum(F,G,1,2) → SignedMul(x1,x2,2)) ∧ (SignedMul(x1,x2,2) → DirichletSum(F,G,1,2)) - 0060
specialize dirichlet_convolution_at_one_iff (F) - 0061
specialize dirichlet_convolution_at_one_iff (G) - 0062
specialize dirichlet_convolution_at_one_iff (x1) - 0063
specialize dirichlet_convolution_at_one_iff (x2) - 0064
specialize dirichlet_convolution_at_one_iff (2) - 0065
apply dirichlet_convolution_at_one_iff - 0066
exact ha_witness - 0067
exact hb_witness - 0068
cases hiff - 0069
have hp : SignedMul(x1,x2,2) - 0070
apply hiff_left - 0071
exact hc - 0072
have hu : (x1=2 /\ x2=2) \/ (x1=1 /\ x2=1) - 0073
specialize dirichlet_signed_unit_product_classification (x1) - 0074
specialize dirichlet_signed_unit_product_classification (x2) - 0075
apply dirichlet_signed_unit_product_classification - 0076
exact hp - 0077
specialize dirichlet_unit_at_one_from_value (F) - 0078
specialize dirichlet_unit_at_one_from_value (x1) - 0079
apply dirichlet_unit_at_one_from_value - 0080
exact ha_witness - 0081
cases hu - 0082
cases hu_left - 0083
left - 0084
exact hu_left_left - 0085
cases hu_right - 0086
right - 0087
exact hu_right_left