dirichlet_inverse_actual_tables

Exact expanded first-order arithmetic statement

forall N F G. (exists di_delta_inverse_tables_source. ((((exists dst_positive_code_inverse_tables_sourcedeltatable dst_positive_scale_inverse_tables_sourcedeltatable dst_negative_code_inverse_tables_sourcedeltatable dst_negative_scale_inverse_tables_sourcedeltatable. (((di_delta_inverse_tables_source) = (((((dst_positive_code_inverse_tables_sourcedeltatable) + (dst_positive_scale_inverse_tables_sourcedeltatable)) * S ((dst_positive_code_inverse_tables_sourcedeltatable) + (dst_positive_scale_inverse_tables_sourcedeltatable)) + ((dst_positive_scale_inverse_tables_sourcedeltatable) + (dst_positive_scale_inverse_tables_sourcedeltatable))) + (((dst_negative_code_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)) * S ((dst_negative_code_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)) + ((dst_negative_scale_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)))) * S ((((dst_positive_code_inverse_tables_sourcedeltatable) + (dst_positive_scale_inverse_tables_sourcedeltatable)) * S ((dst_positive_code_inverse_tables_sourcedeltatable) + (dst_positive_scale_inverse_tables_sourcedeltatable)) + ((dst_positive_scale_inverse_tables_sourcedeltatable) + (dst_positive_scale_inverse_tables_sourcedeltatable))) + (((dst_negative_code_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)) * S ((dst_negative_code_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)) + ((dst_negative_scale_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)))) + ((((dst_negative_code_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)) * S ((dst_negative_code_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)) + ((dst_negative_scale_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable))) + (((dst_negative_code_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)) * S ((dst_negative_code_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)) + ((dst_negative_scale_inverse_tables_sourcedeltatable) + (dst_negative_scale_inverse_tables_sourcedeltatable)))))) /\ (forall dst_index_inverse_tables_sourcedeltatable. (exists pvs_le_gap_inverse_tables_sourcedeltatabledomain. pvs_le_gap_inverse_tables_sourcedeltatabledomain + (dst_index_inverse_tables_sourcedeltatable) = (N)) -> exists dst_positive_inverse_tables_sourcedeltatable dst_negative_inverse_tables_sourcedeltatable dst_value_inverse_tables_sourcedeltatable. ((((exists ff_h_pvs_inverse_tables_sourcedeltatableentrypositive. ff_h_pvs_inverse_tables_sourcedeltatableentrypositive + S (dst_positive_inverse_tables_sourcedeltatable) = S ((S (dst_index_inverse_tables_sourcedeltatable)) * dst_positive_scale_inverse_tables_sourcedeltatable)) /\ exists ff_q_pvs_inverse_tables_sourcedeltatableentrypositive. dst_positive_code_inverse_tables_sourcedeltatable = ff_q_pvs_inverse_tables_sourcedeltatableentrypositive * S ((S (dst_index_inverse_tables_sourcedeltatable)) * dst_positive_scale_inverse_tables_sourcedeltatable) + (dst_positive_inverse_tables_sourcedeltatable))) /\ (((((exists ff_h_pvs_inverse_tables_sourcedeltatableentrynegative. ff_h_pvs_inverse_tables_sourcedeltatableentrynegative + S (dst_negative_inverse_tables_sourcedeltatable) = S ((S (dst_index_inverse_tables_sourcedeltatable)) * dst_negative_scale_inverse_tables_sourcedeltatable)) /\ exists ff_q_pvs_inverse_tables_sourcedeltatableentrynegative. dst_negative_code_inverse_tables_sourcedeltatable = ff_q_pvs_inverse_tables_sourcedeltatableentrynegative * S ((S (dst_index_inverse_tables_sourcedeltatable)) * dst_negative_scale_inverse_tables_sourcedeltatable) + (dst_negative_inverse_tables_sourcedeltatable))) /\ (exists ge_balance_positive_inverse_tables_sourcedeltatableentryvalue ge_balance_negative_inverse_tables_sourcedeltatableentryvalue. (((((dst_value_inverse_tables_sourcedeltatable) = 2 * (ge_balance_positive_inverse_tables_sourcedeltatableentryvalue) /\ (ge_balance_negative_inverse_tables_sourcedeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcedeltatableentryvaluedecode. (((dst_value_inverse_tables_sourcedeltatable) = 2 * ge_signed_half_inverse_tables_sourcedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcedeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcedeltatableentryvalue) = S ge_signed_half_inverse_tables_sourcedeltatableentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourcedeltatable) + ge_balance_negative_inverse_tables_sourcedeltatableentryvalue = (dst_negative_inverse_tables_sourcedeltatable) + ge_balance_positive_inverse_tables_sourcedeltatableentryvalue))))))))) /\ (forall du_index_inverse_tables_sourcedelta du_value_inverse_tables_sourcedelta. ~(du_index_inverse_tables_sourcedelta=0) -> (exists pvs_le_gap_inverse_tables_sourcedeltabound. pvs_le_gap_inverse_tables_sourcedeltabound + (du_index_inverse_tables_sourcedelta) = (N)) -> (exists dst_positive_code_inverse_tables_sourcedeltaentry dst_positive_scale_inverse_tables_sourcedeltaentry dst_negative_code_inverse_tables_sourcedeltaentry dst_negative_scale_inverse_tables_sourcedeltaentry dst_positive_inverse_tables_sourcedeltaentry dst_negative_inverse_tables_sourcedeltaentry. (((di_delta_inverse_tables_source) = (((((dst_positive_code_inverse_tables_sourcedeltaentry) + (dst_positive_scale_inverse_tables_sourcedeltaentry)) * S ((dst_positive_code_inverse_tables_sourcedeltaentry) + (dst_positive_scale_inverse_tables_sourcedeltaentry)) + ((dst_positive_scale_inverse_tables_sourcedeltaentry) + (dst_positive_scale_inverse_tables_sourcedeltaentry))) + (((dst_negative_code_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)) * S ((dst_negative_code_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)) + ((dst_negative_scale_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)))) * S ((((dst_positive_code_inverse_tables_sourcedeltaentry) + (dst_positive_scale_inverse_tables_sourcedeltaentry)) * S ((dst_positive_code_inverse_tables_sourcedeltaentry) + (dst_positive_scale_inverse_tables_sourcedeltaentry)) + ((dst_positive_scale_inverse_tables_sourcedeltaentry) + (dst_positive_scale_inverse_tables_sourcedeltaentry))) + (((dst_negative_code_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)) * S ((dst_negative_code_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)) + ((dst_negative_scale_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)))) + ((((dst_negative_code_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)) * S ((dst_negative_code_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)) + ((dst_negative_scale_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry))) + (((dst_negative_code_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)) * S ((dst_negative_code_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)) + ((dst_negative_scale_inverse_tables_sourcedeltaentry) + (dst_negative_scale_inverse_tables_sourcedeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourcedeltaentrypositive. ff_h_pvs_inverse_tables_sourcedeltaentrypositive + S (dst_positive_inverse_tables_sourcedeltaentry) = S ((S (du_index_inverse_tables_sourcedelta)) * dst_positive_scale_inverse_tables_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_tables_sourcedeltaentrypositive. dst_positive_code_inverse_tables_sourcedeltaentry = ff_q_pvs_inverse_tables_sourcedeltaentrypositive * S ((S (du_index_inverse_tables_sourcedelta)) * dst_positive_scale_inverse_tables_sourcedeltaentry) + (dst_positive_inverse_tables_sourcedeltaentry))) /\ (((((exists ff_h_pvs_inverse_tables_sourcedeltaentrynegative. ff_h_pvs_inverse_tables_sourcedeltaentrynegative + S (dst_negative_inverse_tables_sourcedeltaentry) = S ((S (du_index_inverse_tables_sourcedelta)) * dst_negative_scale_inverse_tables_sourcedeltaentry)) /\ exists ff_q_pvs_inverse_tables_sourcedeltaentrynegative. dst_negative_code_inverse_tables_sourcedeltaentry = ff_q_pvs_inverse_tables_sourcedeltaentrynegative * S ((S (du_index_inverse_tables_sourcedelta)) * dst_negative_scale_inverse_tables_sourcedeltaentry) + (dst_negative_inverse_tables_sourcedeltaentry))) /\ (exists ge_balance_positive_inverse_tables_sourcedeltaentryvalue ge_balance_negative_inverse_tables_sourcedeltaentryvalue. (((((du_value_inverse_tables_sourcedelta) = 2 * (ge_balance_positive_inverse_tables_sourcedeltaentryvalue) /\ (ge_balance_negative_inverse_tables_sourcedeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcedeltaentryvaluedecode. (((du_value_inverse_tables_sourcedelta) = 2 * ge_signed_half_inverse_tables_sourcedeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcedeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcedeltaentryvalue) = S ge_signed_half_inverse_tables_sourcedeltaentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourcedeltaentry) + ge_balance_negative_inverse_tables_sourcedeltaentryvalue = (dst_negative_inverse_tables_sourcedeltaentry) + ge_balance_positive_inverse_tables_sourcedeltaentryvalue))))))))) -> ((((du_index_inverse_tables_sourcedelta)=1 -> (du_value_inverse_tables_sourcedelta)=2) /\ (~((du_index_inverse_tables_sourcedelta)=1) -> (du_value_inverse_tables_sourcedelta)=0)))))) /\ (((((exists dst_positive_code_inverse_tables_sourceleftleft dst_positive_scale_inverse_tables_sourceleftleft dst_negative_code_inverse_tables_sourceleftleft dst_negative_scale_inverse_tables_sourceleftleft. (((F) = (((((dst_positive_code_inverse_tables_sourceleftleft) + (dst_positive_scale_inverse_tables_sourceleftleft)) * S ((dst_positive_code_inverse_tables_sourceleftleft) + (dst_positive_scale_inverse_tables_sourceleftleft)) + ((dst_positive_scale_inverse_tables_sourceleftleft) + (dst_positive_scale_inverse_tables_sourceleftleft))) + (((dst_negative_code_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)) * S ((dst_negative_code_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)) + ((dst_negative_scale_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)))) * S ((((dst_positive_code_inverse_tables_sourceleftleft) + (dst_positive_scale_inverse_tables_sourceleftleft)) * S ((dst_positive_code_inverse_tables_sourceleftleft) + (dst_positive_scale_inverse_tables_sourceleftleft)) + ((dst_positive_scale_inverse_tables_sourceleftleft) + (dst_positive_scale_inverse_tables_sourceleftleft))) + (((dst_negative_code_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)) * S ((dst_negative_code_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)) + ((dst_negative_scale_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)))) + ((((dst_negative_code_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)) * S ((dst_negative_code_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)) + ((dst_negative_scale_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft))) + (((dst_negative_code_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)) * S ((dst_negative_code_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)) + ((dst_negative_scale_inverse_tables_sourceleftleft) + (dst_negative_scale_inverse_tables_sourceleftleft)))))) /\ (forall dst_index_inverse_tables_sourceleftleft. (exists pvs_le_gap_inverse_tables_sourceleftleftdomain. pvs_le_gap_inverse_tables_sourceleftleftdomain + (dst_index_inverse_tables_sourceleftleft) = (N)) -> exists dst_positive_inverse_tables_sourceleftleft dst_negative_inverse_tables_sourceleftleft dst_value_inverse_tables_sourceleftleft. ((((exists ff_h_pvs_inverse_tables_sourceleftleftentrypositive. ff_h_pvs_inverse_tables_sourceleftleftentrypositive + S (dst_positive_inverse_tables_sourceleftleft) = S ((S (dst_index_inverse_tables_sourceleftleft)) * dst_positive_scale_inverse_tables_sourceleftleft)) /\ exists ff_q_pvs_inverse_tables_sourceleftleftentrypositive. dst_positive_code_inverse_tables_sourceleftleft = ff_q_pvs_inverse_tables_sourceleftleftentrypositive * S ((S (dst_index_inverse_tables_sourceleftleft)) * dst_positive_scale_inverse_tables_sourceleftleft) + (dst_positive_inverse_tables_sourceleftleft))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftleftentrynegative. ff_h_pvs_inverse_tables_sourceleftleftentrynegative + S (dst_negative_inverse_tables_sourceleftleft) = S ((S (dst_index_inverse_tables_sourceleftleft)) * dst_negative_scale_inverse_tables_sourceleftleft)) /\ exists ff_q_pvs_inverse_tables_sourceleftleftentrynegative. dst_negative_code_inverse_tables_sourceleftleft = ff_q_pvs_inverse_tables_sourceleftleftentrynegative * S ((S (dst_index_inverse_tables_sourceleftleft)) * dst_negative_scale_inverse_tables_sourceleftleft) + (dst_negative_inverse_tables_sourceleftleft))) /\ (exists ge_balance_positive_inverse_tables_sourceleftleftentryvalue ge_balance_negative_inverse_tables_sourceleftleftentryvalue. (((((dst_value_inverse_tables_sourceleftleft) = 2 * (ge_balance_positive_inverse_tables_sourceleftleftentryvalue) /\ (ge_balance_negative_inverse_tables_sourceleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftleftentryvaluedecode. (((dst_value_inverse_tables_sourceleftleft) = 2 * ge_signed_half_inverse_tables_sourceleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourceleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourceleftleftentryvalue) = S ge_signed_half_inverse_tables_sourceleftleftentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourceleftleft) + ge_balance_negative_inverse_tables_sourceleftleftentryvalue = (dst_negative_inverse_tables_sourceleftleft) + ge_balance_positive_inverse_tables_sourceleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_tables_sourceleftright dst_positive_scale_inverse_tables_sourceleftright dst_negative_code_inverse_tables_sourceleftright dst_negative_scale_inverse_tables_sourceleftright. (((G) = (((((dst_positive_code_inverse_tables_sourceleftright) + (dst_positive_scale_inverse_tables_sourceleftright)) * S ((dst_positive_code_inverse_tables_sourceleftright) + (dst_positive_scale_inverse_tables_sourceleftright)) + ((dst_positive_scale_inverse_tables_sourceleftright) + (dst_positive_scale_inverse_tables_sourceleftright))) + (((dst_negative_code_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)) * S ((dst_negative_code_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)) + ((dst_negative_scale_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)))) * S ((((dst_positive_code_inverse_tables_sourceleftright) + (dst_positive_scale_inverse_tables_sourceleftright)) * S ((dst_positive_code_inverse_tables_sourceleftright) + (dst_positive_scale_inverse_tables_sourceleftright)) + ((dst_positive_scale_inverse_tables_sourceleftright) + (dst_positive_scale_inverse_tables_sourceleftright))) + (((dst_negative_code_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)) * S ((dst_negative_code_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)) + ((dst_negative_scale_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)))) + ((((dst_negative_code_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)) * S ((dst_negative_code_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)) + ((dst_negative_scale_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright))) + (((dst_negative_code_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)) * S ((dst_negative_code_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)) + ((dst_negative_scale_inverse_tables_sourceleftright) + (dst_negative_scale_inverse_tables_sourceleftright)))))) /\ (forall dst_index_inverse_tables_sourceleftright. (exists pvs_le_gap_inverse_tables_sourceleftrightdomain. pvs_le_gap_inverse_tables_sourceleftrightdomain + (dst_index_inverse_tables_sourceleftright) = (N)) -> exists dst_positive_inverse_tables_sourceleftright dst_negative_inverse_tables_sourceleftright dst_value_inverse_tables_sourceleftright. ((((exists ff_h_pvs_inverse_tables_sourceleftrightentrypositive. ff_h_pvs_inverse_tables_sourceleftrightentrypositive + S (dst_positive_inverse_tables_sourceleftright) = S ((S (dst_index_inverse_tables_sourceleftright)) * dst_positive_scale_inverse_tables_sourceleftright)) /\ exists ff_q_pvs_inverse_tables_sourceleftrightentrypositive. dst_positive_code_inverse_tables_sourceleftright = ff_q_pvs_inverse_tables_sourceleftrightentrypositive * S ((S (dst_index_inverse_tables_sourceleftright)) * dst_positive_scale_inverse_tables_sourceleftright) + (dst_positive_inverse_tables_sourceleftright))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftrightentrynegative. ff_h_pvs_inverse_tables_sourceleftrightentrynegative + S (dst_negative_inverse_tables_sourceleftright) = S ((S (dst_index_inverse_tables_sourceleftright)) * dst_negative_scale_inverse_tables_sourceleftright)) /\ exists ff_q_pvs_inverse_tables_sourceleftrightentrynegative. dst_negative_code_inverse_tables_sourceleftright = ff_q_pvs_inverse_tables_sourceleftrightentrynegative * S ((S (dst_index_inverse_tables_sourceleftright)) * dst_negative_scale_inverse_tables_sourceleftright) + (dst_negative_inverse_tables_sourceleftright))) /\ (exists ge_balance_positive_inverse_tables_sourceleftrightentryvalue ge_balance_negative_inverse_tables_sourceleftrightentryvalue. (((((dst_value_inverse_tables_sourceleftright) = 2 * (ge_balance_positive_inverse_tables_sourceleftrightentryvalue) /\ (ge_balance_negative_inverse_tables_sourceleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftrightentryvaluedecode. (((dst_value_inverse_tables_sourceleftright) = 2 * ge_signed_half_inverse_tables_sourceleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourceleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourceleftrightentryvalue) = S ge_signed_half_inverse_tables_sourceleftrightentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourceleftright) + ge_balance_negative_inverse_tables_sourceleftrightentryvalue = (dst_negative_inverse_tables_sourceleftright) + ge_balance_positive_inverse_tables_sourceleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_tables_sourcelefttable dst_positive_scale_inverse_tables_sourcelefttable dst_negative_code_inverse_tables_sourcelefttable dst_negative_scale_inverse_tables_sourcelefttable. (((di_delta_inverse_tables_source) = (((((dst_positive_code_inverse_tables_sourcelefttable) + (dst_positive_scale_inverse_tables_sourcelefttable)) * S ((dst_positive_code_inverse_tables_sourcelefttable) + (dst_positive_scale_inverse_tables_sourcelefttable)) + ((dst_positive_scale_inverse_tables_sourcelefttable) + (dst_positive_scale_inverse_tables_sourcelefttable))) + (((dst_negative_code_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)) * S ((dst_negative_code_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)) + ((dst_negative_scale_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)))) * S ((((dst_positive_code_inverse_tables_sourcelefttable) + (dst_positive_scale_inverse_tables_sourcelefttable)) * S ((dst_positive_code_inverse_tables_sourcelefttable) + (dst_positive_scale_inverse_tables_sourcelefttable)) + ((dst_positive_scale_inverse_tables_sourcelefttable) + (dst_positive_scale_inverse_tables_sourcelefttable))) + (((dst_negative_code_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)) * S ((dst_negative_code_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)) + ((dst_negative_scale_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)))) + ((((dst_negative_code_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)) * S ((dst_negative_code_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)) + ((dst_negative_scale_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable))) + (((dst_negative_code_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)) * S ((dst_negative_code_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)) + ((dst_negative_scale_inverse_tables_sourcelefttable) + (dst_negative_scale_inverse_tables_sourcelefttable)))))) /\ (forall dst_index_inverse_tables_sourcelefttable. (exists pvs_le_gap_inverse_tables_sourcelefttabledomain. pvs_le_gap_inverse_tables_sourcelefttabledomain + (dst_index_inverse_tables_sourcelefttable) = (N)) -> exists dst_positive_inverse_tables_sourcelefttable dst_negative_inverse_tables_sourcelefttable dst_value_inverse_tables_sourcelefttable. ((((exists ff_h_pvs_inverse_tables_sourcelefttableentrypositive. ff_h_pvs_inverse_tables_sourcelefttableentrypositive + S (dst_positive_inverse_tables_sourcelefttable) = S ((S (dst_index_inverse_tables_sourcelefttable)) * dst_positive_scale_inverse_tables_sourcelefttable)) /\ exists ff_q_pvs_inverse_tables_sourcelefttableentrypositive. dst_positive_code_inverse_tables_sourcelefttable = ff_q_pvs_inverse_tables_sourcelefttableentrypositive * S ((S (dst_index_inverse_tables_sourcelefttable)) * dst_positive_scale_inverse_tables_sourcelefttable) + (dst_positive_inverse_tables_sourcelefttable))) /\ (((((exists ff_h_pvs_inverse_tables_sourcelefttableentrynegative. ff_h_pvs_inverse_tables_sourcelefttableentrynegative + S (dst_negative_inverse_tables_sourcelefttable) = S ((S (dst_index_inverse_tables_sourcelefttable)) * dst_negative_scale_inverse_tables_sourcelefttable)) /\ exists ff_q_pvs_inverse_tables_sourcelefttableentrynegative. dst_negative_code_inverse_tables_sourcelefttable = ff_q_pvs_inverse_tables_sourcelefttableentrynegative * S ((S (dst_index_inverse_tables_sourcelefttable)) * dst_negative_scale_inverse_tables_sourcelefttable) + (dst_negative_inverse_tables_sourcelefttable))) /\ (exists ge_balance_positive_inverse_tables_sourcelefttableentryvalue ge_balance_negative_inverse_tables_sourcelefttableentryvalue. (((((dst_value_inverse_tables_sourcelefttable) = 2 * (ge_balance_positive_inverse_tables_sourcelefttableentryvalue) /\ (ge_balance_negative_inverse_tables_sourcelefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcelefttableentryvaluedecode. (((dst_value_inverse_tables_sourcelefttable) = 2 * ge_signed_half_inverse_tables_sourcelefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcelefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcelefttableentryvalue) = S ge_signed_half_inverse_tables_sourcelefttableentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourcelefttable) + ge_balance_negative_inverse_tables_sourcelefttableentryvalue = (dst_negative_inverse_tables_sourcelefttable) + ge_balance_positive_inverse_tables_sourcelefttableentryvalue))))))))) /\ (forall dc_input_inverse_tables_sourceleft dc_output_inverse_tables_sourceleft. ~(dc_input_inverse_tables_sourceleft=0) -> (exists pvs_le_gap_inverse_tables_sourceleftdomain. pvs_le_gap_inverse_tables_sourceleftdomain + (dc_input_inverse_tables_sourceleft) = (N)) -> (exists dst_positive_code_inverse_tables_sourceleftlookup dst_positive_scale_inverse_tables_sourceleftlookup dst_negative_code_inverse_tables_sourceleftlookup dst_negative_scale_inverse_tables_sourceleftlookup dst_positive_inverse_tables_sourceleftlookup dst_negative_inverse_tables_sourceleftlookup. (((di_delta_inverse_tables_source) = (((((dst_positive_code_inverse_tables_sourceleftlookup) + (dst_positive_scale_inverse_tables_sourceleftlookup)) * S ((dst_positive_code_inverse_tables_sourceleftlookup) + (dst_positive_scale_inverse_tables_sourceleftlookup)) + ((dst_positive_scale_inverse_tables_sourceleftlookup) + (dst_positive_scale_inverse_tables_sourceleftlookup))) + (((dst_negative_code_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)) * S ((dst_negative_code_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)) + ((dst_negative_scale_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)))) * S ((((dst_positive_code_inverse_tables_sourceleftlookup) + (dst_positive_scale_inverse_tables_sourceleftlookup)) * S ((dst_positive_code_inverse_tables_sourceleftlookup) + (dst_positive_scale_inverse_tables_sourceleftlookup)) + ((dst_positive_scale_inverse_tables_sourceleftlookup) + (dst_positive_scale_inverse_tables_sourceleftlookup))) + (((dst_negative_code_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)) * S ((dst_negative_code_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)) + ((dst_negative_scale_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)))) + ((((dst_negative_code_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)) * S ((dst_negative_code_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)) + ((dst_negative_scale_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup))) + (((dst_negative_code_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)) * S ((dst_negative_code_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)) + ((dst_negative_scale_inverse_tables_sourceleftlookup) + (dst_negative_scale_inverse_tables_sourceleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftlookuppositive. ff_h_pvs_inverse_tables_sourceleftlookuppositive + S (dst_positive_inverse_tables_sourceleftlookup) = S ((S (dc_input_inverse_tables_sourceleft)) * dst_positive_scale_inverse_tables_sourceleftlookup)) /\ exists ff_q_pvs_inverse_tables_sourceleftlookuppositive. dst_positive_code_inverse_tables_sourceleftlookup = ff_q_pvs_inverse_tables_sourceleftlookuppositive * S ((S (dc_input_inverse_tables_sourceleft)) * dst_positive_scale_inverse_tables_sourceleftlookup) + (dst_positive_inverse_tables_sourceleftlookup))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftlookupnegative. ff_h_pvs_inverse_tables_sourceleftlookupnegative + S (dst_negative_inverse_tables_sourceleftlookup) = S ((S (dc_input_inverse_tables_sourceleft)) * dst_negative_scale_inverse_tables_sourceleftlookup)) /\ exists ff_q_pvs_inverse_tables_sourceleftlookupnegative. dst_negative_code_inverse_tables_sourceleftlookup = ff_q_pvs_inverse_tables_sourceleftlookupnegative * S ((S (dc_input_inverse_tables_sourceleft)) * dst_negative_scale_inverse_tables_sourceleftlookup) + (dst_negative_inverse_tables_sourceleftlookup))) /\ (exists ge_balance_positive_inverse_tables_sourceleftlookupvalue ge_balance_negative_inverse_tables_sourceleftlookupvalue. (((((dc_output_inverse_tables_sourceleft) = 2 * (ge_balance_positive_inverse_tables_sourceleftlookupvalue) /\ (ge_balance_negative_inverse_tables_sourceleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftlookupvaluedecode. (((dc_output_inverse_tables_sourceleft) = 2 * ge_signed_half_inverse_tables_sourceleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourceleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourceleftlookupvalue) = S ge_signed_half_inverse_tables_sourceleftlookupvaluedecode))) /\ ((dst_positive_inverse_tables_sourceleftlookup) + ge_balance_negative_inverse_tables_sourceleftlookupvalue = (dst_negative_inverse_tables_sourceleftlookup) + ge_balance_positive_inverse_tables_sourceleftlookupvalue))))))))) -> (((~((dc_input_inverse_tables_sourceleft)=0)) /\ (exists dc_mask_inverse_tables_sourceleftvalue. ((((exists dst_positive_code_inverse_tables_sourceleftvaluemasktable dst_positive_scale_inverse_tables_sourceleftvaluemasktable dst_negative_code_inverse_tables_sourceleftvaluemasktable dst_negative_scale_inverse_tables_sourceleftvaluemasktable. (((dc_mask_inverse_tables_sourceleftvalue) = (((((dst_positive_code_inverse_tables_sourceleftvaluemasktable) + (dst_positive_scale_inverse_tables_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_tables_sourceleftvaluemasktable) + (dst_positive_scale_inverse_tables_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_tables_sourceleftvaluemasktable) + (dst_positive_scale_inverse_tables_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)))) * S ((((dst_positive_code_inverse_tables_sourceleftvaluemasktable) + (dst_positive_scale_inverse_tables_sourceleftvaluemasktable)) * S ((dst_positive_code_inverse_tables_sourceleftvaluemasktable) + (dst_positive_scale_inverse_tables_sourceleftvaluemasktable)) + ((dst_positive_scale_inverse_tables_sourceleftvaluemasktable) + (dst_positive_scale_inverse_tables_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)))) + ((((dst_negative_code_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable))) + (((dst_negative_code_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemasktable) + (dst_negative_scale_inverse_tables_sourceleftvaluemasktable)))))) /\ (forall dst_index_inverse_tables_sourceleftvaluemasktable. (exists pvs_le_gap_inverse_tables_sourceleftvaluemasktabledomain. pvs_le_gap_inverse_tables_sourceleftvaluemasktabledomain + (dst_index_inverse_tables_sourceleftvaluemasktable) = (dc_input_inverse_tables_sourceleft)) -> exists dst_positive_inverse_tables_sourceleftvaluemasktable dst_negative_inverse_tables_sourceleftvaluemasktable dst_value_inverse_tables_sourceleftvaluemasktable. ((((exists ff_h_pvs_inverse_tables_sourceleftvaluemasktableentrypositive. ff_h_pvs_inverse_tables_sourceleftvaluemasktableentrypositive + S (dst_positive_inverse_tables_sourceleftvaluemasktable) = S ((S (dst_index_inverse_tables_sourceleftvaluemasktable)) * dst_positive_scale_inverse_tables_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_tables_sourceleftvaluemasktableentrypositive. dst_positive_code_inverse_tables_sourceleftvaluemasktable = ff_q_pvs_inverse_tables_sourceleftvaluemasktableentrypositive * S ((S (dst_index_inverse_tables_sourceleftvaluemasktable)) * dst_positive_scale_inverse_tables_sourceleftvaluemasktable) + (dst_positive_inverse_tables_sourceleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftvaluemasktableentrynegative. ff_h_pvs_inverse_tables_sourceleftvaluemasktableentrynegative + S (dst_negative_inverse_tables_sourceleftvaluemasktable) = S ((S (dst_index_inverse_tables_sourceleftvaluemasktable)) * dst_negative_scale_inverse_tables_sourceleftvaluemasktable)) /\ exists ff_q_pvs_inverse_tables_sourceleftvaluemasktableentrynegative. dst_negative_code_inverse_tables_sourceleftvaluemasktable = ff_q_pvs_inverse_tables_sourceleftvaluemasktableentrynegative * S ((S (dst_index_inverse_tables_sourceleftvaluemasktable)) * dst_negative_scale_inverse_tables_sourceleftvaluemasktable) + (dst_negative_inverse_tables_sourceleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_tables_sourceleftvaluemasktableentryvalue ge_balance_negative_inverse_tables_sourceleftvaluemasktableentryvalue. (((((dst_value_inverse_tables_sourceleftvaluemasktable) = 2 * (ge_balance_positive_inverse_tables_sourceleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_tables_sourceleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftvaluemasktableentryvaluedecode. (((dst_value_inverse_tables_sourceleftvaluemasktable) = 2 * ge_signed_half_inverse_tables_sourceleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourceleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourceleftvaluemasktableentryvalue) = S ge_signed_half_inverse_tables_sourceleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourceleftvaluemasktable) + ge_balance_negative_inverse_tables_sourceleftvaluemasktableentryvalue = (dst_negative_inverse_tables_sourceleftvaluemasktable) + ge_balance_positive_inverse_tables_sourceleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_tables_sourceleftvaluemask dc_value_inverse_tables_sourceleftvaluemask. (exists pvs_le_gap_inverse_tables_sourceleftvaluemaskdomain. pvs_le_gap_inverse_tables_sourceleftvaluemaskdomain + (dc_index_inverse_tables_sourceleftvaluemask) = (dc_input_inverse_tables_sourceleft)) -> (exists dst_positive_code_inverse_tables_sourceleftvaluemasklookup dst_positive_scale_inverse_tables_sourceleftvaluemasklookup dst_negative_code_inverse_tables_sourceleftvaluemasklookup dst_negative_scale_inverse_tables_sourceleftvaluemasklookup dst_positive_inverse_tables_sourceleftvaluemasklookup dst_negative_inverse_tables_sourceleftvaluemasklookup. (((dc_mask_inverse_tables_sourceleftvalue) = (((((dst_positive_code_inverse_tables_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_tables_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_tables_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_tables_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_tables_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_tables_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_tables_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_tables_sourceleftvaluemasklookup)) * S ((dst_positive_code_inverse_tables_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_tables_sourceleftvaluemasklookup)) + ((dst_positive_scale_inverse_tables_sourceleftvaluemasklookup) + (dst_positive_scale_inverse_tables_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)))) + ((((dst_negative_code_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup))) + (((dst_negative_code_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftvaluemasklookuppositive. ff_h_pvs_inverse_tables_sourceleftvaluemasklookuppositive + S (dst_positive_inverse_tables_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_tables_sourceleftvaluemask)) * dst_positive_scale_inverse_tables_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_tables_sourceleftvaluemasklookuppositive. dst_positive_code_inverse_tables_sourceleftvaluemasklookup = ff_q_pvs_inverse_tables_sourceleftvaluemasklookuppositive * S ((S (dc_index_inverse_tables_sourceleftvaluemask)) * dst_positive_scale_inverse_tables_sourceleftvaluemasklookup) + (dst_positive_inverse_tables_sourceleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftvaluemasklookupnegative. ff_h_pvs_inverse_tables_sourceleftvaluemasklookupnegative + S (dst_negative_inverse_tables_sourceleftvaluemasklookup) = S ((S (dc_index_inverse_tables_sourceleftvaluemask)) * dst_negative_scale_inverse_tables_sourceleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_tables_sourceleftvaluemasklookupnegative. dst_negative_code_inverse_tables_sourceleftvaluemasklookup = ff_q_pvs_inverse_tables_sourceleftvaluemasklookupnegative * S ((S (dc_index_inverse_tables_sourceleftvaluemask)) * dst_negative_scale_inverse_tables_sourceleftvaluemasklookup) + (dst_negative_inverse_tables_sourceleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_tables_sourceleftvaluemasklookupvalue ge_balance_negative_inverse_tables_sourceleftvaluemasklookupvalue. (((((dc_value_inverse_tables_sourceleftvaluemask) = 2 * (ge_balance_positive_inverse_tables_sourceleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_tables_sourceleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftvaluemasklookupvaluedecode. (((dc_value_inverse_tables_sourceleftvaluemask) = 2 * ge_signed_half_inverse_tables_sourceleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourceleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourceleftvaluemasklookupvalue) = S ge_signed_half_inverse_tables_sourceleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_tables_sourceleftvaluemasklookup) + ge_balance_negative_inverse_tables_sourceleftvaluemasklookupvalue = (dst_negative_inverse_tables_sourceleftvaluemasklookup) + ge_balance_positive_inverse_tables_sourceleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_tables_sourceleftvaluemask)=0)) /\ (exists dc_quotient_inverse_tables_sourceleftvaluemaskentry dc_left_inverse_tables_sourceleftvaluemaskentry dc_right_inverse_tables_sourceleftvaluemaskentry. (((dc_input_inverse_tables_sourceleft)=(dc_index_inverse_tables_sourceleftvaluemask)*dc_quotient_inverse_tables_sourceleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_tables_sourceleftvaluemaskentryleft dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft dst_positive_inverse_tables_sourceleftvaluemaskentryleft dst_negative_inverse_tables_sourceleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft))) + (((dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftvaluemaskentryleftpositive. ff_h_pvs_inverse_tables_sourceleftvaluemaskentryleftpositive + S (dst_positive_inverse_tables_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_tables_sourceleftvaluemask)) * dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_tables_sourceleftvaluemaskentryleftpositive. dst_positive_code_inverse_tables_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_tables_sourceleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_tables_sourceleftvaluemask)) * dst_positive_scale_inverse_tables_sourceleftvaluemaskentryleft) + (dst_positive_inverse_tables_sourceleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftvaluemaskentryleftnegative. ff_h_pvs_inverse_tables_sourceleftvaluemaskentryleftnegative + S (dst_negative_inverse_tables_sourceleftvaluemaskentryleft) = S ((S (dc_index_inverse_tables_sourceleftvaluemask)) * dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_tables_sourceleftvaluemaskentryleftnegative. dst_negative_code_inverse_tables_sourceleftvaluemaskentryleft = ff_q_pvs_inverse_tables_sourceleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_tables_sourceleftvaluemask)) * dst_negative_scale_inverse_tables_sourceleftvaluemaskentryleft) + (dst_negative_inverse_tables_sourceleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_tables_sourceleftvaluemaskentryleftvalue ge_balance_negative_inverse_tables_sourceleftvaluemaskentryleftvalue. (((((dc_left_inverse_tables_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_tables_sourceleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_tables_sourceleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_tables_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_tables_sourceleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourceleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourceleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_tables_sourceleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_tables_sourceleftvaluemaskentryleft) + ge_balance_negative_inverse_tables_sourceleftvaluemaskentryleftvalue = (dst_negative_inverse_tables_sourceleftvaluemaskentryleft) + ge_balance_positive_inverse_tables_sourceleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_tables_sourceleftvaluemaskentryright dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright dst_negative_code_inverse_tables_sourceleftvaluemaskentryright dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright dst_positive_inverse_tables_sourceleftvaluemaskentryright dst_negative_inverse_tables_sourceleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright)) * S ((dst_positive_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright)) + ((dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright))) + (((dst_negative_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) * S ((dst_negative_code_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) + ((dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftvaluemaskentryrightpositive. ff_h_pvs_inverse_tables_sourceleftvaluemaskentryrightpositive + S (dst_positive_inverse_tables_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_tables_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_tables_sourceleftvaluemaskentryrightpositive. dst_positive_code_inverse_tables_sourceleftvaluemaskentryright = ff_q_pvs_inverse_tables_sourceleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_tables_sourceleftvaluemaskentry)) * dst_positive_scale_inverse_tables_sourceleftvaluemaskentryright) + (dst_positive_inverse_tables_sourceleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_tables_sourceleftvaluemaskentryrightnegative. ff_h_pvs_inverse_tables_sourceleftvaluemaskentryrightnegative + S (dst_negative_inverse_tables_sourceleftvaluemaskentryright) = S ((S (dc_quotient_inverse_tables_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_tables_sourceleftvaluemaskentryrightnegative. dst_negative_code_inverse_tables_sourceleftvaluemaskentryright = ff_q_pvs_inverse_tables_sourceleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_tables_sourceleftvaluemaskentry)) * dst_negative_scale_inverse_tables_sourceleftvaluemaskentryright) + (dst_negative_inverse_tables_sourceleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_tables_sourceleftvaluemaskentryrightvalue ge_balance_negative_inverse_tables_sourceleftvaluemaskentryrightvalue. (((((dc_right_inverse_tables_sourceleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_tables_sourceleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_tables_sourceleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_tables_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_tables_sourceleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourceleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourceleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_tables_sourceleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_tables_sourceleftvaluemaskentryright) + ge_balance_negative_inverse_tables_sourceleftvaluemaskentryrightvalue = (dst_negative_inverse_tables_sourceleftvaluemaskentryright) + ge_balance_positive_inverse_tables_sourceleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_tables_sourceleftvaluemaskentryproduct sto_an_inverse_tables_sourceleftvaluemaskentryproduct sto_bp_inverse_tables_sourceleftvaluemaskentryproduct sto_bn_inverse_tables_sourceleftvaluemaskentryproduct sto_cp_inverse_tables_sourceleftvaluemaskentryproduct sto_cn_inverse_tables_sourceleftvaluemaskentryproduct. (((((dc_left_inverse_tables_sourceleftvaluemaskentry) = 2 * (sto_ap_inverse_tables_sourceleftvaluemaskentryproduct) /\ (sto_an_inverse_tables_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductleft. (((dc_left_inverse_tables_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_tables_sourceleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_tables_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_tables_sourceleftvaluemaskentry) = 2 * (sto_bp_inverse_tables_sourceleftvaluemaskentryproduct) /\ (sto_bn_inverse_tables_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductright. (((dc_right_inverse_tables_sourceleftvaluemaskentry) = 2 * ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_tables_sourceleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_tables_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_tables_sourceleftvaluemask) = 2 * (sto_cp_inverse_tables_sourceleftvaluemaskentryproduct) /\ (sto_cn_inverse_tables_sourceleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductoutput. (((dc_value_inverse_tables_sourceleftvaluemask) = 2 * ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_tables_sourceleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_tables_sourceleftvaluemaskentryproduct) = S ge_signed_half_inverse_tables_sourceleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_tables_sourceleftvaluemaskentryproduct * sto_bp_inverse_tables_sourceleftvaluemaskentryproduct + sto_an_inverse_tables_sourceleftvaluemaskentryproduct * sto_bn_inverse_tables_sourceleftvaluemaskentryproduct) + sto_cn_inverse_tables_sourceleftvaluemaskentryproduct = (sto_ap_inverse_tables_sourceleftvaluemaskentryproduct * sto_bn_inverse_tables_sourceleftvaluemaskentryproduct + sto_an_inverse_tables_sourceleftvaluemaskentryproduct * sto_bp_inverse_tables_sourceleftvaluemaskentryproduct) + sto_cp_inverse_tables_sourceleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_tables_sourceleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_tables_sourceleftvaluemaskentrynondivisor. (dc_input_inverse_tables_sourceleft) = (dc_index_inverse_tables_sourceleftvaluemask) * pvs_factor_inverse_tables_sourceleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_tables_sourceleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_tables_sourceleftvaluefold dst_positive_scale_inverse_tables_sourceleftvaluefold dst_negative_code_inverse_tables_sourceleftvaluefold dst_negative_scale_inverse_tables_sourceleftvaluefold dst_positive_sum_inverse_tables_sourceleftvaluefold dst_negative_sum_inverse_tables_sourceleftvaluefold. (((dc_mask_inverse_tables_sourceleftvalue) = (((((dst_positive_code_inverse_tables_sourceleftvaluefold) + (dst_positive_scale_inverse_tables_sourceleftvaluefold)) * S ((dst_positive_code_inverse_tables_sourceleftvaluefold) + (dst_positive_scale_inverse_tables_sourceleftvaluefold)) + ((dst_positive_scale_inverse_tables_sourceleftvaluefold) + (dst_positive_scale_inverse_tables_sourceleftvaluefold))) + (((dst_negative_code_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)) * S ((dst_negative_code_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)) + ((dst_negative_scale_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)))) * S ((((dst_positive_code_inverse_tables_sourceleftvaluefold) + (dst_positive_scale_inverse_tables_sourceleftvaluefold)) * S ((dst_positive_code_inverse_tables_sourceleftvaluefold) + (dst_positive_scale_inverse_tables_sourceleftvaluefold)) + ((dst_positive_scale_inverse_tables_sourceleftvaluefold) + (dst_positive_scale_inverse_tables_sourceleftvaluefold))) + (((dst_negative_code_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)) * S ((dst_negative_code_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)) + ((dst_negative_scale_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)))) + ((((dst_negative_code_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)) * S ((dst_negative_code_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)) + ((dst_negative_scale_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold))) + (((dst_negative_code_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)) * S ((dst_negative_code_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)) + ((dst_negative_scale_inverse_tables_sourceleftvaluefold) + (dst_negative_scale_inverse_tables_sourceleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_tables_sourceleftvaluefoldpositive fs_v_dst_inverse_tables_sourceleftvaluefoldpositive. ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_start. fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_tables_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_start. fs_u_dst_inverse_tables_sourceleftvaluefoldpositive = fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_tables_sourceleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_tables_sourceleftvaluefold) = S ((S (S (dc_input_inverse_tables_sourceleft))) * fs_v_dst_inverse_tables_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_tables_sourceleftvaluefoldpositive = fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_tables_sourceleft))) * fs_v_dst_inverse_tables_sourceleftvaluefoldpositive) + (dst_positive_sum_inverse_tables_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps = S (dc_input_inverse_tables_sourceleft)) -> exists fs_a_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps fs_r_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps fs_s_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_tables_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_tables_sourceleftvaluefold = fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_tables_sourceleftvaluefold) + (fs_a_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_tables_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_tables_sourceleftvaluefoldpositive = fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_tables_sourceleftvaluefoldpositive) + (fs_r_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_tables_sourceleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_tables_sourceleftvaluefoldpositive = fs_q_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_tables_sourceleftvaluefoldpositive) + (fs_s_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps = fs_r_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps + fs_a_dst_inverse_tables_sourceleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_tables_sourceleftvaluefoldnegative fs_v_dst_inverse_tables_sourceleftvaluefoldnegative. ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_start. fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_tables_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_start. fs_u_dst_inverse_tables_sourceleftvaluefoldnegative = fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_tables_sourceleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_tables_sourceleftvaluefold) = S ((S (S (dc_input_inverse_tables_sourceleft))) * fs_v_dst_inverse_tables_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_tables_sourceleftvaluefoldnegative = fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_tables_sourceleft))) * fs_v_dst_inverse_tables_sourceleftvaluefoldnegative) + (dst_negative_sum_inverse_tables_sourceleftvaluefold))) /\ forall fs_i_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps = S (dc_input_inverse_tables_sourceleft)) -> exists fs_a_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps fs_r_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps fs_s_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_tables_sourceleftvaluefold)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_tables_sourceleftvaluefold = fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_tables_sourceleftvaluefold) + (fs_a_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_tables_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_tables_sourceleftvaluefoldnegative = fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_tables_sourceleftvaluefoldnegative) + (fs_r_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_tables_sourceleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_tables_sourceleftvaluefoldnegative = fs_q_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_tables_sourceleftvaluefoldnegative) + (fs_s_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps = fs_r_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps + fs_a_dst_inverse_tables_sourceleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_tables_sourceleftvaluefoldresult ge_balance_negative_inverse_tables_sourceleftvaluefoldresult. (((((dc_output_inverse_tables_sourceleft) = 2 * (ge_balance_positive_inverse_tables_sourceleftvaluefoldresult) /\ (ge_balance_negative_inverse_tables_sourceleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_tables_sourceleftvaluefoldresultdecode. (((dc_output_inverse_tables_sourceleft) = 2 * ge_signed_half_inverse_tables_sourceleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_tables_sourceleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_tables_sourceleftvaluefoldresult) = S ge_signed_half_inverse_tables_sourceleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_tables_sourceleftvaluefold) + ge_balance_negative_inverse_tables_sourceleftvaluefoldresult = (dst_negative_sum_inverse_tables_sourceleftvaluefold) + ge_balance_positive_inverse_tables_sourceleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_tables_sourcerightleft dst_positive_scale_inverse_tables_sourcerightleft dst_negative_code_inverse_tables_sourcerightleft dst_negative_scale_inverse_tables_sourcerightleft. (((G) = (((((dst_positive_code_inverse_tables_sourcerightleft) + (dst_positive_scale_inverse_tables_sourcerightleft)) * S ((dst_positive_code_inverse_tables_sourcerightleft) + (dst_positive_scale_inverse_tables_sourcerightleft)) + ((dst_positive_scale_inverse_tables_sourcerightleft) + (dst_positive_scale_inverse_tables_sourcerightleft))) + (((dst_negative_code_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)) * S ((dst_negative_code_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)) + ((dst_negative_scale_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)))) * S ((((dst_positive_code_inverse_tables_sourcerightleft) + (dst_positive_scale_inverse_tables_sourcerightleft)) * S ((dst_positive_code_inverse_tables_sourcerightleft) + (dst_positive_scale_inverse_tables_sourcerightleft)) + ((dst_positive_scale_inverse_tables_sourcerightleft) + (dst_positive_scale_inverse_tables_sourcerightleft))) + (((dst_negative_code_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)) * S ((dst_negative_code_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)) + ((dst_negative_scale_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)))) + ((((dst_negative_code_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)) * S ((dst_negative_code_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)) + ((dst_negative_scale_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft))) + (((dst_negative_code_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)) * S ((dst_negative_code_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)) + ((dst_negative_scale_inverse_tables_sourcerightleft) + (dst_negative_scale_inverse_tables_sourcerightleft)))))) /\ (forall dst_index_inverse_tables_sourcerightleft. (exists pvs_le_gap_inverse_tables_sourcerightleftdomain. pvs_le_gap_inverse_tables_sourcerightleftdomain + (dst_index_inverse_tables_sourcerightleft) = (N)) -> exists dst_positive_inverse_tables_sourcerightleft dst_negative_inverse_tables_sourcerightleft dst_value_inverse_tables_sourcerightleft. ((((exists ff_h_pvs_inverse_tables_sourcerightleftentrypositive. ff_h_pvs_inverse_tables_sourcerightleftentrypositive + S (dst_positive_inverse_tables_sourcerightleft) = S ((S (dst_index_inverse_tables_sourcerightleft)) * dst_positive_scale_inverse_tables_sourcerightleft)) /\ exists ff_q_pvs_inverse_tables_sourcerightleftentrypositive. dst_positive_code_inverse_tables_sourcerightleft = ff_q_pvs_inverse_tables_sourcerightleftentrypositive * S ((S (dst_index_inverse_tables_sourcerightleft)) * dst_positive_scale_inverse_tables_sourcerightleft) + (dst_positive_inverse_tables_sourcerightleft))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightleftentrynegative. ff_h_pvs_inverse_tables_sourcerightleftentrynegative + S (dst_negative_inverse_tables_sourcerightleft) = S ((S (dst_index_inverse_tables_sourcerightleft)) * dst_negative_scale_inverse_tables_sourcerightleft)) /\ exists ff_q_pvs_inverse_tables_sourcerightleftentrynegative. dst_negative_code_inverse_tables_sourcerightleft = ff_q_pvs_inverse_tables_sourcerightleftentrynegative * S ((S (dst_index_inverse_tables_sourcerightleft)) * dst_negative_scale_inverse_tables_sourcerightleft) + (dst_negative_inverse_tables_sourcerightleft))) /\ (exists ge_balance_positive_inverse_tables_sourcerightleftentryvalue ge_balance_negative_inverse_tables_sourcerightleftentryvalue. (((((dst_value_inverse_tables_sourcerightleft) = 2 * (ge_balance_positive_inverse_tables_sourcerightleftentryvalue) /\ (ge_balance_negative_inverse_tables_sourcerightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightleftentryvaluedecode. (((dst_value_inverse_tables_sourcerightleft) = 2 * ge_signed_half_inverse_tables_sourcerightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcerightleftentryvalue) = S ge_signed_half_inverse_tables_sourcerightleftentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourcerightleft) + ge_balance_negative_inverse_tables_sourcerightleftentryvalue = (dst_negative_inverse_tables_sourcerightleft) + ge_balance_positive_inverse_tables_sourcerightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_tables_sourcerightright dst_positive_scale_inverse_tables_sourcerightright dst_negative_code_inverse_tables_sourcerightright dst_negative_scale_inverse_tables_sourcerightright. (((F) = (((((dst_positive_code_inverse_tables_sourcerightright) + (dst_positive_scale_inverse_tables_sourcerightright)) * S ((dst_positive_code_inverse_tables_sourcerightright) + (dst_positive_scale_inverse_tables_sourcerightright)) + ((dst_positive_scale_inverse_tables_sourcerightright) + (dst_positive_scale_inverse_tables_sourcerightright))) + (((dst_negative_code_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)) * S ((dst_negative_code_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)) + ((dst_negative_scale_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)))) * S ((((dst_positive_code_inverse_tables_sourcerightright) + (dst_positive_scale_inverse_tables_sourcerightright)) * S ((dst_positive_code_inverse_tables_sourcerightright) + (dst_positive_scale_inverse_tables_sourcerightright)) + ((dst_positive_scale_inverse_tables_sourcerightright) + (dst_positive_scale_inverse_tables_sourcerightright))) + (((dst_negative_code_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)) * S ((dst_negative_code_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)) + ((dst_negative_scale_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)))) + ((((dst_negative_code_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)) * S ((dst_negative_code_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)) + ((dst_negative_scale_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright))) + (((dst_negative_code_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)) * S ((dst_negative_code_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)) + ((dst_negative_scale_inverse_tables_sourcerightright) + (dst_negative_scale_inverse_tables_sourcerightright)))))) /\ (forall dst_index_inverse_tables_sourcerightright. (exists pvs_le_gap_inverse_tables_sourcerightrightdomain. pvs_le_gap_inverse_tables_sourcerightrightdomain + (dst_index_inverse_tables_sourcerightright) = (N)) -> exists dst_positive_inverse_tables_sourcerightright dst_negative_inverse_tables_sourcerightright dst_value_inverse_tables_sourcerightright. ((((exists ff_h_pvs_inverse_tables_sourcerightrightentrypositive. ff_h_pvs_inverse_tables_sourcerightrightentrypositive + S (dst_positive_inverse_tables_sourcerightright) = S ((S (dst_index_inverse_tables_sourcerightright)) * dst_positive_scale_inverse_tables_sourcerightright)) /\ exists ff_q_pvs_inverse_tables_sourcerightrightentrypositive. dst_positive_code_inverse_tables_sourcerightright = ff_q_pvs_inverse_tables_sourcerightrightentrypositive * S ((S (dst_index_inverse_tables_sourcerightright)) * dst_positive_scale_inverse_tables_sourcerightright) + (dst_positive_inverse_tables_sourcerightright))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightrightentrynegative. ff_h_pvs_inverse_tables_sourcerightrightentrynegative + S (dst_negative_inverse_tables_sourcerightright) = S ((S (dst_index_inverse_tables_sourcerightright)) * dst_negative_scale_inverse_tables_sourcerightright)) /\ exists ff_q_pvs_inverse_tables_sourcerightrightentrynegative. dst_negative_code_inverse_tables_sourcerightright = ff_q_pvs_inverse_tables_sourcerightrightentrynegative * S ((S (dst_index_inverse_tables_sourcerightright)) * dst_negative_scale_inverse_tables_sourcerightright) + (dst_negative_inverse_tables_sourcerightright))) /\ (exists ge_balance_positive_inverse_tables_sourcerightrightentryvalue ge_balance_negative_inverse_tables_sourcerightrightentryvalue. (((((dst_value_inverse_tables_sourcerightright) = 2 * (ge_balance_positive_inverse_tables_sourcerightrightentryvalue) /\ (ge_balance_negative_inverse_tables_sourcerightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightrightentryvaluedecode. (((dst_value_inverse_tables_sourcerightright) = 2 * ge_signed_half_inverse_tables_sourcerightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcerightrightentryvalue) = S ge_signed_half_inverse_tables_sourcerightrightentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourcerightright) + ge_balance_negative_inverse_tables_sourcerightrightentryvalue = (dst_negative_inverse_tables_sourcerightright) + ge_balance_positive_inverse_tables_sourcerightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_tables_sourcerighttable dst_positive_scale_inverse_tables_sourcerighttable dst_negative_code_inverse_tables_sourcerighttable dst_negative_scale_inverse_tables_sourcerighttable. (((di_delta_inverse_tables_source) = (((((dst_positive_code_inverse_tables_sourcerighttable) + (dst_positive_scale_inverse_tables_sourcerighttable)) * S ((dst_positive_code_inverse_tables_sourcerighttable) + (dst_positive_scale_inverse_tables_sourcerighttable)) + ((dst_positive_scale_inverse_tables_sourcerighttable) + (dst_positive_scale_inverse_tables_sourcerighttable))) + (((dst_negative_code_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)) * S ((dst_negative_code_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)) + ((dst_negative_scale_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)))) * S ((((dst_positive_code_inverse_tables_sourcerighttable) + (dst_positive_scale_inverse_tables_sourcerighttable)) * S ((dst_positive_code_inverse_tables_sourcerighttable) + (dst_positive_scale_inverse_tables_sourcerighttable)) + ((dst_positive_scale_inverse_tables_sourcerighttable) + (dst_positive_scale_inverse_tables_sourcerighttable))) + (((dst_negative_code_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)) * S ((dst_negative_code_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)) + ((dst_negative_scale_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)))) + ((((dst_negative_code_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)) * S ((dst_negative_code_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)) + ((dst_negative_scale_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable))) + (((dst_negative_code_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)) * S ((dst_negative_code_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)) + ((dst_negative_scale_inverse_tables_sourcerighttable) + (dst_negative_scale_inverse_tables_sourcerighttable)))))) /\ (forall dst_index_inverse_tables_sourcerighttable. (exists pvs_le_gap_inverse_tables_sourcerighttabledomain. pvs_le_gap_inverse_tables_sourcerighttabledomain + (dst_index_inverse_tables_sourcerighttable) = (N)) -> exists dst_positive_inverse_tables_sourcerighttable dst_negative_inverse_tables_sourcerighttable dst_value_inverse_tables_sourcerighttable. ((((exists ff_h_pvs_inverse_tables_sourcerighttableentrypositive. ff_h_pvs_inverse_tables_sourcerighttableentrypositive + S (dst_positive_inverse_tables_sourcerighttable) = S ((S (dst_index_inverse_tables_sourcerighttable)) * dst_positive_scale_inverse_tables_sourcerighttable)) /\ exists ff_q_pvs_inverse_tables_sourcerighttableentrypositive. dst_positive_code_inverse_tables_sourcerighttable = ff_q_pvs_inverse_tables_sourcerighttableentrypositive * S ((S (dst_index_inverse_tables_sourcerighttable)) * dst_positive_scale_inverse_tables_sourcerighttable) + (dst_positive_inverse_tables_sourcerighttable))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerighttableentrynegative. ff_h_pvs_inverse_tables_sourcerighttableentrynegative + S (dst_negative_inverse_tables_sourcerighttable) = S ((S (dst_index_inverse_tables_sourcerighttable)) * dst_negative_scale_inverse_tables_sourcerighttable)) /\ exists ff_q_pvs_inverse_tables_sourcerighttableentrynegative. dst_negative_code_inverse_tables_sourcerighttable = ff_q_pvs_inverse_tables_sourcerighttableentrynegative * S ((S (dst_index_inverse_tables_sourcerighttable)) * dst_negative_scale_inverse_tables_sourcerighttable) + (dst_negative_inverse_tables_sourcerighttable))) /\ (exists ge_balance_positive_inverse_tables_sourcerighttableentryvalue ge_balance_negative_inverse_tables_sourcerighttableentryvalue. (((((dst_value_inverse_tables_sourcerighttable) = 2 * (ge_balance_positive_inverse_tables_sourcerighttableentryvalue) /\ (ge_balance_negative_inverse_tables_sourcerighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcerighttableentryvaluedecode. (((dst_value_inverse_tables_sourcerighttable) = 2 * ge_signed_half_inverse_tables_sourcerighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcerighttableentryvalue) = S ge_signed_half_inverse_tables_sourcerighttableentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourcerighttable) + ge_balance_negative_inverse_tables_sourcerighttableentryvalue = (dst_negative_inverse_tables_sourcerighttable) + ge_balance_positive_inverse_tables_sourcerighttableentryvalue))))))))) /\ (forall dc_input_inverse_tables_sourceright dc_output_inverse_tables_sourceright. ~(dc_input_inverse_tables_sourceright=0) -> (exists pvs_le_gap_inverse_tables_sourcerightdomain. pvs_le_gap_inverse_tables_sourcerightdomain + (dc_input_inverse_tables_sourceright) = (N)) -> (exists dst_positive_code_inverse_tables_sourcerightlookup dst_positive_scale_inverse_tables_sourcerightlookup dst_negative_code_inverse_tables_sourcerightlookup dst_negative_scale_inverse_tables_sourcerightlookup dst_positive_inverse_tables_sourcerightlookup dst_negative_inverse_tables_sourcerightlookup. (((di_delta_inverse_tables_source) = (((((dst_positive_code_inverse_tables_sourcerightlookup) + (dst_positive_scale_inverse_tables_sourcerightlookup)) * S ((dst_positive_code_inverse_tables_sourcerightlookup) + (dst_positive_scale_inverse_tables_sourcerightlookup)) + ((dst_positive_scale_inverse_tables_sourcerightlookup) + (dst_positive_scale_inverse_tables_sourcerightlookup))) + (((dst_negative_code_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)) * S ((dst_negative_code_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)) + ((dst_negative_scale_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)))) * S ((((dst_positive_code_inverse_tables_sourcerightlookup) + (dst_positive_scale_inverse_tables_sourcerightlookup)) * S ((dst_positive_code_inverse_tables_sourcerightlookup) + (dst_positive_scale_inverse_tables_sourcerightlookup)) + ((dst_positive_scale_inverse_tables_sourcerightlookup) + (dst_positive_scale_inverse_tables_sourcerightlookup))) + (((dst_negative_code_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)) * S ((dst_negative_code_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)) + ((dst_negative_scale_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)))) + ((((dst_negative_code_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)) * S ((dst_negative_code_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)) + ((dst_negative_scale_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup))) + (((dst_negative_code_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)) * S ((dst_negative_code_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)) + ((dst_negative_scale_inverse_tables_sourcerightlookup) + (dst_negative_scale_inverse_tables_sourcerightlookup)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightlookuppositive. ff_h_pvs_inverse_tables_sourcerightlookuppositive + S (dst_positive_inverse_tables_sourcerightlookup) = S ((S (dc_input_inverse_tables_sourceright)) * dst_positive_scale_inverse_tables_sourcerightlookup)) /\ exists ff_q_pvs_inverse_tables_sourcerightlookuppositive. dst_positive_code_inverse_tables_sourcerightlookup = ff_q_pvs_inverse_tables_sourcerightlookuppositive * S ((S (dc_input_inverse_tables_sourceright)) * dst_positive_scale_inverse_tables_sourcerightlookup) + (dst_positive_inverse_tables_sourcerightlookup))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightlookupnegative. ff_h_pvs_inverse_tables_sourcerightlookupnegative + S (dst_negative_inverse_tables_sourcerightlookup) = S ((S (dc_input_inverse_tables_sourceright)) * dst_negative_scale_inverse_tables_sourcerightlookup)) /\ exists ff_q_pvs_inverse_tables_sourcerightlookupnegative. dst_negative_code_inverse_tables_sourcerightlookup = ff_q_pvs_inverse_tables_sourcerightlookupnegative * S ((S (dc_input_inverse_tables_sourceright)) * dst_negative_scale_inverse_tables_sourcerightlookup) + (dst_negative_inverse_tables_sourcerightlookup))) /\ (exists ge_balance_positive_inverse_tables_sourcerightlookupvalue ge_balance_negative_inverse_tables_sourcerightlookupvalue. (((((dc_output_inverse_tables_sourceright) = 2 * (ge_balance_positive_inverse_tables_sourcerightlookupvalue) /\ (ge_balance_negative_inverse_tables_sourcerightlookupvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightlookupvaluedecode. (((dc_output_inverse_tables_sourceright) = 2 * ge_signed_half_inverse_tables_sourcerightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerightlookupvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcerightlookupvalue) = S ge_signed_half_inverse_tables_sourcerightlookupvaluedecode))) /\ ((dst_positive_inverse_tables_sourcerightlookup) + ge_balance_negative_inverse_tables_sourcerightlookupvalue = (dst_negative_inverse_tables_sourcerightlookup) + ge_balance_positive_inverse_tables_sourcerightlookupvalue))))))))) -> (((~((dc_input_inverse_tables_sourceright)=0)) /\ (exists dc_mask_inverse_tables_sourcerightvalue. ((((exists dst_positive_code_inverse_tables_sourcerightvaluemasktable dst_positive_scale_inverse_tables_sourcerightvaluemasktable dst_negative_code_inverse_tables_sourcerightvaluemasktable dst_negative_scale_inverse_tables_sourcerightvaluemasktable. (((dc_mask_inverse_tables_sourcerightvalue) = (((((dst_positive_code_inverse_tables_sourcerightvaluemasktable) + (dst_positive_scale_inverse_tables_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_tables_sourcerightvaluemasktable) + (dst_positive_scale_inverse_tables_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_tables_sourcerightvaluemasktable) + (dst_positive_scale_inverse_tables_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)))) * S ((((dst_positive_code_inverse_tables_sourcerightvaluemasktable) + (dst_positive_scale_inverse_tables_sourcerightvaluemasktable)) * S ((dst_positive_code_inverse_tables_sourcerightvaluemasktable) + (dst_positive_scale_inverse_tables_sourcerightvaluemasktable)) + ((dst_positive_scale_inverse_tables_sourcerightvaluemasktable) + (dst_positive_scale_inverse_tables_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)))) + ((((dst_negative_code_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable))) + (((dst_negative_code_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemasktable) + (dst_negative_scale_inverse_tables_sourcerightvaluemasktable)))))) /\ (forall dst_index_inverse_tables_sourcerightvaluemasktable. (exists pvs_le_gap_inverse_tables_sourcerightvaluemasktabledomain. pvs_le_gap_inverse_tables_sourcerightvaluemasktabledomain + (dst_index_inverse_tables_sourcerightvaluemasktable) = (dc_input_inverse_tables_sourceright)) -> exists dst_positive_inverse_tables_sourcerightvaluemasktable dst_negative_inverse_tables_sourcerightvaluemasktable dst_value_inverse_tables_sourcerightvaluemasktable. ((((exists ff_h_pvs_inverse_tables_sourcerightvaluemasktableentrypositive. ff_h_pvs_inverse_tables_sourcerightvaluemasktableentrypositive + S (dst_positive_inverse_tables_sourcerightvaluemasktable) = S ((S (dst_index_inverse_tables_sourcerightvaluemasktable)) * dst_positive_scale_inverse_tables_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_tables_sourcerightvaluemasktableentrypositive. dst_positive_code_inverse_tables_sourcerightvaluemasktable = ff_q_pvs_inverse_tables_sourcerightvaluemasktableentrypositive * S ((S (dst_index_inverse_tables_sourcerightvaluemasktable)) * dst_positive_scale_inverse_tables_sourcerightvaluemasktable) + (dst_positive_inverse_tables_sourcerightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightvaluemasktableentrynegative. ff_h_pvs_inverse_tables_sourcerightvaluemasktableentrynegative + S (dst_negative_inverse_tables_sourcerightvaluemasktable) = S ((S (dst_index_inverse_tables_sourcerightvaluemasktable)) * dst_negative_scale_inverse_tables_sourcerightvaluemasktable)) /\ exists ff_q_pvs_inverse_tables_sourcerightvaluemasktableentrynegative. dst_negative_code_inverse_tables_sourcerightvaluemasktable = ff_q_pvs_inverse_tables_sourcerightvaluemasktableentrynegative * S ((S (dst_index_inverse_tables_sourcerightvaluemasktable)) * dst_negative_scale_inverse_tables_sourcerightvaluemasktable) + (dst_negative_inverse_tables_sourcerightvaluemasktable))) /\ (exists ge_balance_positive_inverse_tables_sourcerightvaluemasktableentryvalue ge_balance_negative_inverse_tables_sourcerightvaluemasktableentryvalue. (((((dst_value_inverse_tables_sourcerightvaluemasktable) = 2 * (ge_balance_positive_inverse_tables_sourcerightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_tables_sourcerightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightvaluemasktableentryvaluedecode. (((dst_value_inverse_tables_sourcerightvaluemasktable) = 2 * ge_signed_half_inverse_tables_sourcerightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcerightvaluemasktableentryvalue) = S ge_signed_half_inverse_tables_sourcerightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_tables_sourcerightvaluemasktable) + ge_balance_negative_inverse_tables_sourcerightvaluemasktableentryvalue = (dst_negative_inverse_tables_sourcerightvaluemasktable) + ge_balance_positive_inverse_tables_sourcerightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_tables_sourcerightvaluemask dc_value_inverse_tables_sourcerightvaluemask. (exists pvs_le_gap_inverse_tables_sourcerightvaluemaskdomain. pvs_le_gap_inverse_tables_sourcerightvaluemaskdomain + (dc_index_inverse_tables_sourcerightvaluemask) = (dc_input_inverse_tables_sourceright)) -> (exists dst_positive_code_inverse_tables_sourcerightvaluemasklookup dst_positive_scale_inverse_tables_sourcerightvaluemasklookup dst_negative_code_inverse_tables_sourcerightvaluemasklookup dst_negative_scale_inverse_tables_sourcerightvaluemasklookup dst_positive_inverse_tables_sourcerightvaluemasklookup dst_negative_inverse_tables_sourcerightvaluemasklookup. (((dc_mask_inverse_tables_sourcerightvalue) = (((((dst_positive_code_inverse_tables_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_tables_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_tables_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_tables_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_tables_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_tables_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)))) * S ((((dst_positive_code_inverse_tables_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_tables_sourcerightvaluemasklookup)) * S ((dst_positive_code_inverse_tables_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_tables_sourcerightvaluemasklookup)) + ((dst_positive_scale_inverse_tables_sourcerightvaluemasklookup) + (dst_positive_scale_inverse_tables_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)))) + ((((dst_negative_code_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup))) + (((dst_negative_code_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightvaluemasklookuppositive. ff_h_pvs_inverse_tables_sourcerightvaluemasklookuppositive + S (dst_positive_inverse_tables_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_tables_sourcerightvaluemask)) * dst_positive_scale_inverse_tables_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_tables_sourcerightvaluemasklookuppositive. dst_positive_code_inverse_tables_sourcerightvaluemasklookup = ff_q_pvs_inverse_tables_sourcerightvaluemasklookuppositive * S ((S (dc_index_inverse_tables_sourcerightvaluemask)) * dst_positive_scale_inverse_tables_sourcerightvaluemasklookup) + (dst_positive_inverse_tables_sourcerightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightvaluemasklookupnegative. ff_h_pvs_inverse_tables_sourcerightvaluemasklookupnegative + S (dst_negative_inverse_tables_sourcerightvaluemasklookup) = S ((S (dc_index_inverse_tables_sourcerightvaluemask)) * dst_negative_scale_inverse_tables_sourcerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_tables_sourcerightvaluemasklookupnegative. dst_negative_code_inverse_tables_sourcerightvaluemasklookup = ff_q_pvs_inverse_tables_sourcerightvaluemasklookupnegative * S ((S (dc_index_inverse_tables_sourcerightvaluemask)) * dst_negative_scale_inverse_tables_sourcerightvaluemasklookup) + (dst_negative_inverse_tables_sourcerightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_tables_sourcerightvaluemasklookupvalue ge_balance_negative_inverse_tables_sourcerightvaluemasklookupvalue. (((((dc_value_inverse_tables_sourcerightvaluemask) = 2 * (ge_balance_positive_inverse_tables_sourcerightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_tables_sourcerightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightvaluemasklookupvaluedecode. (((dc_value_inverse_tables_sourcerightvaluemask) = 2 * ge_signed_half_inverse_tables_sourcerightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcerightvaluemasklookupvalue) = S ge_signed_half_inverse_tables_sourcerightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_tables_sourcerightvaluemasklookup) + ge_balance_negative_inverse_tables_sourcerightvaluemasklookupvalue = (dst_negative_inverse_tables_sourcerightvaluemasklookup) + ge_balance_positive_inverse_tables_sourcerightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_tables_sourcerightvaluemask)=0)) /\ (exists dc_quotient_inverse_tables_sourcerightvaluemaskentry dc_left_inverse_tables_sourcerightvaluemaskentry dc_right_inverse_tables_sourcerightvaluemaskentry. (((dc_input_inverse_tables_sourceright)=(dc_index_inverse_tables_sourcerightvaluemask)*dc_quotient_inverse_tables_sourcerightvaluemaskentry) /\ (((exists dst_positive_code_inverse_tables_sourcerightvaluemaskentryleft dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft dst_positive_inverse_tables_sourcerightvaluemaskentryleft dst_negative_inverse_tables_sourcerightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft))) + (((dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightvaluemaskentryleftpositive. ff_h_pvs_inverse_tables_sourcerightvaluemaskentryleftpositive + S (dst_positive_inverse_tables_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_tables_sourcerightvaluemask)) * dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_tables_sourcerightvaluemaskentryleftpositive. dst_positive_code_inverse_tables_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_tables_sourcerightvaluemaskentryleftpositive * S ((S (dc_index_inverse_tables_sourcerightvaluemask)) * dst_positive_scale_inverse_tables_sourcerightvaluemaskentryleft) + (dst_positive_inverse_tables_sourcerightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightvaluemaskentryleftnegative. ff_h_pvs_inverse_tables_sourcerightvaluemaskentryleftnegative + S (dst_negative_inverse_tables_sourcerightvaluemaskentryleft) = S ((S (dc_index_inverse_tables_sourcerightvaluemask)) * dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_tables_sourcerightvaluemaskentryleftnegative. dst_negative_code_inverse_tables_sourcerightvaluemaskentryleft = ff_q_pvs_inverse_tables_sourcerightvaluemaskentryleftnegative * S ((S (dc_index_inverse_tables_sourcerightvaluemask)) * dst_negative_scale_inverse_tables_sourcerightvaluemaskentryleft) + (dst_negative_inverse_tables_sourcerightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_tables_sourcerightvaluemaskentryleftvalue ge_balance_negative_inverse_tables_sourcerightvaluemaskentryleftvalue. (((((dc_left_inverse_tables_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_tables_sourcerightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_tables_sourcerightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightvaluemaskentryleftvaluedecode. (((dc_left_inverse_tables_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_tables_sourcerightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcerightvaluemaskentryleftvalue) = S ge_signed_half_inverse_tables_sourcerightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_tables_sourcerightvaluemaskentryleft) + ge_balance_negative_inverse_tables_sourcerightvaluemaskentryleftvalue = (dst_negative_inverse_tables_sourcerightvaluemaskentryleft) + ge_balance_positive_inverse_tables_sourcerightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_tables_sourcerightvaluemaskentryright dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright dst_negative_code_inverse_tables_sourcerightvaluemaskentryright dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright dst_positive_inverse_tables_sourcerightvaluemaskentryright dst_negative_inverse_tables_sourcerightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright)) * S ((dst_positive_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright)) + ((dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright) + (dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)))) + ((((dst_negative_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright))) + (((dst_negative_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) * S ((dst_negative_code_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) + ((dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightvaluemaskentryrightpositive. ff_h_pvs_inverse_tables_sourcerightvaluemaskentryrightpositive + S (dst_positive_inverse_tables_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_tables_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_tables_sourcerightvaluemaskentryrightpositive. dst_positive_code_inverse_tables_sourcerightvaluemaskentryright = ff_q_pvs_inverse_tables_sourcerightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_tables_sourcerightvaluemaskentry)) * dst_positive_scale_inverse_tables_sourcerightvaluemaskentryright) + (dst_positive_inverse_tables_sourcerightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_tables_sourcerightvaluemaskentryrightnegative. ff_h_pvs_inverse_tables_sourcerightvaluemaskentryrightnegative + S (dst_negative_inverse_tables_sourcerightvaluemaskentryright) = S ((S (dc_quotient_inverse_tables_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_tables_sourcerightvaluemaskentryrightnegative. dst_negative_code_inverse_tables_sourcerightvaluemaskentryright = ff_q_pvs_inverse_tables_sourcerightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_tables_sourcerightvaluemaskentry)) * dst_negative_scale_inverse_tables_sourcerightvaluemaskentryright) + (dst_negative_inverse_tables_sourcerightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_tables_sourcerightvaluemaskentryrightvalue ge_balance_negative_inverse_tables_sourcerightvaluemaskentryrightvalue. (((((dc_right_inverse_tables_sourcerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_tables_sourcerightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_tables_sourcerightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightvaluemaskentryrightvaluedecode. (((dc_right_inverse_tables_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_tables_sourcerightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_tables_sourcerightvaluemaskentryrightvalue) = S ge_signed_half_inverse_tables_sourcerightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_tables_sourcerightvaluemaskentryright) + ge_balance_negative_inverse_tables_sourcerightvaluemaskentryrightvalue = (dst_negative_inverse_tables_sourcerightvaluemaskentryright) + ge_balance_positive_inverse_tables_sourcerightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_tables_sourcerightvaluemaskentryproduct sto_an_inverse_tables_sourcerightvaluemaskentryproduct sto_bp_inverse_tables_sourcerightvaluemaskentryproduct sto_bn_inverse_tables_sourcerightvaluemaskentryproduct sto_cp_inverse_tables_sourcerightvaluemaskentryproduct sto_cn_inverse_tables_sourcerightvaluemaskentryproduct. (((((dc_left_inverse_tables_sourcerightvaluemaskentry) = 2 * (sto_ap_inverse_tables_sourcerightvaluemaskentryproduct) /\ (sto_an_inverse_tables_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductleft. (((dc_left_inverse_tables_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_tables_sourcerightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_tables_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_tables_sourcerightvaluemaskentry) = 2 * (sto_bp_inverse_tables_sourcerightvaluemaskentryproduct) /\ (sto_bn_inverse_tables_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductright. (((dc_right_inverse_tables_sourcerightvaluemaskentry) = 2 * ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_tables_sourcerightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_tables_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_tables_sourcerightvaluemask) = 2 * (sto_cp_inverse_tables_sourcerightvaluemaskentryproduct) /\ (sto_cn_inverse_tables_sourcerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductoutput. (((dc_value_inverse_tables_sourcerightvaluemask) = 2 * ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_tables_sourcerightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_tables_sourcerightvaluemaskentryproduct) = S ge_signed_half_inverse_tables_sourcerightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_tables_sourcerightvaluemaskentryproduct * sto_bp_inverse_tables_sourcerightvaluemaskentryproduct + sto_an_inverse_tables_sourcerightvaluemaskentryproduct * sto_bn_inverse_tables_sourcerightvaluemaskentryproduct) + sto_cn_inverse_tables_sourcerightvaluemaskentryproduct = (sto_ap_inverse_tables_sourcerightvaluemaskentryproduct * sto_bn_inverse_tables_sourcerightvaluemaskentryproduct + sto_an_inverse_tables_sourcerightvaluemaskentryproduct * sto_bp_inverse_tables_sourcerightvaluemaskentryproduct) + sto_cp_inverse_tables_sourcerightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_tables_sourcerightvaluemask)=0 \/ ~(exists pvs_factor_inverse_tables_sourcerightvaluemaskentrynondivisor. (dc_input_inverse_tables_sourceright) = (dc_index_inverse_tables_sourcerightvaluemask) * pvs_factor_inverse_tables_sourcerightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_tables_sourcerightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_tables_sourcerightvaluefold dst_positive_scale_inverse_tables_sourcerightvaluefold dst_negative_code_inverse_tables_sourcerightvaluefold dst_negative_scale_inverse_tables_sourcerightvaluefold dst_positive_sum_inverse_tables_sourcerightvaluefold dst_negative_sum_inverse_tables_sourcerightvaluefold. (((dc_mask_inverse_tables_sourcerightvalue) = (((((dst_positive_code_inverse_tables_sourcerightvaluefold) + (dst_positive_scale_inverse_tables_sourcerightvaluefold)) * S ((dst_positive_code_inverse_tables_sourcerightvaluefold) + (dst_positive_scale_inverse_tables_sourcerightvaluefold)) + ((dst_positive_scale_inverse_tables_sourcerightvaluefold) + (dst_positive_scale_inverse_tables_sourcerightvaluefold))) + (((dst_negative_code_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)) * S ((dst_negative_code_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)) + ((dst_negative_scale_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)))) * S ((((dst_positive_code_inverse_tables_sourcerightvaluefold) + (dst_positive_scale_inverse_tables_sourcerightvaluefold)) * S ((dst_positive_code_inverse_tables_sourcerightvaluefold) + (dst_positive_scale_inverse_tables_sourcerightvaluefold)) + ((dst_positive_scale_inverse_tables_sourcerightvaluefold) + (dst_positive_scale_inverse_tables_sourcerightvaluefold))) + (((dst_negative_code_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)) * S ((dst_negative_code_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)) + ((dst_negative_scale_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)))) + ((((dst_negative_code_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)) * S ((dst_negative_code_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)) + ((dst_negative_scale_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold))) + (((dst_negative_code_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)) * S ((dst_negative_code_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)) + ((dst_negative_scale_inverse_tables_sourcerightvaluefold) + (dst_negative_scale_inverse_tables_sourcerightvaluefold)))))) /\ (((exists fs_u_dst_inverse_tables_sourcerightvaluefoldpositive fs_v_dst_inverse_tables_sourcerightvaluefoldpositive. ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_start. fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_tables_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_start. fs_u_dst_inverse_tables_sourcerightvaluefoldpositive = fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_tables_sourcerightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_terminal. fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_tables_sourcerightvaluefold) = S ((S (S (dc_input_inverse_tables_sourceright))) * fs_v_dst_inverse_tables_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_terminal. fs_u_dst_inverse_tables_sourcerightvaluefoldpositive = fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_tables_sourceright))) * fs_v_dst_inverse_tables_sourcerightvaluefoldpositive) + (dst_positive_sum_inverse_tables_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps = S (dc_input_inverse_tables_sourceright)) -> exists fs_a_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps fs_r_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps fs_s_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_tables_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_tables_sourcerightvaluefold = fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_tables_sourcerightvaluefold) + (fs_a_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_tables_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_tables_sourcerightvaluefoldpositive = fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_tables_sourcerightvaluefoldpositive) + (fs_r_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_tables_sourcerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_tables_sourcerightvaluefoldpositive = fs_q_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_tables_sourcerightvaluefoldpositive) + (fs_s_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps = fs_r_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps + fs_a_dst_inverse_tables_sourcerightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_tables_sourcerightvaluefoldnegative fs_v_dst_inverse_tables_sourcerightvaluefoldnegative. ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_start. fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_tables_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_start. fs_u_dst_inverse_tables_sourcerightvaluefoldnegative = fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_tables_sourcerightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_terminal. fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_tables_sourcerightvaluefold) = S ((S (S (dc_input_inverse_tables_sourceright))) * fs_v_dst_inverse_tables_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_terminal. fs_u_dst_inverse_tables_sourcerightvaluefoldnegative = fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_tables_sourceright))) * fs_v_dst_inverse_tables_sourcerightvaluefoldnegative) + (dst_negative_sum_inverse_tables_sourcerightvaluefold))) /\ forall fs_i_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps = S (dc_input_inverse_tables_sourceright)) -> exists fs_a_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps fs_r_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps fs_s_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_tables_sourcerightvaluefold)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_tables_sourcerightvaluefold = fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_tables_sourcerightvaluefold) + (fs_a_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_tables_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_tables_sourcerightvaluefoldnegative = fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_tables_sourcerightvaluefoldnegative) + (fs_r_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_tables_sourcerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_tables_sourcerightvaluefoldnegative = fs_q_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_tables_sourcerightvaluefoldnegative) + (fs_s_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps = fs_r_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps + fs_a_dst_inverse_tables_sourcerightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_tables_sourcerightvaluefoldresult ge_balance_negative_inverse_tables_sourcerightvaluefoldresult. (((((dc_output_inverse_tables_sourceright) = 2 * (ge_balance_positive_inverse_tables_sourcerightvaluefoldresult) /\ (ge_balance_negative_inverse_tables_sourcerightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_tables_sourcerightvaluefoldresultdecode. (((dc_output_inverse_tables_sourceright) = 2 * ge_signed_half_inverse_tables_sourcerightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_tables_sourcerightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_tables_sourcerightvaluefoldresult) = S ge_signed_half_inverse_tables_sourcerightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_tables_sourcerightvaluefold) + ge_balance_negative_inverse_tables_sourcerightvaluefoldresult = (dst_negative_sum_inverse_tables_sourcerightvaluefold) + ge_balance_positive_inverse_tables_sourcerightvaluefoldresult)))))))))))))))))))))))) -> ((exists dst_positive_code_inverse_tables_left dst_positive_scale_inverse_tables_left dst_negative_code_inverse_tables_left dst_negative_scale_inverse_tables_left. (((F) = (((((dst_positive_code_inverse_tables_left) + (dst_positive_scale_inverse_tables_left)) * S ((dst_positive_code_inverse_tables_left) + (dst_positive_scale_inverse_tables_left)) + ((dst_positive_scale_inverse_tables_left) + (dst_positive_scale_inverse_tables_left))) + (((dst_negative_code_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)) * S ((dst_negative_code_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)) + ((dst_negative_scale_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)))) * S ((((dst_positive_code_inverse_tables_left) + (dst_positive_scale_inverse_tables_left)) * S ((dst_positive_code_inverse_tables_left) + (dst_positive_scale_inverse_tables_left)) + ((dst_positive_scale_inverse_tables_left) + (dst_positive_scale_inverse_tables_left))) + (((dst_negative_code_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)) * S ((dst_negative_code_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)) + ((dst_negative_scale_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)))) + ((((dst_negative_code_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)) * S ((dst_negative_code_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)) + ((dst_negative_scale_inverse_tables_left) + (dst_negative_scale_inverse_tables_left))) + (((dst_negative_code_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)) * S ((dst_negative_code_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)) + ((dst_negative_scale_inverse_tables_left) + (dst_negative_scale_inverse_tables_left)))))) /\ (forall dst_index_inverse_tables_left. (exists pvs_le_gap_inverse_tables_leftdomain. pvs_le_gap_inverse_tables_leftdomain + (dst_index_inverse_tables_left) = (N)) -> exists dst_positive_inverse_tables_left dst_negative_inverse_tables_left dst_value_inverse_tables_left. ((((exists ff_h_pvs_inverse_tables_leftentrypositive. ff_h_pvs_inverse_tables_leftentrypositive + S (dst_positive_inverse_tables_left) = S ((S (dst_index_inverse_tables_left)) * dst_positive_scale_inverse_tables_left)) /\ exists ff_q_pvs_inverse_tables_leftentrypositive. dst_positive_code_inverse_tables_left = ff_q_pvs_inverse_tables_leftentrypositive * S ((S (dst_index_inverse_tables_left)) * dst_positive_scale_inverse_tables_left) + (dst_positive_inverse_tables_left))) /\ (((((exists ff_h_pvs_inverse_tables_leftentrynegative. ff_h_pvs_inverse_tables_leftentrynegative + S (dst_negative_inverse_tables_left) = S ((S (dst_index_inverse_tables_left)) * dst_negative_scale_inverse_tables_left)) /\ exists ff_q_pvs_inverse_tables_leftentrynegative. dst_negative_code_inverse_tables_left = ff_q_pvs_inverse_tables_leftentrynegative * S ((S (dst_index_inverse_tables_left)) * dst_negative_scale_inverse_tables_left) + (dst_negative_inverse_tables_left))) /\ (exists ge_balance_positive_inverse_tables_leftentryvalue ge_balance_negative_inverse_tables_leftentryvalue. (((((dst_value_inverse_tables_left) = 2 * (ge_balance_positive_inverse_tables_leftentryvalue) /\ (ge_balance_negative_inverse_tables_leftentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_leftentryvaluedecode. (((dst_value_inverse_tables_left) = 2 * ge_signed_half_inverse_tables_leftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_leftentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_leftentryvalue) = S ge_signed_half_inverse_tables_leftentryvaluedecode))) /\ ((dst_positive_inverse_tables_left) + ge_balance_negative_inverse_tables_leftentryvalue = (dst_negative_inverse_tables_left) + ge_balance_positive_inverse_tables_leftentryvalue))))))))) /\ (exists dst_positive_code_inverse_tables_right dst_positive_scale_inverse_tables_right dst_negative_code_inverse_tables_right dst_negative_scale_inverse_tables_right. (((G) = (((((dst_positive_code_inverse_tables_right) + (dst_positive_scale_inverse_tables_right)) * S ((dst_positive_code_inverse_tables_right) + (dst_positive_scale_inverse_tables_right)) + ((dst_positive_scale_inverse_tables_right) + (dst_positive_scale_inverse_tables_right))) + (((dst_negative_code_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)) * S ((dst_negative_code_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)) + ((dst_negative_scale_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)))) * S ((((dst_positive_code_inverse_tables_right) + (dst_positive_scale_inverse_tables_right)) * S ((dst_positive_code_inverse_tables_right) + (dst_positive_scale_inverse_tables_right)) + ((dst_positive_scale_inverse_tables_right) + (dst_positive_scale_inverse_tables_right))) + (((dst_negative_code_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)) * S ((dst_negative_code_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)) + ((dst_negative_scale_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)))) + ((((dst_negative_code_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)) * S ((dst_negative_code_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)) + ((dst_negative_scale_inverse_tables_right) + (dst_negative_scale_inverse_tables_right))) + (((dst_negative_code_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)) * S ((dst_negative_code_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)) + ((dst_negative_scale_inverse_tables_right) + (dst_negative_scale_inverse_tables_right)))))) /\ (forall dst_index_inverse_tables_right. (exists pvs_le_gap_inverse_tables_rightdomain. pvs_le_gap_inverse_tables_rightdomain + (dst_index_inverse_tables_right) = (N)) -> exists dst_positive_inverse_tables_right dst_negative_inverse_tables_right dst_value_inverse_tables_right. ((((exists ff_h_pvs_inverse_tables_rightentrypositive. ff_h_pvs_inverse_tables_rightentrypositive + S (dst_positive_inverse_tables_right) = S ((S (dst_index_inverse_tables_right)) * dst_positive_scale_inverse_tables_right)) /\ exists ff_q_pvs_inverse_tables_rightentrypositive. dst_positive_code_inverse_tables_right = ff_q_pvs_inverse_tables_rightentrypositive * S ((S (dst_index_inverse_tables_right)) * dst_positive_scale_inverse_tables_right) + (dst_positive_inverse_tables_right))) /\ (((((exists ff_h_pvs_inverse_tables_rightentrynegative. ff_h_pvs_inverse_tables_rightentrynegative + S (dst_negative_inverse_tables_right) = S ((S (dst_index_inverse_tables_right)) * dst_negative_scale_inverse_tables_right)) /\ exists ff_q_pvs_inverse_tables_rightentrynegative. dst_negative_code_inverse_tables_right = ff_q_pvs_inverse_tables_rightentrynegative * S ((S (dst_index_inverse_tables_right)) * dst_negative_scale_inverse_tables_right) + (dst_negative_inverse_tables_right))) /\ (exists ge_balance_positive_inverse_tables_rightentryvalue ge_balance_negative_inverse_tables_rightentryvalue. (((((dst_value_inverse_tables_right) = 2 * (ge_balance_positive_inverse_tables_rightentryvalue) /\ (ge_balance_negative_inverse_tables_rightentryvalue) = 0) \/ exists ge_signed_half_inverse_tables_rightentryvaluedecode. (((dst_value_inverse_tables_right) = 2 * ge_signed_half_inverse_tables_rightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_tables_rightentryvalue) = 0) /\ (ge_balance_negative_inverse_tables_rightentryvalue) = S ge_signed_half_inverse_tables_rightentryvaluedecode))) /\ ((dst_positive_inverse_tables_right) + ge_balance_negative_inverse_tables_rightentryvalue = (dst_negative_inverse_tables_right) + ge_balance_positive_inverse_tables_rightentryvalue))))))))))