Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall N K F G H. (exists di_delta_inverse_prefix_large. ((((exists dst_positive_code_inverse_prefix_largedeltatable dst_positive_scale_inverse_prefix_largedeltatable dst_negative_code_inverse_prefix_largedeltatable dst_negative_scale_inverse_prefix_largedeltatable. (((di_delta_inverse_prefix_large) = (((((dst_positive_code_inverse_prefix_largedeltatable) + (dst_positive_scale_inverse_prefix_largedeltatable)) * S ((dst_positive_code_inverse_prefix_largedeltatable) + (dst_positive_scale_inverse_prefix_largedeltatable)) + ((dst_positive_scale_inverse_prefix_largedeltatable) + (dst_positive_scale_inverse_prefix_largedeltatable))) + (((dst_negative_code_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)) * S ((dst_negative_code_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)) + ((dst_negative_scale_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)))) * S ((((dst_positive_code_inverse_prefix_largedeltatable) + (dst_positive_scale_inverse_prefix_largedeltatable)) * S ((dst_positive_code_inverse_prefix_largedeltatable) + (dst_positive_scale_inverse_prefix_largedeltatable)) + ((dst_positive_scale_inverse_prefix_largedeltatable) + (dst_positive_scale_inverse_prefix_largedeltatable))) + (((dst_negative_code_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)) * S ((dst_negative_code_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)) + ((dst_negative_scale_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)))) + ((((dst_negative_code_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)) * S ((dst_negative_code_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)) + ((dst_negative_scale_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable))) + (((dst_negative_code_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)) * S ((dst_negative_code_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)) + ((dst_negative_scale_inverse_prefix_largedeltatable) + (dst_negative_scale_inverse_prefix_largedeltatable)))))) /\ (forall dst_index_inverse_prefix_largedeltatable. (exists pvs_le_gap_inverse_prefix_largedeltatabledomain. pvs_le_gap_inverse_prefix_largedeltatabledomain + (dst_index_inverse_prefix_largedeltatable) = (N)) -> exists dst_positive_inverse_prefix_largedeltatable dst_negative_inverse_prefix_largedeltatable dst_value_inverse_prefix_largedeltatable. ((((exists ff_h_pvs_inverse_prefix_largedeltatableentrypositive. ff_h_pvs_inverse_prefix_largedeltatableentrypositive + S (dst_positive_inverse_prefix_largedeltatable) = S ((S (dst_index_inverse_prefix_largedeltatable)) * dst_positive_scale_inverse_prefix_largedeltatable)) /\ exists ff_q_pvs_inverse_prefix_largedeltatableentrypositive. dst_positive_code_inverse_prefix_largedeltatable = ff_q_pvs_inverse_prefix_largedeltatableentrypositive * S ((S (dst_index_inverse_prefix_largedeltatable)) * dst_positive_scale_inverse_prefix_largedeltatable) + (dst_positive_inverse_prefix_largedeltatable))) /\ (((((exists ff_h_pvs_inverse_prefix_largedeltatableentrynegative. ff_h_pvs_inverse_prefix_largedeltatableentrynegative + S (dst_negative_inverse_prefix_largedeltatable) = S ((S (dst_index_inverse_prefix_largedeltatable)) * dst_negative_scale_inverse_prefix_largedeltatable)) /\ exists ff_q_pvs_inverse_prefix_largedeltatableentrynegative. dst_negative_code_inverse_prefix_largedeltatable = ff_q_pvs_inverse_prefix_largedeltatableentrynegative * S ((S (dst_index_inverse_prefix_largedeltatable)) * dst_negative_scale_inverse_prefix_largedeltatable) + (dst_negative_inverse_prefix_largedeltatable))) /\ (exists ge_balance_positive_inverse_prefix_largedeltatableentryvalue ge_balance_negative_inverse_prefix_largedeltatableentryvalue. (((((dst_value_inverse_prefix_largedeltatable) = 2 * (ge_balance_positive_inverse_prefix_largedeltatableentryvalue) /\ (ge_balance_negative_inverse_prefix_largedeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largedeltatableentryvaluedecode. (((dst_value_inverse_prefix_largedeltatable) = 2 * ge_signed_half_inverse_prefix_largedeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largedeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largedeltatableentryvalue) = S ge_signed_half_inverse_prefix_largedeltatableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largedeltatable) + ge_balance_negative_inverse_prefix_largedeltatableentryvalue = (dst_negative_inverse_prefix_largedeltatable) + ge_balance_positive_inverse_prefix_largedeltatableentryvalue))))))))) /\ (forall du_index_inverse_prefix_largedelta du_value_inverse_prefix_largedelta. ~(du_index_inverse_prefix_largedelta=0) -> (exists pvs_le_gap_inverse_prefix_largedeltabound. pvs_le_gap_inverse_prefix_largedeltabound + (du_index_inverse_prefix_largedelta) = (N)) -> (exists dst_positive_code_inverse_prefix_largedeltaentry dst_positive_scale_inverse_prefix_largedeltaentry dst_negative_code_inverse_prefix_largedeltaentry dst_negative_scale_inverse_prefix_largedeltaentry dst_positive_inverse_prefix_largedeltaentry dst_negative_inverse_prefix_largedeltaentry. (((di_delta_inverse_prefix_large) = (((((dst_positive_code_inverse_prefix_largedeltaentry) + (dst_positive_scale_inverse_prefix_largedeltaentry)) * S ((dst_positive_code_inverse_prefix_largedeltaentry) + (dst_positive_scale_inverse_prefix_largedeltaentry)) + ((dst_positive_scale_inverse_prefix_largedeltaentry) + (dst_positive_scale_inverse_prefix_largedeltaentry))) + (((dst_negative_code_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)) * S ((dst_negative_code_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)) + ((dst_negative_scale_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)))) * S ((((dst_positive_code_inverse_prefix_largedeltaentry) + (dst_positive_scale_inverse_prefix_largedeltaentry)) * S ((dst_positive_code_inverse_prefix_largedeltaentry) + (dst_positive_scale_inverse_prefix_largedeltaentry)) + ((dst_positive_scale_inverse_prefix_largedeltaentry) + (dst_positive_scale_inverse_prefix_largedeltaentry))) + (((dst_negative_code_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)) * S ((dst_negative_code_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)) + ((dst_negative_scale_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)))) + ((((dst_negative_code_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)) * S ((dst_negative_code_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)) + ((dst_negative_scale_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry))) + (((dst_negative_code_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)) * S ((dst_negative_code_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)) + ((dst_negative_scale_inverse_prefix_largedeltaentry) + (dst_negative_scale_inverse_prefix_largedeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largedeltaentrypositive. ff_h_pvs_inverse_prefix_largedeltaentrypositive + S (dst_positive_inverse_prefix_largedeltaentry) = S ((S (du_index_inverse_prefix_largedelta)) * dst_positive_scale_inverse_prefix_largedeltaentry)) /\ exists ff_q_pvs_inverse_prefix_largedeltaentrypositive. dst_positive_code_inverse_prefix_largedeltaentry = ff_q_pvs_inverse_prefix_largedeltaentrypositive * S ((S (du_index_inverse_prefix_largedelta)) * dst_positive_scale_inverse_prefix_largedeltaentry) + (dst_positive_inverse_prefix_largedeltaentry))) /\ (((((exists ff_h_pvs_inverse_prefix_largedeltaentrynegative. ff_h_pvs_inverse_prefix_largedeltaentrynegative + S (dst_negative_inverse_prefix_largedeltaentry) = S ((S (du_index_inverse_prefix_largedelta)) * dst_negative_scale_inverse_prefix_largedeltaentry)) /\ exists ff_q_pvs_inverse_prefix_largedeltaentrynegative. dst_negative_code_inverse_prefix_largedeltaentry = ff_q_pvs_inverse_prefix_largedeltaentrynegative * S ((S (du_index_inverse_prefix_largedelta)) * dst_negative_scale_inverse_prefix_largedeltaentry) + (dst_negative_inverse_prefix_largedeltaentry))) /\ (exists ge_balance_positive_inverse_prefix_largedeltaentryvalue ge_balance_negative_inverse_prefix_largedeltaentryvalue. (((((du_value_inverse_prefix_largedelta) = 2 * (ge_balance_positive_inverse_prefix_largedeltaentryvalue) /\ (ge_balance_negative_inverse_prefix_largedeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largedeltaentryvaluedecode. (((du_value_inverse_prefix_largedelta) = 2 * ge_signed_half_inverse_prefix_largedeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largedeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largedeltaentryvalue) = S ge_signed_half_inverse_prefix_largedeltaentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largedeltaentry) + ge_balance_negative_inverse_prefix_largedeltaentryvalue = (dst_negative_inverse_prefix_largedeltaentry) + ge_balance_positive_inverse_prefix_largedeltaentryvalue))))))))) -> ((((du_index_inverse_prefix_largedelta)=1 -> (du_value_inverse_prefix_largedelta)=2) /\ (~((du_index_inverse_prefix_largedelta)=1) -> (du_value_inverse_prefix_largedelta)=0)))))) /\ (((((exists dst_positive_code_inverse_prefix_largeleftleft dst_positive_scale_inverse_prefix_largeleftleft dst_negative_code_inverse_prefix_largeleftleft dst_negative_scale_inverse_prefix_largeleftleft. (((F) = (((((dst_positive_code_inverse_prefix_largeleftleft) + (dst_positive_scale_inverse_prefix_largeleftleft)) * S ((dst_positive_code_inverse_prefix_largeleftleft) + (dst_positive_scale_inverse_prefix_largeleftleft)) + ((dst_positive_scale_inverse_prefix_largeleftleft) + (dst_positive_scale_inverse_prefix_largeleftleft))) + (((dst_negative_code_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)) * S ((dst_negative_code_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)) + ((dst_negative_scale_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)))) * S ((((dst_positive_code_inverse_prefix_largeleftleft) + (dst_positive_scale_inverse_prefix_largeleftleft)) * S ((dst_positive_code_inverse_prefix_largeleftleft) + (dst_positive_scale_inverse_prefix_largeleftleft)) + ((dst_positive_scale_inverse_prefix_largeleftleft) + (dst_positive_scale_inverse_prefix_largeleftleft))) + (((dst_negative_code_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)) * S ((dst_negative_code_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)) + ((dst_negative_scale_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)))) + ((((dst_negative_code_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)) * S ((dst_negative_code_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)) + ((dst_negative_scale_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft))) + (((dst_negative_code_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)) * S ((dst_negative_code_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)) + ((dst_negative_scale_inverse_prefix_largeleftleft) + (dst_negative_scale_inverse_prefix_largeleftleft)))))) /\ (forall dst_index_inverse_prefix_largeleftleft. (exists pvs_le_gap_inverse_prefix_largeleftleftdomain. pvs_le_gap_inverse_prefix_largeleftleftdomain + (dst_index_inverse_prefix_largeleftleft) = (N)) -> exists dst_positive_inverse_prefix_largeleftleft dst_negative_inverse_prefix_largeleftleft dst_value_inverse_prefix_largeleftleft. ((((exists ff_h_pvs_inverse_prefix_largeleftleftentrypositive. ff_h_pvs_inverse_prefix_largeleftleftentrypositive + S (dst_positive_inverse_prefix_largeleftleft) = S ((S (dst_index_inverse_prefix_largeleftleft)) * dst_positive_scale_inverse_prefix_largeleftleft)) /\ exists ff_q_pvs_inverse_prefix_largeleftleftentrypositive. dst_positive_code_inverse_prefix_largeleftleft = ff_q_pvs_inverse_prefix_largeleftleftentrypositive * S ((S (dst_index_inverse_prefix_largeleftleft)) * dst_positive_scale_inverse_prefix_largeleftleft) + (dst_positive_inverse_prefix_largeleftleft))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftleftentrynegative. ff_h_pvs_inverse_prefix_largeleftleftentrynegative + S (dst_negative_inverse_prefix_largeleftleft) = S ((S (dst_index_inverse_prefix_largeleftleft)) * dst_negative_scale_inverse_prefix_largeleftleft)) /\ exists ff_q_pvs_inverse_prefix_largeleftleftentrynegative. dst_negative_code_inverse_prefix_largeleftleft = ff_q_pvs_inverse_prefix_largeleftleftentrynegative * S ((S (dst_index_inverse_prefix_largeleftleft)) * dst_negative_scale_inverse_prefix_largeleftleft) + (dst_negative_inverse_prefix_largeleftleft))) /\ (exists ge_balance_positive_inverse_prefix_largeleftleftentryvalue ge_balance_negative_inverse_prefix_largeleftleftentryvalue. (((((dst_value_inverse_prefix_largeleftleft) = 2 * (ge_balance_positive_inverse_prefix_largeleftleftentryvalue) /\ (ge_balance_negative_inverse_prefix_largeleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftleftentryvaluedecode. (((dst_value_inverse_prefix_largeleftleft) = 2 * ge_signed_half_inverse_prefix_largeleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largeleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largeleftleftentryvalue) = S ge_signed_half_inverse_prefix_largeleftleftentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largeleftleft) + ge_balance_negative_inverse_prefix_largeleftleftentryvalue = (dst_negative_inverse_prefix_largeleftleft) + ge_balance_positive_inverse_prefix_largeleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_largeleftright dst_positive_scale_inverse_prefix_largeleftright dst_negative_code_inverse_prefix_largeleftright dst_negative_scale_inverse_prefix_largeleftright. (((G) = (((((dst_positive_code_inverse_prefix_largeleftright) + (dst_positive_scale_inverse_prefix_largeleftright)) * S ((dst_positive_code_inverse_prefix_largeleftright) + (dst_positive_scale_inverse_prefix_largeleftright)) + ((dst_positive_scale_inverse_prefix_largeleftright) + (dst_positive_scale_inverse_prefix_largeleftright))) + (((dst_negative_code_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)) * S ((dst_negative_code_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)) + ((dst_negative_scale_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)))) * S ((((dst_positive_code_inverse_prefix_largeleftright) + (dst_positive_scale_inverse_prefix_largeleftright)) * S ((dst_positive_code_inverse_prefix_largeleftright) + (dst_positive_scale_inverse_prefix_largeleftright)) + ((dst_positive_scale_inverse_prefix_largeleftright) + (dst_positive_scale_inverse_prefix_largeleftright))) + (((dst_negative_code_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)) * S ((dst_negative_code_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)) + ((dst_negative_scale_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)))) + ((((dst_negative_code_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)) * S ((dst_negative_code_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)) + ((dst_negative_scale_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright))) + (((dst_negative_code_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)) * S ((dst_negative_code_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)) + ((dst_negative_scale_inverse_prefix_largeleftright) + (dst_negative_scale_inverse_prefix_largeleftright)))))) /\ (forall dst_index_inverse_prefix_largeleftright. (exists pvs_le_gap_inverse_prefix_largeleftrightdomain. pvs_le_gap_inverse_prefix_largeleftrightdomain + (dst_index_inverse_prefix_largeleftright) = (N)) -> exists dst_positive_inverse_prefix_largeleftright dst_negative_inverse_prefix_largeleftright dst_value_inverse_prefix_largeleftright. ((((exists ff_h_pvs_inverse_prefix_largeleftrightentrypositive. ff_h_pvs_inverse_prefix_largeleftrightentrypositive + S (dst_positive_inverse_prefix_largeleftright) = S ((S (dst_index_inverse_prefix_largeleftright)) * dst_positive_scale_inverse_prefix_largeleftright)) /\ exists ff_q_pvs_inverse_prefix_largeleftrightentrypositive. dst_positive_code_inverse_prefix_largeleftright = ff_q_pvs_inverse_prefix_largeleftrightentrypositive * S ((S (dst_index_inverse_prefix_largeleftright)) * dst_positive_scale_inverse_prefix_largeleftright) + (dst_positive_inverse_prefix_largeleftright))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftrightentrynegative. ff_h_pvs_inverse_prefix_largeleftrightentrynegative + S (dst_negative_inverse_prefix_largeleftright) = S ((S (dst_index_inverse_prefix_largeleftright)) * dst_negative_scale_inverse_prefix_largeleftright)) /\ exists ff_q_pvs_inverse_prefix_largeleftrightentrynegative. dst_negative_code_inverse_prefix_largeleftright = ff_q_pvs_inverse_prefix_largeleftrightentrynegative * S ((S (dst_index_inverse_prefix_largeleftright)) * dst_negative_scale_inverse_prefix_largeleftright) + (dst_negative_inverse_prefix_largeleftright))) /\ (exists ge_balance_positive_inverse_prefix_largeleftrightentryvalue ge_balance_negative_inverse_prefix_largeleftrightentryvalue. (((((dst_value_inverse_prefix_largeleftright) = 2 * (ge_balance_positive_inverse_prefix_largeleftrightentryvalue) /\ (ge_balance_negative_inverse_prefix_largeleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftrightentryvaluedecode. (((dst_value_inverse_prefix_largeleftright) = 2 * ge_signed_half_inverse_prefix_largeleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largeleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largeleftrightentryvalue) = S ge_signed_half_inverse_prefix_largeleftrightentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largeleftright) + ge_balance_negative_inverse_prefix_largeleftrightentryvalue = (dst_negative_inverse_prefix_largeleftright) + ge_balance_positive_inverse_prefix_largeleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_largelefttable dst_positive_scale_inverse_prefix_largelefttable dst_negative_code_inverse_prefix_largelefttable dst_negative_scale_inverse_prefix_largelefttable. (((di_delta_inverse_prefix_large) = (((((dst_positive_code_inverse_prefix_largelefttable) + (dst_positive_scale_inverse_prefix_largelefttable)) * S ((dst_positive_code_inverse_prefix_largelefttable) + (dst_positive_scale_inverse_prefix_largelefttable)) + ((dst_positive_scale_inverse_prefix_largelefttable) + (dst_positive_scale_inverse_prefix_largelefttable))) + (((dst_negative_code_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)) * S ((dst_negative_code_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)) + ((dst_negative_scale_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)))) * S ((((dst_positive_code_inverse_prefix_largelefttable) + (dst_positive_scale_inverse_prefix_largelefttable)) * S ((dst_positive_code_inverse_prefix_largelefttable) + (dst_positive_scale_inverse_prefix_largelefttable)) + ((dst_positive_scale_inverse_prefix_largelefttable) + (dst_positive_scale_inverse_prefix_largelefttable))) + (((dst_negative_code_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)) * S ((dst_negative_code_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)) + ((dst_negative_scale_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)))) + ((((dst_negative_code_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)) * S ((dst_negative_code_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)) + ((dst_negative_scale_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable))) + (((dst_negative_code_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)) * S ((dst_negative_code_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)) + ((dst_negative_scale_inverse_prefix_largelefttable) + (dst_negative_scale_inverse_prefix_largelefttable)))))) /\ (forall dst_index_inverse_prefix_largelefttable. (exists pvs_le_gap_inverse_prefix_largelefttabledomain. pvs_le_gap_inverse_prefix_largelefttabledomain + (dst_index_inverse_prefix_largelefttable) = (N)) -> exists dst_positive_inverse_prefix_largelefttable dst_negative_inverse_prefix_largelefttable dst_value_inverse_prefix_largelefttable. ((((exists ff_h_pvs_inverse_prefix_largelefttableentrypositive. ff_h_pvs_inverse_prefix_largelefttableentrypositive + S (dst_positive_inverse_prefix_largelefttable) = S ((S (dst_index_inverse_prefix_largelefttable)) * dst_positive_scale_inverse_prefix_largelefttable)) /\ exists ff_q_pvs_inverse_prefix_largelefttableentrypositive. dst_positive_code_inverse_prefix_largelefttable = ff_q_pvs_inverse_prefix_largelefttableentrypositive * S ((S (dst_index_inverse_prefix_largelefttable)) * dst_positive_scale_inverse_prefix_largelefttable) + (dst_positive_inverse_prefix_largelefttable))) /\ (((((exists ff_h_pvs_inverse_prefix_largelefttableentrynegative. ff_h_pvs_inverse_prefix_largelefttableentrynegative + S (dst_negative_inverse_prefix_largelefttable) = S ((S (dst_index_inverse_prefix_largelefttable)) * dst_negative_scale_inverse_prefix_largelefttable)) /\ exists ff_q_pvs_inverse_prefix_largelefttableentrynegative. dst_negative_code_inverse_prefix_largelefttable = ff_q_pvs_inverse_prefix_largelefttableentrynegative * S ((S (dst_index_inverse_prefix_largelefttable)) * dst_negative_scale_inverse_prefix_largelefttable) + (dst_negative_inverse_prefix_largelefttable))) /\ (exists ge_balance_positive_inverse_prefix_largelefttableentryvalue ge_balance_negative_inverse_prefix_largelefttableentryvalue. (((((dst_value_inverse_prefix_largelefttable) = 2 * (ge_balance_positive_inverse_prefix_largelefttableentryvalue) /\ (ge_balance_negative_inverse_prefix_largelefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largelefttableentryvaluedecode. (((dst_value_inverse_prefix_largelefttable) = 2 * ge_signed_half_inverse_prefix_largelefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largelefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largelefttableentryvalue) = S ge_signed_half_inverse_prefix_largelefttableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largelefttable) + ge_balance_negative_inverse_prefix_largelefttableentryvalue = (dst_negative_inverse_prefix_largelefttable) + ge_balance_positive_inverse_prefix_largelefttableentryvalue))))))))) /\ (forall dc_input_inverse_prefix_largeleft dc_output_inverse_prefix_largeleft. ~(dc_input_inverse_prefix_largeleft=0) -> (exists pvs_le_gap_inverse_prefix_largeleftdomain. pvs_le_gap_inverse_prefix_largeleftdomain + (dc_input_inverse_prefix_largeleft) = (N)) -> (exists dst_positive_code_inverse_prefix_largeleftlookup dst_positive_scale_inverse_prefix_largeleftlookup dst_negative_code_inverse_prefix_largeleftlookup dst_negative_scale_inverse_prefix_largeleftlookup dst_positive_inverse_prefix_largeleftlookup dst_negative_inverse_prefix_largeleftlookup. (((di_delta_inverse_prefix_large) = (((((dst_positive_code_inverse_prefix_largeleftlookup) + (dst_positive_scale_inverse_prefix_largeleftlookup)) * S ((dst_positive_code_inverse_prefix_largeleftlookup) + (dst_positive_scale_inverse_prefix_largeleftlookup)) + ((dst_positive_scale_inverse_prefix_largeleftlookup) + (dst_positive_scale_inverse_prefix_largeleftlookup))) + (((dst_negative_code_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)) * S ((dst_negative_code_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)) + ((dst_negative_scale_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)))) * S ((((dst_positive_code_inverse_prefix_largeleftlookup) + (dst_positive_scale_inverse_prefix_largeleftlookup)) * S ((dst_positive_code_inverse_prefix_largeleftlookup) + (dst_positive_scale_inverse_prefix_largeleftlookup)) + ((dst_positive_scale_inverse_prefix_largeleftlookup) + (dst_positive_scale_inverse_prefix_largeleftlookup))) + (((dst_negative_code_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)) * S ((dst_negative_code_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)) + ((dst_negative_scale_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)))) + ((((dst_negative_code_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)) * S ((dst_negative_code_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)) + ((dst_negative_scale_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup))) + (((dst_negative_code_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)) * S ((dst_negative_code_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)) + ((dst_negative_scale_inverse_prefix_largeleftlookup) + (dst_negative_scale_inverse_prefix_largeleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftlookuppositive. ff_h_pvs_inverse_prefix_largeleftlookuppositive + S (dst_positive_inverse_prefix_largeleftlookup) = S ((S (dc_input_inverse_prefix_largeleft)) * dst_positive_scale_inverse_prefix_largeleftlookup)) /\ exists ff_q_pvs_inverse_prefix_largeleftlookuppositive. dst_positive_code_inverse_prefix_largeleftlookup = ff_q_pvs_inverse_prefix_largeleftlookuppositive * S ((S (dc_input_inverse_prefix_largeleft)) * dst_positive_scale_inverse_prefix_largeleftlookup) + (dst_positive_inverse_prefix_largeleftlookup))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftlookupnegative. ff_h_pvs_inverse_prefix_largeleftlookupnegative + S (dst_negative_inverse_prefix_largeleftlookup) = S ((S (dc_input_inverse_prefix_largeleft)) * dst_negative_scale_inverse_prefix_largeleftlookup)) /\ exists ff_q_pvs_inverse_prefix_largeleftlookupnegative. dst_negative_code_inverse_prefix_largeleftlookup = ff_q_pvs_inverse_prefix_largeleftlookupnegative * S ((S (dc_input_inverse_prefix_largeleft)) * dst_negative_scale_inverse_prefix_largeleftlookup) + (dst_negative_inverse_prefix_largeleftlookup))) /\ (exists ge_balance_positive_inverse_prefix_largeleftlookupvalue ge_balance_negative_inverse_prefix_largeleftlookupvalue. (((((dc_output_inverse_prefix_largeleft) = 2 * (ge_balance_positive_inverse_prefix_largeleftlookupvalue) /\ (ge_balance_negative_inverse_prefix_largeleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftlookupvaluedecode. (((dc_output_inverse_prefix_largeleft) = 2 * ge_signed_half_inverse_prefix_largeleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largeleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largeleftlookupvalue) = S ge_signed_half_inverse_prefix_largeleftlookupvaluedecode))) /\ ((dst_positive_inverse_prefix_largeleftlookup) + ge_balance_negative_inverse_prefix_largeleftlookupvalue = (dst_negative_inverse_prefix_largeleftlookup) + ge_balance_positive_inverse_prefix_largeleftlookupvalue))))))))) -> (((~((dc_input_inverse_prefix_largeleft)=0)) /\ (exists dc_mask_inverse_prefix_largeleftvalue. ((((exists dst_positive_code_inverse_prefix_largeleftvaluemasktable dst_positive_scale_inverse_prefix_largeleftvaluemasktable dst_negative_code_inverse_prefix_largeleftvaluemasktable dst_negative_scale_inverse_prefix_largeleftvaluemasktable. (((dc_mask_inverse_prefix_largeleftvalue) = (((((dst_positive_code_inverse_prefix_largeleftvaluemasktable) + (dst_positive_scale_inverse_prefix_largeleftvaluemasktable)) * S ((dst_positive_code_inverse_prefix_largeleftvaluemasktable) + (dst_positive_scale_inverse_prefix_largeleftvaluemasktable)) + ((dst_positive_scale_inverse_prefix_largeleftvaluemasktable) + (dst_positive_scale_inverse_prefix_largeleftvaluemasktable))) + (((dst_negative_code_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)))) * S ((((dst_positive_code_inverse_prefix_largeleftvaluemasktable) + (dst_positive_scale_inverse_prefix_largeleftvaluemasktable)) * S ((dst_positive_code_inverse_prefix_largeleftvaluemasktable) + (dst_positive_scale_inverse_prefix_largeleftvaluemasktable)) + ((dst_positive_scale_inverse_prefix_largeleftvaluemasktable) + (dst_positive_scale_inverse_prefix_largeleftvaluemasktable))) + (((dst_negative_code_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)))) + ((((dst_negative_code_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable))) + (((dst_negative_code_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemasktable) + (dst_negative_scale_inverse_prefix_largeleftvaluemasktable)))))) /\ (forall dst_index_inverse_prefix_largeleftvaluemasktable. (exists pvs_le_gap_inverse_prefix_largeleftvaluemasktabledomain. pvs_le_gap_inverse_prefix_largeleftvaluemasktabledomain + (dst_index_inverse_prefix_largeleftvaluemasktable) = (dc_input_inverse_prefix_largeleft)) -> exists dst_positive_inverse_prefix_largeleftvaluemasktable dst_negative_inverse_prefix_largeleftvaluemasktable dst_value_inverse_prefix_largeleftvaluemasktable. ((((exists ff_h_pvs_inverse_prefix_largeleftvaluemasktableentrypositive. ff_h_pvs_inverse_prefix_largeleftvaluemasktableentrypositive + S (dst_positive_inverse_prefix_largeleftvaluemasktable) = S ((S (dst_index_inverse_prefix_largeleftvaluemasktable)) * dst_positive_scale_inverse_prefix_largeleftvaluemasktable)) /\ exists ff_q_pvs_inverse_prefix_largeleftvaluemasktableentrypositive. dst_positive_code_inverse_prefix_largeleftvaluemasktable = ff_q_pvs_inverse_prefix_largeleftvaluemasktableentrypositive * S ((S (dst_index_inverse_prefix_largeleftvaluemasktable)) * dst_positive_scale_inverse_prefix_largeleftvaluemasktable) + (dst_positive_inverse_prefix_largeleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftvaluemasktableentrynegative. ff_h_pvs_inverse_prefix_largeleftvaluemasktableentrynegative + S (dst_negative_inverse_prefix_largeleftvaluemasktable) = S ((S (dst_index_inverse_prefix_largeleftvaluemasktable)) * dst_negative_scale_inverse_prefix_largeleftvaluemasktable)) /\ exists ff_q_pvs_inverse_prefix_largeleftvaluemasktableentrynegative. dst_negative_code_inverse_prefix_largeleftvaluemasktable = ff_q_pvs_inverse_prefix_largeleftvaluemasktableentrynegative * S ((S (dst_index_inverse_prefix_largeleftvaluemasktable)) * dst_negative_scale_inverse_prefix_largeleftvaluemasktable) + (dst_negative_inverse_prefix_largeleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_prefix_largeleftvaluemasktableentryvalue ge_balance_negative_inverse_prefix_largeleftvaluemasktableentryvalue. (((((dst_value_inverse_prefix_largeleftvaluemasktable) = 2 * (ge_balance_positive_inverse_prefix_largeleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_prefix_largeleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftvaluemasktableentryvaluedecode. (((dst_value_inverse_prefix_largeleftvaluemasktable) = 2 * ge_signed_half_inverse_prefix_largeleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largeleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largeleftvaluemasktableentryvalue) = S ge_signed_half_inverse_prefix_largeleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largeleftvaluemasktable) + ge_balance_negative_inverse_prefix_largeleftvaluemasktableentryvalue = (dst_negative_inverse_prefix_largeleftvaluemasktable) + ge_balance_positive_inverse_prefix_largeleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_prefix_largeleftvaluemask dc_value_inverse_prefix_largeleftvaluemask. (exists pvs_le_gap_inverse_prefix_largeleftvaluemaskdomain. pvs_le_gap_inverse_prefix_largeleftvaluemaskdomain + (dc_index_inverse_prefix_largeleftvaluemask) = (dc_input_inverse_prefix_largeleft)) -> (exists dst_positive_code_inverse_prefix_largeleftvaluemasklookup dst_positive_scale_inverse_prefix_largeleftvaluemasklookup dst_negative_code_inverse_prefix_largeleftvaluemasklookup dst_negative_scale_inverse_prefix_largeleftvaluemasklookup dst_positive_inverse_prefix_largeleftvaluemasklookup dst_negative_inverse_prefix_largeleftvaluemasklookup. (((dc_mask_inverse_prefix_largeleftvalue) = (((((dst_positive_code_inverse_prefix_largeleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_largeleftvaluemasklookup)) * S ((dst_positive_code_inverse_prefix_largeleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_largeleftvaluemasklookup)) + ((dst_positive_scale_inverse_prefix_largeleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_largeleftvaluemasklookup))) + (((dst_negative_code_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_prefix_largeleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_largeleftvaluemasklookup)) * S ((dst_positive_code_inverse_prefix_largeleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_largeleftvaluemasklookup)) + ((dst_positive_scale_inverse_prefix_largeleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_largeleftvaluemasklookup))) + (((dst_negative_code_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)))) + ((((dst_negative_code_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup))) + (((dst_negative_code_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftvaluemasklookuppositive. ff_h_pvs_inverse_prefix_largeleftvaluemasklookuppositive + S (dst_positive_inverse_prefix_largeleftvaluemasklookup) = S ((S (dc_index_inverse_prefix_largeleftvaluemask)) * dst_positive_scale_inverse_prefix_largeleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_prefix_largeleftvaluemasklookuppositive. dst_positive_code_inverse_prefix_largeleftvaluemasklookup = ff_q_pvs_inverse_prefix_largeleftvaluemasklookuppositive * S ((S (dc_index_inverse_prefix_largeleftvaluemask)) * dst_positive_scale_inverse_prefix_largeleftvaluemasklookup) + (dst_positive_inverse_prefix_largeleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftvaluemasklookupnegative. ff_h_pvs_inverse_prefix_largeleftvaluemasklookupnegative + S (dst_negative_inverse_prefix_largeleftvaluemasklookup) = S ((S (dc_index_inverse_prefix_largeleftvaluemask)) * dst_negative_scale_inverse_prefix_largeleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_prefix_largeleftvaluemasklookupnegative. dst_negative_code_inverse_prefix_largeleftvaluemasklookup = ff_q_pvs_inverse_prefix_largeleftvaluemasklookupnegative * S ((S (dc_index_inverse_prefix_largeleftvaluemask)) * dst_negative_scale_inverse_prefix_largeleftvaluemasklookup) + (dst_negative_inverse_prefix_largeleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_prefix_largeleftvaluemasklookupvalue ge_balance_negative_inverse_prefix_largeleftvaluemasklookupvalue. (((((dc_value_inverse_prefix_largeleftvaluemask) = 2 * (ge_balance_positive_inverse_prefix_largeleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_prefix_largeleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftvaluemasklookupvaluedecode. (((dc_value_inverse_prefix_largeleftvaluemask) = 2 * ge_signed_half_inverse_prefix_largeleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largeleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largeleftvaluemasklookupvalue) = S ge_signed_half_inverse_prefix_largeleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_prefix_largeleftvaluemasklookup) + ge_balance_negative_inverse_prefix_largeleftvaluemasklookupvalue = (dst_negative_inverse_prefix_largeleftvaluemasklookup) + ge_balance_positive_inverse_prefix_largeleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_prefix_largeleftvaluemask)=0)) /\ (exists dc_quotient_inverse_prefix_largeleftvaluemaskentry dc_left_inverse_prefix_largeleftvaluemaskentry dc_right_inverse_prefix_largeleftvaluemaskentry. (((dc_input_inverse_prefix_largeleft)=(dc_index_inverse_prefix_largeleftvaluemask)*dc_quotient_inverse_prefix_largeleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_prefix_largeleftvaluemaskentryleft dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft dst_positive_inverse_prefix_largeleftvaluemaskentryleft dst_negative_inverse_prefix_largeleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftvaluemaskentryleftpositive. ff_h_pvs_inverse_prefix_largeleftvaluemaskentryleftpositive + S (dst_positive_inverse_prefix_largeleftvaluemaskentryleft) = S ((S (dc_index_inverse_prefix_largeleftvaluemask)) * dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_prefix_largeleftvaluemaskentryleftpositive. dst_positive_code_inverse_prefix_largeleftvaluemaskentryleft = ff_q_pvs_inverse_prefix_largeleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_prefix_largeleftvaluemask)) * dst_positive_scale_inverse_prefix_largeleftvaluemaskentryleft) + (dst_positive_inverse_prefix_largeleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftvaluemaskentryleftnegative. ff_h_pvs_inverse_prefix_largeleftvaluemaskentryleftnegative + S (dst_negative_inverse_prefix_largeleftvaluemaskentryleft) = S ((S (dc_index_inverse_prefix_largeleftvaluemask)) * dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_prefix_largeleftvaluemaskentryleftnegative. dst_negative_code_inverse_prefix_largeleftvaluemaskentryleft = ff_q_pvs_inverse_prefix_largeleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_prefix_largeleftvaluemask)) * dst_negative_scale_inverse_prefix_largeleftvaluemaskentryleft) + (dst_negative_inverse_prefix_largeleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_prefix_largeleftvaluemaskentryleftvalue ge_balance_negative_inverse_prefix_largeleftvaluemaskentryleftvalue. (((((dc_left_inverse_prefix_largeleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_prefix_largeleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_prefix_largeleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_prefix_largeleftvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_largeleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largeleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largeleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_prefix_largeleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_prefix_largeleftvaluemaskentryleft) + ge_balance_negative_inverse_prefix_largeleftvaluemaskentryleftvalue = (dst_negative_inverse_prefix_largeleftvaluemaskentryleft) + ge_balance_positive_inverse_prefix_largeleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_largeleftvaluemaskentryright dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright dst_negative_code_inverse_prefix_largeleftvaluemaskentryright dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright dst_positive_inverse_prefix_largeleftvaluemaskentryright dst_negative_inverse_prefix_largeleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright)) * S ((dst_positive_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright)) + ((dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright)) * S ((dst_positive_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright)) + ((dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftvaluemaskentryrightpositive. ff_h_pvs_inverse_prefix_largeleftvaluemaskentryrightpositive + S (dst_positive_inverse_prefix_largeleftvaluemaskentryright) = S ((S (dc_quotient_inverse_prefix_largeleftvaluemaskentry)) * dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_prefix_largeleftvaluemaskentryrightpositive. dst_positive_code_inverse_prefix_largeleftvaluemaskentryright = ff_q_pvs_inverse_prefix_largeleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_prefix_largeleftvaluemaskentry)) * dst_positive_scale_inverse_prefix_largeleftvaluemaskentryright) + (dst_positive_inverse_prefix_largeleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_prefix_largeleftvaluemaskentryrightnegative. ff_h_pvs_inverse_prefix_largeleftvaluemaskentryrightnegative + S (dst_negative_inverse_prefix_largeleftvaluemaskentryright) = S ((S (dc_quotient_inverse_prefix_largeleftvaluemaskentry)) * dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_prefix_largeleftvaluemaskentryrightnegative. dst_negative_code_inverse_prefix_largeleftvaluemaskentryright = ff_q_pvs_inverse_prefix_largeleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_prefix_largeleftvaluemaskentry)) * dst_negative_scale_inverse_prefix_largeleftvaluemaskentryright) + (dst_negative_inverse_prefix_largeleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_prefix_largeleftvaluemaskentryrightvalue ge_balance_negative_inverse_prefix_largeleftvaluemaskentryrightvalue. (((((dc_right_inverse_prefix_largeleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_prefix_largeleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_prefix_largeleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_prefix_largeleftvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_largeleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largeleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largeleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_prefix_largeleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_prefix_largeleftvaluemaskentryright) + ge_balance_negative_inverse_prefix_largeleftvaluemaskentryrightvalue = (dst_negative_inverse_prefix_largeleftvaluemaskentryright) + ge_balance_positive_inverse_prefix_largeleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_prefix_largeleftvaluemaskentryproduct sto_an_inverse_prefix_largeleftvaluemaskentryproduct sto_bp_inverse_prefix_largeleftvaluemaskentryproduct sto_bn_inverse_prefix_largeleftvaluemaskentryproduct sto_cp_inverse_prefix_largeleftvaluemaskentryproduct sto_cn_inverse_prefix_largeleftvaluemaskentryproduct. (((((dc_left_inverse_prefix_largeleftvaluemaskentry) = 2 * (sto_ap_inverse_prefix_largeleftvaluemaskentryproduct) /\ (sto_an_inverse_prefix_largeleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductleft. (((dc_left_inverse_prefix_largeleftvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_prefix_largeleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_prefix_largeleftvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_prefix_largeleftvaluemaskentry) = 2 * (sto_bp_inverse_prefix_largeleftvaluemaskentryproduct) /\ (sto_bn_inverse_prefix_largeleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductright. (((dc_right_inverse_prefix_largeleftvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_prefix_largeleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_prefix_largeleftvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_prefix_largeleftvaluemask) = 2 * (sto_cp_inverse_prefix_largeleftvaluemaskentryproduct) /\ (sto_cn_inverse_prefix_largeleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductoutput. (((dc_value_inverse_prefix_largeleftvaluemask) = 2 * ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_prefix_largeleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_prefix_largeleftvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_largeleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_prefix_largeleftvaluemaskentryproduct * sto_bp_inverse_prefix_largeleftvaluemaskentryproduct + sto_an_inverse_prefix_largeleftvaluemaskentryproduct * sto_bn_inverse_prefix_largeleftvaluemaskentryproduct) + sto_cn_inverse_prefix_largeleftvaluemaskentryproduct = (sto_ap_inverse_prefix_largeleftvaluemaskentryproduct * sto_bn_inverse_prefix_largeleftvaluemaskentryproduct + sto_an_inverse_prefix_largeleftvaluemaskentryproduct * sto_bp_inverse_prefix_largeleftvaluemaskentryproduct) + sto_cp_inverse_prefix_largeleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_prefix_largeleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_prefix_largeleftvaluemaskentrynondivisor. (dc_input_inverse_prefix_largeleft) = (dc_index_inverse_prefix_largeleftvaluemask) * pvs_factor_inverse_prefix_largeleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_prefix_largeleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_prefix_largeleftvaluefold dst_positive_scale_inverse_prefix_largeleftvaluefold dst_negative_code_inverse_prefix_largeleftvaluefold dst_negative_scale_inverse_prefix_largeleftvaluefold dst_positive_sum_inverse_prefix_largeleftvaluefold dst_negative_sum_inverse_prefix_largeleftvaluefold. (((dc_mask_inverse_prefix_largeleftvalue) = (((((dst_positive_code_inverse_prefix_largeleftvaluefold) + (dst_positive_scale_inverse_prefix_largeleftvaluefold)) * S ((dst_positive_code_inverse_prefix_largeleftvaluefold) + (dst_positive_scale_inverse_prefix_largeleftvaluefold)) + ((dst_positive_scale_inverse_prefix_largeleftvaluefold) + (dst_positive_scale_inverse_prefix_largeleftvaluefold))) + (((dst_negative_code_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)) * S ((dst_negative_code_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)) + ((dst_negative_scale_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)))) * S ((((dst_positive_code_inverse_prefix_largeleftvaluefold) + (dst_positive_scale_inverse_prefix_largeleftvaluefold)) * S ((dst_positive_code_inverse_prefix_largeleftvaluefold) + (dst_positive_scale_inverse_prefix_largeleftvaluefold)) + ((dst_positive_scale_inverse_prefix_largeleftvaluefold) + (dst_positive_scale_inverse_prefix_largeleftvaluefold))) + (((dst_negative_code_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)) * S ((dst_negative_code_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)) + ((dst_negative_scale_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)))) + ((((dst_negative_code_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)) * S ((dst_negative_code_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)) + ((dst_negative_scale_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold))) + (((dst_negative_code_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)) * S ((dst_negative_code_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)) + ((dst_negative_scale_inverse_prefix_largeleftvaluefold) + (dst_negative_scale_inverse_prefix_largeleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_prefix_largeleftvaluefoldpositive fs_v_dst_inverse_prefix_largeleftvaluefoldpositive. ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_start. fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_prefix_largeleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_start. fs_u_dst_inverse_prefix_largeleftvaluefoldpositive = fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_prefix_largeleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_prefix_largeleftvaluefold) = S ((S (S (dc_input_inverse_prefix_largeleft))) * fs_v_dst_inverse_prefix_largeleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_prefix_largeleftvaluefoldpositive = fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_prefix_largeleft))) * fs_v_dst_inverse_prefix_largeleftvaluefoldpositive) + (dst_positive_sum_inverse_prefix_largeleftvaluefold))) /\ forall fs_i_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps = S (dc_input_inverse_prefix_largeleft)) -> exists fs_a_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps fs_r_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps fs_s_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_prefix_largeleftvaluefold)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_prefix_largeleftvaluefold = fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_prefix_largeleftvaluefold) + (fs_a_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_largeleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_prefix_largeleftvaluefoldpositive = fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_largeleftvaluefoldpositive) + (fs_r_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_largeleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_prefix_largeleftvaluefoldpositive = fs_q_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_largeleftvaluefoldpositive) + (fs_s_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps = fs_r_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps + fs_a_dst_inverse_prefix_largeleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_prefix_largeleftvaluefoldnegative fs_v_dst_inverse_prefix_largeleftvaluefoldnegative. ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_start. fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_prefix_largeleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_start. fs_u_dst_inverse_prefix_largeleftvaluefoldnegative = fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_prefix_largeleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_prefix_largeleftvaluefold) = S ((S (S (dc_input_inverse_prefix_largeleft))) * fs_v_dst_inverse_prefix_largeleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_prefix_largeleftvaluefoldnegative = fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_prefix_largeleft))) * fs_v_dst_inverse_prefix_largeleftvaluefoldnegative) + (dst_negative_sum_inverse_prefix_largeleftvaluefold))) /\ forall fs_i_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps = S (dc_input_inverse_prefix_largeleft)) -> exists fs_a_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps fs_r_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps fs_s_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_prefix_largeleftvaluefold)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_prefix_largeleftvaluefold = fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_prefix_largeleftvaluefold) + (fs_a_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_largeleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_prefix_largeleftvaluefoldnegative = fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_largeleftvaluefoldnegative) + (fs_r_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_largeleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_prefix_largeleftvaluefoldnegative = fs_q_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_largeleftvaluefoldnegative) + (fs_s_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps = fs_r_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps + fs_a_dst_inverse_prefix_largeleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_prefix_largeleftvaluefoldresult ge_balance_negative_inverse_prefix_largeleftvaluefoldresult. (((((dc_output_inverse_prefix_largeleft) = 2 * (ge_balance_positive_inverse_prefix_largeleftvaluefoldresult) /\ (ge_balance_negative_inverse_prefix_largeleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_prefix_largeleftvaluefoldresultdecode. (((dc_output_inverse_prefix_largeleft) = 2 * ge_signed_half_inverse_prefix_largeleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_prefix_largeleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_prefix_largeleftvaluefoldresult) = S ge_signed_half_inverse_prefix_largeleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_prefix_largeleftvaluefold) + ge_balance_negative_inverse_prefix_largeleftvaluefoldresult = (dst_negative_sum_inverse_prefix_largeleftvaluefold) + ge_balance_positive_inverse_prefix_largeleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_prefix_largerightleft dst_positive_scale_inverse_prefix_largerightleft dst_negative_code_inverse_prefix_largerightleft dst_negative_scale_inverse_prefix_largerightleft. (((G) = (((((dst_positive_code_inverse_prefix_largerightleft) + (dst_positive_scale_inverse_prefix_largerightleft)) * S ((dst_positive_code_inverse_prefix_largerightleft) + (dst_positive_scale_inverse_prefix_largerightleft)) + ((dst_positive_scale_inverse_prefix_largerightleft) + (dst_positive_scale_inverse_prefix_largerightleft))) + (((dst_negative_code_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)) * S ((dst_negative_code_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)) + ((dst_negative_scale_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)))) * S ((((dst_positive_code_inverse_prefix_largerightleft) + (dst_positive_scale_inverse_prefix_largerightleft)) * S ((dst_positive_code_inverse_prefix_largerightleft) + (dst_positive_scale_inverse_prefix_largerightleft)) + ((dst_positive_scale_inverse_prefix_largerightleft) + (dst_positive_scale_inverse_prefix_largerightleft))) + (((dst_negative_code_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)) * S ((dst_negative_code_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)) + ((dst_negative_scale_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)))) + ((((dst_negative_code_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)) * S ((dst_negative_code_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)) + ((dst_negative_scale_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft))) + (((dst_negative_code_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)) * S ((dst_negative_code_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)) + ((dst_negative_scale_inverse_prefix_largerightleft) + (dst_negative_scale_inverse_prefix_largerightleft)))))) /\ (forall dst_index_inverse_prefix_largerightleft. (exists pvs_le_gap_inverse_prefix_largerightleftdomain. pvs_le_gap_inverse_prefix_largerightleftdomain + (dst_index_inverse_prefix_largerightleft) = (N)) -> exists dst_positive_inverse_prefix_largerightleft dst_negative_inverse_prefix_largerightleft dst_value_inverse_prefix_largerightleft. ((((exists ff_h_pvs_inverse_prefix_largerightleftentrypositive. ff_h_pvs_inverse_prefix_largerightleftentrypositive + S (dst_positive_inverse_prefix_largerightleft) = S ((S (dst_index_inverse_prefix_largerightleft)) * dst_positive_scale_inverse_prefix_largerightleft)) /\ exists ff_q_pvs_inverse_prefix_largerightleftentrypositive. dst_positive_code_inverse_prefix_largerightleft = ff_q_pvs_inverse_prefix_largerightleftentrypositive * S ((S (dst_index_inverse_prefix_largerightleft)) * dst_positive_scale_inverse_prefix_largerightleft) + (dst_positive_inverse_prefix_largerightleft))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightleftentrynegative. ff_h_pvs_inverse_prefix_largerightleftentrynegative + S (dst_negative_inverse_prefix_largerightleft) = S ((S (dst_index_inverse_prefix_largerightleft)) * dst_negative_scale_inverse_prefix_largerightleft)) /\ exists ff_q_pvs_inverse_prefix_largerightleftentrynegative. dst_negative_code_inverse_prefix_largerightleft = ff_q_pvs_inverse_prefix_largerightleftentrynegative * S ((S (dst_index_inverse_prefix_largerightleft)) * dst_negative_scale_inverse_prefix_largerightleft) + (dst_negative_inverse_prefix_largerightleft))) /\ (exists ge_balance_positive_inverse_prefix_largerightleftentryvalue ge_balance_negative_inverse_prefix_largerightleftentryvalue. (((((dst_value_inverse_prefix_largerightleft) = 2 * (ge_balance_positive_inverse_prefix_largerightleftentryvalue) /\ (ge_balance_negative_inverse_prefix_largerightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largerightleftentryvaluedecode. (((dst_value_inverse_prefix_largerightleft) = 2 * ge_signed_half_inverse_prefix_largerightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largerightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largerightleftentryvalue) = S ge_signed_half_inverse_prefix_largerightleftentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largerightleft) + ge_balance_negative_inverse_prefix_largerightleftentryvalue = (dst_negative_inverse_prefix_largerightleft) + ge_balance_positive_inverse_prefix_largerightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_largerightright dst_positive_scale_inverse_prefix_largerightright dst_negative_code_inverse_prefix_largerightright dst_negative_scale_inverse_prefix_largerightright. (((F) = (((((dst_positive_code_inverse_prefix_largerightright) + (dst_positive_scale_inverse_prefix_largerightright)) * S ((dst_positive_code_inverse_prefix_largerightright) + (dst_positive_scale_inverse_prefix_largerightright)) + ((dst_positive_scale_inverse_prefix_largerightright) + (dst_positive_scale_inverse_prefix_largerightright))) + (((dst_negative_code_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)) * S ((dst_negative_code_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)) + ((dst_negative_scale_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)))) * S ((((dst_positive_code_inverse_prefix_largerightright) + (dst_positive_scale_inverse_prefix_largerightright)) * S ((dst_positive_code_inverse_prefix_largerightright) + (dst_positive_scale_inverse_prefix_largerightright)) + ((dst_positive_scale_inverse_prefix_largerightright) + (dst_positive_scale_inverse_prefix_largerightright))) + (((dst_negative_code_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)) * S ((dst_negative_code_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)) + ((dst_negative_scale_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)))) + ((((dst_negative_code_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)) * S ((dst_negative_code_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)) + ((dst_negative_scale_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright))) + (((dst_negative_code_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)) * S ((dst_negative_code_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)) + ((dst_negative_scale_inverse_prefix_largerightright) + (dst_negative_scale_inverse_prefix_largerightright)))))) /\ (forall dst_index_inverse_prefix_largerightright. (exists pvs_le_gap_inverse_prefix_largerightrightdomain. pvs_le_gap_inverse_prefix_largerightrightdomain + (dst_index_inverse_prefix_largerightright) = (N)) -> exists dst_positive_inverse_prefix_largerightright dst_negative_inverse_prefix_largerightright dst_value_inverse_prefix_largerightright. ((((exists ff_h_pvs_inverse_prefix_largerightrightentrypositive. ff_h_pvs_inverse_prefix_largerightrightentrypositive + S (dst_positive_inverse_prefix_largerightright) = S ((S (dst_index_inverse_prefix_largerightright)) * dst_positive_scale_inverse_prefix_largerightright)) /\ exists ff_q_pvs_inverse_prefix_largerightrightentrypositive. dst_positive_code_inverse_prefix_largerightright = ff_q_pvs_inverse_prefix_largerightrightentrypositive * S ((S (dst_index_inverse_prefix_largerightright)) * dst_positive_scale_inverse_prefix_largerightright) + (dst_positive_inverse_prefix_largerightright))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightrightentrynegative. ff_h_pvs_inverse_prefix_largerightrightentrynegative + S (dst_negative_inverse_prefix_largerightright) = S ((S (dst_index_inverse_prefix_largerightright)) * dst_negative_scale_inverse_prefix_largerightright)) /\ exists ff_q_pvs_inverse_prefix_largerightrightentrynegative. dst_negative_code_inverse_prefix_largerightright = ff_q_pvs_inverse_prefix_largerightrightentrynegative * S ((S (dst_index_inverse_prefix_largerightright)) * dst_negative_scale_inverse_prefix_largerightright) + (dst_negative_inverse_prefix_largerightright))) /\ (exists ge_balance_positive_inverse_prefix_largerightrightentryvalue ge_balance_negative_inverse_prefix_largerightrightentryvalue. (((((dst_value_inverse_prefix_largerightright) = 2 * (ge_balance_positive_inverse_prefix_largerightrightentryvalue) /\ (ge_balance_negative_inverse_prefix_largerightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largerightrightentryvaluedecode. (((dst_value_inverse_prefix_largerightright) = 2 * ge_signed_half_inverse_prefix_largerightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largerightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largerightrightentryvalue) = S ge_signed_half_inverse_prefix_largerightrightentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largerightright) + ge_balance_negative_inverse_prefix_largerightrightentryvalue = (dst_negative_inverse_prefix_largerightright) + ge_balance_positive_inverse_prefix_largerightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_largerighttable dst_positive_scale_inverse_prefix_largerighttable dst_negative_code_inverse_prefix_largerighttable dst_negative_scale_inverse_prefix_largerighttable. (((di_delta_inverse_prefix_large) = (((((dst_positive_code_inverse_prefix_largerighttable) + (dst_positive_scale_inverse_prefix_largerighttable)) * S ((dst_positive_code_inverse_prefix_largerighttable) + (dst_positive_scale_inverse_prefix_largerighttable)) + ((dst_positive_scale_inverse_prefix_largerighttable) + (dst_positive_scale_inverse_prefix_largerighttable))) + (((dst_negative_code_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)) * S ((dst_negative_code_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)) + ((dst_negative_scale_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)))) * S ((((dst_positive_code_inverse_prefix_largerighttable) + (dst_positive_scale_inverse_prefix_largerighttable)) * S ((dst_positive_code_inverse_prefix_largerighttable) + (dst_positive_scale_inverse_prefix_largerighttable)) + ((dst_positive_scale_inverse_prefix_largerighttable) + (dst_positive_scale_inverse_prefix_largerighttable))) + (((dst_negative_code_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)) * S ((dst_negative_code_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)) + ((dst_negative_scale_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)))) + ((((dst_negative_code_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)) * S ((dst_negative_code_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)) + ((dst_negative_scale_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable))) + (((dst_negative_code_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)) * S ((dst_negative_code_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)) + ((dst_negative_scale_inverse_prefix_largerighttable) + (dst_negative_scale_inverse_prefix_largerighttable)))))) /\ (forall dst_index_inverse_prefix_largerighttable. (exists pvs_le_gap_inverse_prefix_largerighttabledomain. pvs_le_gap_inverse_prefix_largerighttabledomain + (dst_index_inverse_prefix_largerighttable) = (N)) -> exists dst_positive_inverse_prefix_largerighttable dst_negative_inverse_prefix_largerighttable dst_value_inverse_prefix_largerighttable. ((((exists ff_h_pvs_inverse_prefix_largerighttableentrypositive. ff_h_pvs_inverse_prefix_largerighttableentrypositive + S (dst_positive_inverse_prefix_largerighttable) = S ((S (dst_index_inverse_prefix_largerighttable)) * dst_positive_scale_inverse_prefix_largerighttable)) /\ exists ff_q_pvs_inverse_prefix_largerighttableentrypositive. dst_positive_code_inverse_prefix_largerighttable = ff_q_pvs_inverse_prefix_largerighttableentrypositive * S ((S (dst_index_inverse_prefix_largerighttable)) * dst_positive_scale_inverse_prefix_largerighttable) + (dst_positive_inverse_prefix_largerighttable))) /\ (((((exists ff_h_pvs_inverse_prefix_largerighttableentrynegative. ff_h_pvs_inverse_prefix_largerighttableentrynegative + S (dst_negative_inverse_prefix_largerighttable) = S ((S (dst_index_inverse_prefix_largerighttable)) * dst_negative_scale_inverse_prefix_largerighttable)) /\ exists ff_q_pvs_inverse_prefix_largerighttableentrynegative. dst_negative_code_inverse_prefix_largerighttable = ff_q_pvs_inverse_prefix_largerighttableentrynegative * S ((S (dst_index_inverse_prefix_largerighttable)) * dst_negative_scale_inverse_prefix_largerighttable) + (dst_negative_inverse_prefix_largerighttable))) /\ (exists ge_balance_positive_inverse_prefix_largerighttableentryvalue ge_balance_negative_inverse_prefix_largerighttableentryvalue. (((((dst_value_inverse_prefix_largerighttable) = 2 * (ge_balance_positive_inverse_prefix_largerighttableentryvalue) /\ (ge_balance_negative_inverse_prefix_largerighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largerighttableentryvaluedecode. (((dst_value_inverse_prefix_largerighttable) = 2 * ge_signed_half_inverse_prefix_largerighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largerighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largerighttableentryvalue) = S ge_signed_half_inverse_prefix_largerighttableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largerighttable) + ge_balance_negative_inverse_prefix_largerighttableentryvalue = (dst_negative_inverse_prefix_largerighttable) + ge_balance_positive_inverse_prefix_largerighttableentryvalue))))))))) /\ (forall dc_input_inverse_prefix_largeright dc_output_inverse_prefix_largeright. ~(dc_input_inverse_prefix_largeright=0) -> (exists pvs_le_gap_inverse_prefix_largerightdomain. pvs_le_gap_inverse_prefix_largerightdomain + (dc_input_inverse_prefix_largeright) = (N)) -> (exists dst_positive_code_inverse_prefix_largerightlookup dst_positive_scale_inverse_prefix_largerightlookup dst_negative_code_inverse_prefix_largerightlookup dst_negative_scale_inverse_prefix_largerightlookup dst_positive_inverse_prefix_largerightlookup dst_negative_inverse_prefix_largerightlookup. (((di_delta_inverse_prefix_large) = (((((dst_positive_code_inverse_prefix_largerightlookup) + (dst_positive_scale_inverse_prefix_largerightlookup)) * S ((dst_positive_code_inverse_prefix_largerightlookup) + (dst_positive_scale_inverse_prefix_largerightlookup)) + ((dst_positive_scale_inverse_prefix_largerightlookup) + (dst_positive_scale_inverse_prefix_largerightlookup))) + (((dst_negative_code_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)) * S ((dst_negative_code_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)) + ((dst_negative_scale_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)))) * S ((((dst_positive_code_inverse_prefix_largerightlookup) + (dst_positive_scale_inverse_prefix_largerightlookup)) * S ((dst_positive_code_inverse_prefix_largerightlookup) + (dst_positive_scale_inverse_prefix_largerightlookup)) + ((dst_positive_scale_inverse_prefix_largerightlookup) + (dst_positive_scale_inverse_prefix_largerightlookup))) + (((dst_negative_code_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)) * S ((dst_negative_code_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)) + ((dst_negative_scale_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)))) + ((((dst_negative_code_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)) * S ((dst_negative_code_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)) + ((dst_negative_scale_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup))) + (((dst_negative_code_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)) * S ((dst_negative_code_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)) + ((dst_negative_scale_inverse_prefix_largerightlookup) + (dst_negative_scale_inverse_prefix_largerightlookup)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightlookuppositive. ff_h_pvs_inverse_prefix_largerightlookuppositive + S (dst_positive_inverse_prefix_largerightlookup) = S ((S (dc_input_inverse_prefix_largeright)) * dst_positive_scale_inverse_prefix_largerightlookup)) /\ exists ff_q_pvs_inverse_prefix_largerightlookuppositive. dst_positive_code_inverse_prefix_largerightlookup = ff_q_pvs_inverse_prefix_largerightlookuppositive * S ((S (dc_input_inverse_prefix_largeright)) * dst_positive_scale_inverse_prefix_largerightlookup) + (dst_positive_inverse_prefix_largerightlookup))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightlookupnegative. ff_h_pvs_inverse_prefix_largerightlookupnegative + S (dst_negative_inverse_prefix_largerightlookup) = S ((S (dc_input_inverse_prefix_largeright)) * dst_negative_scale_inverse_prefix_largerightlookup)) /\ exists ff_q_pvs_inverse_prefix_largerightlookupnegative. dst_negative_code_inverse_prefix_largerightlookup = ff_q_pvs_inverse_prefix_largerightlookupnegative * S ((S (dc_input_inverse_prefix_largeright)) * dst_negative_scale_inverse_prefix_largerightlookup) + (dst_negative_inverse_prefix_largerightlookup))) /\ (exists ge_balance_positive_inverse_prefix_largerightlookupvalue ge_balance_negative_inverse_prefix_largerightlookupvalue. (((((dc_output_inverse_prefix_largeright) = 2 * (ge_balance_positive_inverse_prefix_largerightlookupvalue) /\ (ge_balance_negative_inverse_prefix_largerightlookupvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largerightlookupvaluedecode. (((dc_output_inverse_prefix_largeright) = 2 * ge_signed_half_inverse_prefix_largerightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largerightlookupvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largerightlookupvalue) = S ge_signed_half_inverse_prefix_largerightlookupvaluedecode))) /\ ((dst_positive_inverse_prefix_largerightlookup) + ge_balance_negative_inverse_prefix_largerightlookupvalue = (dst_negative_inverse_prefix_largerightlookup) + ge_balance_positive_inverse_prefix_largerightlookupvalue))))))))) -> (((~((dc_input_inverse_prefix_largeright)=0)) /\ (exists dc_mask_inverse_prefix_largerightvalue. ((((exists dst_positive_code_inverse_prefix_largerightvaluemasktable dst_positive_scale_inverse_prefix_largerightvaluemasktable dst_negative_code_inverse_prefix_largerightvaluemasktable dst_negative_scale_inverse_prefix_largerightvaluemasktable. (((dc_mask_inverse_prefix_largerightvalue) = (((((dst_positive_code_inverse_prefix_largerightvaluemasktable) + (dst_positive_scale_inverse_prefix_largerightvaluemasktable)) * S ((dst_positive_code_inverse_prefix_largerightvaluemasktable) + (dst_positive_scale_inverse_prefix_largerightvaluemasktable)) + ((dst_positive_scale_inverse_prefix_largerightvaluemasktable) + (dst_positive_scale_inverse_prefix_largerightvaluemasktable))) + (((dst_negative_code_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)) * S ((dst_negative_code_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)) + ((dst_negative_scale_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)))) * S ((((dst_positive_code_inverse_prefix_largerightvaluemasktable) + (dst_positive_scale_inverse_prefix_largerightvaluemasktable)) * S ((dst_positive_code_inverse_prefix_largerightvaluemasktable) + (dst_positive_scale_inverse_prefix_largerightvaluemasktable)) + ((dst_positive_scale_inverse_prefix_largerightvaluemasktable) + (dst_positive_scale_inverse_prefix_largerightvaluemasktable))) + (((dst_negative_code_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)) * S ((dst_negative_code_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)) + ((dst_negative_scale_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)))) + ((((dst_negative_code_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)) * S ((dst_negative_code_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)) + ((dst_negative_scale_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable))) + (((dst_negative_code_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)) * S ((dst_negative_code_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)) + ((dst_negative_scale_inverse_prefix_largerightvaluemasktable) + (dst_negative_scale_inverse_prefix_largerightvaluemasktable)))))) /\ (forall dst_index_inverse_prefix_largerightvaluemasktable. (exists pvs_le_gap_inverse_prefix_largerightvaluemasktabledomain. pvs_le_gap_inverse_prefix_largerightvaluemasktabledomain + (dst_index_inverse_prefix_largerightvaluemasktable) = (dc_input_inverse_prefix_largeright)) -> exists dst_positive_inverse_prefix_largerightvaluemasktable dst_negative_inverse_prefix_largerightvaluemasktable dst_value_inverse_prefix_largerightvaluemasktable. ((((exists ff_h_pvs_inverse_prefix_largerightvaluemasktableentrypositive. ff_h_pvs_inverse_prefix_largerightvaluemasktableentrypositive + S (dst_positive_inverse_prefix_largerightvaluemasktable) = S ((S (dst_index_inverse_prefix_largerightvaluemasktable)) * dst_positive_scale_inverse_prefix_largerightvaluemasktable)) /\ exists ff_q_pvs_inverse_prefix_largerightvaluemasktableentrypositive. dst_positive_code_inverse_prefix_largerightvaluemasktable = ff_q_pvs_inverse_prefix_largerightvaluemasktableentrypositive * S ((S (dst_index_inverse_prefix_largerightvaluemasktable)) * dst_positive_scale_inverse_prefix_largerightvaluemasktable) + (dst_positive_inverse_prefix_largerightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightvaluemasktableentrynegative. ff_h_pvs_inverse_prefix_largerightvaluemasktableentrynegative + S (dst_negative_inverse_prefix_largerightvaluemasktable) = S ((S (dst_index_inverse_prefix_largerightvaluemasktable)) * dst_negative_scale_inverse_prefix_largerightvaluemasktable)) /\ exists ff_q_pvs_inverse_prefix_largerightvaluemasktableentrynegative. dst_negative_code_inverse_prefix_largerightvaluemasktable = ff_q_pvs_inverse_prefix_largerightvaluemasktableentrynegative * S ((S (dst_index_inverse_prefix_largerightvaluemasktable)) * dst_negative_scale_inverse_prefix_largerightvaluemasktable) + (dst_negative_inverse_prefix_largerightvaluemasktable))) /\ (exists ge_balance_positive_inverse_prefix_largerightvaluemasktableentryvalue ge_balance_negative_inverse_prefix_largerightvaluemasktableentryvalue. (((((dst_value_inverse_prefix_largerightvaluemasktable) = 2 * (ge_balance_positive_inverse_prefix_largerightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_prefix_largerightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largerightvaluemasktableentryvaluedecode. (((dst_value_inverse_prefix_largerightvaluemasktable) = 2 * ge_signed_half_inverse_prefix_largerightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largerightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largerightvaluemasktableentryvalue) = S ge_signed_half_inverse_prefix_largerightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_largerightvaluemasktable) + ge_balance_negative_inverse_prefix_largerightvaluemasktableentryvalue = (dst_negative_inverse_prefix_largerightvaluemasktable) + ge_balance_positive_inverse_prefix_largerightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_prefix_largerightvaluemask dc_value_inverse_prefix_largerightvaluemask. (exists pvs_le_gap_inverse_prefix_largerightvaluemaskdomain. pvs_le_gap_inverse_prefix_largerightvaluemaskdomain + (dc_index_inverse_prefix_largerightvaluemask) = (dc_input_inverse_prefix_largeright)) -> (exists dst_positive_code_inverse_prefix_largerightvaluemasklookup dst_positive_scale_inverse_prefix_largerightvaluemasklookup dst_negative_code_inverse_prefix_largerightvaluemasklookup dst_negative_scale_inverse_prefix_largerightvaluemasklookup dst_positive_inverse_prefix_largerightvaluemasklookup dst_negative_inverse_prefix_largerightvaluemasklookup. (((dc_mask_inverse_prefix_largerightvalue) = (((((dst_positive_code_inverse_prefix_largerightvaluemasklookup) + (dst_positive_scale_inverse_prefix_largerightvaluemasklookup)) * S ((dst_positive_code_inverse_prefix_largerightvaluemasklookup) + (dst_positive_scale_inverse_prefix_largerightvaluemasklookup)) + ((dst_positive_scale_inverse_prefix_largerightvaluemasklookup) + (dst_positive_scale_inverse_prefix_largerightvaluemasklookup))) + (((dst_negative_code_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)))) * S ((((dst_positive_code_inverse_prefix_largerightvaluemasklookup) + (dst_positive_scale_inverse_prefix_largerightvaluemasklookup)) * S ((dst_positive_code_inverse_prefix_largerightvaluemasklookup) + (dst_positive_scale_inverse_prefix_largerightvaluemasklookup)) + ((dst_positive_scale_inverse_prefix_largerightvaluemasklookup) + (dst_positive_scale_inverse_prefix_largerightvaluemasklookup))) + (((dst_negative_code_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)))) + ((((dst_negative_code_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup))) + (((dst_negative_code_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_largerightvaluemasklookup) + (dst_negative_scale_inverse_prefix_largerightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightvaluemasklookuppositive. ff_h_pvs_inverse_prefix_largerightvaluemasklookuppositive + S (dst_positive_inverse_prefix_largerightvaluemasklookup) = S ((S (dc_index_inverse_prefix_largerightvaluemask)) * dst_positive_scale_inverse_prefix_largerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_prefix_largerightvaluemasklookuppositive. dst_positive_code_inverse_prefix_largerightvaluemasklookup = ff_q_pvs_inverse_prefix_largerightvaluemasklookuppositive * S ((S (dc_index_inverse_prefix_largerightvaluemask)) * dst_positive_scale_inverse_prefix_largerightvaluemasklookup) + (dst_positive_inverse_prefix_largerightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightvaluemasklookupnegative. ff_h_pvs_inverse_prefix_largerightvaluemasklookupnegative + S (dst_negative_inverse_prefix_largerightvaluemasklookup) = S ((S (dc_index_inverse_prefix_largerightvaluemask)) * dst_negative_scale_inverse_prefix_largerightvaluemasklookup)) /\ exists ff_q_pvs_inverse_prefix_largerightvaluemasklookupnegative. dst_negative_code_inverse_prefix_largerightvaluemasklookup = ff_q_pvs_inverse_prefix_largerightvaluemasklookupnegative * S ((S (dc_index_inverse_prefix_largerightvaluemask)) * dst_negative_scale_inverse_prefix_largerightvaluemasklookup) + (dst_negative_inverse_prefix_largerightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_prefix_largerightvaluemasklookupvalue ge_balance_negative_inverse_prefix_largerightvaluemasklookupvalue. (((((dc_value_inverse_prefix_largerightvaluemask) = 2 * (ge_balance_positive_inverse_prefix_largerightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_prefix_largerightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largerightvaluemasklookupvaluedecode. (((dc_value_inverse_prefix_largerightvaluemask) = 2 * ge_signed_half_inverse_prefix_largerightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largerightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largerightvaluemasklookupvalue) = S ge_signed_half_inverse_prefix_largerightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_prefix_largerightvaluemasklookup) + ge_balance_negative_inverse_prefix_largerightvaluemasklookupvalue = (dst_negative_inverse_prefix_largerightvaluemasklookup) + ge_balance_positive_inverse_prefix_largerightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_prefix_largerightvaluemask)=0)) /\ (exists dc_quotient_inverse_prefix_largerightvaluemaskentry dc_left_inverse_prefix_largerightvaluemaskentry dc_right_inverse_prefix_largerightvaluemaskentry. (((dc_input_inverse_prefix_largeright)=(dc_index_inverse_prefix_largerightvaluemask)*dc_quotient_inverse_prefix_largerightvaluemaskentry) /\ (((exists dst_positive_code_inverse_prefix_largerightvaluemaskentryleft dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft dst_negative_code_inverse_prefix_largerightvaluemaskentryleft dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft dst_positive_inverse_prefix_largerightvaluemaskentryleft dst_negative_inverse_prefix_largerightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft)) * S ((dst_positive_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft)) + ((dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightvaluemaskentryleftpositive. ff_h_pvs_inverse_prefix_largerightvaluemaskentryleftpositive + S (dst_positive_inverse_prefix_largerightvaluemaskentryleft) = S ((S (dc_index_inverse_prefix_largerightvaluemask)) * dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_prefix_largerightvaluemaskentryleftpositive. dst_positive_code_inverse_prefix_largerightvaluemaskentryleft = ff_q_pvs_inverse_prefix_largerightvaluemaskentryleftpositive * S ((S (dc_index_inverse_prefix_largerightvaluemask)) * dst_positive_scale_inverse_prefix_largerightvaluemaskentryleft) + (dst_positive_inverse_prefix_largerightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightvaluemaskentryleftnegative. ff_h_pvs_inverse_prefix_largerightvaluemaskentryleftnegative + S (dst_negative_inverse_prefix_largerightvaluemaskentryleft) = S ((S (dc_index_inverse_prefix_largerightvaluemask)) * dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_prefix_largerightvaluemaskentryleftnegative. dst_negative_code_inverse_prefix_largerightvaluemaskentryleft = ff_q_pvs_inverse_prefix_largerightvaluemaskentryleftnegative * S ((S (dc_index_inverse_prefix_largerightvaluemask)) * dst_negative_scale_inverse_prefix_largerightvaluemaskentryleft) + (dst_negative_inverse_prefix_largerightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_prefix_largerightvaluemaskentryleftvalue ge_balance_negative_inverse_prefix_largerightvaluemaskentryleftvalue. (((((dc_left_inverse_prefix_largerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_prefix_largerightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_prefix_largerightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largerightvaluemaskentryleftvaluedecode. (((dc_left_inverse_prefix_largerightvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_largerightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largerightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largerightvaluemaskentryleftvalue) = S ge_signed_half_inverse_prefix_largerightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_prefix_largerightvaluemaskentryleft) + ge_balance_negative_inverse_prefix_largerightvaluemaskentryleftvalue = (dst_negative_inverse_prefix_largerightvaluemaskentryleft) + ge_balance_positive_inverse_prefix_largerightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_largerightvaluemaskentryright dst_positive_scale_inverse_prefix_largerightvaluemaskentryright dst_negative_code_inverse_prefix_largerightvaluemaskentryright dst_negative_scale_inverse_prefix_largerightvaluemaskentryright dst_positive_inverse_prefix_largerightvaluemaskentryright dst_negative_inverse_prefix_largerightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_prefix_largerightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryright)) * S ((dst_positive_code_inverse_prefix_largerightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryright)) + ((dst_positive_scale_inverse_prefix_largerightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_prefix_largerightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryright)) * S ((dst_positive_code_inverse_prefix_largerightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryright)) + ((dst_positive_scale_inverse_prefix_largerightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_largerightvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)))) + ((((dst_negative_code_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightvaluemaskentryrightpositive. ff_h_pvs_inverse_prefix_largerightvaluemaskentryrightpositive + S (dst_positive_inverse_prefix_largerightvaluemaskentryright) = S ((S (dc_quotient_inverse_prefix_largerightvaluemaskentry)) * dst_positive_scale_inverse_prefix_largerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_prefix_largerightvaluemaskentryrightpositive. dst_positive_code_inverse_prefix_largerightvaluemaskentryright = ff_q_pvs_inverse_prefix_largerightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_prefix_largerightvaluemaskentry)) * dst_positive_scale_inverse_prefix_largerightvaluemaskentryright) + (dst_positive_inverse_prefix_largerightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_prefix_largerightvaluemaskentryrightnegative. ff_h_pvs_inverse_prefix_largerightvaluemaskentryrightnegative + S (dst_negative_inverse_prefix_largerightvaluemaskentryright) = S ((S (dc_quotient_inverse_prefix_largerightvaluemaskentry)) * dst_negative_scale_inverse_prefix_largerightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_prefix_largerightvaluemaskentryrightnegative. dst_negative_code_inverse_prefix_largerightvaluemaskentryright = ff_q_pvs_inverse_prefix_largerightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_prefix_largerightvaluemaskentry)) * dst_negative_scale_inverse_prefix_largerightvaluemaskentryright) + (dst_negative_inverse_prefix_largerightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_prefix_largerightvaluemaskentryrightvalue ge_balance_negative_inverse_prefix_largerightvaluemaskentryrightvalue. (((((dc_right_inverse_prefix_largerightvaluemaskentry) = 2 * (ge_balance_positive_inverse_prefix_largerightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_prefix_largerightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_prefix_largerightvaluemaskentryrightvaluedecode. (((dc_right_inverse_prefix_largerightvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_largerightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_largerightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_prefix_largerightvaluemaskentryrightvalue) = S ge_signed_half_inverse_prefix_largerightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_prefix_largerightvaluemaskentryright) + ge_balance_negative_inverse_prefix_largerightvaluemaskentryrightvalue = (dst_negative_inverse_prefix_largerightvaluemaskentryright) + ge_balance_positive_inverse_prefix_largerightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_prefix_largerightvaluemaskentryproduct sto_an_inverse_prefix_largerightvaluemaskentryproduct sto_bp_inverse_prefix_largerightvaluemaskentryproduct sto_bn_inverse_prefix_largerightvaluemaskentryproduct sto_cp_inverse_prefix_largerightvaluemaskentryproduct sto_cn_inverse_prefix_largerightvaluemaskentryproduct. (((((dc_left_inverse_prefix_largerightvaluemaskentry) = 2 * (sto_ap_inverse_prefix_largerightvaluemaskentryproduct) /\ (sto_an_inverse_prefix_largerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_largerightvaluemaskentryproductleft. (((dc_left_inverse_prefix_largerightvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_largerightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_prefix_largerightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_prefix_largerightvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_largerightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_prefix_largerightvaluemaskentry) = 2 * (sto_bp_inverse_prefix_largerightvaluemaskentryproduct) /\ (sto_bn_inverse_prefix_largerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_largerightvaluemaskentryproductright. (((dc_right_inverse_prefix_largerightvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_largerightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_prefix_largerightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_prefix_largerightvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_largerightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_prefix_largerightvaluemask) = 2 * (sto_cp_inverse_prefix_largerightvaluemaskentryproduct) /\ (sto_cn_inverse_prefix_largerightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_largerightvaluemaskentryproductoutput. (((dc_value_inverse_prefix_largerightvaluemask) = 2 * ge_signed_half_inverse_prefix_largerightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_prefix_largerightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_prefix_largerightvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_largerightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_prefix_largerightvaluemaskentryproduct * sto_bp_inverse_prefix_largerightvaluemaskentryproduct + sto_an_inverse_prefix_largerightvaluemaskentryproduct * sto_bn_inverse_prefix_largerightvaluemaskentryproduct) + sto_cn_inverse_prefix_largerightvaluemaskentryproduct = (sto_ap_inverse_prefix_largerightvaluemaskentryproduct * sto_bn_inverse_prefix_largerightvaluemaskentryproduct + sto_an_inverse_prefix_largerightvaluemaskentryproduct * sto_bp_inverse_prefix_largerightvaluemaskentryproduct) + sto_cp_inverse_prefix_largerightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_prefix_largerightvaluemask)=0 \/ ~(exists pvs_factor_inverse_prefix_largerightvaluemaskentrynondivisor. (dc_input_inverse_prefix_largeright) = (dc_index_inverse_prefix_largerightvaluemask) * pvs_factor_inverse_prefix_largerightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_prefix_largerightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_prefix_largerightvaluefold dst_positive_scale_inverse_prefix_largerightvaluefold dst_negative_code_inverse_prefix_largerightvaluefold dst_negative_scale_inverse_prefix_largerightvaluefold dst_positive_sum_inverse_prefix_largerightvaluefold dst_negative_sum_inverse_prefix_largerightvaluefold. (((dc_mask_inverse_prefix_largerightvalue) = (((((dst_positive_code_inverse_prefix_largerightvaluefold) + (dst_positive_scale_inverse_prefix_largerightvaluefold)) * S ((dst_positive_code_inverse_prefix_largerightvaluefold) + (dst_positive_scale_inverse_prefix_largerightvaluefold)) + ((dst_positive_scale_inverse_prefix_largerightvaluefold) + (dst_positive_scale_inverse_prefix_largerightvaluefold))) + (((dst_negative_code_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)) * S ((dst_negative_code_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)) + ((dst_negative_scale_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)))) * S ((((dst_positive_code_inverse_prefix_largerightvaluefold) + (dst_positive_scale_inverse_prefix_largerightvaluefold)) * S ((dst_positive_code_inverse_prefix_largerightvaluefold) + (dst_positive_scale_inverse_prefix_largerightvaluefold)) + ((dst_positive_scale_inverse_prefix_largerightvaluefold) + (dst_positive_scale_inverse_prefix_largerightvaluefold))) + (((dst_negative_code_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)) * S ((dst_negative_code_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)) + ((dst_negative_scale_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)))) + ((((dst_negative_code_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)) * S ((dst_negative_code_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)) + ((dst_negative_scale_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold))) + (((dst_negative_code_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)) * S ((dst_negative_code_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)) + ((dst_negative_scale_inverse_prefix_largerightvaluefold) + (dst_negative_scale_inverse_prefix_largerightvaluefold)))))) /\ (((exists fs_u_dst_inverse_prefix_largerightvaluefoldpositive fs_v_dst_inverse_prefix_largerightvaluefoldpositive. ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_start. fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_prefix_largerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_start. fs_u_dst_inverse_prefix_largerightvaluefoldpositive = fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_prefix_largerightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_terminal. fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_prefix_largerightvaluefold) = S ((S (S (dc_input_inverse_prefix_largeright))) * fs_v_dst_inverse_prefix_largerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_terminal. fs_u_dst_inverse_prefix_largerightvaluefoldpositive = fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_prefix_largeright))) * fs_v_dst_inverse_prefix_largerightvaluefoldpositive) + (dst_positive_sum_inverse_prefix_largerightvaluefold))) /\ forall fs_i_dst_inverse_prefix_largerightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_prefix_largerightvaluefoldpositive_body_steps = S (dc_input_inverse_prefix_largeright)) -> exists fs_a_dst_inverse_prefix_largerightvaluefoldpositive_body_steps fs_r_dst_inverse_prefix_largerightvaluefoldpositive_body_steps fs_s_dst_inverse_prefix_largerightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_prefix_largerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_prefix_largerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_prefix_largerightvaluefold)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_prefix_largerightvaluefold = fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_prefix_largerightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_prefix_largerightvaluefold) + (fs_a_dst_inverse_prefix_largerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_prefix_largerightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_prefix_largerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_largerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_prefix_largerightvaluefoldpositive = fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_prefix_largerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_largerightvaluefoldpositive) + (fs_r_dst_inverse_prefix_largerightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_prefix_largerightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_prefix_largerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_largerightvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_prefix_largerightvaluefoldpositive = fs_q_dst_inverse_prefix_largerightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_prefix_largerightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_largerightvaluefoldpositive) + (fs_s_dst_inverse_prefix_largerightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_prefix_largerightvaluefoldpositive_body_steps = fs_r_dst_inverse_prefix_largerightvaluefoldpositive_body_steps + fs_a_dst_inverse_prefix_largerightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_prefix_largerightvaluefoldnegative fs_v_dst_inverse_prefix_largerightvaluefoldnegative. ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_start. fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_prefix_largerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_start. fs_u_dst_inverse_prefix_largerightvaluefoldnegative = fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_prefix_largerightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_terminal. fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_prefix_largerightvaluefold) = S ((S (S (dc_input_inverse_prefix_largeright))) * fs_v_dst_inverse_prefix_largerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_terminal. fs_u_dst_inverse_prefix_largerightvaluefoldnegative = fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_prefix_largeright))) * fs_v_dst_inverse_prefix_largerightvaluefoldnegative) + (dst_negative_sum_inverse_prefix_largerightvaluefold))) /\ forall fs_i_dst_inverse_prefix_largerightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_prefix_largerightvaluefoldnegative_body_steps = S (dc_input_inverse_prefix_largeright)) -> exists fs_a_dst_inverse_prefix_largerightvaluefoldnegative_body_steps fs_r_dst_inverse_prefix_largerightvaluefoldnegative_body_steps fs_s_dst_inverse_prefix_largerightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_prefix_largerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_prefix_largerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_prefix_largerightvaluefold)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_prefix_largerightvaluefold = fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_prefix_largerightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_prefix_largerightvaluefold) + (fs_a_dst_inverse_prefix_largerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_prefix_largerightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_prefix_largerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_largerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_prefix_largerightvaluefoldnegative = fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_prefix_largerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_largerightvaluefoldnegative) + (fs_r_dst_inverse_prefix_largerightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_prefix_largerightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_prefix_largerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_largerightvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_prefix_largerightvaluefoldnegative = fs_q_dst_inverse_prefix_largerightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_prefix_largerightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_largerightvaluefoldnegative) + (fs_s_dst_inverse_prefix_largerightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_prefix_largerightvaluefoldnegative_body_steps = fs_r_dst_inverse_prefix_largerightvaluefoldnegative_body_steps + fs_a_dst_inverse_prefix_largerightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_prefix_largerightvaluefoldresult ge_balance_negative_inverse_prefix_largerightvaluefoldresult. (((((dc_output_inverse_prefix_largeright) = 2 * (ge_balance_positive_inverse_prefix_largerightvaluefoldresult) /\ (ge_balance_negative_inverse_prefix_largerightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_prefix_largerightvaluefoldresultdecode. (((dc_output_inverse_prefix_largeright) = 2 * ge_signed_half_inverse_prefix_largerightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_prefix_largerightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_prefix_largerightvaluefoldresult) = S ge_signed_half_inverse_prefix_largerightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_prefix_largerightvaluefold) + ge_balance_negative_inverse_prefix_largerightvaluefoldresult = (dst_negative_sum_inverse_prefix_largerightvaluefold) + ge_balance_positive_inverse_prefix_largerightvaluefoldresult)))))))))))))))))))))))) -> (exists di_delta_inverse_prefix_small. ((((exists dst_positive_code_inverse_prefix_smalldeltatable dst_positive_scale_inverse_prefix_smalldeltatable dst_negative_code_inverse_prefix_smalldeltatable dst_negative_scale_inverse_prefix_smalldeltatable. (((di_delta_inverse_prefix_small) = (((((dst_positive_code_inverse_prefix_smalldeltatable) + (dst_positive_scale_inverse_prefix_smalldeltatable)) * S ((dst_positive_code_inverse_prefix_smalldeltatable) + (dst_positive_scale_inverse_prefix_smalldeltatable)) + ((dst_positive_scale_inverse_prefix_smalldeltatable) + (dst_positive_scale_inverse_prefix_smalldeltatable))) + (((dst_negative_code_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)) * S ((dst_negative_code_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)) + ((dst_negative_scale_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)))) * S ((((dst_positive_code_inverse_prefix_smalldeltatable) + (dst_positive_scale_inverse_prefix_smalldeltatable)) * S ((dst_positive_code_inverse_prefix_smalldeltatable) + (dst_positive_scale_inverse_prefix_smalldeltatable)) + ((dst_positive_scale_inverse_prefix_smalldeltatable) + (dst_positive_scale_inverse_prefix_smalldeltatable))) + (((dst_negative_code_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)) * S ((dst_negative_code_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)) + ((dst_negative_scale_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)))) + ((((dst_negative_code_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)) * S ((dst_negative_code_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)) + ((dst_negative_scale_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable))) + (((dst_negative_code_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)) * S ((dst_negative_code_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)) + ((dst_negative_scale_inverse_prefix_smalldeltatable) + (dst_negative_scale_inverse_prefix_smalldeltatable)))))) /\ (forall dst_index_inverse_prefix_smalldeltatable. (exists pvs_le_gap_inverse_prefix_smalldeltatabledomain. pvs_le_gap_inverse_prefix_smalldeltatabledomain + (dst_index_inverse_prefix_smalldeltatable) = (K)) -> exists dst_positive_inverse_prefix_smalldeltatable dst_negative_inverse_prefix_smalldeltatable dst_value_inverse_prefix_smalldeltatable. ((((exists ff_h_pvs_inverse_prefix_smalldeltatableentrypositive. ff_h_pvs_inverse_prefix_smalldeltatableentrypositive + S (dst_positive_inverse_prefix_smalldeltatable) = S ((S (dst_index_inverse_prefix_smalldeltatable)) * dst_positive_scale_inverse_prefix_smalldeltatable)) /\ exists ff_q_pvs_inverse_prefix_smalldeltatableentrypositive. dst_positive_code_inverse_prefix_smalldeltatable = ff_q_pvs_inverse_prefix_smalldeltatableentrypositive * S ((S (dst_index_inverse_prefix_smalldeltatable)) * dst_positive_scale_inverse_prefix_smalldeltatable) + (dst_positive_inverse_prefix_smalldeltatable))) /\ (((((exists ff_h_pvs_inverse_prefix_smalldeltatableentrynegative. ff_h_pvs_inverse_prefix_smalldeltatableentrynegative + S (dst_negative_inverse_prefix_smalldeltatable) = S ((S (dst_index_inverse_prefix_smalldeltatable)) * dst_negative_scale_inverse_prefix_smalldeltatable)) /\ exists ff_q_pvs_inverse_prefix_smalldeltatableentrynegative. dst_negative_code_inverse_prefix_smalldeltatable = ff_q_pvs_inverse_prefix_smalldeltatableentrynegative * S ((S (dst_index_inverse_prefix_smalldeltatable)) * dst_negative_scale_inverse_prefix_smalldeltatable) + (dst_negative_inverse_prefix_smalldeltatable))) /\ (exists ge_balance_positive_inverse_prefix_smalldeltatableentryvalue ge_balance_negative_inverse_prefix_smalldeltatableentryvalue. (((((dst_value_inverse_prefix_smalldeltatable) = 2 * (ge_balance_positive_inverse_prefix_smalldeltatableentryvalue) /\ (ge_balance_negative_inverse_prefix_smalldeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smalldeltatableentryvaluedecode. (((dst_value_inverse_prefix_smalldeltatable) = 2 * ge_signed_half_inverse_prefix_smalldeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smalldeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smalldeltatableentryvalue) = S ge_signed_half_inverse_prefix_smalldeltatableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smalldeltatable) + ge_balance_negative_inverse_prefix_smalldeltatableentryvalue = (dst_negative_inverse_prefix_smalldeltatable) + ge_balance_positive_inverse_prefix_smalldeltatableentryvalue))))))))) /\ (forall du_index_inverse_prefix_smalldelta du_value_inverse_prefix_smalldelta. ~(du_index_inverse_prefix_smalldelta=0) -> (exists pvs_le_gap_inverse_prefix_smalldeltabound. pvs_le_gap_inverse_prefix_smalldeltabound + (du_index_inverse_prefix_smalldelta) = (K)) -> (exists dst_positive_code_inverse_prefix_smalldeltaentry dst_positive_scale_inverse_prefix_smalldeltaentry dst_negative_code_inverse_prefix_smalldeltaentry dst_negative_scale_inverse_prefix_smalldeltaentry dst_positive_inverse_prefix_smalldeltaentry dst_negative_inverse_prefix_smalldeltaentry. (((di_delta_inverse_prefix_small) = (((((dst_positive_code_inverse_prefix_smalldeltaentry) + (dst_positive_scale_inverse_prefix_smalldeltaentry)) * S ((dst_positive_code_inverse_prefix_smalldeltaentry) + (dst_positive_scale_inverse_prefix_smalldeltaentry)) + ((dst_positive_scale_inverse_prefix_smalldeltaentry) + (dst_positive_scale_inverse_prefix_smalldeltaentry))) + (((dst_negative_code_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)) * S ((dst_negative_code_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)) + ((dst_negative_scale_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)))) * S ((((dst_positive_code_inverse_prefix_smalldeltaentry) + (dst_positive_scale_inverse_prefix_smalldeltaentry)) * S ((dst_positive_code_inverse_prefix_smalldeltaentry) + (dst_positive_scale_inverse_prefix_smalldeltaentry)) + ((dst_positive_scale_inverse_prefix_smalldeltaentry) + (dst_positive_scale_inverse_prefix_smalldeltaentry))) + (((dst_negative_code_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)) * S ((dst_negative_code_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)) + ((dst_negative_scale_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)))) + ((((dst_negative_code_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)) * S ((dst_negative_code_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)) + ((dst_negative_scale_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry))) + (((dst_negative_code_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)) * S ((dst_negative_code_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)) + ((dst_negative_scale_inverse_prefix_smalldeltaentry) + (dst_negative_scale_inverse_prefix_smalldeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smalldeltaentrypositive. ff_h_pvs_inverse_prefix_smalldeltaentrypositive + S (dst_positive_inverse_prefix_smalldeltaentry) = S ((S (du_index_inverse_prefix_smalldelta)) * dst_positive_scale_inverse_prefix_smalldeltaentry)) /\ exists ff_q_pvs_inverse_prefix_smalldeltaentrypositive. dst_positive_code_inverse_prefix_smalldeltaentry = ff_q_pvs_inverse_prefix_smalldeltaentrypositive * S ((S (du_index_inverse_prefix_smalldelta)) * dst_positive_scale_inverse_prefix_smalldeltaentry) + (dst_positive_inverse_prefix_smalldeltaentry))) /\ (((((exists ff_h_pvs_inverse_prefix_smalldeltaentrynegative. ff_h_pvs_inverse_prefix_smalldeltaentrynegative + S (dst_negative_inverse_prefix_smalldeltaentry) = S ((S (du_index_inverse_prefix_smalldelta)) * dst_negative_scale_inverse_prefix_smalldeltaentry)) /\ exists ff_q_pvs_inverse_prefix_smalldeltaentrynegative. dst_negative_code_inverse_prefix_smalldeltaentry = ff_q_pvs_inverse_prefix_smalldeltaentrynegative * S ((S (du_index_inverse_prefix_smalldelta)) * dst_negative_scale_inverse_prefix_smalldeltaentry) + (dst_negative_inverse_prefix_smalldeltaentry))) /\ (exists ge_balance_positive_inverse_prefix_smalldeltaentryvalue ge_balance_negative_inverse_prefix_smalldeltaentryvalue. (((((du_value_inverse_prefix_smalldelta) = 2 * (ge_balance_positive_inverse_prefix_smalldeltaentryvalue) /\ (ge_balance_negative_inverse_prefix_smalldeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smalldeltaentryvaluedecode. (((du_value_inverse_prefix_smalldelta) = 2 * ge_signed_half_inverse_prefix_smalldeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smalldeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smalldeltaentryvalue) = S ge_signed_half_inverse_prefix_smalldeltaentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smalldeltaentry) + ge_balance_negative_inverse_prefix_smalldeltaentryvalue = (dst_negative_inverse_prefix_smalldeltaentry) + ge_balance_positive_inverse_prefix_smalldeltaentryvalue))))))))) -> ((((du_index_inverse_prefix_smalldelta)=1 -> (du_value_inverse_prefix_smalldelta)=2) /\ (~((du_index_inverse_prefix_smalldelta)=1) -> (du_value_inverse_prefix_smalldelta)=0)))))) /\ (((((exists dst_positive_code_inverse_prefix_smallleftleft dst_positive_scale_inverse_prefix_smallleftleft dst_negative_code_inverse_prefix_smallleftleft dst_negative_scale_inverse_prefix_smallleftleft. (((F) = (((((dst_positive_code_inverse_prefix_smallleftleft) + (dst_positive_scale_inverse_prefix_smallleftleft)) * S ((dst_positive_code_inverse_prefix_smallleftleft) + (dst_positive_scale_inverse_prefix_smallleftleft)) + ((dst_positive_scale_inverse_prefix_smallleftleft) + (dst_positive_scale_inverse_prefix_smallleftleft))) + (((dst_negative_code_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)) * S ((dst_negative_code_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)) + ((dst_negative_scale_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)))) * S ((((dst_positive_code_inverse_prefix_smallleftleft) + (dst_positive_scale_inverse_prefix_smallleftleft)) * S ((dst_positive_code_inverse_prefix_smallleftleft) + (dst_positive_scale_inverse_prefix_smallleftleft)) + ((dst_positive_scale_inverse_prefix_smallleftleft) + (dst_positive_scale_inverse_prefix_smallleftleft))) + (((dst_negative_code_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)) * S ((dst_negative_code_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)) + ((dst_negative_scale_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)))) + ((((dst_negative_code_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)) * S ((dst_negative_code_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)) + ((dst_negative_scale_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft))) + (((dst_negative_code_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)) * S ((dst_negative_code_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)) + ((dst_negative_scale_inverse_prefix_smallleftleft) + (dst_negative_scale_inverse_prefix_smallleftleft)))))) /\ (forall dst_index_inverse_prefix_smallleftleft. (exists pvs_le_gap_inverse_prefix_smallleftleftdomain. pvs_le_gap_inverse_prefix_smallleftleftdomain + (dst_index_inverse_prefix_smallleftleft) = (K)) -> exists dst_positive_inverse_prefix_smallleftleft dst_negative_inverse_prefix_smallleftleft dst_value_inverse_prefix_smallleftleft. ((((exists ff_h_pvs_inverse_prefix_smallleftleftentrypositive. ff_h_pvs_inverse_prefix_smallleftleftentrypositive + S (dst_positive_inverse_prefix_smallleftleft) = S ((S (dst_index_inverse_prefix_smallleftleft)) * dst_positive_scale_inverse_prefix_smallleftleft)) /\ exists ff_q_pvs_inverse_prefix_smallleftleftentrypositive. dst_positive_code_inverse_prefix_smallleftleft = ff_q_pvs_inverse_prefix_smallleftleftentrypositive * S ((S (dst_index_inverse_prefix_smallleftleft)) * dst_positive_scale_inverse_prefix_smallleftleft) + (dst_positive_inverse_prefix_smallleftleft))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftleftentrynegative. ff_h_pvs_inverse_prefix_smallleftleftentrynegative + S (dst_negative_inverse_prefix_smallleftleft) = S ((S (dst_index_inverse_prefix_smallleftleft)) * dst_negative_scale_inverse_prefix_smallleftleft)) /\ exists ff_q_pvs_inverse_prefix_smallleftleftentrynegative. dst_negative_code_inverse_prefix_smallleftleft = ff_q_pvs_inverse_prefix_smallleftleftentrynegative * S ((S (dst_index_inverse_prefix_smallleftleft)) * dst_negative_scale_inverse_prefix_smallleftleft) + (dst_negative_inverse_prefix_smallleftleft))) /\ (exists ge_balance_positive_inverse_prefix_smallleftleftentryvalue ge_balance_negative_inverse_prefix_smallleftleftentryvalue. (((((dst_value_inverse_prefix_smallleftleft) = 2 * (ge_balance_positive_inverse_prefix_smallleftleftentryvalue) /\ (ge_balance_negative_inverse_prefix_smallleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftleftentryvaluedecode. (((dst_value_inverse_prefix_smallleftleft) = 2 * ge_signed_half_inverse_prefix_smallleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallleftleftentryvalue) = S ge_signed_half_inverse_prefix_smallleftleftentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smallleftleft) + ge_balance_negative_inverse_prefix_smallleftleftentryvalue = (dst_negative_inverse_prefix_smallleftleft) + ge_balance_positive_inverse_prefix_smallleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_smallleftright dst_positive_scale_inverse_prefix_smallleftright dst_negative_code_inverse_prefix_smallleftright dst_negative_scale_inverse_prefix_smallleftright. (((H) = (((((dst_positive_code_inverse_prefix_smallleftright) + (dst_positive_scale_inverse_prefix_smallleftright)) * S ((dst_positive_code_inverse_prefix_smallleftright) + (dst_positive_scale_inverse_prefix_smallleftright)) + ((dst_positive_scale_inverse_prefix_smallleftright) + (dst_positive_scale_inverse_prefix_smallleftright))) + (((dst_negative_code_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)) * S ((dst_negative_code_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)) + ((dst_negative_scale_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)))) * S ((((dst_positive_code_inverse_prefix_smallleftright) + (dst_positive_scale_inverse_prefix_smallleftright)) * S ((dst_positive_code_inverse_prefix_smallleftright) + (dst_positive_scale_inverse_prefix_smallleftright)) + ((dst_positive_scale_inverse_prefix_smallleftright) + (dst_positive_scale_inverse_prefix_smallleftright))) + (((dst_negative_code_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)) * S ((dst_negative_code_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)) + ((dst_negative_scale_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)))) + ((((dst_negative_code_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)) * S ((dst_negative_code_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)) + ((dst_negative_scale_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright))) + (((dst_negative_code_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)) * S ((dst_negative_code_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)) + ((dst_negative_scale_inverse_prefix_smallleftright) + (dst_negative_scale_inverse_prefix_smallleftright)))))) /\ (forall dst_index_inverse_prefix_smallleftright. (exists pvs_le_gap_inverse_prefix_smallleftrightdomain. pvs_le_gap_inverse_prefix_smallleftrightdomain + (dst_index_inverse_prefix_smallleftright) = (K)) -> exists dst_positive_inverse_prefix_smallleftright dst_negative_inverse_prefix_smallleftright dst_value_inverse_prefix_smallleftright. ((((exists ff_h_pvs_inverse_prefix_smallleftrightentrypositive. ff_h_pvs_inverse_prefix_smallleftrightentrypositive + S (dst_positive_inverse_prefix_smallleftright) = S ((S (dst_index_inverse_prefix_smallleftright)) * dst_positive_scale_inverse_prefix_smallleftright)) /\ exists ff_q_pvs_inverse_prefix_smallleftrightentrypositive. dst_positive_code_inverse_prefix_smallleftright = ff_q_pvs_inverse_prefix_smallleftrightentrypositive * S ((S (dst_index_inverse_prefix_smallleftright)) * dst_positive_scale_inverse_prefix_smallleftright) + (dst_positive_inverse_prefix_smallleftright))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftrightentrynegative. ff_h_pvs_inverse_prefix_smallleftrightentrynegative + S (dst_negative_inverse_prefix_smallleftright) = S ((S (dst_index_inverse_prefix_smallleftright)) * dst_negative_scale_inverse_prefix_smallleftright)) /\ exists ff_q_pvs_inverse_prefix_smallleftrightentrynegative. dst_negative_code_inverse_prefix_smallleftright = ff_q_pvs_inverse_prefix_smallleftrightentrynegative * S ((S (dst_index_inverse_prefix_smallleftright)) * dst_negative_scale_inverse_prefix_smallleftright) + (dst_negative_inverse_prefix_smallleftright))) /\ (exists ge_balance_positive_inverse_prefix_smallleftrightentryvalue ge_balance_negative_inverse_prefix_smallleftrightentryvalue. (((((dst_value_inverse_prefix_smallleftright) = 2 * (ge_balance_positive_inverse_prefix_smallleftrightentryvalue) /\ (ge_balance_negative_inverse_prefix_smallleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftrightentryvaluedecode. (((dst_value_inverse_prefix_smallleftright) = 2 * ge_signed_half_inverse_prefix_smallleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallleftrightentryvalue) = S ge_signed_half_inverse_prefix_smallleftrightentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smallleftright) + ge_balance_negative_inverse_prefix_smallleftrightentryvalue = (dst_negative_inverse_prefix_smallleftright) + ge_balance_positive_inverse_prefix_smallleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_smalllefttable dst_positive_scale_inverse_prefix_smalllefttable dst_negative_code_inverse_prefix_smalllefttable dst_negative_scale_inverse_prefix_smalllefttable. (((di_delta_inverse_prefix_small) = (((((dst_positive_code_inverse_prefix_smalllefttable) + (dst_positive_scale_inverse_prefix_smalllefttable)) * S ((dst_positive_code_inverse_prefix_smalllefttable) + (dst_positive_scale_inverse_prefix_smalllefttable)) + ((dst_positive_scale_inverse_prefix_smalllefttable) + (dst_positive_scale_inverse_prefix_smalllefttable))) + (((dst_negative_code_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)) * S ((dst_negative_code_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)) + ((dst_negative_scale_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)))) * S ((((dst_positive_code_inverse_prefix_smalllefttable) + (dst_positive_scale_inverse_prefix_smalllefttable)) * S ((dst_positive_code_inverse_prefix_smalllefttable) + (dst_positive_scale_inverse_prefix_smalllefttable)) + ((dst_positive_scale_inverse_prefix_smalllefttable) + (dst_positive_scale_inverse_prefix_smalllefttable))) + (((dst_negative_code_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)) * S ((dst_negative_code_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)) + ((dst_negative_scale_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)))) + ((((dst_negative_code_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)) * S ((dst_negative_code_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)) + ((dst_negative_scale_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable))) + (((dst_negative_code_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)) * S ((dst_negative_code_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)) + ((dst_negative_scale_inverse_prefix_smalllefttable) + (dst_negative_scale_inverse_prefix_smalllefttable)))))) /\ (forall dst_index_inverse_prefix_smalllefttable. (exists pvs_le_gap_inverse_prefix_smalllefttabledomain. pvs_le_gap_inverse_prefix_smalllefttabledomain + (dst_index_inverse_prefix_smalllefttable) = (K)) -> exists dst_positive_inverse_prefix_smalllefttable dst_negative_inverse_prefix_smalllefttable dst_value_inverse_prefix_smalllefttable. ((((exists ff_h_pvs_inverse_prefix_smalllefttableentrypositive. ff_h_pvs_inverse_prefix_smalllefttableentrypositive + S (dst_positive_inverse_prefix_smalllefttable) = S ((S (dst_index_inverse_prefix_smalllefttable)) * dst_positive_scale_inverse_prefix_smalllefttable)) /\ exists ff_q_pvs_inverse_prefix_smalllefttableentrypositive. dst_positive_code_inverse_prefix_smalllefttable = ff_q_pvs_inverse_prefix_smalllefttableentrypositive * S ((S (dst_index_inverse_prefix_smalllefttable)) * dst_positive_scale_inverse_prefix_smalllefttable) + (dst_positive_inverse_prefix_smalllefttable))) /\ (((((exists ff_h_pvs_inverse_prefix_smalllefttableentrynegative. ff_h_pvs_inverse_prefix_smalllefttableentrynegative + S (dst_negative_inverse_prefix_smalllefttable) = S ((S (dst_index_inverse_prefix_smalllefttable)) * dst_negative_scale_inverse_prefix_smalllefttable)) /\ exists ff_q_pvs_inverse_prefix_smalllefttableentrynegative. dst_negative_code_inverse_prefix_smalllefttable = ff_q_pvs_inverse_prefix_smalllefttableentrynegative * S ((S (dst_index_inverse_prefix_smalllefttable)) * dst_negative_scale_inverse_prefix_smalllefttable) + (dst_negative_inverse_prefix_smalllefttable))) /\ (exists ge_balance_positive_inverse_prefix_smalllefttableentryvalue ge_balance_negative_inverse_prefix_smalllefttableentryvalue. (((((dst_value_inverse_prefix_smalllefttable) = 2 * (ge_balance_positive_inverse_prefix_smalllefttableentryvalue) /\ (ge_balance_negative_inverse_prefix_smalllefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smalllefttableentryvaluedecode. (((dst_value_inverse_prefix_smalllefttable) = 2 * ge_signed_half_inverse_prefix_smalllefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smalllefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smalllefttableentryvalue) = S ge_signed_half_inverse_prefix_smalllefttableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smalllefttable) + ge_balance_negative_inverse_prefix_smalllefttableentryvalue = (dst_negative_inverse_prefix_smalllefttable) + ge_balance_positive_inverse_prefix_smalllefttableentryvalue))))))))) /\ (forall dc_input_inverse_prefix_smallleft dc_output_inverse_prefix_smallleft. ~(dc_input_inverse_prefix_smallleft=0) -> (exists pvs_le_gap_inverse_prefix_smallleftdomain. pvs_le_gap_inverse_prefix_smallleftdomain + (dc_input_inverse_prefix_smallleft) = (K)) -> (exists dst_positive_code_inverse_prefix_smallleftlookup dst_positive_scale_inverse_prefix_smallleftlookup dst_negative_code_inverse_prefix_smallleftlookup dst_negative_scale_inverse_prefix_smallleftlookup dst_positive_inverse_prefix_smallleftlookup dst_negative_inverse_prefix_smallleftlookup. (((di_delta_inverse_prefix_small) = (((((dst_positive_code_inverse_prefix_smallleftlookup) + (dst_positive_scale_inverse_prefix_smallleftlookup)) * S ((dst_positive_code_inverse_prefix_smallleftlookup) + (dst_positive_scale_inverse_prefix_smallleftlookup)) + ((dst_positive_scale_inverse_prefix_smallleftlookup) + (dst_positive_scale_inverse_prefix_smallleftlookup))) + (((dst_negative_code_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)) * S ((dst_negative_code_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)) + ((dst_negative_scale_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)))) * S ((((dst_positive_code_inverse_prefix_smallleftlookup) + (dst_positive_scale_inverse_prefix_smallleftlookup)) * S ((dst_positive_code_inverse_prefix_smallleftlookup) + (dst_positive_scale_inverse_prefix_smallleftlookup)) + ((dst_positive_scale_inverse_prefix_smallleftlookup) + (dst_positive_scale_inverse_prefix_smallleftlookup))) + (((dst_negative_code_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)) * S ((dst_negative_code_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)) + ((dst_negative_scale_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)))) + ((((dst_negative_code_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)) * S ((dst_negative_code_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)) + ((dst_negative_scale_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup))) + (((dst_negative_code_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)) * S ((dst_negative_code_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)) + ((dst_negative_scale_inverse_prefix_smallleftlookup) + (dst_negative_scale_inverse_prefix_smallleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftlookuppositive. ff_h_pvs_inverse_prefix_smallleftlookuppositive + S (dst_positive_inverse_prefix_smallleftlookup) = S ((S (dc_input_inverse_prefix_smallleft)) * dst_positive_scale_inverse_prefix_smallleftlookup)) /\ exists ff_q_pvs_inverse_prefix_smallleftlookuppositive. dst_positive_code_inverse_prefix_smallleftlookup = ff_q_pvs_inverse_prefix_smallleftlookuppositive * S ((S (dc_input_inverse_prefix_smallleft)) * dst_positive_scale_inverse_prefix_smallleftlookup) + (dst_positive_inverse_prefix_smallleftlookup))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftlookupnegative. ff_h_pvs_inverse_prefix_smallleftlookupnegative + S (dst_negative_inverse_prefix_smallleftlookup) = S ((S (dc_input_inverse_prefix_smallleft)) * dst_negative_scale_inverse_prefix_smallleftlookup)) /\ exists ff_q_pvs_inverse_prefix_smallleftlookupnegative. dst_negative_code_inverse_prefix_smallleftlookup = ff_q_pvs_inverse_prefix_smallleftlookupnegative * S ((S (dc_input_inverse_prefix_smallleft)) * dst_negative_scale_inverse_prefix_smallleftlookup) + (dst_negative_inverse_prefix_smallleftlookup))) /\ (exists ge_balance_positive_inverse_prefix_smallleftlookupvalue ge_balance_negative_inverse_prefix_smallleftlookupvalue. (((((dc_output_inverse_prefix_smallleft) = 2 * (ge_balance_positive_inverse_prefix_smallleftlookupvalue) /\ (ge_balance_negative_inverse_prefix_smallleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftlookupvaluedecode. (((dc_output_inverse_prefix_smallleft) = 2 * ge_signed_half_inverse_prefix_smallleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallleftlookupvalue) = S ge_signed_half_inverse_prefix_smallleftlookupvaluedecode))) /\ ((dst_positive_inverse_prefix_smallleftlookup) + ge_balance_negative_inverse_prefix_smallleftlookupvalue = (dst_negative_inverse_prefix_smallleftlookup) + ge_balance_positive_inverse_prefix_smallleftlookupvalue))))))))) -> (((~((dc_input_inverse_prefix_smallleft)=0)) /\ (exists dc_mask_inverse_prefix_smallleftvalue. ((((exists dst_positive_code_inverse_prefix_smallleftvaluemasktable dst_positive_scale_inverse_prefix_smallleftvaluemasktable dst_negative_code_inverse_prefix_smallleftvaluemasktable dst_negative_scale_inverse_prefix_smallleftvaluemasktable. (((dc_mask_inverse_prefix_smallleftvalue) = (((((dst_positive_code_inverse_prefix_smallleftvaluemasktable) + (dst_positive_scale_inverse_prefix_smallleftvaluemasktable)) * S ((dst_positive_code_inverse_prefix_smallleftvaluemasktable) + (dst_positive_scale_inverse_prefix_smallleftvaluemasktable)) + ((dst_positive_scale_inverse_prefix_smallleftvaluemasktable) + (dst_positive_scale_inverse_prefix_smallleftvaluemasktable))) + (((dst_negative_code_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)))) * S ((((dst_positive_code_inverse_prefix_smallleftvaluemasktable) + (dst_positive_scale_inverse_prefix_smallleftvaluemasktable)) * S ((dst_positive_code_inverse_prefix_smallleftvaluemasktable) + (dst_positive_scale_inverse_prefix_smallleftvaluemasktable)) + ((dst_positive_scale_inverse_prefix_smallleftvaluemasktable) + (dst_positive_scale_inverse_prefix_smallleftvaluemasktable))) + (((dst_negative_code_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)))) + ((((dst_negative_code_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable))) + (((dst_negative_code_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemasktable) + (dst_negative_scale_inverse_prefix_smallleftvaluemasktable)))))) /\ (forall dst_index_inverse_prefix_smallleftvaluemasktable. (exists pvs_le_gap_inverse_prefix_smallleftvaluemasktabledomain. pvs_le_gap_inverse_prefix_smallleftvaluemasktabledomain + (dst_index_inverse_prefix_smallleftvaluemasktable) = (dc_input_inverse_prefix_smallleft)) -> exists dst_positive_inverse_prefix_smallleftvaluemasktable dst_negative_inverse_prefix_smallleftvaluemasktable dst_value_inverse_prefix_smallleftvaluemasktable. ((((exists ff_h_pvs_inverse_prefix_smallleftvaluemasktableentrypositive. ff_h_pvs_inverse_prefix_smallleftvaluemasktableentrypositive + S (dst_positive_inverse_prefix_smallleftvaluemasktable) = S ((S (dst_index_inverse_prefix_smallleftvaluemasktable)) * dst_positive_scale_inverse_prefix_smallleftvaluemasktable)) /\ exists ff_q_pvs_inverse_prefix_smallleftvaluemasktableentrypositive. dst_positive_code_inverse_prefix_smallleftvaluemasktable = ff_q_pvs_inverse_prefix_smallleftvaluemasktableentrypositive * S ((S (dst_index_inverse_prefix_smallleftvaluemasktable)) * dst_positive_scale_inverse_prefix_smallleftvaluemasktable) + (dst_positive_inverse_prefix_smallleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftvaluemasktableentrynegative. ff_h_pvs_inverse_prefix_smallleftvaluemasktableentrynegative + S (dst_negative_inverse_prefix_smallleftvaluemasktable) = S ((S (dst_index_inverse_prefix_smallleftvaluemasktable)) * dst_negative_scale_inverse_prefix_smallleftvaluemasktable)) /\ exists ff_q_pvs_inverse_prefix_smallleftvaluemasktableentrynegative. dst_negative_code_inverse_prefix_smallleftvaluemasktable = ff_q_pvs_inverse_prefix_smallleftvaluemasktableentrynegative * S ((S (dst_index_inverse_prefix_smallleftvaluemasktable)) * dst_negative_scale_inverse_prefix_smallleftvaluemasktable) + (dst_negative_inverse_prefix_smallleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_prefix_smallleftvaluemasktableentryvalue ge_balance_negative_inverse_prefix_smallleftvaluemasktableentryvalue. (((((dst_value_inverse_prefix_smallleftvaluemasktable) = 2 * (ge_balance_positive_inverse_prefix_smallleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_prefix_smallleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftvaluemasktableentryvaluedecode. (((dst_value_inverse_prefix_smallleftvaluemasktable) = 2 * ge_signed_half_inverse_prefix_smallleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallleftvaluemasktableentryvalue) = S ge_signed_half_inverse_prefix_smallleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smallleftvaluemasktable) + ge_balance_negative_inverse_prefix_smallleftvaluemasktableentryvalue = (dst_negative_inverse_prefix_smallleftvaluemasktable) + ge_balance_positive_inverse_prefix_smallleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_prefix_smallleftvaluemask dc_value_inverse_prefix_smallleftvaluemask. (exists pvs_le_gap_inverse_prefix_smallleftvaluemaskdomain. pvs_le_gap_inverse_prefix_smallleftvaluemaskdomain + (dc_index_inverse_prefix_smallleftvaluemask) = (dc_input_inverse_prefix_smallleft)) -> (exists dst_positive_code_inverse_prefix_smallleftvaluemasklookup dst_positive_scale_inverse_prefix_smallleftvaluemasklookup dst_negative_code_inverse_prefix_smallleftvaluemasklookup dst_negative_scale_inverse_prefix_smallleftvaluemasklookup dst_positive_inverse_prefix_smallleftvaluemasklookup dst_negative_inverse_prefix_smallleftvaluemasklookup. (((dc_mask_inverse_prefix_smallleftvalue) = (((((dst_positive_code_inverse_prefix_smallleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallleftvaluemasklookup)) * S ((dst_positive_code_inverse_prefix_smallleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallleftvaluemasklookup)) + ((dst_positive_scale_inverse_prefix_smallleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallleftvaluemasklookup))) + (((dst_negative_code_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_prefix_smallleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallleftvaluemasklookup)) * S ((dst_positive_code_inverse_prefix_smallleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallleftvaluemasklookup)) + ((dst_positive_scale_inverse_prefix_smallleftvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallleftvaluemasklookup))) + (((dst_negative_code_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)))) + ((((dst_negative_code_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup))) + (((dst_negative_code_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftvaluemasklookuppositive. ff_h_pvs_inverse_prefix_smallleftvaluemasklookuppositive + S (dst_positive_inverse_prefix_smallleftvaluemasklookup) = S ((S (dc_index_inverse_prefix_smallleftvaluemask)) * dst_positive_scale_inverse_prefix_smallleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_prefix_smallleftvaluemasklookuppositive. dst_positive_code_inverse_prefix_smallleftvaluemasklookup = ff_q_pvs_inverse_prefix_smallleftvaluemasklookuppositive * S ((S (dc_index_inverse_prefix_smallleftvaluemask)) * dst_positive_scale_inverse_prefix_smallleftvaluemasklookup) + (dst_positive_inverse_prefix_smallleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftvaluemasklookupnegative. ff_h_pvs_inverse_prefix_smallleftvaluemasklookupnegative + S (dst_negative_inverse_prefix_smallleftvaluemasklookup) = S ((S (dc_index_inverse_prefix_smallleftvaluemask)) * dst_negative_scale_inverse_prefix_smallleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_prefix_smallleftvaluemasklookupnegative. dst_negative_code_inverse_prefix_smallleftvaluemasklookup = ff_q_pvs_inverse_prefix_smallleftvaluemasklookupnegative * S ((S (dc_index_inverse_prefix_smallleftvaluemask)) * dst_negative_scale_inverse_prefix_smallleftvaluemasklookup) + (dst_negative_inverse_prefix_smallleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_prefix_smallleftvaluemasklookupvalue ge_balance_negative_inverse_prefix_smallleftvaluemasklookupvalue. (((((dc_value_inverse_prefix_smallleftvaluemask) = 2 * (ge_balance_positive_inverse_prefix_smallleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_prefix_smallleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftvaluemasklookupvaluedecode. (((dc_value_inverse_prefix_smallleftvaluemask) = 2 * ge_signed_half_inverse_prefix_smallleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallleftvaluemasklookupvalue) = S ge_signed_half_inverse_prefix_smallleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_prefix_smallleftvaluemasklookup) + ge_balance_negative_inverse_prefix_smallleftvaluemasklookupvalue = (dst_negative_inverse_prefix_smallleftvaluemasklookup) + ge_balance_positive_inverse_prefix_smallleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_prefix_smallleftvaluemask)=0)) /\ (exists dc_quotient_inverse_prefix_smallleftvaluemaskentry dc_left_inverse_prefix_smallleftvaluemaskentry dc_right_inverse_prefix_smallleftvaluemaskentry. (((dc_input_inverse_prefix_smallleft)=(dc_index_inverse_prefix_smallleftvaluemask)*dc_quotient_inverse_prefix_smallleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_prefix_smallleftvaluemaskentryleft dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft dst_positive_inverse_prefix_smallleftvaluemaskentryleft dst_negative_inverse_prefix_smallleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftvaluemaskentryleftpositive. ff_h_pvs_inverse_prefix_smallleftvaluemaskentryleftpositive + S (dst_positive_inverse_prefix_smallleftvaluemaskentryleft) = S ((S (dc_index_inverse_prefix_smallleftvaluemask)) * dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_prefix_smallleftvaluemaskentryleftpositive. dst_positive_code_inverse_prefix_smallleftvaluemaskentryleft = ff_q_pvs_inverse_prefix_smallleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_prefix_smallleftvaluemask)) * dst_positive_scale_inverse_prefix_smallleftvaluemaskentryleft) + (dst_positive_inverse_prefix_smallleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftvaluemaskentryleftnegative. ff_h_pvs_inverse_prefix_smallleftvaluemaskentryleftnegative + S (dst_negative_inverse_prefix_smallleftvaluemaskentryleft) = S ((S (dc_index_inverse_prefix_smallleftvaluemask)) * dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_prefix_smallleftvaluemaskentryleftnegative. dst_negative_code_inverse_prefix_smallleftvaluemaskentryleft = ff_q_pvs_inverse_prefix_smallleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_prefix_smallleftvaluemask)) * dst_negative_scale_inverse_prefix_smallleftvaluemaskentryleft) + (dst_negative_inverse_prefix_smallleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_prefix_smallleftvaluemaskentryleftvalue ge_balance_negative_inverse_prefix_smallleftvaluemaskentryleftvalue. (((((dc_left_inverse_prefix_smallleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_prefix_smallleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_prefix_smallleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_prefix_smallleftvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_smallleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_prefix_smallleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_prefix_smallleftvaluemaskentryleft) + ge_balance_negative_inverse_prefix_smallleftvaluemaskentryleftvalue = (dst_negative_inverse_prefix_smallleftvaluemaskentryleft) + ge_balance_positive_inverse_prefix_smallleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_smallleftvaluemaskentryright dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright dst_negative_code_inverse_prefix_smallleftvaluemaskentryright dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright dst_positive_inverse_prefix_smallleftvaluemaskentryright dst_negative_inverse_prefix_smallleftvaluemaskentryright. (((H) = (((((dst_positive_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright)) * S ((dst_positive_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright)) + ((dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright)) * S ((dst_positive_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright)) + ((dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftvaluemaskentryrightpositive. ff_h_pvs_inverse_prefix_smallleftvaluemaskentryrightpositive + S (dst_positive_inverse_prefix_smallleftvaluemaskentryright) = S ((S (dc_quotient_inverse_prefix_smallleftvaluemaskentry)) * dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_prefix_smallleftvaluemaskentryrightpositive. dst_positive_code_inverse_prefix_smallleftvaluemaskentryright = ff_q_pvs_inverse_prefix_smallleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_prefix_smallleftvaluemaskentry)) * dst_positive_scale_inverse_prefix_smallleftvaluemaskentryright) + (dst_positive_inverse_prefix_smallleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_prefix_smallleftvaluemaskentryrightnegative. ff_h_pvs_inverse_prefix_smallleftvaluemaskentryrightnegative + S (dst_negative_inverse_prefix_smallleftvaluemaskentryright) = S ((S (dc_quotient_inverse_prefix_smallleftvaluemaskentry)) * dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_prefix_smallleftvaluemaskentryrightnegative. dst_negative_code_inverse_prefix_smallleftvaluemaskentryright = ff_q_pvs_inverse_prefix_smallleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_prefix_smallleftvaluemaskentry)) * dst_negative_scale_inverse_prefix_smallleftvaluemaskentryright) + (dst_negative_inverse_prefix_smallleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_prefix_smallleftvaluemaskentryrightvalue ge_balance_negative_inverse_prefix_smallleftvaluemaskentryrightvalue. (((((dc_right_inverse_prefix_smallleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_prefix_smallleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_prefix_smallleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_prefix_smallleftvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_smallleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_prefix_smallleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_prefix_smallleftvaluemaskentryright) + ge_balance_negative_inverse_prefix_smallleftvaluemaskentryrightvalue = (dst_negative_inverse_prefix_smallleftvaluemaskentryright) + ge_balance_positive_inverse_prefix_smallleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_prefix_smallleftvaluemaskentryproduct sto_an_inverse_prefix_smallleftvaluemaskentryproduct sto_bp_inverse_prefix_smallleftvaluemaskentryproduct sto_bn_inverse_prefix_smallleftvaluemaskentryproduct sto_cp_inverse_prefix_smallleftvaluemaskentryproduct sto_cn_inverse_prefix_smallleftvaluemaskentryproduct. (((((dc_left_inverse_prefix_smallleftvaluemaskentry) = 2 * (sto_ap_inverse_prefix_smallleftvaluemaskentryproduct) /\ (sto_an_inverse_prefix_smallleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductleft. (((dc_left_inverse_prefix_smallleftvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_prefix_smallleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_prefix_smallleftvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_prefix_smallleftvaluemaskentry) = 2 * (sto_bp_inverse_prefix_smallleftvaluemaskentryproduct) /\ (sto_bn_inverse_prefix_smallleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductright. (((dc_right_inverse_prefix_smallleftvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_prefix_smallleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_prefix_smallleftvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_prefix_smallleftvaluemask) = 2 * (sto_cp_inverse_prefix_smallleftvaluemaskentryproduct) /\ (sto_cn_inverse_prefix_smallleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductoutput. (((dc_value_inverse_prefix_smallleftvaluemask) = 2 * ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_prefix_smallleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_prefix_smallleftvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_smallleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_prefix_smallleftvaluemaskentryproduct * sto_bp_inverse_prefix_smallleftvaluemaskentryproduct + sto_an_inverse_prefix_smallleftvaluemaskentryproduct * sto_bn_inverse_prefix_smallleftvaluemaskentryproduct) + sto_cn_inverse_prefix_smallleftvaluemaskentryproduct = (sto_ap_inverse_prefix_smallleftvaluemaskentryproduct * sto_bn_inverse_prefix_smallleftvaluemaskentryproduct + sto_an_inverse_prefix_smallleftvaluemaskentryproduct * sto_bp_inverse_prefix_smallleftvaluemaskentryproduct) + sto_cp_inverse_prefix_smallleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_prefix_smallleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_prefix_smallleftvaluemaskentrynondivisor. (dc_input_inverse_prefix_smallleft) = (dc_index_inverse_prefix_smallleftvaluemask) * pvs_factor_inverse_prefix_smallleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_prefix_smallleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_prefix_smallleftvaluefold dst_positive_scale_inverse_prefix_smallleftvaluefold dst_negative_code_inverse_prefix_smallleftvaluefold dst_negative_scale_inverse_prefix_smallleftvaluefold dst_positive_sum_inverse_prefix_smallleftvaluefold dst_negative_sum_inverse_prefix_smallleftvaluefold. (((dc_mask_inverse_prefix_smallleftvalue) = (((((dst_positive_code_inverse_prefix_smallleftvaluefold) + (dst_positive_scale_inverse_prefix_smallleftvaluefold)) * S ((dst_positive_code_inverse_prefix_smallleftvaluefold) + (dst_positive_scale_inverse_prefix_smallleftvaluefold)) + ((dst_positive_scale_inverse_prefix_smallleftvaluefold) + (dst_positive_scale_inverse_prefix_smallleftvaluefold))) + (((dst_negative_code_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)) * S ((dst_negative_code_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)) + ((dst_negative_scale_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)))) * S ((((dst_positive_code_inverse_prefix_smallleftvaluefold) + (dst_positive_scale_inverse_prefix_smallleftvaluefold)) * S ((dst_positive_code_inverse_prefix_smallleftvaluefold) + (dst_positive_scale_inverse_prefix_smallleftvaluefold)) + ((dst_positive_scale_inverse_prefix_smallleftvaluefold) + (dst_positive_scale_inverse_prefix_smallleftvaluefold))) + (((dst_negative_code_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)) * S ((dst_negative_code_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)) + ((dst_negative_scale_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)))) + ((((dst_negative_code_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)) * S ((dst_negative_code_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)) + ((dst_negative_scale_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold))) + (((dst_negative_code_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)) * S ((dst_negative_code_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)) + ((dst_negative_scale_inverse_prefix_smallleftvaluefold) + (dst_negative_scale_inverse_prefix_smallleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_prefix_smallleftvaluefoldpositive fs_v_dst_inverse_prefix_smallleftvaluefoldpositive. ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_start. fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_prefix_smallleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_start. fs_u_dst_inverse_prefix_smallleftvaluefoldpositive = fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_prefix_smallleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_prefix_smallleftvaluefold) = S ((S (S (dc_input_inverse_prefix_smallleft))) * fs_v_dst_inverse_prefix_smallleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_prefix_smallleftvaluefoldpositive = fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_prefix_smallleft))) * fs_v_dst_inverse_prefix_smallleftvaluefoldpositive) + (dst_positive_sum_inverse_prefix_smallleftvaluefold))) /\ forall fs_i_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps = S (dc_input_inverse_prefix_smallleft)) -> exists fs_a_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps fs_r_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps fs_s_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_prefix_smallleftvaluefold)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_prefix_smallleftvaluefold = fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_prefix_smallleftvaluefold) + (fs_a_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_smallleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_prefix_smallleftvaluefoldpositive = fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_smallleftvaluefoldpositive) + (fs_r_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_smallleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_prefix_smallleftvaluefoldpositive = fs_q_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_smallleftvaluefoldpositive) + (fs_s_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps = fs_r_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps + fs_a_dst_inverse_prefix_smallleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_prefix_smallleftvaluefoldnegative fs_v_dst_inverse_prefix_smallleftvaluefoldnegative. ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_start. fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_prefix_smallleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_start. fs_u_dst_inverse_prefix_smallleftvaluefoldnegative = fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_prefix_smallleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_prefix_smallleftvaluefold) = S ((S (S (dc_input_inverse_prefix_smallleft))) * fs_v_dst_inverse_prefix_smallleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_prefix_smallleftvaluefoldnegative = fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_prefix_smallleft))) * fs_v_dst_inverse_prefix_smallleftvaluefoldnegative) + (dst_negative_sum_inverse_prefix_smallleftvaluefold))) /\ forall fs_i_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps = S (dc_input_inverse_prefix_smallleft)) -> exists fs_a_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps fs_r_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps fs_s_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_prefix_smallleftvaluefold)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_prefix_smallleftvaluefold = fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_prefix_smallleftvaluefold) + (fs_a_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_smallleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_prefix_smallleftvaluefoldnegative = fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_smallleftvaluefoldnegative) + (fs_r_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_smallleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_prefix_smallleftvaluefoldnegative = fs_q_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_smallleftvaluefoldnegative) + (fs_s_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps = fs_r_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps + fs_a_dst_inverse_prefix_smallleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_prefix_smallleftvaluefoldresult ge_balance_negative_inverse_prefix_smallleftvaluefoldresult. (((((dc_output_inverse_prefix_smallleft) = 2 * (ge_balance_positive_inverse_prefix_smallleftvaluefoldresult) /\ (ge_balance_negative_inverse_prefix_smallleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_prefix_smallleftvaluefoldresultdecode. (((dc_output_inverse_prefix_smallleft) = 2 * ge_signed_half_inverse_prefix_smallleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_prefix_smallleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_prefix_smallleftvaluefoldresult) = S ge_signed_half_inverse_prefix_smallleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_prefix_smallleftvaluefold) + ge_balance_negative_inverse_prefix_smallleftvaluefoldresult = (dst_negative_sum_inverse_prefix_smallleftvaluefold) + ge_balance_positive_inverse_prefix_smallleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_prefix_smallrightleft dst_positive_scale_inverse_prefix_smallrightleft dst_negative_code_inverse_prefix_smallrightleft dst_negative_scale_inverse_prefix_smallrightleft. (((H) = (((((dst_positive_code_inverse_prefix_smallrightleft) + (dst_positive_scale_inverse_prefix_smallrightleft)) * S ((dst_positive_code_inverse_prefix_smallrightleft) + (dst_positive_scale_inverse_prefix_smallrightleft)) + ((dst_positive_scale_inverse_prefix_smallrightleft) + (dst_positive_scale_inverse_prefix_smallrightleft))) + (((dst_negative_code_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)) * S ((dst_negative_code_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)) + ((dst_negative_scale_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)))) * S ((((dst_positive_code_inverse_prefix_smallrightleft) + (dst_positive_scale_inverse_prefix_smallrightleft)) * S ((dst_positive_code_inverse_prefix_smallrightleft) + (dst_positive_scale_inverse_prefix_smallrightleft)) + ((dst_positive_scale_inverse_prefix_smallrightleft) + (dst_positive_scale_inverse_prefix_smallrightleft))) + (((dst_negative_code_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)) * S ((dst_negative_code_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)) + ((dst_negative_scale_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)))) + ((((dst_negative_code_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)) * S ((dst_negative_code_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)) + ((dst_negative_scale_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft))) + (((dst_negative_code_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)) * S ((dst_negative_code_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)) + ((dst_negative_scale_inverse_prefix_smallrightleft) + (dst_negative_scale_inverse_prefix_smallrightleft)))))) /\ (forall dst_index_inverse_prefix_smallrightleft. (exists pvs_le_gap_inverse_prefix_smallrightleftdomain. pvs_le_gap_inverse_prefix_smallrightleftdomain + (dst_index_inverse_prefix_smallrightleft) = (K)) -> exists dst_positive_inverse_prefix_smallrightleft dst_negative_inverse_prefix_smallrightleft dst_value_inverse_prefix_smallrightleft. ((((exists ff_h_pvs_inverse_prefix_smallrightleftentrypositive. ff_h_pvs_inverse_prefix_smallrightleftentrypositive + S (dst_positive_inverse_prefix_smallrightleft) = S ((S (dst_index_inverse_prefix_smallrightleft)) * dst_positive_scale_inverse_prefix_smallrightleft)) /\ exists ff_q_pvs_inverse_prefix_smallrightleftentrypositive. dst_positive_code_inverse_prefix_smallrightleft = ff_q_pvs_inverse_prefix_smallrightleftentrypositive * S ((S (dst_index_inverse_prefix_smallrightleft)) * dst_positive_scale_inverse_prefix_smallrightleft) + (dst_positive_inverse_prefix_smallrightleft))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightleftentrynegative. ff_h_pvs_inverse_prefix_smallrightleftentrynegative + S (dst_negative_inverse_prefix_smallrightleft) = S ((S (dst_index_inverse_prefix_smallrightleft)) * dst_negative_scale_inverse_prefix_smallrightleft)) /\ exists ff_q_pvs_inverse_prefix_smallrightleftentrynegative. dst_negative_code_inverse_prefix_smallrightleft = ff_q_pvs_inverse_prefix_smallrightleftentrynegative * S ((S (dst_index_inverse_prefix_smallrightleft)) * dst_negative_scale_inverse_prefix_smallrightleft) + (dst_negative_inverse_prefix_smallrightleft))) /\ (exists ge_balance_positive_inverse_prefix_smallrightleftentryvalue ge_balance_negative_inverse_prefix_smallrightleftentryvalue. (((((dst_value_inverse_prefix_smallrightleft) = 2 * (ge_balance_positive_inverse_prefix_smallrightleftentryvalue) /\ (ge_balance_negative_inverse_prefix_smallrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightleftentryvaluedecode. (((dst_value_inverse_prefix_smallrightleft) = 2 * ge_signed_half_inverse_prefix_smallrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallrightleftentryvalue) = S ge_signed_half_inverse_prefix_smallrightleftentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smallrightleft) + ge_balance_negative_inverse_prefix_smallrightleftentryvalue = (dst_negative_inverse_prefix_smallrightleft) + ge_balance_positive_inverse_prefix_smallrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_smallrightright dst_positive_scale_inverse_prefix_smallrightright dst_negative_code_inverse_prefix_smallrightright dst_negative_scale_inverse_prefix_smallrightright. (((F) = (((((dst_positive_code_inverse_prefix_smallrightright) + (dst_positive_scale_inverse_prefix_smallrightright)) * S ((dst_positive_code_inverse_prefix_smallrightright) + (dst_positive_scale_inverse_prefix_smallrightright)) + ((dst_positive_scale_inverse_prefix_smallrightright) + (dst_positive_scale_inverse_prefix_smallrightright))) + (((dst_negative_code_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)) * S ((dst_negative_code_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)) + ((dst_negative_scale_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)))) * S ((((dst_positive_code_inverse_prefix_smallrightright) + (dst_positive_scale_inverse_prefix_smallrightright)) * S ((dst_positive_code_inverse_prefix_smallrightright) + (dst_positive_scale_inverse_prefix_smallrightright)) + ((dst_positive_scale_inverse_prefix_smallrightright) + (dst_positive_scale_inverse_prefix_smallrightright))) + (((dst_negative_code_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)) * S ((dst_negative_code_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)) + ((dst_negative_scale_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)))) + ((((dst_negative_code_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)) * S ((dst_negative_code_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)) + ((dst_negative_scale_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright))) + (((dst_negative_code_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)) * S ((dst_negative_code_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)) + ((dst_negative_scale_inverse_prefix_smallrightright) + (dst_negative_scale_inverse_prefix_smallrightright)))))) /\ (forall dst_index_inverse_prefix_smallrightright. (exists pvs_le_gap_inverse_prefix_smallrightrightdomain. pvs_le_gap_inverse_prefix_smallrightrightdomain + (dst_index_inverse_prefix_smallrightright) = (K)) -> exists dst_positive_inverse_prefix_smallrightright dst_negative_inverse_prefix_smallrightright dst_value_inverse_prefix_smallrightright. ((((exists ff_h_pvs_inverse_prefix_smallrightrightentrypositive. ff_h_pvs_inverse_prefix_smallrightrightentrypositive + S (dst_positive_inverse_prefix_smallrightright) = S ((S (dst_index_inverse_prefix_smallrightright)) * dst_positive_scale_inverse_prefix_smallrightright)) /\ exists ff_q_pvs_inverse_prefix_smallrightrightentrypositive. dst_positive_code_inverse_prefix_smallrightright = ff_q_pvs_inverse_prefix_smallrightrightentrypositive * S ((S (dst_index_inverse_prefix_smallrightright)) * dst_positive_scale_inverse_prefix_smallrightright) + (dst_positive_inverse_prefix_smallrightright))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightrightentrynegative. ff_h_pvs_inverse_prefix_smallrightrightentrynegative + S (dst_negative_inverse_prefix_smallrightright) = S ((S (dst_index_inverse_prefix_smallrightright)) * dst_negative_scale_inverse_prefix_smallrightright)) /\ exists ff_q_pvs_inverse_prefix_smallrightrightentrynegative. dst_negative_code_inverse_prefix_smallrightright = ff_q_pvs_inverse_prefix_smallrightrightentrynegative * S ((S (dst_index_inverse_prefix_smallrightright)) * dst_negative_scale_inverse_prefix_smallrightright) + (dst_negative_inverse_prefix_smallrightright))) /\ (exists ge_balance_positive_inverse_prefix_smallrightrightentryvalue ge_balance_negative_inverse_prefix_smallrightrightentryvalue. (((((dst_value_inverse_prefix_smallrightright) = 2 * (ge_balance_positive_inverse_prefix_smallrightrightentryvalue) /\ (ge_balance_negative_inverse_prefix_smallrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightrightentryvaluedecode. (((dst_value_inverse_prefix_smallrightright) = 2 * ge_signed_half_inverse_prefix_smallrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallrightrightentryvalue) = S ge_signed_half_inverse_prefix_smallrightrightentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smallrightright) + ge_balance_negative_inverse_prefix_smallrightrightentryvalue = (dst_negative_inverse_prefix_smallrightright) + ge_balance_positive_inverse_prefix_smallrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_smallrighttable dst_positive_scale_inverse_prefix_smallrighttable dst_negative_code_inverse_prefix_smallrighttable dst_negative_scale_inverse_prefix_smallrighttable. (((di_delta_inverse_prefix_small) = (((((dst_positive_code_inverse_prefix_smallrighttable) + (dst_positive_scale_inverse_prefix_smallrighttable)) * S ((dst_positive_code_inverse_prefix_smallrighttable) + (dst_positive_scale_inverse_prefix_smallrighttable)) + ((dst_positive_scale_inverse_prefix_smallrighttable) + (dst_positive_scale_inverse_prefix_smallrighttable))) + (((dst_negative_code_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)) * S ((dst_negative_code_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)) + ((dst_negative_scale_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)))) * S ((((dst_positive_code_inverse_prefix_smallrighttable) + (dst_positive_scale_inverse_prefix_smallrighttable)) * S ((dst_positive_code_inverse_prefix_smallrighttable) + (dst_positive_scale_inverse_prefix_smallrighttable)) + ((dst_positive_scale_inverse_prefix_smallrighttable) + (dst_positive_scale_inverse_prefix_smallrighttable))) + (((dst_negative_code_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)) * S ((dst_negative_code_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)) + ((dst_negative_scale_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)))) + ((((dst_negative_code_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)) * S ((dst_negative_code_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)) + ((dst_negative_scale_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable))) + (((dst_negative_code_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)) * S ((dst_negative_code_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)) + ((dst_negative_scale_inverse_prefix_smallrighttable) + (dst_negative_scale_inverse_prefix_smallrighttable)))))) /\ (forall dst_index_inverse_prefix_smallrighttable. (exists pvs_le_gap_inverse_prefix_smallrighttabledomain. pvs_le_gap_inverse_prefix_smallrighttabledomain + (dst_index_inverse_prefix_smallrighttable) = (K)) -> exists dst_positive_inverse_prefix_smallrighttable dst_negative_inverse_prefix_smallrighttable dst_value_inverse_prefix_smallrighttable. ((((exists ff_h_pvs_inverse_prefix_smallrighttableentrypositive. ff_h_pvs_inverse_prefix_smallrighttableentrypositive + S (dst_positive_inverse_prefix_smallrighttable) = S ((S (dst_index_inverse_prefix_smallrighttable)) * dst_positive_scale_inverse_prefix_smallrighttable)) /\ exists ff_q_pvs_inverse_prefix_smallrighttableentrypositive. dst_positive_code_inverse_prefix_smallrighttable = ff_q_pvs_inverse_prefix_smallrighttableentrypositive * S ((S (dst_index_inverse_prefix_smallrighttable)) * dst_positive_scale_inverse_prefix_smallrighttable) + (dst_positive_inverse_prefix_smallrighttable))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrighttableentrynegative. ff_h_pvs_inverse_prefix_smallrighttableentrynegative + S (dst_negative_inverse_prefix_smallrighttable) = S ((S (dst_index_inverse_prefix_smallrighttable)) * dst_negative_scale_inverse_prefix_smallrighttable)) /\ exists ff_q_pvs_inverse_prefix_smallrighttableentrynegative. dst_negative_code_inverse_prefix_smallrighttable = ff_q_pvs_inverse_prefix_smallrighttableentrynegative * S ((S (dst_index_inverse_prefix_smallrighttable)) * dst_negative_scale_inverse_prefix_smallrighttable) + (dst_negative_inverse_prefix_smallrighttable))) /\ (exists ge_balance_positive_inverse_prefix_smallrighttableentryvalue ge_balance_negative_inverse_prefix_smallrighttableentryvalue. (((((dst_value_inverse_prefix_smallrighttable) = 2 * (ge_balance_positive_inverse_prefix_smallrighttableentryvalue) /\ (ge_balance_negative_inverse_prefix_smallrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallrighttableentryvaluedecode. (((dst_value_inverse_prefix_smallrighttable) = 2 * ge_signed_half_inverse_prefix_smallrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallrighttableentryvalue) = S ge_signed_half_inverse_prefix_smallrighttableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smallrighttable) + ge_balance_negative_inverse_prefix_smallrighttableentryvalue = (dst_negative_inverse_prefix_smallrighttable) + ge_balance_positive_inverse_prefix_smallrighttableentryvalue))))))))) /\ (forall dc_input_inverse_prefix_smallright dc_output_inverse_prefix_smallright. ~(dc_input_inverse_prefix_smallright=0) -> (exists pvs_le_gap_inverse_prefix_smallrightdomain. pvs_le_gap_inverse_prefix_smallrightdomain + (dc_input_inverse_prefix_smallright) = (K)) -> (exists dst_positive_code_inverse_prefix_smallrightlookup dst_positive_scale_inverse_prefix_smallrightlookup dst_negative_code_inverse_prefix_smallrightlookup dst_negative_scale_inverse_prefix_smallrightlookup dst_positive_inverse_prefix_smallrightlookup dst_negative_inverse_prefix_smallrightlookup. (((di_delta_inverse_prefix_small) = (((((dst_positive_code_inverse_prefix_smallrightlookup) + (dst_positive_scale_inverse_prefix_smallrightlookup)) * S ((dst_positive_code_inverse_prefix_smallrightlookup) + (dst_positive_scale_inverse_prefix_smallrightlookup)) + ((dst_positive_scale_inverse_prefix_smallrightlookup) + (dst_positive_scale_inverse_prefix_smallrightlookup))) + (((dst_negative_code_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)) * S ((dst_negative_code_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)) + ((dst_negative_scale_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)))) * S ((((dst_positive_code_inverse_prefix_smallrightlookup) + (dst_positive_scale_inverse_prefix_smallrightlookup)) * S ((dst_positive_code_inverse_prefix_smallrightlookup) + (dst_positive_scale_inverse_prefix_smallrightlookup)) + ((dst_positive_scale_inverse_prefix_smallrightlookup) + (dst_positive_scale_inverse_prefix_smallrightlookup))) + (((dst_negative_code_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)) * S ((dst_negative_code_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)) + ((dst_negative_scale_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)))) + ((((dst_negative_code_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)) * S ((dst_negative_code_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)) + ((dst_negative_scale_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup))) + (((dst_negative_code_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)) * S ((dst_negative_code_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)) + ((dst_negative_scale_inverse_prefix_smallrightlookup) + (dst_negative_scale_inverse_prefix_smallrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightlookuppositive. ff_h_pvs_inverse_prefix_smallrightlookuppositive + S (dst_positive_inverse_prefix_smallrightlookup) = S ((S (dc_input_inverse_prefix_smallright)) * dst_positive_scale_inverse_prefix_smallrightlookup)) /\ exists ff_q_pvs_inverse_prefix_smallrightlookuppositive. dst_positive_code_inverse_prefix_smallrightlookup = ff_q_pvs_inverse_prefix_smallrightlookuppositive * S ((S (dc_input_inverse_prefix_smallright)) * dst_positive_scale_inverse_prefix_smallrightlookup) + (dst_positive_inverse_prefix_smallrightlookup))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightlookupnegative. ff_h_pvs_inverse_prefix_smallrightlookupnegative + S (dst_negative_inverse_prefix_smallrightlookup) = S ((S (dc_input_inverse_prefix_smallright)) * dst_negative_scale_inverse_prefix_smallrightlookup)) /\ exists ff_q_pvs_inverse_prefix_smallrightlookupnegative. dst_negative_code_inverse_prefix_smallrightlookup = ff_q_pvs_inverse_prefix_smallrightlookupnegative * S ((S (dc_input_inverse_prefix_smallright)) * dst_negative_scale_inverse_prefix_smallrightlookup) + (dst_negative_inverse_prefix_smallrightlookup))) /\ (exists ge_balance_positive_inverse_prefix_smallrightlookupvalue ge_balance_negative_inverse_prefix_smallrightlookupvalue. (((((dc_output_inverse_prefix_smallright) = 2 * (ge_balance_positive_inverse_prefix_smallrightlookupvalue) /\ (ge_balance_negative_inverse_prefix_smallrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightlookupvaluedecode. (((dc_output_inverse_prefix_smallright) = 2 * ge_signed_half_inverse_prefix_smallrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallrightlookupvalue) = S ge_signed_half_inverse_prefix_smallrightlookupvaluedecode))) /\ ((dst_positive_inverse_prefix_smallrightlookup) + ge_balance_negative_inverse_prefix_smallrightlookupvalue = (dst_negative_inverse_prefix_smallrightlookup) + ge_balance_positive_inverse_prefix_smallrightlookupvalue))))))))) -> (((~((dc_input_inverse_prefix_smallright)=0)) /\ (exists dc_mask_inverse_prefix_smallrightvalue. ((((exists dst_positive_code_inverse_prefix_smallrightvaluemasktable dst_positive_scale_inverse_prefix_smallrightvaluemasktable dst_negative_code_inverse_prefix_smallrightvaluemasktable dst_negative_scale_inverse_prefix_smallrightvaluemasktable. (((dc_mask_inverse_prefix_smallrightvalue) = (((((dst_positive_code_inverse_prefix_smallrightvaluemasktable) + (dst_positive_scale_inverse_prefix_smallrightvaluemasktable)) * S ((dst_positive_code_inverse_prefix_smallrightvaluemasktable) + (dst_positive_scale_inverse_prefix_smallrightvaluemasktable)) + ((dst_positive_scale_inverse_prefix_smallrightvaluemasktable) + (dst_positive_scale_inverse_prefix_smallrightvaluemasktable))) + (((dst_negative_code_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)))) * S ((((dst_positive_code_inverse_prefix_smallrightvaluemasktable) + (dst_positive_scale_inverse_prefix_smallrightvaluemasktable)) * S ((dst_positive_code_inverse_prefix_smallrightvaluemasktable) + (dst_positive_scale_inverse_prefix_smallrightvaluemasktable)) + ((dst_positive_scale_inverse_prefix_smallrightvaluemasktable) + (dst_positive_scale_inverse_prefix_smallrightvaluemasktable))) + (((dst_negative_code_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)))) + ((((dst_negative_code_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable))) + (((dst_negative_code_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemasktable) + (dst_negative_scale_inverse_prefix_smallrightvaluemasktable)))))) /\ (forall dst_index_inverse_prefix_smallrightvaluemasktable. (exists pvs_le_gap_inverse_prefix_smallrightvaluemasktabledomain. pvs_le_gap_inverse_prefix_smallrightvaluemasktabledomain + (dst_index_inverse_prefix_smallrightvaluemasktable) = (dc_input_inverse_prefix_smallright)) -> exists dst_positive_inverse_prefix_smallrightvaluemasktable dst_negative_inverse_prefix_smallrightvaluemasktable dst_value_inverse_prefix_smallrightvaluemasktable. ((((exists ff_h_pvs_inverse_prefix_smallrightvaluemasktableentrypositive. ff_h_pvs_inverse_prefix_smallrightvaluemasktableentrypositive + S (dst_positive_inverse_prefix_smallrightvaluemasktable) = S ((S (dst_index_inverse_prefix_smallrightvaluemasktable)) * dst_positive_scale_inverse_prefix_smallrightvaluemasktable)) /\ exists ff_q_pvs_inverse_prefix_smallrightvaluemasktableentrypositive. dst_positive_code_inverse_prefix_smallrightvaluemasktable = ff_q_pvs_inverse_prefix_smallrightvaluemasktableentrypositive * S ((S (dst_index_inverse_prefix_smallrightvaluemasktable)) * dst_positive_scale_inverse_prefix_smallrightvaluemasktable) + (dst_positive_inverse_prefix_smallrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightvaluemasktableentrynegative. ff_h_pvs_inverse_prefix_smallrightvaluemasktableentrynegative + S (dst_negative_inverse_prefix_smallrightvaluemasktable) = S ((S (dst_index_inverse_prefix_smallrightvaluemasktable)) * dst_negative_scale_inverse_prefix_smallrightvaluemasktable)) /\ exists ff_q_pvs_inverse_prefix_smallrightvaluemasktableentrynegative. dst_negative_code_inverse_prefix_smallrightvaluemasktable = ff_q_pvs_inverse_prefix_smallrightvaluemasktableentrynegative * S ((S (dst_index_inverse_prefix_smallrightvaluemasktable)) * dst_negative_scale_inverse_prefix_smallrightvaluemasktable) + (dst_negative_inverse_prefix_smallrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_prefix_smallrightvaluemasktableentryvalue ge_balance_negative_inverse_prefix_smallrightvaluemasktableentryvalue. (((((dst_value_inverse_prefix_smallrightvaluemasktable) = 2 * (ge_balance_positive_inverse_prefix_smallrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_prefix_smallrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightvaluemasktableentryvaluedecode. (((dst_value_inverse_prefix_smallrightvaluemasktable) = 2 * ge_signed_half_inverse_prefix_smallrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallrightvaluemasktableentryvalue) = S ge_signed_half_inverse_prefix_smallrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_prefix_smallrightvaluemasktable) + ge_balance_negative_inverse_prefix_smallrightvaluemasktableentryvalue = (dst_negative_inverse_prefix_smallrightvaluemasktable) + ge_balance_positive_inverse_prefix_smallrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_prefix_smallrightvaluemask dc_value_inverse_prefix_smallrightvaluemask. (exists pvs_le_gap_inverse_prefix_smallrightvaluemaskdomain. pvs_le_gap_inverse_prefix_smallrightvaluemaskdomain + (dc_index_inverse_prefix_smallrightvaluemask) = (dc_input_inverse_prefix_smallright)) -> (exists dst_positive_code_inverse_prefix_smallrightvaluemasklookup dst_positive_scale_inverse_prefix_smallrightvaluemasklookup dst_negative_code_inverse_prefix_smallrightvaluemasklookup dst_negative_scale_inverse_prefix_smallrightvaluemasklookup dst_positive_inverse_prefix_smallrightvaluemasklookup dst_negative_inverse_prefix_smallrightvaluemasklookup. (((dc_mask_inverse_prefix_smallrightvalue) = (((((dst_positive_code_inverse_prefix_smallrightvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallrightvaluemasklookup)) * S ((dst_positive_code_inverse_prefix_smallrightvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallrightvaluemasklookup)) + ((dst_positive_scale_inverse_prefix_smallrightvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallrightvaluemasklookup))) + (((dst_negative_code_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_prefix_smallrightvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallrightvaluemasklookup)) * S ((dst_positive_code_inverse_prefix_smallrightvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallrightvaluemasklookup)) + ((dst_positive_scale_inverse_prefix_smallrightvaluemasklookup) + (dst_positive_scale_inverse_prefix_smallrightvaluemasklookup))) + (((dst_negative_code_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)))) + ((((dst_negative_code_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup))) + (((dst_negative_code_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightvaluemasklookuppositive. ff_h_pvs_inverse_prefix_smallrightvaluemasklookuppositive + S (dst_positive_inverse_prefix_smallrightvaluemasklookup) = S ((S (dc_index_inverse_prefix_smallrightvaluemask)) * dst_positive_scale_inverse_prefix_smallrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_prefix_smallrightvaluemasklookuppositive. dst_positive_code_inverse_prefix_smallrightvaluemasklookup = ff_q_pvs_inverse_prefix_smallrightvaluemasklookuppositive * S ((S (dc_index_inverse_prefix_smallrightvaluemask)) * dst_positive_scale_inverse_prefix_smallrightvaluemasklookup) + (dst_positive_inverse_prefix_smallrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightvaluemasklookupnegative. ff_h_pvs_inverse_prefix_smallrightvaluemasklookupnegative + S (dst_negative_inverse_prefix_smallrightvaluemasklookup) = S ((S (dc_index_inverse_prefix_smallrightvaluemask)) * dst_negative_scale_inverse_prefix_smallrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_prefix_smallrightvaluemasklookupnegative. dst_negative_code_inverse_prefix_smallrightvaluemasklookup = ff_q_pvs_inverse_prefix_smallrightvaluemasklookupnegative * S ((S (dc_index_inverse_prefix_smallrightvaluemask)) * dst_negative_scale_inverse_prefix_smallrightvaluemasklookup) + (dst_negative_inverse_prefix_smallrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_prefix_smallrightvaluemasklookupvalue ge_balance_negative_inverse_prefix_smallrightvaluemasklookupvalue. (((((dc_value_inverse_prefix_smallrightvaluemask) = 2 * (ge_balance_positive_inverse_prefix_smallrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_prefix_smallrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightvaluemasklookupvaluedecode. (((dc_value_inverse_prefix_smallrightvaluemask) = 2 * ge_signed_half_inverse_prefix_smallrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallrightvaluemasklookupvalue) = S ge_signed_half_inverse_prefix_smallrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_prefix_smallrightvaluemasklookup) + ge_balance_negative_inverse_prefix_smallrightvaluemasklookupvalue = (dst_negative_inverse_prefix_smallrightvaluemasklookup) + ge_balance_positive_inverse_prefix_smallrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_prefix_smallrightvaluemask)=0)) /\ (exists dc_quotient_inverse_prefix_smallrightvaluemaskentry dc_left_inverse_prefix_smallrightvaluemaskentry dc_right_inverse_prefix_smallrightvaluemaskentry. (((dc_input_inverse_prefix_smallright)=(dc_index_inverse_prefix_smallrightvaluemask)*dc_quotient_inverse_prefix_smallrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_prefix_smallrightvaluemaskentryleft dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft dst_positive_inverse_prefix_smallrightvaluemaskentryleft dst_negative_inverse_prefix_smallrightvaluemaskentryleft. (((H) = (((((dst_positive_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft))) + (((dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightvaluemaskentryleftpositive. ff_h_pvs_inverse_prefix_smallrightvaluemaskentryleftpositive + S (dst_positive_inverse_prefix_smallrightvaluemaskentryleft) = S ((S (dc_index_inverse_prefix_smallrightvaluemask)) * dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_prefix_smallrightvaluemaskentryleftpositive. dst_positive_code_inverse_prefix_smallrightvaluemaskentryleft = ff_q_pvs_inverse_prefix_smallrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_prefix_smallrightvaluemask)) * dst_positive_scale_inverse_prefix_smallrightvaluemaskentryleft) + (dst_positive_inverse_prefix_smallrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightvaluemaskentryleftnegative. ff_h_pvs_inverse_prefix_smallrightvaluemaskentryleftnegative + S (dst_negative_inverse_prefix_smallrightvaluemaskentryleft) = S ((S (dc_index_inverse_prefix_smallrightvaluemask)) * dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_prefix_smallrightvaluemaskentryleftnegative. dst_negative_code_inverse_prefix_smallrightvaluemaskentryleft = ff_q_pvs_inverse_prefix_smallrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_prefix_smallrightvaluemask)) * dst_negative_scale_inverse_prefix_smallrightvaluemaskentryleft) + (dst_negative_inverse_prefix_smallrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_prefix_smallrightvaluemaskentryleftvalue ge_balance_negative_inverse_prefix_smallrightvaluemaskentryleftvalue. (((((dc_left_inverse_prefix_smallrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_prefix_smallrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_prefix_smallrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_prefix_smallrightvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_smallrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_prefix_smallrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_prefix_smallrightvaluemaskentryleft) + ge_balance_negative_inverse_prefix_smallrightvaluemaskentryleftvalue = (dst_negative_inverse_prefix_smallrightvaluemaskentryleft) + ge_balance_positive_inverse_prefix_smallrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_prefix_smallrightvaluemaskentryright dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright dst_negative_code_inverse_prefix_smallrightvaluemaskentryright dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright dst_positive_inverse_prefix_smallrightvaluemaskentryright dst_negative_inverse_prefix_smallrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright)) * S ((dst_positive_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright)) + ((dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright)) * S ((dst_positive_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright)) + ((dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright) + (dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright))) + (((dst_negative_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) * S ((dst_negative_code_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) + ((dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightvaluemaskentryrightpositive. ff_h_pvs_inverse_prefix_smallrightvaluemaskentryrightpositive + S (dst_positive_inverse_prefix_smallrightvaluemaskentryright) = S ((S (dc_quotient_inverse_prefix_smallrightvaluemaskentry)) * dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_prefix_smallrightvaluemaskentryrightpositive. dst_positive_code_inverse_prefix_smallrightvaluemaskentryright = ff_q_pvs_inverse_prefix_smallrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_prefix_smallrightvaluemaskentry)) * dst_positive_scale_inverse_prefix_smallrightvaluemaskentryright) + (dst_positive_inverse_prefix_smallrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_prefix_smallrightvaluemaskentryrightnegative. ff_h_pvs_inverse_prefix_smallrightvaluemaskentryrightnegative + S (dst_negative_inverse_prefix_smallrightvaluemaskentryright) = S ((S (dc_quotient_inverse_prefix_smallrightvaluemaskentry)) * dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_prefix_smallrightvaluemaskentryrightnegative. dst_negative_code_inverse_prefix_smallrightvaluemaskentryright = ff_q_pvs_inverse_prefix_smallrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_prefix_smallrightvaluemaskentry)) * dst_negative_scale_inverse_prefix_smallrightvaluemaskentryright) + (dst_negative_inverse_prefix_smallrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_prefix_smallrightvaluemaskentryrightvalue ge_balance_negative_inverse_prefix_smallrightvaluemaskentryrightvalue. (((((dc_right_inverse_prefix_smallrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_prefix_smallrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_prefix_smallrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_prefix_smallrightvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_smallrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_prefix_smallrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_prefix_smallrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_prefix_smallrightvaluemaskentryright) + ge_balance_negative_inverse_prefix_smallrightvaluemaskentryrightvalue = (dst_negative_inverse_prefix_smallrightvaluemaskentryright) + ge_balance_positive_inverse_prefix_smallrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_prefix_smallrightvaluemaskentryproduct sto_an_inverse_prefix_smallrightvaluemaskentryproduct sto_bp_inverse_prefix_smallrightvaluemaskentryproduct sto_bn_inverse_prefix_smallrightvaluemaskentryproduct sto_cp_inverse_prefix_smallrightvaluemaskentryproduct sto_cn_inverse_prefix_smallrightvaluemaskentryproduct. (((((dc_left_inverse_prefix_smallrightvaluemaskentry) = 2 * (sto_ap_inverse_prefix_smallrightvaluemaskentryproduct) /\ (sto_an_inverse_prefix_smallrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductleft. (((dc_left_inverse_prefix_smallrightvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_prefix_smallrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_prefix_smallrightvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_prefix_smallrightvaluemaskentry) = 2 * (sto_bp_inverse_prefix_smallrightvaluemaskentryproduct) /\ (sto_bn_inverse_prefix_smallrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductright. (((dc_right_inverse_prefix_smallrightvaluemaskentry) = 2 * ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_prefix_smallrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_prefix_smallrightvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_prefix_smallrightvaluemask) = 2 * (sto_cp_inverse_prefix_smallrightvaluemaskentryproduct) /\ (sto_cn_inverse_prefix_smallrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductoutput. (((dc_value_inverse_prefix_smallrightvaluemask) = 2 * ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_prefix_smallrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_prefix_smallrightvaluemaskentryproduct) = S ge_signed_half_inverse_prefix_smallrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_prefix_smallrightvaluemaskentryproduct * sto_bp_inverse_prefix_smallrightvaluemaskentryproduct + sto_an_inverse_prefix_smallrightvaluemaskentryproduct * sto_bn_inverse_prefix_smallrightvaluemaskentryproduct) + sto_cn_inverse_prefix_smallrightvaluemaskentryproduct = (sto_ap_inverse_prefix_smallrightvaluemaskentryproduct * sto_bn_inverse_prefix_smallrightvaluemaskentryproduct + sto_an_inverse_prefix_smallrightvaluemaskentryproduct * sto_bp_inverse_prefix_smallrightvaluemaskentryproduct) + sto_cp_inverse_prefix_smallrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_prefix_smallrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_prefix_smallrightvaluemaskentrynondivisor. (dc_input_inverse_prefix_smallright) = (dc_index_inverse_prefix_smallrightvaluemask) * pvs_factor_inverse_prefix_smallrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_prefix_smallrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_prefix_smallrightvaluefold dst_positive_scale_inverse_prefix_smallrightvaluefold dst_negative_code_inverse_prefix_smallrightvaluefold dst_negative_scale_inverse_prefix_smallrightvaluefold dst_positive_sum_inverse_prefix_smallrightvaluefold dst_negative_sum_inverse_prefix_smallrightvaluefold. (((dc_mask_inverse_prefix_smallrightvalue) = (((((dst_positive_code_inverse_prefix_smallrightvaluefold) + (dst_positive_scale_inverse_prefix_smallrightvaluefold)) * S ((dst_positive_code_inverse_prefix_smallrightvaluefold) + (dst_positive_scale_inverse_prefix_smallrightvaluefold)) + ((dst_positive_scale_inverse_prefix_smallrightvaluefold) + (dst_positive_scale_inverse_prefix_smallrightvaluefold))) + (((dst_negative_code_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)) * S ((dst_negative_code_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)) + ((dst_negative_scale_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)))) * S ((((dst_positive_code_inverse_prefix_smallrightvaluefold) + (dst_positive_scale_inverse_prefix_smallrightvaluefold)) * S ((dst_positive_code_inverse_prefix_smallrightvaluefold) + (dst_positive_scale_inverse_prefix_smallrightvaluefold)) + ((dst_positive_scale_inverse_prefix_smallrightvaluefold) + (dst_positive_scale_inverse_prefix_smallrightvaluefold))) + (((dst_negative_code_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)) * S ((dst_negative_code_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)) + ((dst_negative_scale_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)))) + ((((dst_negative_code_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)) * S ((dst_negative_code_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)) + ((dst_negative_scale_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold))) + (((dst_negative_code_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)) * S ((dst_negative_code_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)) + ((dst_negative_scale_inverse_prefix_smallrightvaluefold) + (dst_negative_scale_inverse_prefix_smallrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_prefix_smallrightvaluefoldpositive fs_v_dst_inverse_prefix_smallrightvaluefoldpositive. ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_start. fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_prefix_smallrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_start. fs_u_dst_inverse_prefix_smallrightvaluefoldpositive = fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_prefix_smallrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_prefix_smallrightvaluefold) = S ((S (S (dc_input_inverse_prefix_smallright))) * fs_v_dst_inverse_prefix_smallrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_prefix_smallrightvaluefoldpositive = fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_prefix_smallright))) * fs_v_dst_inverse_prefix_smallrightvaluefoldpositive) + (dst_positive_sum_inverse_prefix_smallrightvaluefold))) /\ forall fs_i_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps = S (dc_input_inverse_prefix_smallright)) -> exists fs_a_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps fs_r_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps fs_s_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_prefix_smallrightvaluefold)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_prefix_smallrightvaluefold = fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_prefix_smallrightvaluefold) + (fs_a_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_smallrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_prefix_smallrightvaluefoldpositive = fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_smallrightvaluefoldpositive) + (fs_r_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_smallrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_prefix_smallrightvaluefoldpositive = fs_q_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_prefix_smallrightvaluefoldpositive) + (fs_s_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps = fs_r_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps + fs_a_dst_inverse_prefix_smallrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_prefix_smallrightvaluefoldnegative fs_v_dst_inverse_prefix_smallrightvaluefoldnegative. ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_start. fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_prefix_smallrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_start. fs_u_dst_inverse_prefix_smallrightvaluefoldnegative = fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_prefix_smallrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_prefix_smallrightvaluefold) = S ((S (S (dc_input_inverse_prefix_smallright))) * fs_v_dst_inverse_prefix_smallrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_prefix_smallrightvaluefoldnegative = fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_prefix_smallright))) * fs_v_dst_inverse_prefix_smallrightvaluefoldnegative) + (dst_negative_sum_inverse_prefix_smallrightvaluefold))) /\ forall fs_i_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps = S (dc_input_inverse_prefix_smallright)) -> exists fs_a_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps fs_r_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps fs_s_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_prefix_smallrightvaluefold)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_prefix_smallrightvaluefold = fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_prefix_smallrightvaluefold) + (fs_a_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_smallrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_prefix_smallrightvaluefoldnegative = fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_smallrightvaluefoldnegative) + (fs_r_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_smallrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_prefix_smallrightvaluefoldnegative = fs_q_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_prefix_smallrightvaluefoldnegative) + (fs_s_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps = fs_r_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps + fs_a_dst_inverse_prefix_smallrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_prefix_smallrightvaluefoldresult ge_balance_negative_inverse_prefix_smallrightvaluefoldresult. (((((dc_output_inverse_prefix_smallright) = 2 * (ge_balance_positive_inverse_prefix_smallrightvaluefoldresult) /\ (ge_balance_negative_inverse_prefix_smallrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_prefix_smallrightvaluefoldresultdecode. (((dc_output_inverse_prefix_smallright) = 2 * ge_signed_half_inverse_prefix_smallrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_prefix_smallrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_prefix_smallrightvaluefoldresult) = S ge_signed_half_inverse_prefix_smallrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_prefix_smallrightvaluefold) + ge_balance_negative_inverse_prefix_smallrightvaluefoldresult = (dst_negative_sum_inverse_prefix_smallrightvaluefold) + ge_balance_positive_inverse_prefix_smallrightvaluefoldresult)))))))))))))))))))))))) -> (exists pvs_le_gap_inverse_prefix_bound. pvs_le_gap_inverse_prefix_bound + (K) = (N)) -> (forall dm_index_inverse_prefix_result dm_first_value_inverse_prefix_result dm_second_value_inverse_prefix_result. ~(dm_index_inverse_prefix_result=0) -> (exists pvs_le_gap_inverse_prefix_resultdomain. pvs_le_gap_inverse_prefix_resultdomain + (dm_index_inverse_prefix_result) = (K)) -> (exists dst_positive_code_inverse_prefix_resultfirst dst_positive_scale_inverse_prefix_resultfirst dst_negative_code_inverse_prefix_resultfirst dst_negative_scale_inverse_prefix_resultfirst dst_positive_inverse_prefix_resultfirst dst_negative_inverse_prefix_resultfirst. (((G) = (((((dst_positive_code_inverse_prefix_resultfirst) + (dst_positive_scale_inverse_prefix_resultfirst)) * S ((dst_positive_code_inverse_prefix_resultfirst) + (dst_positive_scale_inverse_prefix_resultfirst)) + ((dst_positive_scale_inverse_prefix_resultfirst) + (dst_positive_scale_inverse_prefix_resultfirst))) + (((dst_negative_code_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)) * S ((dst_negative_code_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)) + ((dst_negative_scale_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)))) * S ((((dst_positive_code_inverse_prefix_resultfirst) + (dst_positive_scale_inverse_prefix_resultfirst)) * S ((dst_positive_code_inverse_prefix_resultfirst) + (dst_positive_scale_inverse_prefix_resultfirst)) + ((dst_positive_scale_inverse_prefix_resultfirst) + (dst_positive_scale_inverse_prefix_resultfirst))) + (((dst_negative_code_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)) * S ((dst_negative_code_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)) + ((dst_negative_scale_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)))) + ((((dst_negative_code_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)) * S ((dst_negative_code_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)) + ((dst_negative_scale_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst))) + (((dst_negative_code_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)) * S ((dst_negative_code_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)) + ((dst_negative_scale_inverse_prefix_resultfirst) + (dst_negative_scale_inverse_prefix_resultfirst)))))) /\ (((((exists ff_h_pvs_inverse_prefix_resultfirstpositive. ff_h_pvs_inverse_prefix_resultfirstpositive + S (dst_positive_inverse_prefix_resultfirst) = S ((S (dm_index_inverse_prefix_result)) * dst_positive_scale_inverse_prefix_resultfirst)) /\ exists ff_q_pvs_inverse_prefix_resultfirstpositive. dst_positive_code_inverse_prefix_resultfirst = ff_q_pvs_inverse_prefix_resultfirstpositive * S ((S (dm_index_inverse_prefix_result)) * dst_positive_scale_inverse_prefix_resultfirst) + (dst_positive_inverse_prefix_resultfirst))) /\ (((((exists ff_h_pvs_inverse_prefix_resultfirstnegative. ff_h_pvs_inverse_prefix_resultfirstnegative + S (dst_negative_inverse_prefix_resultfirst) = S ((S (dm_index_inverse_prefix_result)) * dst_negative_scale_inverse_prefix_resultfirst)) /\ exists ff_q_pvs_inverse_prefix_resultfirstnegative. dst_negative_code_inverse_prefix_resultfirst = ff_q_pvs_inverse_prefix_resultfirstnegative * S ((S (dm_index_inverse_prefix_result)) * dst_negative_scale_inverse_prefix_resultfirst) + (dst_negative_inverse_prefix_resultfirst))) /\ (exists ge_balance_positive_inverse_prefix_resultfirstvalue ge_balance_negative_inverse_prefix_resultfirstvalue. (((((dm_first_value_inverse_prefix_result) = 2 * (ge_balance_positive_inverse_prefix_resultfirstvalue) /\ (ge_balance_negative_inverse_prefix_resultfirstvalue) = 0) \/ exists ge_signed_half_inverse_prefix_resultfirstvaluedecode. (((dm_first_value_inverse_prefix_result) = 2 * ge_signed_half_inverse_prefix_resultfirstvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_resultfirstvalue) = 0) /\ (ge_balance_negative_inverse_prefix_resultfirstvalue) = S ge_signed_half_inverse_prefix_resultfirstvaluedecode))) /\ ((dst_positive_inverse_prefix_resultfirst) + ge_balance_negative_inverse_prefix_resultfirstvalue = (dst_negative_inverse_prefix_resultfirst) + ge_balance_positive_inverse_prefix_resultfirstvalue))))))))) -> (exists dst_positive_code_inverse_prefix_resultsecond dst_positive_scale_inverse_prefix_resultsecond dst_negative_code_inverse_prefix_resultsecond dst_negative_scale_inverse_prefix_resultsecond dst_positive_inverse_prefix_resultsecond dst_negative_inverse_prefix_resultsecond. (((H) = (((((dst_positive_code_inverse_prefix_resultsecond) + (dst_positive_scale_inverse_prefix_resultsecond)) * S ((dst_positive_code_inverse_prefix_resultsecond) + (dst_positive_scale_inverse_prefix_resultsecond)) + ((dst_positive_scale_inverse_prefix_resultsecond) + (dst_positive_scale_inverse_prefix_resultsecond))) + (((dst_negative_code_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)) * S ((dst_negative_code_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)) + ((dst_negative_scale_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)))) * S ((((dst_positive_code_inverse_prefix_resultsecond) + (dst_positive_scale_inverse_prefix_resultsecond)) * S ((dst_positive_code_inverse_prefix_resultsecond) + (dst_positive_scale_inverse_prefix_resultsecond)) + ((dst_positive_scale_inverse_prefix_resultsecond) + (dst_positive_scale_inverse_prefix_resultsecond))) + (((dst_negative_code_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)) * S ((dst_negative_code_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)) + ((dst_negative_scale_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)))) + ((((dst_negative_code_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)) * S ((dst_negative_code_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)) + ((dst_negative_scale_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond))) + (((dst_negative_code_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)) * S ((dst_negative_code_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)) + ((dst_negative_scale_inverse_prefix_resultsecond) + (dst_negative_scale_inverse_prefix_resultsecond)))))) /\ (((((exists ff_h_pvs_inverse_prefix_resultsecondpositive. ff_h_pvs_inverse_prefix_resultsecondpositive + S (dst_positive_inverse_prefix_resultsecond) = S ((S (dm_index_inverse_prefix_result)) * dst_positive_scale_inverse_prefix_resultsecond)) /\ exists ff_q_pvs_inverse_prefix_resultsecondpositive. dst_positive_code_inverse_prefix_resultsecond = ff_q_pvs_inverse_prefix_resultsecondpositive * S ((S (dm_index_inverse_prefix_result)) * dst_positive_scale_inverse_prefix_resultsecond) + (dst_positive_inverse_prefix_resultsecond))) /\ (((((exists ff_h_pvs_inverse_prefix_resultsecondnegative. ff_h_pvs_inverse_prefix_resultsecondnegative + S (dst_negative_inverse_prefix_resultsecond) = S ((S (dm_index_inverse_prefix_result)) * dst_negative_scale_inverse_prefix_resultsecond)) /\ exists ff_q_pvs_inverse_prefix_resultsecondnegative. dst_negative_code_inverse_prefix_resultsecond = ff_q_pvs_inverse_prefix_resultsecondnegative * S ((S (dm_index_inverse_prefix_result)) * dst_negative_scale_inverse_prefix_resultsecond) + (dst_negative_inverse_prefix_resultsecond))) /\ (exists ge_balance_positive_inverse_prefix_resultsecondvalue ge_balance_negative_inverse_prefix_resultsecondvalue. (((((dm_second_value_inverse_prefix_result) = 2 * (ge_balance_positive_inverse_prefix_resultsecondvalue) /\ (ge_balance_negative_inverse_prefix_resultsecondvalue) = 0) \/ exists ge_signed_half_inverse_prefix_resultsecondvaluedecode. (((dm_second_value_inverse_prefix_result) = 2 * ge_signed_half_inverse_prefix_resultsecondvaluedecode + 1 /\ (ge_balance_positive_inverse_prefix_resultsecondvalue) = 0) /\ (ge_balance_negative_inverse_prefix_resultsecondvalue) = S ge_signed_half_inverse_prefix_resultsecondvaluedecode))) /\ ((dst_positive_inverse_prefix_resultsecond) + ge_balance_negative_inverse_prefix_resultsecondvalue = (dst_negative_inverse_prefix_resultsecond) + ge_balance_positive_inverse_prefix_resultsecondvalue))))))))) -> dm_first_value_inverse_prefix_result=dm_second_value_inverse_prefix_result)Constructive proof overview
Generated structural guide
Independently constructed inverse prefixes have identical represented positive values on their common smaller domain.
The unchanged tactic script uses 2 declared prerequisites and contains 21 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
none
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–8
02Use earlier factsL9–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
specialize dirichlet_inverse_positive_unique (K) - L10
specialize dirichlet_inverse_positive_unique (F) - L11
specialize dirichlet_inverse_positive_unique (G) - L12
specialize dirichlet_inverse_positive_unique (H) - L13
apply dirichlet_inverse_positive_unique - L14
specialize dirichlet_inverse_restrict (N) - L15
specialize dirichlet_inverse_restrict (K) - L16
specialize dirichlet_inverse_restrict (F) - L17
specialize dirichlet_inverse_restrict (G) - L18
apply dirichlet_inverse_restrict
Original exact command ledger · 21 lines
- 0001
intro N - 0002
intro K - 0003
intro F - 0004
intro G - 0005
intro H - 0006
intro hg - 0007
intro hh - 0008
intro hb - 0009
specialize dirichlet_inverse_positive_unique (K) - 0010
specialize dirichlet_inverse_positive_unique (F) - 0011
specialize dirichlet_inverse_positive_unique (G) - 0012
specialize dirichlet_inverse_positive_unique (H) - 0013
apply dirichlet_inverse_positive_unique - 0014
specialize dirichlet_inverse_restrict (N) - 0015
specialize dirichlet_inverse_restrict (K) - 0016
specialize dirichlet_inverse_restrict (F) - 0017
specialize dirichlet_inverse_restrict (G) - 0018
apply dirichlet_inverse_restrict - 0019
exact hg - 0020
exact hb - 0021
exact hh