dirichlet_inverse_from_right_delta

Exact expanded first-order arithmetic statement

forall N F G E. (((exists dst_positive_code_inverse_right_deltatable dst_positive_scale_inverse_right_deltatable dst_negative_code_inverse_right_deltatable dst_negative_scale_inverse_right_deltatable. (((E) = (((((dst_positive_code_inverse_right_deltatable) + (dst_positive_scale_inverse_right_deltatable)) * S ((dst_positive_code_inverse_right_deltatable) + (dst_positive_scale_inverse_right_deltatable)) + ((dst_positive_scale_inverse_right_deltatable) + (dst_positive_scale_inverse_right_deltatable))) + (((dst_negative_code_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)) * S ((dst_negative_code_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)) + ((dst_negative_scale_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)))) * S ((((dst_positive_code_inverse_right_deltatable) + (dst_positive_scale_inverse_right_deltatable)) * S ((dst_positive_code_inverse_right_deltatable) + (dst_positive_scale_inverse_right_deltatable)) + ((dst_positive_scale_inverse_right_deltatable) + (dst_positive_scale_inverse_right_deltatable))) + (((dst_negative_code_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)) * S ((dst_negative_code_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)) + ((dst_negative_scale_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)))) + ((((dst_negative_code_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)) * S ((dst_negative_code_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)) + ((dst_negative_scale_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable))) + (((dst_negative_code_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)) * S ((dst_negative_code_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)) + ((dst_negative_scale_inverse_right_deltatable) + (dst_negative_scale_inverse_right_deltatable)))))) /\ (forall dst_index_inverse_right_deltatable. (exists pvs_le_gap_inverse_right_deltatabledomain. pvs_le_gap_inverse_right_deltatabledomain + (dst_index_inverse_right_deltatable) = (N)) -> exists dst_positive_inverse_right_deltatable dst_negative_inverse_right_deltatable dst_value_inverse_right_deltatable. ((((exists ff_h_pvs_inverse_right_deltatableentrypositive. ff_h_pvs_inverse_right_deltatableentrypositive + S (dst_positive_inverse_right_deltatable) = S ((S (dst_index_inverse_right_deltatable)) * dst_positive_scale_inverse_right_deltatable)) /\ exists ff_q_pvs_inverse_right_deltatableentrypositive. dst_positive_code_inverse_right_deltatable = ff_q_pvs_inverse_right_deltatableentrypositive * S ((S (dst_index_inverse_right_deltatable)) * dst_positive_scale_inverse_right_deltatable) + (dst_positive_inverse_right_deltatable))) /\ (((((exists ff_h_pvs_inverse_right_deltatableentrynegative. ff_h_pvs_inverse_right_deltatableentrynegative + S (dst_negative_inverse_right_deltatable) = S ((S (dst_index_inverse_right_deltatable)) * dst_negative_scale_inverse_right_deltatable)) /\ exists ff_q_pvs_inverse_right_deltatableentrynegative. dst_negative_code_inverse_right_deltatable = ff_q_pvs_inverse_right_deltatableentrynegative * S ((S (dst_index_inverse_right_deltatable)) * dst_negative_scale_inverse_right_deltatable) + (dst_negative_inverse_right_deltatable))) /\ (exists ge_balance_positive_inverse_right_deltatableentryvalue ge_balance_negative_inverse_right_deltatableentryvalue. (((((dst_value_inverse_right_deltatable) = 2 * (ge_balance_positive_inverse_right_deltatableentryvalue) /\ (ge_balance_negative_inverse_right_deltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_right_deltatableentryvaluedecode. (((dst_value_inverse_right_deltatable) = 2 * ge_signed_half_inverse_right_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_deltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_right_deltatableentryvalue) = S ge_signed_half_inverse_right_deltatableentryvaluedecode))) /\ ((dst_positive_inverse_right_deltatable) + ge_balance_negative_inverse_right_deltatableentryvalue = (dst_negative_inverse_right_deltatable) + ge_balance_positive_inverse_right_deltatableentryvalue))))))))) /\ (forall du_index_inverse_right_delta du_value_inverse_right_delta. ~(du_index_inverse_right_delta=0) -> (exists pvs_le_gap_inverse_right_deltabound. pvs_le_gap_inverse_right_deltabound + (du_index_inverse_right_delta) = (N)) -> (exists dst_positive_code_inverse_right_deltaentry dst_positive_scale_inverse_right_deltaentry dst_negative_code_inverse_right_deltaentry dst_negative_scale_inverse_right_deltaentry dst_positive_inverse_right_deltaentry dst_negative_inverse_right_deltaentry. (((E) = (((((dst_positive_code_inverse_right_deltaentry) + (dst_positive_scale_inverse_right_deltaentry)) * S ((dst_positive_code_inverse_right_deltaentry) + (dst_positive_scale_inverse_right_deltaentry)) + ((dst_positive_scale_inverse_right_deltaentry) + (dst_positive_scale_inverse_right_deltaentry))) + (((dst_negative_code_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)) * S ((dst_negative_code_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)) + ((dst_negative_scale_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)))) * S ((((dst_positive_code_inverse_right_deltaentry) + (dst_positive_scale_inverse_right_deltaentry)) * S ((dst_positive_code_inverse_right_deltaentry) + (dst_positive_scale_inverse_right_deltaentry)) + ((dst_positive_scale_inverse_right_deltaentry) + (dst_positive_scale_inverse_right_deltaentry))) + (((dst_negative_code_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)) * S ((dst_negative_code_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)) + ((dst_negative_scale_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)))) + ((((dst_negative_code_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)) * S ((dst_negative_code_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)) + ((dst_negative_scale_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry))) + (((dst_negative_code_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)) * S ((dst_negative_code_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)) + ((dst_negative_scale_inverse_right_deltaentry) + (dst_negative_scale_inverse_right_deltaentry)))))) /\ (((((exists ff_h_pvs_inverse_right_deltaentrypositive. ff_h_pvs_inverse_right_deltaentrypositive + S (dst_positive_inverse_right_deltaentry) = S ((S (du_index_inverse_right_delta)) * dst_positive_scale_inverse_right_deltaentry)) /\ exists ff_q_pvs_inverse_right_deltaentrypositive. dst_positive_code_inverse_right_deltaentry = ff_q_pvs_inverse_right_deltaentrypositive * S ((S (du_index_inverse_right_delta)) * dst_positive_scale_inverse_right_deltaentry) + (dst_positive_inverse_right_deltaentry))) /\ (((((exists ff_h_pvs_inverse_right_deltaentrynegative. ff_h_pvs_inverse_right_deltaentrynegative + S (dst_negative_inverse_right_deltaentry) = S ((S (du_index_inverse_right_delta)) * dst_negative_scale_inverse_right_deltaentry)) /\ exists ff_q_pvs_inverse_right_deltaentrynegative. dst_negative_code_inverse_right_deltaentry = ff_q_pvs_inverse_right_deltaentrynegative * S ((S (du_index_inverse_right_delta)) * dst_negative_scale_inverse_right_deltaentry) + (dst_negative_inverse_right_deltaentry))) /\ (exists ge_balance_positive_inverse_right_deltaentryvalue ge_balance_negative_inverse_right_deltaentryvalue. (((((du_value_inverse_right_delta) = 2 * (ge_balance_positive_inverse_right_deltaentryvalue) /\ (ge_balance_negative_inverse_right_deltaentryvalue) = 0) \/ exists ge_signed_half_inverse_right_deltaentryvaluedecode. (((du_value_inverse_right_delta) = 2 * ge_signed_half_inverse_right_deltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_deltaentryvalue) = 0) /\ (ge_balance_negative_inverse_right_deltaentryvalue) = S ge_signed_half_inverse_right_deltaentryvaluedecode))) /\ ((dst_positive_inverse_right_deltaentry) + ge_balance_negative_inverse_right_deltaentryvalue = (dst_negative_inverse_right_deltaentry) + ge_balance_positive_inverse_right_deltaentryvalue))))))))) -> ((((du_index_inverse_right_delta)=1 -> (du_value_inverse_right_delta)=2) /\ (~((du_index_inverse_right_delta)=1) -> (du_value_inverse_right_delta)=0)))))) -> (((exists dst_positive_code_inverse_right_productleft dst_positive_scale_inverse_right_productleft dst_negative_code_inverse_right_productleft dst_negative_scale_inverse_right_productleft. (((G) = (((((dst_positive_code_inverse_right_productleft) + (dst_positive_scale_inverse_right_productleft)) * S ((dst_positive_code_inverse_right_productleft) + (dst_positive_scale_inverse_right_productleft)) + ((dst_positive_scale_inverse_right_productleft) + (dst_positive_scale_inverse_right_productleft))) + (((dst_negative_code_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)) * S ((dst_negative_code_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)) + ((dst_negative_scale_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)))) * S ((((dst_positive_code_inverse_right_productleft) + (dst_positive_scale_inverse_right_productleft)) * S ((dst_positive_code_inverse_right_productleft) + (dst_positive_scale_inverse_right_productleft)) + ((dst_positive_scale_inverse_right_productleft) + (dst_positive_scale_inverse_right_productleft))) + (((dst_negative_code_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)) * S ((dst_negative_code_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)) + ((dst_negative_scale_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)))) + ((((dst_negative_code_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)) * S ((dst_negative_code_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)) + ((dst_negative_scale_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft))) + (((dst_negative_code_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)) * S ((dst_negative_code_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)) + ((dst_negative_scale_inverse_right_productleft) + (dst_negative_scale_inverse_right_productleft)))))) /\ (forall dst_index_inverse_right_productleft. (exists pvs_le_gap_inverse_right_productleftdomain. pvs_le_gap_inverse_right_productleftdomain + (dst_index_inverse_right_productleft) = (N)) -> exists dst_positive_inverse_right_productleft dst_negative_inverse_right_productleft dst_value_inverse_right_productleft. ((((exists ff_h_pvs_inverse_right_productleftentrypositive. ff_h_pvs_inverse_right_productleftentrypositive + S (dst_positive_inverse_right_productleft) = S ((S (dst_index_inverse_right_productleft)) * dst_positive_scale_inverse_right_productleft)) /\ exists ff_q_pvs_inverse_right_productleftentrypositive. dst_positive_code_inverse_right_productleft = ff_q_pvs_inverse_right_productleftentrypositive * S ((S (dst_index_inverse_right_productleft)) * dst_positive_scale_inverse_right_productleft) + (dst_positive_inverse_right_productleft))) /\ (((((exists ff_h_pvs_inverse_right_productleftentrynegative. ff_h_pvs_inverse_right_productleftentrynegative + S (dst_negative_inverse_right_productleft) = S ((S (dst_index_inverse_right_productleft)) * dst_negative_scale_inverse_right_productleft)) /\ exists ff_q_pvs_inverse_right_productleftentrynegative. dst_negative_code_inverse_right_productleft = ff_q_pvs_inverse_right_productleftentrynegative * S ((S (dst_index_inverse_right_productleft)) * dst_negative_scale_inverse_right_productleft) + (dst_negative_inverse_right_productleft))) /\ (exists ge_balance_positive_inverse_right_productleftentryvalue ge_balance_negative_inverse_right_productleftentryvalue. (((((dst_value_inverse_right_productleft) = 2 * (ge_balance_positive_inverse_right_productleftentryvalue) /\ (ge_balance_negative_inverse_right_productleftentryvalue) = 0) \/ exists ge_signed_half_inverse_right_productleftentryvaluedecode. (((dst_value_inverse_right_productleft) = 2 * ge_signed_half_inverse_right_productleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_productleftentryvalue) = 0) /\ (ge_balance_negative_inverse_right_productleftentryvalue) = S ge_signed_half_inverse_right_productleftentryvaluedecode))) /\ ((dst_positive_inverse_right_productleft) + ge_balance_negative_inverse_right_productleftentryvalue = (dst_negative_inverse_right_productleft) + ge_balance_positive_inverse_right_productleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_right_productright dst_positive_scale_inverse_right_productright dst_negative_code_inverse_right_productright dst_negative_scale_inverse_right_productright. (((F) = (((((dst_positive_code_inverse_right_productright) + (dst_positive_scale_inverse_right_productright)) * S ((dst_positive_code_inverse_right_productright) + (dst_positive_scale_inverse_right_productright)) + ((dst_positive_scale_inverse_right_productright) + (dst_positive_scale_inverse_right_productright))) + (((dst_negative_code_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)) * S ((dst_negative_code_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)) + ((dst_negative_scale_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)))) * S ((((dst_positive_code_inverse_right_productright) + (dst_positive_scale_inverse_right_productright)) * S ((dst_positive_code_inverse_right_productright) + (dst_positive_scale_inverse_right_productright)) + ((dst_positive_scale_inverse_right_productright) + (dst_positive_scale_inverse_right_productright))) + (((dst_negative_code_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)) * S ((dst_negative_code_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)) + ((dst_negative_scale_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)))) + ((((dst_negative_code_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)) * S ((dst_negative_code_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)) + ((dst_negative_scale_inverse_right_productright) + (dst_negative_scale_inverse_right_productright))) + (((dst_negative_code_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)) * S ((dst_negative_code_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)) + ((dst_negative_scale_inverse_right_productright) + (dst_negative_scale_inverse_right_productright)))))) /\ (forall dst_index_inverse_right_productright. (exists pvs_le_gap_inverse_right_productrightdomain. pvs_le_gap_inverse_right_productrightdomain + (dst_index_inverse_right_productright) = (N)) -> exists dst_positive_inverse_right_productright dst_negative_inverse_right_productright dst_value_inverse_right_productright. ((((exists ff_h_pvs_inverse_right_productrightentrypositive. ff_h_pvs_inverse_right_productrightentrypositive + S (dst_positive_inverse_right_productright) = S ((S (dst_index_inverse_right_productright)) * dst_positive_scale_inverse_right_productright)) /\ exists ff_q_pvs_inverse_right_productrightentrypositive. dst_positive_code_inverse_right_productright = ff_q_pvs_inverse_right_productrightentrypositive * S ((S (dst_index_inverse_right_productright)) * dst_positive_scale_inverse_right_productright) + (dst_positive_inverse_right_productright))) /\ (((((exists ff_h_pvs_inverse_right_productrightentrynegative. ff_h_pvs_inverse_right_productrightentrynegative + S (dst_negative_inverse_right_productright) = S ((S (dst_index_inverse_right_productright)) * dst_negative_scale_inverse_right_productright)) /\ exists ff_q_pvs_inverse_right_productrightentrynegative. dst_negative_code_inverse_right_productright = ff_q_pvs_inverse_right_productrightentrynegative * S ((S (dst_index_inverse_right_productright)) * dst_negative_scale_inverse_right_productright) + (dst_negative_inverse_right_productright))) /\ (exists ge_balance_positive_inverse_right_productrightentryvalue ge_balance_negative_inverse_right_productrightentryvalue. (((((dst_value_inverse_right_productright) = 2 * (ge_balance_positive_inverse_right_productrightentryvalue) /\ (ge_balance_negative_inverse_right_productrightentryvalue) = 0) \/ exists ge_signed_half_inverse_right_productrightentryvaluedecode. (((dst_value_inverse_right_productright) = 2 * ge_signed_half_inverse_right_productrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_productrightentryvalue) = 0) /\ (ge_balance_negative_inverse_right_productrightentryvalue) = S ge_signed_half_inverse_right_productrightentryvaluedecode))) /\ ((dst_positive_inverse_right_productright) + ge_balance_negative_inverse_right_productrightentryvalue = (dst_negative_inverse_right_productright) + ge_balance_positive_inverse_right_productrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_right_producttable dst_positive_scale_inverse_right_producttable dst_negative_code_inverse_right_producttable dst_negative_scale_inverse_right_producttable. (((E) = (((((dst_positive_code_inverse_right_producttable) + (dst_positive_scale_inverse_right_producttable)) * S ((dst_positive_code_inverse_right_producttable) + (dst_positive_scale_inverse_right_producttable)) + ((dst_positive_scale_inverse_right_producttable) + (dst_positive_scale_inverse_right_producttable))) + (((dst_negative_code_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)) * S ((dst_negative_code_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)) + ((dst_negative_scale_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)))) * S ((((dst_positive_code_inverse_right_producttable) + (dst_positive_scale_inverse_right_producttable)) * S ((dst_positive_code_inverse_right_producttable) + (dst_positive_scale_inverse_right_producttable)) + ((dst_positive_scale_inverse_right_producttable) + (dst_positive_scale_inverse_right_producttable))) + (((dst_negative_code_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)) * S ((dst_negative_code_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)) + ((dst_negative_scale_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)))) + ((((dst_negative_code_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)) * S ((dst_negative_code_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)) + ((dst_negative_scale_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable))) + (((dst_negative_code_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)) * S ((dst_negative_code_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)) + ((dst_negative_scale_inverse_right_producttable) + (dst_negative_scale_inverse_right_producttable)))))) /\ (forall dst_index_inverse_right_producttable. (exists pvs_le_gap_inverse_right_producttabledomain. pvs_le_gap_inverse_right_producttabledomain + (dst_index_inverse_right_producttable) = (N)) -> exists dst_positive_inverse_right_producttable dst_negative_inverse_right_producttable dst_value_inverse_right_producttable. ((((exists ff_h_pvs_inverse_right_producttableentrypositive. ff_h_pvs_inverse_right_producttableentrypositive + S (dst_positive_inverse_right_producttable) = S ((S (dst_index_inverse_right_producttable)) * dst_positive_scale_inverse_right_producttable)) /\ exists ff_q_pvs_inverse_right_producttableentrypositive. dst_positive_code_inverse_right_producttable = ff_q_pvs_inverse_right_producttableentrypositive * S ((S (dst_index_inverse_right_producttable)) * dst_positive_scale_inverse_right_producttable) + (dst_positive_inverse_right_producttable))) /\ (((((exists ff_h_pvs_inverse_right_producttableentrynegative. ff_h_pvs_inverse_right_producttableentrynegative + S (dst_negative_inverse_right_producttable) = S ((S (dst_index_inverse_right_producttable)) * dst_negative_scale_inverse_right_producttable)) /\ exists ff_q_pvs_inverse_right_producttableentrynegative. dst_negative_code_inverse_right_producttable = ff_q_pvs_inverse_right_producttableentrynegative * S ((S (dst_index_inverse_right_producttable)) * dst_negative_scale_inverse_right_producttable) + (dst_negative_inverse_right_producttable))) /\ (exists ge_balance_positive_inverse_right_producttableentryvalue ge_balance_negative_inverse_right_producttableentryvalue. (((((dst_value_inverse_right_producttable) = 2 * (ge_balance_positive_inverse_right_producttableentryvalue) /\ (ge_balance_negative_inverse_right_producttableentryvalue) = 0) \/ exists ge_signed_half_inverse_right_producttableentryvaluedecode. (((dst_value_inverse_right_producttable) = 2 * ge_signed_half_inverse_right_producttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_producttableentryvalue) = 0) /\ (ge_balance_negative_inverse_right_producttableentryvalue) = S ge_signed_half_inverse_right_producttableentryvaluedecode))) /\ ((dst_positive_inverse_right_producttable) + ge_balance_negative_inverse_right_producttableentryvalue = (dst_negative_inverse_right_producttable) + ge_balance_positive_inverse_right_producttableentryvalue))))))))) /\ (forall dc_input_inverse_right_product dc_output_inverse_right_product. ~(dc_input_inverse_right_product=0) -> (exists pvs_le_gap_inverse_right_productdomain. pvs_le_gap_inverse_right_productdomain + (dc_input_inverse_right_product) = (N)) -> (exists dst_positive_code_inverse_right_productlookup dst_positive_scale_inverse_right_productlookup dst_negative_code_inverse_right_productlookup dst_negative_scale_inverse_right_productlookup dst_positive_inverse_right_productlookup dst_negative_inverse_right_productlookup. (((E) = (((((dst_positive_code_inverse_right_productlookup) + (dst_positive_scale_inverse_right_productlookup)) * S ((dst_positive_code_inverse_right_productlookup) + (dst_positive_scale_inverse_right_productlookup)) + ((dst_positive_scale_inverse_right_productlookup) + (dst_positive_scale_inverse_right_productlookup))) + (((dst_negative_code_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)) * S ((dst_negative_code_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)) + ((dst_negative_scale_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)))) * S ((((dst_positive_code_inverse_right_productlookup) + (dst_positive_scale_inverse_right_productlookup)) * S ((dst_positive_code_inverse_right_productlookup) + (dst_positive_scale_inverse_right_productlookup)) + ((dst_positive_scale_inverse_right_productlookup) + (dst_positive_scale_inverse_right_productlookup))) + (((dst_negative_code_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)) * S ((dst_negative_code_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)) + ((dst_negative_scale_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)))) + ((((dst_negative_code_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)) * S ((dst_negative_code_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)) + ((dst_negative_scale_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup))) + (((dst_negative_code_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)) * S ((dst_negative_code_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)) + ((dst_negative_scale_inverse_right_productlookup) + (dst_negative_scale_inverse_right_productlookup)))))) /\ (((((exists ff_h_pvs_inverse_right_productlookuppositive. ff_h_pvs_inverse_right_productlookuppositive + S (dst_positive_inverse_right_productlookup) = S ((S (dc_input_inverse_right_product)) * dst_positive_scale_inverse_right_productlookup)) /\ exists ff_q_pvs_inverse_right_productlookuppositive. dst_positive_code_inverse_right_productlookup = ff_q_pvs_inverse_right_productlookuppositive * S ((S (dc_input_inverse_right_product)) * dst_positive_scale_inverse_right_productlookup) + (dst_positive_inverse_right_productlookup))) /\ (((((exists ff_h_pvs_inverse_right_productlookupnegative. ff_h_pvs_inverse_right_productlookupnegative + S (dst_negative_inverse_right_productlookup) = S ((S (dc_input_inverse_right_product)) * dst_negative_scale_inverse_right_productlookup)) /\ exists ff_q_pvs_inverse_right_productlookupnegative. dst_negative_code_inverse_right_productlookup = ff_q_pvs_inverse_right_productlookupnegative * S ((S (dc_input_inverse_right_product)) * dst_negative_scale_inverse_right_productlookup) + (dst_negative_inverse_right_productlookup))) /\ (exists ge_balance_positive_inverse_right_productlookupvalue ge_balance_negative_inverse_right_productlookupvalue. (((((dc_output_inverse_right_product) = 2 * (ge_balance_positive_inverse_right_productlookupvalue) /\ (ge_balance_negative_inverse_right_productlookupvalue) = 0) \/ exists ge_signed_half_inverse_right_productlookupvaluedecode. (((dc_output_inverse_right_product) = 2 * ge_signed_half_inverse_right_productlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_right_productlookupvalue) = 0) /\ (ge_balance_negative_inverse_right_productlookupvalue) = S ge_signed_half_inverse_right_productlookupvaluedecode))) /\ ((dst_positive_inverse_right_productlookup) + ge_balance_negative_inverse_right_productlookupvalue = (dst_negative_inverse_right_productlookup) + ge_balance_positive_inverse_right_productlookupvalue))))))))) -> (((~((dc_input_inverse_right_product)=0)) /\ (exists dc_mask_inverse_right_productvalue. ((((exists dst_positive_code_inverse_right_productvaluemasktable dst_positive_scale_inverse_right_productvaluemasktable dst_negative_code_inverse_right_productvaluemasktable dst_negative_scale_inverse_right_productvaluemasktable. (((dc_mask_inverse_right_productvalue) = (((((dst_positive_code_inverse_right_productvaluemasktable) + (dst_positive_scale_inverse_right_productvaluemasktable)) * S ((dst_positive_code_inverse_right_productvaluemasktable) + (dst_positive_scale_inverse_right_productvaluemasktable)) + ((dst_positive_scale_inverse_right_productvaluemasktable) + (dst_positive_scale_inverse_right_productvaluemasktable))) + (((dst_negative_code_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)) * S ((dst_negative_code_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)) + ((dst_negative_scale_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)))) * S ((((dst_positive_code_inverse_right_productvaluemasktable) + (dst_positive_scale_inverse_right_productvaluemasktable)) * S ((dst_positive_code_inverse_right_productvaluemasktable) + (dst_positive_scale_inverse_right_productvaluemasktable)) + ((dst_positive_scale_inverse_right_productvaluemasktable) + (dst_positive_scale_inverse_right_productvaluemasktable))) + (((dst_negative_code_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)) * S ((dst_negative_code_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)) + ((dst_negative_scale_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)))) + ((((dst_negative_code_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)) * S ((dst_negative_code_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)) + ((dst_negative_scale_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable))) + (((dst_negative_code_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)) * S ((dst_negative_code_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)) + ((dst_negative_scale_inverse_right_productvaluemasktable) + (dst_negative_scale_inverse_right_productvaluemasktable)))))) /\ (forall dst_index_inverse_right_productvaluemasktable. (exists pvs_le_gap_inverse_right_productvaluemasktabledomain. pvs_le_gap_inverse_right_productvaluemasktabledomain + (dst_index_inverse_right_productvaluemasktable) = (dc_input_inverse_right_product)) -> exists dst_positive_inverse_right_productvaluemasktable dst_negative_inverse_right_productvaluemasktable dst_value_inverse_right_productvaluemasktable. ((((exists ff_h_pvs_inverse_right_productvaluemasktableentrypositive. ff_h_pvs_inverse_right_productvaluemasktableentrypositive + S (dst_positive_inverse_right_productvaluemasktable) = S ((S (dst_index_inverse_right_productvaluemasktable)) * dst_positive_scale_inverse_right_productvaluemasktable)) /\ exists ff_q_pvs_inverse_right_productvaluemasktableentrypositive. dst_positive_code_inverse_right_productvaluemasktable = ff_q_pvs_inverse_right_productvaluemasktableentrypositive * S ((S (dst_index_inverse_right_productvaluemasktable)) * dst_positive_scale_inverse_right_productvaluemasktable) + (dst_positive_inverse_right_productvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_right_productvaluemasktableentrynegative. ff_h_pvs_inverse_right_productvaluemasktableentrynegative + S (dst_negative_inverse_right_productvaluemasktable) = S ((S (dst_index_inverse_right_productvaluemasktable)) * dst_negative_scale_inverse_right_productvaluemasktable)) /\ exists ff_q_pvs_inverse_right_productvaluemasktableentrynegative. dst_negative_code_inverse_right_productvaluemasktable = ff_q_pvs_inverse_right_productvaluemasktableentrynegative * S ((S (dst_index_inverse_right_productvaluemasktable)) * dst_negative_scale_inverse_right_productvaluemasktable) + (dst_negative_inverse_right_productvaluemasktable))) /\ (exists ge_balance_positive_inverse_right_productvaluemasktableentryvalue ge_balance_negative_inverse_right_productvaluemasktableentryvalue. (((((dst_value_inverse_right_productvaluemasktable) = 2 * (ge_balance_positive_inverse_right_productvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_right_productvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_right_productvaluemasktableentryvaluedecode. (((dst_value_inverse_right_productvaluemasktable) = 2 * ge_signed_half_inverse_right_productvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_productvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_right_productvaluemasktableentryvalue) = S ge_signed_half_inverse_right_productvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_right_productvaluemasktable) + ge_balance_negative_inverse_right_productvaluemasktableentryvalue = (dst_negative_inverse_right_productvaluemasktable) + ge_balance_positive_inverse_right_productvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_right_productvaluemask dc_value_inverse_right_productvaluemask. (exists pvs_le_gap_inverse_right_productvaluemaskdomain. pvs_le_gap_inverse_right_productvaluemaskdomain + (dc_index_inverse_right_productvaluemask) = (dc_input_inverse_right_product)) -> (exists dst_positive_code_inverse_right_productvaluemasklookup dst_positive_scale_inverse_right_productvaluemasklookup dst_negative_code_inverse_right_productvaluemasklookup dst_negative_scale_inverse_right_productvaluemasklookup dst_positive_inverse_right_productvaluemasklookup dst_negative_inverse_right_productvaluemasklookup. (((dc_mask_inverse_right_productvalue) = (((((dst_positive_code_inverse_right_productvaluemasklookup) + (dst_positive_scale_inverse_right_productvaluemasklookup)) * S ((dst_positive_code_inverse_right_productvaluemasklookup) + (dst_positive_scale_inverse_right_productvaluemasklookup)) + ((dst_positive_scale_inverse_right_productvaluemasklookup) + (dst_positive_scale_inverse_right_productvaluemasklookup))) + (((dst_negative_code_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)) * S ((dst_negative_code_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)) + ((dst_negative_scale_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)))) * S ((((dst_positive_code_inverse_right_productvaluemasklookup) + (dst_positive_scale_inverse_right_productvaluemasklookup)) * S ((dst_positive_code_inverse_right_productvaluemasklookup) + (dst_positive_scale_inverse_right_productvaluemasklookup)) + ((dst_positive_scale_inverse_right_productvaluemasklookup) + (dst_positive_scale_inverse_right_productvaluemasklookup))) + (((dst_negative_code_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)) * S ((dst_negative_code_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)) + ((dst_negative_scale_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)))) + ((((dst_negative_code_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)) * S ((dst_negative_code_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)) + ((dst_negative_scale_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup))) + (((dst_negative_code_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)) * S ((dst_negative_code_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)) + ((dst_negative_scale_inverse_right_productvaluemasklookup) + (dst_negative_scale_inverse_right_productvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_right_productvaluemasklookuppositive. ff_h_pvs_inverse_right_productvaluemasklookuppositive + S (dst_positive_inverse_right_productvaluemasklookup) = S ((S (dc_index_inverse_right_productvaluemask)) * dst_positive_scale_inverse_right_productvaluemasklookup)) /\ exists ff_q_pvs_inverse_right_productvaluemasklookuppositive. dst_positive_code_inverse_right_productvaluemasklookup = ff_q_pvs_inverse_right_productvaluemasklookuppositive * S ((S (dc_index_inverse_right_productvaluemask)) * dst_positive_scale_inverse_right_productvaluemasklookup) + (dst_positive_inverse_right_productvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_right_productvaluemasklookupnegative. ff_h_pvs_inverse_right_productvaluemasklookupnegative + S (dst_negative_inverse_right_productvaluemasklookup) = S ((S (dc_index_inverse_right_productvaluemask)) * dst_negative_scale_inverse_right_productvaluemasklookup)) /\ exists ff_q_pvs_inverse_right_productvaluemasklookupnegative. dst_negative_code_inverse_right_productvaluemasklookup = ff_q_pvs_inverse_right_productvaluemasklookupnegative * S ((S (dc_index_inverse_right_productvaluemask)) * dst_negative_scale_inverse_right_productvaluemasklookup) + (dst_negative_inverse_right_productvaluemasklookup))) /\ (exists ge_balance_positive_inverse_right_productvaluemasklookupvalue ge_balance_negative_inverse_right_productvaluemasklookupvalue. (((((dc_value_inverse_right_productvaluemask) = 2 * (ge_balance_positive_inverse_right_productvaluemasklookupvalue) /\ (ge_balance_negative_inverse_right_productvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_right_productvaluemasklookupvaluedecode. (((dc_value_inverse_right_productvaluemask) = 2 * ge_signed_half_inverse_right_productvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_right_productvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_right_productvaluemasklookupvalue) = S ge_signed_half_inverse_right_productvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_right_productvaluemasklookup) + ge_balance_negative_inverse_right_productvaluemasklookupvalue = (dst_negative_inverse_right_productvaluemasklookup) + ge_balance_positive_inverse_right_productvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_right_productvaluemask)=0)) /\ (exists dc_quotient_inverse_right_productvaluemaskentry dc_left_inverse_right_productvaluemaskentry dc_right_inverse_right_productvaluemaskentry. (((dc_input_inverse_right_product)=(dc_index_inverse_right_productvaluemask)*dc_quotient_inverse_right_productvaluemaskentry) /\ (((exists dst_positive_code_inverse_right_productvaluemaskentryleft dst_positive_scale_inverse_right_productvaluemaskentryleft dst_negative_code_inverse_right_productvaluemaskentryleft dst_negative_scale_inverse_right_productvaluemaskentryleft dst_positive_inverse_right_productvaluemaskentryleft dst_negative_inverse_right_productvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_right_productvaluemaskentryleft) + (dst_positive_scale_inverse_right_productvaluemaskentryleft)) * S ((dst_positive_code_inverse_right_productvaluemaskentryleft) + (dst_positive_scale_inverse_right_productvaluemaskentryleft)) + ((dst_positive_scale_inverse_right_productvaluemaskentryleft) + (dst_positive_scale_inverse_right_productvaluemaskentryleft))) + (((dst_negative_code_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_right_productvaluemaskentryleft) + (dst_positive_scale_inverse_right_productvaluemaskentryleft)) * S ((dst_positive_code_inverse_right_productvaluemaskentryleft) + (dst_positive_scale_inverse_right_productvaluemaskentryleft)) + ((dst_positive_scale_inverse_right_productvaluemaskentryleft) + (dst_positive_scale_inverse_right_productvaluemaskentryleft))) + (((dst_negative_code_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)))) + ((((dst_negative_code_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft))) + (((dst_negative_code_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_productvaluemaskentryleft) + (dst_negative_scale_inverse_right_productvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_right_productvaluemaskentryleftpositive. ff_h_pvs_inverse_right_productvaluemaskentryleftpositive + S (dst_positive_inverse_right_productvaluemaskentryleft) = S ((S (dc_index_inverse_right_productvaluemask)) * dst_positive_scale_inverse_right_productvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_right_productvaluemaskentryleftpositive. dst_positive_code_inverse_right_productvaluemaskentryleft = ff_q_pvs_inverse_right_productvaluemaskentryleftpositive * S ((S (dc_index_inverse_right_productvaluemask)) * dst_positive_scale_inverse_right_productvaluemaskentryleft) + (dst_positive_inverse_right_productvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_right_productvaluemaskentryleftnegative. ff_h_pvs_inverse_right_productvaluemaskentryleftnegative + S (dst_negative_inverse_right_productvaluemaskentryleft) = S ((S (dc_index_inverse_right_productvaluemask)) * dst_negative_scale_inverse_right_productvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_right_productvaluemaskentryleftnegative. dst_negative_code_inverse_right_productvaluemaskentryleft = ff_q_pvs_inverse_right_productvaluemaskentryleftnegative * S ((S (dc_index_inverse_right_productvaluemask)) * dst_negative_scale_inverse_right_productvaluemaskentryleft) + (dst_negative_inverse_right_productvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_right_productvaluemaskentryleftvalue ge_balance_negative_inverse_right_productvaluemaskentryleftvalue. (((((dc_left_inverse_right_productvaluemaskentry) = 2 * (ge_balance_positive_inverse_right_productvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_right_productvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_right_productvaluemaskentryleftvaluedecode. (((dc_left_inverse_right_productvaluemaskentry) = 2 * ge_signed_half_inverse_right_productvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_right_productvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_right_productvaluemaskentryleftvalue) = S ge_signed_half_inverse_right_productvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_right_productvaluemaskentryleft) + ge_balance_negative_inverse_right_productvaluemaskentryleftvalue = (dst_negative_inverse_right_productvaluemaskentryleft) + ge_balance_positive_inverse_right_productvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_right_productvaluemaskentryright dst_positive_scale_inverse_right_productvaluemaskentryright dst_negative_code_inverse_right_productvaluemaskentryright dst_negative_scale_inverse_right_productvaluemaskentryright dst_positive_inverse_right_productvaluemaskentryright dst_negative_inverse_right_productvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_right_productvaluemaskentryright) + (dst_positive_scale_inverse_right_productvaluemaskentryright)) * S ((dst_positive_code_inverse_right_productvaluemaskentryright) + (dst_positive_scale_inverse_right_productvaluemaskentryright)) + ((dst_positive_scale_inverse_right_productvaluemaskentryright) + (dst_positive_scale_inverse_right_productvaluemaskentryright))) + (((dst_negative_code_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)) * S ((dst_negative_code_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)) + ((dst_negative_scale_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)))) * S ((((dst_positive_code_inverse_right_productvaluemaskentryright) + (dst_positive_scale_inverse_right_productvaluemaskentryright)) * S ((dst_positive_code_inverse_right_productvaluemaskentryright) + (dst_positive_scale_inverse_right_productvaluemaskentryright)) + ((dst_positive_scale_inverse_right_productvaluemaskentryright) + (dst_positive_scale_inverse_right_productvaluemaskentryright))) + (((dst_negative_code_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)) * S ((dst_negative_code_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)) + ((dst_negative_scale_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)))) + ((((dst_negative_code_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)) * S ((dst_negative_code_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)) + ((dst_negative_scale_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright))) + (((dst_negative_code_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)) * S ((dst_negative_code_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)) + ((dst_negative_scale_inverse_right_productvaluemaskentryright) + (dst_negative_scale_inverse_right_productvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_right_productvaluemaskentryrightpositive. ff_h_pvs_inverse_right_productvaluemaskentryrightpositive + S (dst_positive_inverse_right_productvaluemaskentryright) = S ((S (dc_quotient_inverse_right_productvaluemaskentry)) * dst_positive_scale_inverse_right_productvaluemaskentryright)) /\ exists ff_q_pvs_inverse_right_productvaluemaskentryrightpositive. dst_positive_code_inverse_right_productvaluemaskentryright = ff_q_pvs_inverse_right_productvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_right_productvaluemaskentry)) * dst_positive_scale_inverse_right_productvaluemaskentryright) + (dst_positive_inverse_right_productvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_right_productvaluemaskentryrightnegative. ff_h_pvs_inverse_right_productvaluemaskentryrightnegative + S (dst_negative_inverse_right_productvaluemaskentryright) = S ((S (dc_quotient_inverse_right_productvaluemaskentry)) * dst_negative_scale_inverse_right_productvaluemaskentryright)) /\ exists ff_q_pvs_inverse_right_productvaluemaskentryrightnegative. dst_negative_code_inverse_right_productvaluemaskentryright = ff_q_pvs_inverse_right_productvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_right_productvaluemaskentry)) * dst_negative_scale_inverse_right_productvaluemaskentryright) + (dst_negative_inverse_right_productvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_right_productvaluemaskentryrightvalue ge_balance_negative_inverse_right_productvaluemaskentryrightvalue. (((((dc_right_inverse_right_productvaluemaskentry) = 2 * (ge_balance_positive_inverse_right_productvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_right_productvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_right_productvaluemaskentryrightvaluedecode. (((dc_right_inverse_right_productvaluemaskentry) = 2 * ge_signed_half_inverse_right_productvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_right_productvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_right_productvaluemaskentryrightvalue) = S ge_signed_half_inverse_right_productvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_right_productvaluemaskentryright) + ge_balance_negative_inverse_right_productvaluemaskentryrightvalue = (dst_negative_inverse_right_productvaluemaskentryright) + ge_balance_positive_inverse_right_productvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_right_productvaluemaskentryproduct sto_an_inverse_right_productvaluemaskentryproduct sto_bp_inverse_right_productvaluemaskentryproduct sto_bn_inverse_right_productvaluemaskentryproduct sto_cp_inverse_right_productvaluemaskentryproduct sto_cn_inverse_right_productvaluemaskentryproduct. (((((dc_left_inverse_right_productvaluemaskentry) = 2 * (sto_ap_inverse_right_productvaluemaskentryproduct) /\ (sto_an_inverse_right_productvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_productvaluemaskentryproductleft. (((dc_left_inverse_right_productvaluemaskentry) = 2 * ge_signed_half_inverse_right_productvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_right_productvaluemaskentryproduct) = 0) /\ (sto_an_inverse_right_productvaluemaskentryproduct) = S ge_signed_half_inverse_right_productvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_right_productvaluemaskentry) = 2 * (sto_bp_inverse_right_productvaluemaskentryproduct) /\ (sto_bn_inverse_right_productvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_productvaluemaskentryproductright. (((dc_right_inverse_right_productvaluemaskentry) = 2 * ge_signed_half_inverse_right_productvaluemaskentryproductright + 1 /\ (sto_bp_inverse_right_productvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_right_productvaluemaskentryproduct) = S ge_signed_half_inverse_right_productvaluemaskentryproductright))) /\ ((((((dc_value_inverse_right_productvaluemask) = 2 * (sto_cp_inverse_right_productvaluemaskentryproduct) /\ (sto_cn_inverse_right_productvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_productvaluemaskentryproductoutput. (((dc_value_inverse_right_productvaluemask) = 2 * ge_signed_half_inverse_right_productvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_right_productvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_right_productvaluemaskentryproduct) = S ge_signed_half_inverse_right_productvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_right_productvaluemaskentryproduct * sto_bp_inverse_right_productvaluemaskentryproduct + sto_an_inverse_right_productvaluemaskentryproduct * sto_bn_inverse_right_productvaluemaskentryproduct) + sto_cn_inverse_right_productvaluemaskentryproduct = (sto_ap_inverse_right_productvaluemaskentryproduct * sto_bn_inverse_right_productvaluemaskentryproduct + sto_an_inverse_right_productvaluemaskentryproduct * sto_bp_inverse_right_productvaluemaskentryproduct) + sto_cp_inverse_right_productvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_right_productvaluemask)=0 \/ ~(exists pvs_factor_inverse_right_productvaluemaskentrynondivisor. (dc_input_inverse_right_product) = (dc_index_inverse_right_productvaluemask) * pvs_factor_inverse_right_productvaluemaskentrynondivisor)) /\ ((dc_value_inverse_right_productvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_right_productvaluefold dst_positive_scale_inverse_right_productvaluefold dst_negative_code_inverse_right_productvaluefold dst_negative_scale_inverse_right_productvaluefold dst_positive_sum_inverse_right_productvaluefold dst_negative_sum_inverse_right_productvaluefold. (((dc_mask_inverse_right_productvalue) = (((((dst_positive_code_inverse_right_productvaluefold) + (dst_positive_scale_inverse_right_productvaluefold)) * S ((dst_positive_code_inverse_right_productvaluefold) + (dst_positive_scale_inverse_right_productvaluefold)) + ((dst_positive_scale_inverse_right_productvaluefold) + (dst_positive_scale_inverse_right_productvaluefold))) + (((dst_negative_code_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)) * S ((dst_negative_code_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)) + ((dst_negative_scale_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)))) * S ((((dst_positive_code_inverse_right_productvaluefold) + (dst_positive_scale_inverse_right_productvaluefold)) * S ((dst_positive_code_inverse_right_productvaluefold) + (dst_positive_scale_inverse_right_productvaluefold)) + ((dst_positive_scale_inverse_right_productvaluefold) + (dst_positive_scale_inverse_right_productvaluefold))) + (((dst_negative_code_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)) * S ((dst_negative_code_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)) + ((dst_negative_scale_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)))) + ((((dst_negative_code_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)) * S ((dst_negative_code_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)) + ((dst_negative_scale_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold))) + (((dst_negative_code_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)) * S ((dst_negative_code_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)) + ((dst_negative_scale_inverse_right_productvaluefold) + (dst_negative_scale_inverse_right_productvaluefold)))))) /\ (((exists fs_u_dst_inverse_right_productvaluefoldpositive fs_v_dst_inverse_right_productvaluefoldpositive. ((((exists fs_h_dst_inverse_right_productvaluefoldpositive_body_start. fs_h_dst_inverse_right_productvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_right_productvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_productvaluefoldpositive_body_start. fs_u_dst_inverse_right_productvaluefoldpositive = fs_q_dst_inverse_right_productvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_right_productvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_right_productvaluefoldpositive_body_terminal. fs_h_dst_inverse_right_productvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_right_productvaluefold) = S ((S (S (dc_input_inverse_right_product))) * fs_v_dst_inverse_right_productvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_productvaluefoldpositive_body_terminal. fs_u_dst_inverse_right_productvaluefoldpositive = fs_q_dst_inverse_right_productvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_right_product))) * fs_v_dst_inverse_right_productvaluefoldpositive) + (dst_positive_sum_inverse_right_productvaluefold))) /\ forall fs_i_dst_inverse_right_productvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_right_productvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_right_productvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_right_productvaluefoldpositive_body_steps = S (dc_input_inverse_right_product)) -> exists fs_a_dst_inverse_right_productvaluefoldpositive_body_steps fs_r_dst_inverse_right_productvaluefoldpositive_body_steps fs_s_dst_inverse_right_productvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_right_productvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_right_productvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_right_productvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_right_productvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_right_productvaluefold)) /\ exists fs_q_dst_inverse_right_productvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_right_productvaluefold = fs_q_dst_inverse_right_productvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_right_productvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_right_productvaluefold) + (fs_a_dst_inverse_right_productvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_right_productvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_right_productvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_right_productvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_right_productvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_productvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_productvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_right_productvaluefoldpositive = fs_q_dst_inverse_right_productvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_right_productvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_productvaluefoldpositive) + (fs_r_dst_inverse_right_productvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_right_productvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_right_productvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_right_productvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_right_productvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_productvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_productvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_right_productvaluefoldpositive = fs_q_dst_inverse_right_productvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_right_productvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_productvaluefoldpositive) + (fs_s_dst_inverse_right_productvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_right_productvaluefoldpositive_body_steps = fs_r_dst_inverse_right_productvaluefoldpositive_body_steps + fs_a_dst_inverse_right_productvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_right_productvaluefoldnegative fs_v_dst_inverse_right_productvaluefoldnegative. ((((exists fs_h_dst_inverse_right_productvaluefoldnegative_body_start. fs_h_dst_inverse_right_productvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_right_productvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_productvaluefoldnegative_body_start. fs_u_dst_inverse_right_productvaluefoldnegative = fs_q_dst_inverse_right_productvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_right_productvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_right_productvaluefoldnegative_body_terminal. fs_h_dst_inverse_right_productvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_right_productvaluefold) = S ((S (S (dc_input_inverse_right_product))) * fs_v_dst_inverse_right_productvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_productvaluefoldnegative_body_terminal. fs_u_dst_inverse_right_productvaluefoldnegative = fs_q_dst_inverse_right_productvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_right_product))) * fs_v_dst_inverse_right_productvaluefoldnegative) + (dst_negative_sum_inverse_right_productvaluefold))) /\ forall fs_i_dst_inverse_right_productvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_right_productvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_right_productvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_right_productvaluefoldnegative_body_steps = S (dc_input_inverse_right_product)) -> exists fs_a_dst_inverse_right_productvaluefoldnegative_body_steps fs_r_dst_inverse_right_productvaluefoldnegative_body_steps fs_s_dst_inverse_right_productvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_right_productvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_right_productvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_right_productvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_right_productvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_right_productvaluefold)) /\ exists fs_q_dst_inverse_right_productvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_right_productvaluefold = fs_q_dst_inverse_right_productvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_right_productvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_right_productvaluefold) + (fs_a_dst_inverse_right_productvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_right_productvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_right_productvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_right_productvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_right_productvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_productvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_productvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_right_productvaluefoldnegative = fs_q_dst_inverse_right_productvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_right_productvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_productvaluefoldnegative) + (fs_r_dst_inverse_right_productvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_right_productvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_right_productvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_right_productvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_right_productvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_productvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_productvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_right_productvaluefoldnegative = fs_q_dst_inverse_right_productvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_right_productvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_productvaluefoldnegative) + (fs_s_dst_inverse_right_productvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_right_productvaluefoldnegative_body_steps = fs_r_dst_inverse_right_productvaluefoldnegative_body_steps + fs_a_dst_inverse_right_productvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_right_productvaluefoldresult ge_balance_negative_inverse_right_productvaluefoldresult. (((((dc_output_inverse_right_product) = 2 * (ge_balance_positive_inverse_right_productvaluefoldresult) /\ (ge_balance_negative_inverse_right_productvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_right_productvaluefoldresultdecode. (((dc_output_inverse_right_product) = 2 * ge_signed_half_inverse_right_productvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_right_productvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_right_productvaluefoldresult) = S ge_signed_half_inverse_right_productvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_right_productvaluefold) + ge_balance_negative_inverse_right_productvaluefoldresult = (dst_negative_sum_inverse_right_productvaluefold) + ge_balance_positive_inverse_right_productvaluefoldresult)))))))))))))))))))) -> (exists di_delta_inverse_right_result. ((((exists dst_positive_code_inverse_right_resultdeltatable dst_positive_scale_inverse_right_resultdeltatable dst_negative_code_inverse_right_resultdeltatable dst_negative_scale_inverse_right_resultdeltatable. (((di_delta_inverse_right_result) = (((((dst_positive_code_inverse_right_resultdeltatable) + (dst_positive_scale_inverse_right_resultdeltatable)) * S ((dst_positive_code_inverse_right_resultdeltatable) + (dst_positive_scale_inverse_right_resultdeltatable)) + ((dst_positive_scale_inverse_right_resultdeltatable) + (dst_positive_scale_inverse_right_resultdeltatable))) + (((dst_negative_code_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)) * S ((dst_negative_code_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)) + ((dst_negative_scale_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)))) * S ((((dst_positive_code_inverse_right_resultdeltatable) + (dst_positive_scale_inverse_right_resultdeltatable)) * S ((dst_positive_code_inverse_right_resultdeltatable) + (dst_positive_scale_inverse_right_resultdeltatable)) + ((dst_positive_scale_inverse_right_resultdeltatable) + (dst_positive_scale_inverse_right_resultdeltatable))) + (((dst_negative_code_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)) * S ((dst_negative_code_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)) + ((dst_negative_scale_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)))) + ((((dst_negative_code_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)) * S ((dst_negative_code_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)) + ((dst_negative_scale_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable))) + (((dst_negative_code_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)) * S ((dst_negative_code_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)) + ((dst_negative_scale_inverse_right_resultdeltatable) + (dst_negative_scale_inverse_right_resultdeltatable)))))) /\ (forall dst_index_inverse_right_resultdeltatable. (exists pvs_le_gap_inverse_right_resultdeltatabledomain. pvs_le_gap_inverse_right_resultdeltatabledomain + (dst_index_inverse_right_resultdeltatable) = (N)) -> exists dst_positive_inverse_right_resultdeltatable dst_negative_inverse_right_resultdeltatable dst_value_inverse_right_resultdeltatable. ((((exists ff_h_pvs_inverse_right_resultdeltatableentrypositive. ff_h_pvs_inverse_right_resultdeltatableentrypositive + S (dst_positive_inverse_right_resultdeltatable) = S ((S (dst_index_inverse_right_resultdeltatable)) * dst_positive_scale_inverse_right_resultdeltatable)) /\ exists ff_q_pvs_inverse_right_resultdeltatableentrypositive. dst_positive_code_inverse_right_resultdeltatable = ff_q_pvs_inverse_right_resultdeltatableentrypositive * S ((S (dst_index_inverse_right_resultdeltatable)) * dst_positive_scale_inverse_right_resultdeltatable) + (dst_positive_inverse_right_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_right_resultdeltatableentrynegative. ff_h_pvs_inverse_right_resultdeltatableentrynegative + S (dst_negative_inverse_right_resultdeltatable) = S ((S (dst_index_inverse_right_resultdeltatable)) * dst_negative_scale_inverse_right_resultdeltatable)) /\ exists ff_q_pvs_inverse_right_resultdeltatableentrynegative. dst_negative_code_inverse_right_resultdeltatable = ff_q_pvs_inverse_right_resultdeltatableentrynegative * S ((S (dst_index_inverse_right_resultdeltatable)) * dst_negative_scale_inverse_right_resultdeltatable) + (dst_negative_inverse_right_resultdeltatable))) /\ (exists ge_balance_positive_inverse_right_resultdeltatableentryvalue ge_balance_negative_inverse_right_resultdeltatableentryvalue. (((((dst_value_inverse_right_resultdeltatable) = 2 * (ge_balance_positive_inverse_right_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_right_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultdeltatableentryvaluedecode. (((dst_value_inverse_right_resultdeltatable) = 2 * ge_signed_half_inverse_right_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultdeltatableentryvalue) = S ge_signed_half_inverse_right_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_right_resultdeltatable) + ge_balance_negative_inverse_right_resultdeltatableentryvalue = (dst_negative_inverse_right_resultdeltatable) + ge_balance_positive_inverse_right_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_right_resultdelta du_value_inverse_right_resultdelta. ~(du_index_inverse_right_resultdelta=0) -> (exists pvs_le_gap_inverse_right_resultdeltabound. pvs_le_gap_inverse_right_resultdeltabound + (du_index_inverse_right_resultdelta) = (N)) -> (exists dst_positive_code_inverse_right_resultdeltaentry dst_positive_scale_inverse_right_resultdeltaentry dst_negative_code_inverse_right_resultdeltaentry dst_negative_scale_inverse_right_resultdeltaentry dst_positive_inverse_right_resultdeltaentry dst_negative_inverse_right_resultdeltaentry. (((di_delta_inverse_right_result) = (((((dst_positive_code_inverse_right_resultdeltaentry) + (dst_positive_scale_inverse_right_resultdeltaentry)) * S ((dst_positive_code_inverse_right_resultdeltaentry) + (dst_positive_scale_inverse_right_resultdeltaentry)) + ((dst_positive_scale_inverse_right_resultdeltaentry) + (dst_positive_scale_inverse_right_resultdeltaentry))) + (((dst_negative_code_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)) * S ((dst_negative_code_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)) + ((dst_negative_scale_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)))) * S ((((dst_positive_code_inverse_right_resultdeltaentry) + (dst_positive_scale_inverse_right_resultdeltaentry)) * S ((dst_positive_code_inverse_right_resultdeltaentry) + (dst_positive_scale_inverse_right_resultdeltaentry)) + ((dst_positive_scale_inverse_right_resultdeltaentry) + (dst_positive_scale_inverse_right_resultdeltaentry))) + (((dst_negative_code_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)) * S ((dst_negative_code_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)) + ((dst_negative_scale_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)))) + ((((dst_negative_code_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)) * S ((dst_negative_code_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)) + ((dst_negative_scale_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry))) + (((dst_negative_code_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)) * S ((dst_negative_code_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)) + ((dst_negative_scale_inverse_right_resultdeltaentry) + (dst_negative_scale_inverse_right_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_right_resultdeltaentrypositive. ff_h_pvs_inverse_right_resultdeltaentrypositive + S (dst_positive_inverse_right_resultdeltaentry) = S ((S (du_index_inverse_right_resultdelta)) * dst_positive_scale_inverse_right_resultdeltaentry)) /\ exists ff_q_pvs_inverse_right_resultdeltaentrypositive. dst_positive_code_inverse_right_resultdeltaentry = ff_q_pvs_inverse_right_resultdeltaentrypositive * S ((S (du_index_inverse_right_resultdelta)) * dst_positive_scale_inverse_right_resultdeltaentry) + (dst_positive_inverse_right_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_right_resultdeltaentrynegative. ff_h_pvs_inverse_right_resultdeltaentrynegative + S (dst_negative_inverse_right_resultdeltaentry) = S ((S (du_index_inverse_right_resultdelta)) * dst_negative_scale_inverse_right_resultdeltaentry)) /\ exists ff_q_pvs_inverse_right_resultdeltaentrynegative. dst_negative_code_inverse_right_resultdeltaentry = ff_q_pvs_inverse_right_resultdeltaentrynegative * S ((S (du_index_inverse_right_resultdelta)) * dst_negative_scale_inverse_right_resultdeltaentry) + (dst_negative_inverse_right_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_right_resultdeltaentryvalue ge_balance_negative_inverse_right_resultdeltaentryvalue. (((((du_value_inverse_right_resultdelta) = 2 * (ge_balance_positive_inverse_right_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_right_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultdeltaentryvaluedecode. (((du_value_inverse_right_resultdelta) = 2 * ge_signed_half_inverse_right_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultdeltaentryvalue) = S ge_signed_half_inverse_right_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_right_resultdeltaentry) + ge_balance_negative_inverse_right_resultdeltaentryvalue = (dst_negative_inverse_right_resultdeltaentry) + ge_balance_positive_inverse_right_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_right_resultdelta)=1 -> (du_value_inverse_right_resultdelta)=2) /\ (~((du_index_inverse_right_resultdelta)=1) -> (du_value_inverse_right_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_right_resultleftleft dst_positive_scale_inverse_right_resultleftleft dst_negative_code_inverse_right_resultleftleft dst_negative_scale_inverse_right_resultleftleft. (((F) = (((((dst_positive_code_inverse_right_resultleftleft) + (dst_positive_scale_inverse_right_resultleftleft)) * S ((dst_positive_code_inverse_right_resultleftleft) + (dst_positive_scale_inverse_right_resultleftleft)) + ((dst_positive_scale_inverse_right_resultleftleft) + (dst_positive_scale_inverse_right_resultleftleft))) + (((dst_negative_code_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)) * S ((dst_negative_code_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)) + ((dst_negative_scale_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)))) * S ((((dst_positive_code_inverse_right_resultleftleft) + (dst_positive_scale_inverse_right_resultleftleft)) * S ((dst_positive_code_inverse_right_resultleftleft) + (dst_positive_scale_inverse_right_resultleftleft)) + ((dst_positive_scale_inverse_right_resultleftleft) + (dst_positive_scale_inverse_right_resultleftleft))) + (((dst_negative_code_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)) * S ((dst_negative_code_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)) + ((dst_negative_scale_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)))) + ((((dst_negative_code_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)) * S ((dst_negative_code_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)) + ((dst_negative_scale_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft))) + (((dst_negative_code_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)) * S ((dst_negative_code_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)) + ((dst_negative_scale_inverse_right_resultleftleft) + (dst_negative_scale_inverse_right_resultleftleft)))))) /\ (forall dst_index_inverse_right_resultleftleft. (exists pvs_le_gap_inverse_right_resultleftleftdomain. pvs_le_gap_inverse_right_resultleftleftdomain + (dst_index_inverse_right_resultleftleft) = (N)) -> exists dst_positive_inverse_right_resultleftleft dst_negative_inverse_right_resultleftleft dst_value_inverse_right_resultleftleft. ((((exists ff_h_pvs_inverse_right_resultleftleftentrypositive. ff_h_pvs_inverse_right_resultleftleftentrypositive + S (dst_positive_inverse_right_resultleftleft) = S ((S (dst_index_inverse_right_resultleftleft)) * dst_positive_scale_inverse_right_resultleftleft)) /\ exists ff_q_pvs_inverse_right_resultleftleftentrypositive. dst_positive_code_inverse_right_resultleftleft = ff_q_pvs_inverse_right_resultleftleftentrypositive * S ((S (dst_index_inverse_right_resultleftleft)) * dst_positive_scale_inverse_right_resultleftleft) + (dst_positive_inverse_right_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_right_resultleftleftentrynegative. ff_h_pvs_inverse_right_resultleftleftentrynegative + S (dst_negative_inverse_right_resultleftleft) = S ((S (dst_index_inverse_right_resultleftleft)) * dst_negative_scale_inverse_right_resultleftleft)) /\ exists ff_q_pvs_inverse_right_resultleftleftentrynegative. dst_negative_code_inverse_right_resultleftleft = ff_q_pvs_inverse_right_resultleftleftentrynegative * S ((S (dst_index_inverse_right_resultleftleft)) * dst_negative_scale_inverse_right_resultleftleft) + (dst_negative_inverse_right_resultleftleft))) /\ (exists ge_balance_positive_inverse_right_resultleftleftentryvalue ge_balance_negative_inverse_right_resultleftleftentryvalue. (((((dst_value_inverse_right_resultleftleft) = 2 * (ge_balance_positive_inverse_right_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_right_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultleftleftentryvaluedecode. (((dst_value_inverse_right_resultleftleft) = 2 * ge_signed_half_inverse_right_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultleftleftentryvalue) = S ge_signed_half_inverse_right_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_right_resultleftleft) + ge_balance_negative_inverse_right_resultleftleftentryvalue = (dst_negative_inverse_right_resultleftleft) + ge_balance_positive_inverse_right_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_right_resultleftright dst_positive_scale_inverse_right_resultleftright dst_negative_code_inverse_right_resultleftright dst_negative_scale_inverse_right_resultleftright. (((G) = (((((dst_positive_code_inverse_right_resultleftright) + (dst_positive_scale_inverse_right_resultleftright)) * S ((dst_positive_code_inverse_right_resultleftright) + (dst_positive_scale_inverse_right_resultleftright)) + ((dst_positive_scale_inverse_right_resultleftright) + (dst_positive_scale_inverse_right_resultleftright))) + (((dst_negative_code_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)) * S ((dst_negative_code_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)) + ((dst_negative_scale_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)))) * S ((((dst_positive_code_inverse_right_resultleftright) + (dst_positive_scale_inverse_right_resultleftright)) * S ((dst_positive_code_inverse_right_resultleftright) + (dst_positive_scale_inverse_right_resultleftright)) + ((dst_positive_scale_inverse_right_resultleftright) + (dst_positive_scale_inverse_right_resultleftright))) + (((dst_negative_code_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)) * S ((dst_negative_code_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)) + ((dst_negative_scale_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)))) + ((((dst_negative_code_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)) * S ((dst_negative_code_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)) + ((dst_negative_scale_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright))) + (((dst_negative_code_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)) * S ((dst_negative_code_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)) + ((dst_negative_scale_inverse_right_resultleftright) + (dst_negative_scale_inverse_right_resultleftright)))))) /\ (forall dst_index_inverse_right_resultleftright. (exists pvs_le_gap_inverse_right_resultleftrightdomain. pvs_le_gap_inverse_right_resultleftrightdomain + (dst_index_inverse_right_resultleftright) = (N)) -> exists dst_positive_inverse_right_resultleftright dst_negative_inverse_right_resultleftright dst_value_inverse_right_resultleftright. ((((exists ff_h_pvs_inverse_right_resultleftrightentrypositive. ff_h_pvs_inverse_right_resultleftrightentrypositive + S (dst_positive_inverse_right_resultleftright) = S ((S (dst_index_inverse_right_resultleftright)) * dst_positive_scale_inverse_right_resultleftright)) /\ exists ff_q_pvs_inverse_right_resultleftrightentrypositive. dst_positive_code_inverse_right_resultleftright = ff_q_pvs_inverse_right_resultleftrightentrypositive * S ((S (dst_index_inverse_right_resultleftright)) * dst_positive_scale_inverse_right_resultleftright) + (dst_positive_inverse_right_resultleftright))) /\ (((((exists ff_h_pvs_inverse_right_resultleftrightentrynegative. ff_h_pvs_inverse_right_resultleftrightentrynegative + S (dst_negative_inverse_right_resultleftright) = S ((S (dst_index_inverse_right_resultleftright)) * dst_negative_scale_inverse_right_resultleftright)) /\ exists ff_q_pvs_inverse_right_resultleftrightentrynegative. dst_negative_code_inverse_right_resultleftright = ff_q_pvs_inverse_right_resultleftrightentrynegative * S ((S (dst_index_inverse_right_resultleftright)) * dst_negative_scale_inverse_right_resultleftright) + (dst_negative_inverse_right_resultleftright))) /\ (exists ge_balance_positive_inverse_right_resultleftrightentryvalue ge_balance_negative_inverse_right_resultleftrightentryvalue. (((((dst_value_inverse_right_resultleftright) = 2 * (ge_balance_positive_inverse_right_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_right_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultleftrightentryvaluedecode. (((dst_value_inverse_right_resultleftright) = 2 * ge_signed_half_inverse_right_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultleftrightentryvalue) = S ge_signed_half_inverse_right_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_right_resultleftright) + ge_balance_negative_inverse_right_resultleftrightentryvalue = (dst_negative_inverse_right_resultleftright) + ge_balance_positive_inverse_right_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_right_resultlefttable dst_positive_scale_inverse_right_resultlefttable dst_negative_code_inverse_right_resultlefttable dst_negative_scale_inverse_right_resultlefttable. (((di_delta_inverse_right_result) = (((((dst_positive_code_inverse_right_resultlefttable) + (dst_positive_scale_inverse_right_resultlefttable)) * S ((dst_positive_code_inverse_right_resultlefttable) + (dst_positive_scale_inverse_right_resultlefttable)) + ((dst_positive_scale_inverse_right_resultlefttable) + (dst_positive_scale_inverse_right_resultlefttable))) + (((dst_negative_code_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)) * S ((dst_negative_code_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)) + ((dst_negative_scale_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)))) * S ((((dst_positive_code_inverse_right_resultlefttable) + (dst_positive_scale_inverse_right_resultlefttable)) * S ((dst_positive_code_inverse_right_resultlefttable) + (dst_positive_scale_inverse_right_resultlefttable)) + ((dst_positive_scale_inverse_right_resultlefttable) + (dst_positive_scale_inverse_right_resultlefttable))) + (((dst_negative_code_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)) * S ((dst_negative_code_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)) + ((dst_negative_scale_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)))) + ((((dst_negative_code_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)) * S ((dst_negative_code_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)) + ((dst_negative_scale_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable))) + (((dst_negative_code_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)) * S ((dst_negative_code_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)) + ((dst_negative_scale_inverse_right_resultlefttable) + (dst_negative_scale_inverse_right_resultlefttable)))))) /\ (forall dst_index_inverse_right_resultlefttable. (exists pvs_le_gap_inverse_right_resultlefttabledomain. pvs_le_gap_inverse_right_resultlefttabledomain + (dst_index_inverse_right_resultlefttable) = (N)) -> exists dst_positive_inverse_right_resultlefttable dst_negative_inverse_right_resultlefttable dst_value_inverse_right_resultlefttable. ((((exists ff_h_pvs_inverse_right_resultlefttableentrypositive. ff_h_pvs_inverse_right_resultlefttableentrypositive + S (dst_positive_inverse_right_resultlefttable) = S ((S (dst_index_inverse_right_resultlefttable)) * dst_positive_scale_inverse_right_resultlefttable)) /\ exists ff_q_pvs_inverse_right_resultlefttableentrypositive. dst_positive_code_inverse_right_resultlefttable = ff_q_pvs_inverse_right_resultlefttableentrypositive * S ((S (dst_index_inverse_right_resultlefttable)) * dst_positive_scale_inverse_right_resultlefttable) + (dst_positive_inverse_right_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_right_resultlefttableentrynegative. ff_h_pvs_inverse_right_resultlefttableentrynegative + S (dst_negative_inverse_right_resultlefttable) = S ((S (dst_index_inverse_right_resultlefttable)) * dst_negative_scale_inverse_right_resultlefttable)) /\ exists ff_q_pvs_inverse_right_resultlefttableentrynegative. dst_negative_code_inverse_right_resultlefttable = ff_q_pvs_inverse_right_resultlefttableentrynegative * S ((S (dst_index_inverse_right_resultlefttable)) * dst_negative_scale_inverse_right_resultlefttable) + (dst_negative_inverse_right_resultlefttable))) /\ (exists ge_balance_positive_inverse_right_resultlefttableentryvalue ge_balance_negative_inverse_right_resultlefttableentryvalue. (((((dst_value_inverse_right_resultlefttable) = 2 * (ge_balance_positive_inverse_right_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_right_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultlefttableentryvaluedecode. (((dst_value_inverse_right_resultlefttable) = 2 * ge_signed_half_inverse_right_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultlefttableentryvalue) = S ge_signed_half_inverse_right_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_right_resultlefttable) + ge_balance_negative_inverse_right_resultlefttableentryvalue = (dst_negative_inverse_right_resultlefttable) + ge_balance_positive_inverse_right_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_right_resultleft dc_output_inverse_right_resultleft. ~(dc_input_inverse_right_resultleft=0) -> (exists pvs_le_gap_inverse_right_resultleftdomain. pvs_le_gap_inverse_right_resultleftdomain + (dc_input_inverse_right_resultleft) = (N)) -> (exists dst_positive_code_inverse_right_resultleftlookup dst_positive_scale_inverse_right_resultleftlookup dst_negative_code_inverse_right_resultleftlookup dst_negative_scale_inverse_right_resultleftlookup dst_positive_inverse_right_resultleftlookup dst_negative_inverse_right_resultleftlookup. (((di_delta_inverse_right_result) = (((((dst_positive_code_inverse_right_resultleftlookup) + (dst_positive_scale_inverse_right_resultleftlookup)) * S ((dst_positive_code_inverse_right_resultleftlookup) + (dst_positive_scale_inverse_right_resultleftlookup)) + ((dst_positive_scale_inverse_right_resultleftlookup) + (dst_positive_scale_inverse_right_resultleftlookup))) + (((dst_negative_code_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)) * S ((dst_negative_code_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)) + ((dst_negative_scale_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)))) * S ((((dst_positive_code_inverse_right_resultleftlookup) + (dst_positive_scale_inverse_right_resultleftlookup)) * S ((dst_positive_code_inverse_right_resultleftlookup) + (dst_positive_scale_inverse_right_resultleftlookup)) + ((dst_positive_scale_inverse_right_resultleftlookup) + (dst_positive_scale_inverse_right_resultleftlookup))) + (((dst_negative_code_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)) * S ((dst_negative_code_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)) + ((dst_negative_scale_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)))) + ((((dst_negative_code_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)) * S ((dst_negative_code_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)) + ((dst_negative_scale_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup))) + (((dst_negative_code_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)) * S ((dst_negative_code_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)) + ((dst_negative_scale_inverse_right_resultleftlookup) + (dst_negative_scale_inverse_right_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_right_resultleftlookuppositive. ff_h_pvs_inverse_right_resultleftlookuppositive + S (dst_positive_inverse_right_resultleftlookup) = S ((S (dc_input_inverse_right_resultleft)) * dst_positive_scale_inverse_right_resultleftlookup)) /\ exists ff_q_pvs_inverse_right_resultleftlookuppositive. dst_positive_code_inverse_right_resultleftlookup = ff_q_pvs_inverse_right_resultleftlookuppositive * S ((S (dc_input_inverse_right_resultleft)) * dst_positive_scale_inverse_right_resultleftlookup) + (dst_positive_inverse_right_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_right_resultleftlookupnegative. ff_h_pvs_inverse_right_resultleftlookupnegative + S (dst_negative_inverse_right_resultleftlookup) = S ((S (dc_input_inverse_right_resultleft)) * dst_negative_scale_inverse_right_resultleftlookup)) /\ exists ff_q_pvs_inverse_right_resultleftlookupnegative. dst_negative_code_inverse_right_resultleftlookup = ff_q_pvs_inverse_right_resultleftlookupnegative * S ((S (dc_input_inverse_right_resultleft)) * dst_negative_scale_inverse_right_resultleftlookup) + (dst_negative_inverse_right_resultleftlookup))) /\ (exists ge_balance_positive_inverse_right_resultleftlookupvalue ge_balance_negative_inverse_right_resultleftlookupvalue. (((((dc_output_inverse_right_resultleft) = 2 * (ge_balance_positive_inverse_right_resultleftlookupvalue) /\ (ge_balance_negative_inverse_right_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_right_resultleftlookupvaluedecode. (((dc_output_inverse_right_resultleft) = 2 * ge_signed_half_inverse_right_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_right_resultleftlookupvalue) = S ge_signed_half_inverse_right_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_right_resultleftlookup) + ge_balance_negative_inverse_right_resultleftlookupvalue = (dst_negative_inverse_right_resultleftlookup) + ge_balance_positive_inverse_right_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_right_resultleft)=0)) /\ (exists dc_mask_inverse_right_resultleftvalue. ((((exists dst_positive_code_inverse_right_resultleftvaluemasktable dst_positive_scale_inverse_right_resultleftvaluemasktable dst_negative_code_inverse_right_resultleftvaluemasktable dst_negative_scale_inverse_right_resultleftvaluemasktable. (((dc_mask_inverse_right_resultleftvalue) = (((((dst_positive_code_inverse_right_resultleftvaluemasktable) + (dst_positive_scale_inverse_right_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_right_resultleftvaluemasktable) + (dst_positive_scale_inverse_right_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_right_resultleftvaluemasktable) + (dst_positive_scale_inverse_right_resultleftvaluemasktable))) + (((dst_negative_code_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_right_resultleftvaluemasktable) + (dst_positive_scale_inverse_right_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_right_resultleftvaluemasktable) + (dst_positive_scale_inverse_right_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_right_resultleftvaluemasktable) + (dst_positive_scale_inverse_right_resultleftvaluemasktable))) + (((dst_negative_code_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable))) + (((dst_negative_code_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_right_resultleftvaluemasktable) + (dst_negative_scale_inverse_right_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_right_resultleftvaluemasktable. (exists pvs_le_gap_inverse_right_resultleftvaluemasktabledomain. pvs_le_gap_inverse_right_resultleftvaluemasktabledomain + (dst_index_inverse_right_resultleftvaluemasktable) = (dc_input_inverse_right_resultleft)) -> exists dst_positive_inverse_right_resultleftvaluemasktable dst_negative_inverse_right_resultleftvaluemasktable dst_value_inverse_right_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_right_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_right_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_right_resultleftvaluemasktable) = S ((S (dst_index_inverse_right_resultleftvaluemasktable)) * dst_positive_scale_inverse_right_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_right_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_right_resultleftvaluemasktable = ff_q_pvs_inverse_right_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_right_resultleftvaluemasktable)) * dst_positive_scale_inverse_right_resultleftvaluemasktable) + (dst_positive_inverse_right_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_right_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_right_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_right_resultleftvaluemasktable) = S ((S (dst_index_inverse_right_resultleftvaluemasktable)) * dst_negative_scale_inverse_right_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_right_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_right_resultleftvaluemasktable = ff_q_pvs_inverse_right_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_right_resultleftvaluemasktable)) * dst_negative_scale_inverse_right_resultleftvaluemasktable) + (dst_negative_inverse_right_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_right_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_right_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_right_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_right_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_right_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_right_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_right_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_right_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_right_resultleftvaluemasktable) + ge_balance_negative_inverse_right_resultleftvaluemasktableentryvalue = (dst_negative_inverse_right_resultleftvaluemasktable) + ge_balance_positive_inverse_right_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_right_resultleftvaluemask dc_value_inverse_right_resultleftvaluemask. (exists pvs_le_gap_inverse_right_resultleftvaluemaskdomain. pvs_le_gap_inverse_right_resultleftvaluemaskdomain + (dc_index_inverse_right_resultleftvaluemask) = (dc_input_inverse_right_resultleft)) -> (exists dst_positive_code_inverse_right_resultleftvaluemasklookup dst_positive_scale_inverse_right_resultleftvaluemasklookup dst_negative_code_inverse_right_resultleftvaluemasklookup dst_negative_scale_inverse_right_resultleftvaluemasklookup dst_positive_inverse_right_resultleftvaluemasklookup dst_negative_inverse_right_resultleftvaluemasklookup. (((dc_mask_inverse_right_resultleftvalue) = (((((dst_positive_code_inverse_right_resultleftvaluemasklookup) + (dst_positive_scale_inverse_right_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_right_resultleftvaluemasklookup) + (dst_positive_scale_inverse_right_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_right_resultleftvaluemasklookup) + (dst_positive_scale_inverse_right_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_right_resultleftvaluemasklookup) + (dst_positive_scale_inverse_right_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_right_resultleftvaluemasklookup) + (dst_positive_scale_inverse_right_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_right_resultleftvaluemasklookup) + (dst_positive_scale_inverse_right_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_right_resultleftvaluemasklookup) + (dst_negative_scale_inverse_right_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_right_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_right_resultleftvaluemasklookuppositive + S (dst_positive_inverse_right_resultleftvaluemasklookup) = S ((S (dc_index_inverse_right_resultleftvaluemask)) * dst_positive_scale_inverse_right_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_right_resultleftvaluemasklookuppositive. dst_positive_code_inverse_right_resultleftvaluemasklookup = ff_q_pvs_inverse_right_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_right_resultleftvaluemask)) * dst_positive_scale_inverse_right_resultleftvaluemasklookup) + (dst_positive_inverse_right_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_right_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_right_resultleftvaluemasklookupnegative + S (dst_negative_inverse_right_resultleftvaluemasklookup) = S ((S (dc_index_inverse_right_resultleftvaluemask)) * dst_negative_scale_inverse_right_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_right_resultleftvaluemasklookupnegative. dst_negative_code_inverse_right_resultleftvaluemasklookup = ff_q_pvs_inverse_right_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_right_resultleftvaluemask)) * dst_negative_scale_inverse_right_resultleftvaluemasklookup) + (dst_negative_inverse_right_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_right_resultleftvaluemasklookupvalue ge_balance_negative_inverse_right_resultleftvaluemasklookupvalue. (((((dc_value_inverse_right_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_right_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_right_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_right_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_right_resultleftvaluemask) = 2 * ge_signed_half_inverse_right_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_right_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_right_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_right_resultleftvaluemasklookup) + ge_balance_negative_inverse_right_resultleftvaluemasklookupvalue = (dst_negative_inverse_right_resultleftvaluemasklookup) + ge_balance_positive_inverse_right_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_right_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_right_resultleftvaluemaskentry dc_left_inverse_right_resultleftvaluemaskentry dc_right_inverse_right_resultleftvaluemaskentry. (((dc_input_inverse_right_resultleft)=(dc_index_inverse_right_resultleftvaluemask)*dc_quotient_inverse_right_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_right_resultleftvaluemaskentryleft dst_positive_scale_inverse_right_resultleftvaluemaskentryleft dst_negative_code_inverse_right_resultleftvaluemaskentryleft dst_negative_scale_inverse_right_resultleftvaluemaskentryleft dst_positive_inverse_right_resultleftvaluemaskentryleft dst_negative_inverse_right_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_right_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_right_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_right_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_right_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_right_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_right_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_right_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_right_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_right_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_right_resultleftvaluemask)) * dst_positive_scale_inverse_right_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_right_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_right_resultleftvaluemaskentryleft = ff_q_pvs_inverse_right_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_right_resultleftvaluemask)) * dst_positive_scale_inverse_right_resultleftvaluemaskentryleft) + (dst_positive_inverse_right_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_right_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_right_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_right_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_right_resultleftvaluemask)) * dst_negative_scale_inverse_right_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_right_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_right_resultleftvaluemaskentryleft = ff_q_pvs_inverse_right_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_right_resultleftvaluemask)) * dst_negative_scale_inverse_right_resultleftvaluemaskentryleft) + (dst_negative_inverse_right_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_right_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_right_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_right_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_right_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_right_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_right_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_right_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_right_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_right_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_right_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_right_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_right_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_right_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_right_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_right_resultleftvaluemaskentryright dst_positive_scale_inverse_right_resultleftvaluemaskentryright dst_negative_code_inverse_right_resultleftvaluemaskentryright dst_negative_scale_inverse_right_resultleftvaluemaskentryright dst_positive_inverse_right_resultleftvaluemaskentryright dst_negative_inverse_right_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_right_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_right_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_right_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_right_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_right_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_right_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_right_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_right_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_right_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_right_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_right_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_right_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_right_resultleftvaluemaskentry)) * dst_positive_scale_inverse_right_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_right_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_right_resultleftvaluemaskentryright = ff_q_pvs_inverse_right_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_right_resultleftvaluemaskentry)) * dst_positive_scale_inverse_right_resultleftvaluemaskentryright) + (dst_positive_inverse_right_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_right_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_right_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_right_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_right_resultleftvaluemaskentry)) * dst_negative_scale_inverse_right_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_right_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_right_resultleftvaluemaskentryright = ff_q_pvs_inverse_right_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_right_resultleftvaluemaskentry)) * dst_negative_scale_inverse_right_resultleftvaluemaskentryright) + (dst_negative_inverse_right_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_right_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_right_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_right_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_right_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_right_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_right_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_right_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_right_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_right_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_right_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_right_resultleftvaluemaskentryright) + ge_balance_negative_inverse_right_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_right_resultleftvaluemaskentryright) + ge_balance_positive_inverse_right_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_right_resultleftvaluemaskentryproduct sto_an_inverse_right_resultleftvaluemaskentryproduct sto_bp_inverse_right_resultleftvaluemaskentryproduct sto_bn_inverse_right_resultleftvaluemaskentryproduct sto_cp_inverse_right_resultleftvaluemaskentryproduct sto_cn_inverse_right_resultleftvaluemaskentryproduct. (((((dc_left_inverse_right_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_right_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_right_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_resultleftvaluemaskentryproductleft. (((dc_left_inverse_right_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_right_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_right_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_right_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_right_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_right_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_right_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_right_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_resultleftvaluemaskentryproductright. (((dc_right_inverse_right_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_right_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_right_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_right_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_right_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_right_resultleftvaluemask) = 2 * (sto_cp_inverse_right_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_right_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_right_resultleftvaluemask) = 2 * ge_signed_half_inverse_right_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_right_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_right_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_right_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_right_resultleftvaluemaskentryproduct * sto_bp_inverse_right_resultleftvaluemaskentryproduct + sto_an_inverse_right_resultleftvaluemaskentryproduct * sto_bn_inverse_right_resultleftvaluemaskentryproduct) + sto_cn_inverse_right_resultleftvaluemaskentryproduct = (sto_ap_inverse_right_resultleftvaluemaskentryproduct * sto_bn_inverse_right_resultleftvaluemaskentryproduct + sto_an_inverse_right_resultleftvaluemaskentryproduct * sto_bp_inverse_right_resultleftvaluemaskentryproduct) + sto_cp_inverse_right_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_right_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_right_resultleftvaluemaskentrynondivisor. (dc_input_inverse_right_resultleft) = (dc_index_inverse_right_resultleftvaluemask) * pvs_factor_inverse_right_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_right_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_right_resultleftvaluefold dst_positive_scale_inverse_right_resultleftvaluefold dst_negative_code_inverse_right_resultleftvaluefold dst_negative_scale_inverse_right_resultleftvaluefold dst_positive_sum_inverse_right_resultleftvaluefold dst_negative_sum_inverse_right_resultleftvaluefold. (((dc_mask_inverse_right_resultleftvalue) = (((((dst_positive_code_inverse_right_resultleftvaluefold) + (dst_positive_scale_inverse_right_resultleftvaluefold)) * S ((dst_positive_code_inverse_right_resultleftvaluefold) + (dst_positive_scale_inverse_right_resultleftvaluefold)) + ((dst_positive_scale_inverse_right_resultleftvaluefold) + (dst_positive_scale_inverse_right_resultleftvaluefold))) + (((dst_negative_code_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)) * S ((dst_negative_code_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)) + ((dst_negative_scale_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_right_resultleftvaluefold) + (dst_positive_scale_inverse_right_resultleftvaluefold)) * S ((dst_positive_code_inverse_right_resultleftvaluefold) + (dst_positive_scale_inverse_right_resultleftvaluefold)) + ((dst_positive_scale_inverse_right_resultleftvaluefold) + (dst_positive_scale_inverse_right_resultleftvaluefold))) + (((dst_negative_code_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)) * S ((dst_negative_code_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)) + ((dst_negative_scale_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)))) + ((((dst_negative_code_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)) * S ((dst_negative_code_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)) + ((dst_negative_scale_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold))) + (((dst_negative_code_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)) * S ((dst_negative_code_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)) + ((dst_negative_scale_inverse_right_resultleftvaluefold) + (dst_negative_scale_inverse_right_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_right_resultleftvaluefoldpositive fs_v_dst_inverse_right_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_right_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_right_resultleftvaluefoldpositive = fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_right_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_right_resultleftvaluefold) = S ((S (S (dc_input_inverse_right_resultleft))) * fs_v_dst_inverse_right_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_right_resultleftvaluefoldpositive = fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_right_resultleft))) * fs_v_dst_inverse_right_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_right_resultleftvaluefold))) /\ forall fs_i_dst_inverse_right_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_right_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_right_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_right_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_right_resultleft)) -> exists fs_a_dst_inverse_right_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_right_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_right_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_right_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_right_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_right_resultleftvaluefold)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_right_resultleftvaluefold = fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_right_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_right_resultleftvaluefold) + (fs_a_dst_inverse_right_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_right_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_right_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_right_resultleftvaluefoldpositive = fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_right_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_resultleftvaluefoldpositive) + (fs_r_dst_inverse_right_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_right_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_right_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_right_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_right_resultleftvaluefoldpositive = fs_q_dst_inverse_right_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_right_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_resultleftvaluefoldpositive) + (fs_s_dst_inverse_right_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_right_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_right_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_right_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_right_resultleftvaluefoldnegative fs_v_dst_inverse_right_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_right_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_right_resultleftvaluefoldnegative = fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_right_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_right_resultleftvaluefold) = S ((S (S (dc_input_inverse_right_resultleft))) * fs_v_dst_inverse_right_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_right_resultleftvaluefoldnegative = fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_right_resultleft))) * fs_v_dst_inverse_right_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_right_resultleftvaluefold))) /\ forall fs_i_dst_inverse_right_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_right_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_right_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_right_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_right_resultleft)) -> exists fs_a_dst_inverse_right_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_right_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_right_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_right_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_right_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_right_resultleftvaluefold)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_right_resultleftvaluefold = fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_right_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_right_resultleftvaluefold) + (fs_a_dst_inverse_right_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_right_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_right_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_right_resultleftvaluefoldnegative = fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_right_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_resultleftvaluefoldnegative) + (fs_r_dst_inverse_right_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_right_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_right_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_right_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_right_resultleftvaluefoldnegative = fs_q_dst_inverse_right_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_right_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_resultleftvaluefoldnegative) + (fs_s_dst_inverse_right_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_right_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_right_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_right_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_right_resultleftvaluefoldresult ge_balance_negative_inverse_right_resultleftvaluefoldresult. (((((dc_output_inverse_right_resultleft) = 2 * (ge_balance_positive_inverse_right_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_right_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_right_resultleftvaluefoldresultdecode. (((dc_output_inverse_right_resultleft) = 2 * ge_signed_half_inverse_right_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_right_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_right_resultleftvaluefoldresult) = S ge_signed_half_inverse_right_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_right_resultleftvaluefold) + ge_balance_negative_inverse_right_resultleftvaluefoldresult = (dst_negative_sum_inverse_right_resultleftvaluefold) + ge_balance_positive_inverse_right_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_right_resultrightleft dst_positive_scale_inverse_right_resultrightleft dst_negative_code_inverse_right_resultrightleft dst_negative_scale_inverse_right_resultrightleft. (((G) = (((((dst_positive_code_inverse_right_resultrightleft) + (dst_positive_scale_inverse_right_resultrightleft)) * S ((dst_positive_code_inverse_right_resultrightleft) + (dst_positive_scale_inverse_right_resultrightleft)) + ((dst_positive_scale_inverse_right_resultrightleft) + (dst_positive_scale_inverse_right_resultrightleft))) + (((dst_negative_code_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)) * S ((dst_negative_code_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)) + ((dst_negative_scale_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)))) * S ((((dst_positive_code_inverse_right_resultrightleft) + (dst_positive_scale_inverse_right_resultrightleft)) * S ((dst_positive_code_inverse_right_resultrightleft) + (dst_positive_scale_inverse_right_resultrightleft)) + ((dst_positive_scale_inverse_right_resultrightleft) + (dst_positive_scale_inverse_right_resultrightleft))) + (((dst_negative_code_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)) * S ((dst_negative_code_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)) + ((dst_negative_scale_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)))) + ((((dst_negative_code_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)) * S ((dst_negative_code_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)) + ((dst_negative_scale_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft))) + (((dst_negative_code_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)) * S ((dst_negative_code_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)) + ((dst_negative_scale_inverse_right_resultrightleft) + (dst_negative_scale_inverse_right_resultrightleft)))))) /\ (forall dst_index_inverse_right_resultrightleft. (exists pvs_le_gap_inverse_right_resultrightleftdomain. pvs_le_gap_inverse_right_resultrightleftdomain + (dst_index_inverse_right_resultrightleft) = (N)) -> exists dst_positive_inverse_right_resultrightleft dst_negative_inverse_right_resultrightleft dst_value_inverse_right_resultrightleft. ((((exists ff_h_pvs_inverse_right_resultrightleftentrypositive. ff_h_pvs_inverse_right_resultrightleftentrypositive + S (dst_positive_inverse_right_resultrightleft) = S ((S (dst_index_inverse_right_resultrightleft)) * dst_positive_scale_inverse_right_resultrightleft)) /\ exists ff_q_pvs_inverse_right_resultrightleftentrypositive. dst_positive_code_inverse_right_resultrightleft = ff_q_pvs_inverse_right_resultrightleftentrypositive * S ((S (dst_index_inverse_right_resultrightleft)) * dst_positive_scale_inverse_right_resultrightleft) + (dst_positive_inverse_right_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_right_resultrightleftentrynegative. ff_h_pvs_inverse_right_resultrightleftentrynegative + S (dst_negative_inverse_right_resultrightleft) = S ((S (dst_index_inverse_right_resultrightleft)) * dst_negative_scale_inverse_right_resultrightleft)) /\ exists ff_q_pvs_inverse_right_resultrightleftentrynegative. dst_negative_code_inverse_right_resultrightleft = ff_q_pvs_inverse_right_resultrightleftentrynegative * S ((S (dst_index_inverse_right_resultrightleft)) * dst_negative_scale_inverse_right_resultrightleft) + (dst_negative_inverse_right_resultrightleft))) /\ (exists ge_balance_positive_inverse_right_resultrightleftentryvalue ge_balance_negative_inverse_right_resultrightleftentryvalue. (((((dst_value_inverse_right_resultrightleft) = 2 * (ge_balance_positive_inverse_right_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_right_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultrightleftentryvaluedecode. (((dst_value_inverse_right_resultrightleft) = 2 * ge_signed_half_inverse_right_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultrightleftentryvalue) = S ge_signed_half_inverse_right_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_right_resultrightleft) + ge_balance_negative_inverse_right_resultrightleftentryvalue = (dst_negative_inverse_right_resultrightleft) + ge_balance_positive_inverse_right_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_right_resultrightright dst_positive_scale_inverse_right_resultrightright dst_negative_code_inverse_right_resultrightright dst_negative_scale_inverse_right_resultrightright. (((F) = (((((dst_positive_code_inverse_right_resultrightright) + (dst_positive_scale_inverse_right_resultrightright)) * S ((dst_positive_code_inverse_right_resultrightright) + (dst_positive_scale_inverse_right_resultrightright)) + ((dst_positive_scale_inverse_right_resultrightright) + (dst_positive_scale_inverse_right_resultrightright))) + (((dst_negative_code_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)) * S ((dst_negative_code_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)) + ((dst_negative_scale_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)))) * S ((((dst_positive_code_inverse_right_resultrightright) + (dst_positive_scale_inverse_right_resultrightright)) * S ((dst_positive_code_inverse_right_resultrightright) + (dst_positive_scale_inverse_right_resultrightright)) + ((dst_positive_scale_inverse_right_resultrightright) + (dst_positive_scale_inverse_right_resultrightright))) + (((dst_negative_code_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)) * S ((dst_negative_code_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)) + ((dst_negative_scale_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)))) + ((((dst_negative_code_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)) * S ((dst_negative_code_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)) + ((dst_negative_scale_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright))) + (((dst_negative_code_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)) * S ((dst_negative_code_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)) + ((dst_negative_scale_inverse_right_resultrightright) + (dst_negative_scale_inverse_right_resultrightright)))))) /\ (forall dst_index_inverse_right_resultrightright. (exists pvs_le_gap_inverse_right_resultrightrightdomain. pvs_le_gap_inverse_right_resultrightrightdomain + (dst_index_inverse_right_resultrightright) = (N)) -> exists dst_positive_inverse_right_resultrightright dst_negative_inverse_right_resultrightright dst_value_inverse_right_resultrightright. ((((exists ff_h_pvs_inverse_right_resultrightrightentrypositive. ff_h_pvs_inverse_right_resultrightrightentrypositive + S (dst_positive_inverse_right_resultrightright) = S ((S (dst_index_inverse_right_resultrightright)) * dst_positive_scale_inverse_right_resultrightright)) /\ exists ff_q_pvs_inverse_right_resultrightrightentrypositive. dst_positive_code_inverse_right_resultrightright = ff_q_pvs_inverse_right_resultrightrightentrypositive * S ((S (dst_index_inverse_right_resultrightright)) * dst_positive_scale_inverse_right_resultrightright) + (dst_positive_inverse_right_resultrightright))) /\ (((((exists ff_h_pvs_inverse_right_resultrightrightentrynegative. ff_h_pvs_inverse_right_resultrightrightentrynegative + S (dst_negative_inverse_right_resultrightright) = S ((S (dst_index_inverse_right_resultrightright)) * dst_negative_scale_inverse_right_resultrightright)) /\ exists ff_q_pvs_inverse_right_resultrightrightentrynegative. dst_negative_code_inverse_right_resultrightright = ff_q_pvs_inverse_right_resultrightrightentrynegative * S ((S (dst_index_inverse_right_resultrightright)) * dst_negative_scale_inverse_right_resultrightright) + (dst_negative_inverse_right_resultrightright))) /\ (exists ge_balance_positive_inverse_right_resultrightrightentryvalue ge_balance_negative_inverse_right_resultrightrightentryvalue. (((((dst_value_inverse_right_resultrightright) = 2 * (ge_balance_positive_inverse_right_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_right_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultrightrightentryvaluedecode. (((dst_value_inverse_right_resultrightright) = 2 * ge_signed_half_inverse_right_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultrightrightentryvalue) = S ge_signed_half_inverse_right_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_right_resultrightright) + ge_balance_negative_inverse_right_resultrightrightentryvalue = (dst_negative_inverse_right_resultrightright) + ge_balance_positive_inverse_right_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_right_resultrighttable dst_positive_scale_inverse_right_resultrighttable dst_negative_code_inverse_right_resultrighttable dst_negative_scale_inverse_right_resultrighttable. (((di_delta_inverse_right_result) = (((((dst_positive_code_inverse_right_resultrighttable) + (dst_positive_scale_inverse_right_resultrighttable)) * S ((dst_positive_code_inverse_right_resultrighttable) + (dst_positive_scale_inverse_right_resultrighttable)) + ((dst_positive_scale_inverse_right_resultrighttable) + (dst_positive_scale_inverse_right_resultrighttable))) + (((dst_negative_code_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)) * S ((dst_negative_code_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)) + ((dst_negative_scale_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)))) * S ((((dst_positive_code_inverse_right_resultrighttable) + (dst_positive_scale_inverse_right_resultrighttable)) * S ((dst_positive_code_inverse_right_resultrighttable) + (dst_positive_scale_inverse_right_resultrighttable)) + ((dst_positive_scale_inverse_right_resultrighttable) + (dst_positive_scale_inverse_right_resultrighttable))) + (((dst_negative_code_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)) * S ((dst_negative_code_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)) + ((dst_negative_scale_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)))) + ((((dst_negative_code_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)) * S ((dst_negative_code_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)) + ((dst_negative_scale_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable))) + (((dst_negative_code_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)) * S ((dst_negative_code_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)) + ((dst_negative_scale_inverse_right_resultrighttable) + (dst_negative_scale_inverse_right_resultrighttable)))))) /\ (forall dst_index_inverse_right_resultrighttable. (exists pvs_le_gap_inverse_right_resultrighttabledomain. pvs_le_gap_inverse_right_resultrighttabledomain + (dst_index_inverse_right_resultrighttable) = (N)) -> exists dst_positive_inverse_right_resultrighttable dst_negative_inverse_right_resultrighttable dst_value_inverse_right_resultrighttable. ((((exists ff_h_pvs_inverse_right_resultrighttableentrypositive. ff_h_pvs_inverse_right_resultrighttableentrypositive + S (dst_positive_inverse_right_resultrighttable) = S ((S (dst_index_inverse_right_resultrighttable)) * dst_positive_scale_inverse_right_resultrighttable)) /\ exists ff_q_pvs_inverse_right_resultrighttableentrypositive. dst_positive_code_inverse_right_resultrighttable = ff_q_pvs_inverse_right_resultrighttableentrypositive * S ((S (dst_index_inverse_right_resultrighttable)) * dst_positive_scale_inverse_right_resultrighttable) + (dst_positive_inverse_right_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_right_resultrighttableentrynegative. ff_h_pvs_inverse_right_resultrighttableentrynegative + S (dst_negative_inverse_right_resultrighttable) = S ((S (dst_index_inverse_right_resultrighttable)) * dst_negative_scale_inverse_right_resultrighttable)) /\ exists ff_q_pvs_inverse_right_resultrighttableentrynegative. dst_negative_code_inverse_right_resultrighttable = ff_q_pvs_inverse_right_resultrighttableentrynegative * S ((S (dst_index_inverse_right_resultrighttable)) * dst_negative_scale_inverse_right_resultrighttable) + (dst_negative_inverse_right_resultrighttable))) /\ (exists ge_balance_positive_inverse_right_resultrighttableentryvalue ge_balance_negative_inverse_right_resultrighttableentryvalue. (((((dst_value_inverse_right_resultrighttable) = 2 * (ge_balance_positive_inverse_right_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_right_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultrighttableentryvaluedecode. (((dst_value_inverse_right_resultrighttable) = 2 * ge_signed_half_inverse_right_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultrighttableentryvalue) = S ge_signed_half_inverse_right_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_right_resultrighttable) + ge_balance_negative_inverse_right_resultrighttableentryvalue = (dst_negative_inverse_right_resultrighttable) + ge_balance_positive_inverse_right_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_right_resultright dc_output_inverse_right_resultright. ~(dc_input_inverse_right_resultright=0) -> (exists pvs_le_gap_inverse_right_resultrightdomain. pvs_le_gap_inverse_right_resultrightdomain + (dc_input_inverse_right_resultright) = (N)) -> (exists dst_positive_code_inverse_right_resultrightlookup dst_positive_scale_inverse_right_resultrightlookup dst_negative_code_inverse_right_resultrightlookup dst_negative_scale_inverse_right_resultrightlookup dst_positive_inverse_right_resultrightlookup dst_negative_inverse_right_resultrightlookup. (((di_delta_inverse_right_result) = (((((dst_positive_code_inverse_right_resultrightlookup) + (dst_positive_scale_inverse_right_resultrightlookup)) * S ((dst_positive_code_inverse_right_resultrightlookup) + (dst_positive_scale_inverse_right_resultrightlookup)) + ((dst_positive_scale_inverse_right_resultrightlookup) + (dst_positive_scale_inverse_right_resultrightlookup))) + (((dst_negative_code_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)) * S ((dst_negative_code_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)) + ((dst_negative_scale_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)))) * S ((((dst_positive_code_inverse_right_resultrightlookup) + (dst_positive_scale_inverse_right_resultrightlookup)) * S ((dst_positive_code_inverse_right_resultrightlookup) + (dst_positive_scale_inverse_right_resultrightlookup)) + ((dst_positive_scale_inverse_right_resultrightlookup) + (dst_positive_scale_inverse_right_resultrightlookup))) + (((dst_negative_code_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)) * S ((dst_negative_code_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)) + ((dst_negative_scale_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)))) + ((((dst_negative_code_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)) * S ((dst_negative_code_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)) + ((dst_negative_scale_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup))) + (((dst_negative_code_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)) * S ((dst_negative_code_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)) + ((dst_negative_scale_inverse_right_resultrightlookup) + (dst_negative_scale_inverse_right_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_right_resultrightlookuppositive. ff_h_pvs_inverse_right_resultrightlookuppositive + S (dst_positive_inverse_right_resultrightlookup) = S ((S (dc_input_inverse_right_resultright)) * dst_positive_scale_inverse_right_resultrightlookup)) /\ exists ff_q_pvs_inverse_right_resultrightlookuppositive. dst_positive_code_inverse_right_resultrightlookup = ff_q_pvs_inverse_right_resultrightlookuppositive * S ((S (dc_input_inverse_right_resultright)) * dst_positive_scale_inverse_right_resultrightlookup) + (dst_positive_inverse_right_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_right_resultrightlookupnegative. ff_h_pvs_inverse_right_resultrightlookupnegative + S (dst_negative_inverse_right_resultrightlookup) = S ((S (dc_input_inverse_right_resultright)) * dst_negative_scale_inverse_right_resultrightlookup)) /\ exists ff_q_pvs_inverse_right_resultrightlookupnegative. dst_negative_code_inverse_right_resultrightlookup = ff_q_pvs_inverse_right_resultrightlookupnegative * S ((S (dc_input_inverse_right_resultright)) * dst_negative_scale_inverse_right_resultrightlookup) + (dst_negative_inverse_right_resultrightlookup))) /\ (exists ge_balance_positive_inverse_right_resultrightlookupvalue ge_balance_negative_inverse_right_resultrightlookupvalue. (((((dc_output_inverse_right_resultright) = 2 * (ge_balance_positive_inverse_right_resultrightlookupvalue) /\ (ge_balance_negative_inverse_right_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_right_resultrightlookupvaluedecode. (((dc_output_inverse_right_resultright) = 2 * ge_signed_half_inverse_right_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_right_resultrightlookupvalue) = S ge_signed_half_inverse_right_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_right_resultrightlookup) + ge_balance_negative_inverse_right_resultrightlookupvalue = (dst_negative_inverse_right_resultrightlookup) + ge_balance_positive_inverse_right_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_right_resultright)=0)) /\ (exists dc_mask_inverse_right_resultrightvalue. ((((exists dst_positive_code_inverse_right_resultrightvaluemasktable dst_positive_scale_inverse_right_resultrightvaluemasktable dst_negative_code_inverse_right_resultrightvaluemasktable dst_negative_scale_inverse_right_resultrightvaluemasktable. (((dc_mask_inverse_right_resultrightvalue) = (((((dst_positive_code_inverse_right_resultrightvaluemasktable) + (dst_positive_scale_inverse_right_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_right_resultrightvaluemasktable) + (dst_positive_scale_inverse_right_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_right_resultrightvaluemasktable) + (dst_positive_scale_inverse_right_resultrightvaluemasktable))) + (((dst_negative_code_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_right_resultrightvaluemasktable) + (dst_positive_scale_inverse_right_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_right_resultrightvaluemasktable) + (dst_positive_scale_inverse_right_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_right_resultrightvaluemasktable) + (dst_positive_scale_inverse_right_resultrightvaluemasktable))) + (((dst_negative_code_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable))) + (((dst_negative_code_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_right_resultrightvaluemasktable) + (dst_negative_scale_inverse_right_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_right_resultrightvaluemasktable. (exists pvs_le_gap_inverse_right_resultrightvaluemasktabledomain. pvs_le_gap_inverse_right_resultrightvaluemasktabledomain + (dst_index_inverse_right_resultrightvaluemasktable) = (dc_input_inverse_right_resultright)) -> exists dst_positive_inverse_right_resultrightvaluemasktable dst_negative_inverse_right_resultrightvaluemasktable dst_value_inverse_right_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_right_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_right_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_right_resultrightvaluemasktable) = S ((S (dst_index_inverse_right_resultrightvaluemasktable)) * dst_positive_scale_inverse_right_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_right_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_right_resultrightvaluemasktable = ff_q_pvs_inverse_right_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_right_resultrightvaluemasktable)) * dst_positive_scale_inverse_right_resultrightvaluemasktable) + (dst_positive_inverse_right_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_right_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_right_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_right_resultrightvaluemasktable) = S ((S (dst_index_inverse_right_resultrightvaluemasktable)) * dst_negative_scale_inverse_right_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_right_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_right_resultrightvaluemasktable = ff_q_pvs_inverse_right_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_right_resultrightvaluemasktable)) * dst_negative_scale_inverse_right_resultrightvaluemasktable) + (dst_negative_inverse_right_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_right_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_right_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_right_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_right_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_right_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_right_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_right_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_right_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_right_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_right_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_right_resultrightvaluemasktable) + ge_balance_negative_inverse_right_resultrightvaluemasktableentryvalue = (dst_negative_inverse_right_resultrightvaluemasktable) + ge_balance_positive_inverse_right_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_right_resultrightvaluemask dc_value_inverse_right_resultrightvaluemask. (exists pvs_le_gap_inverse_right_resultrightvaluemaskdomain. pvs_le_gap_inverse_right_resultrightvaluemaskdomain + (dc_index_inverse_right_resultrightvaluemask) = (dc_input_inverse_right_resultright)) -> (exists dst_positive_code_inverse_right_resultrightvaluemasklookup dst_positive_scale_inverse_right_resultrightvaluemasklookup dst_negative_code_inverse_right_resultrightvaluemasklookup dst_negative_scale_inverse_right_resultrightvaluemasklookup dst_positive_inverse_right_resultrightvaluemasklookup dst_negative_inverse_right_resultrightvaluemasklookup. (((dc_mask_inverse_right_resultrightvalue) = (((((dst_positive_code_inverse_right_resultrightvaluemasklookup) + (dst_positive_scale_inverse_right_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_right_resultrightvaluemasklookup) + (dst_positive_scale_inverse_right_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_right_resultrightvaluemasklookup) + (dst_positive_scale_inverse_right_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_right_resultrightvaluemasklookup) + (dst_positive_scale_inverse_right_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_right_resultrightvaluemasklookup) + (dst_positive_scale_inverse_right_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_right_resultrightvaluemasklookup) + (dst_positive_scale_inverse_right_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_right_resultrightvaluemasklookup) + (dst_negative_scale_inverse_right_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_right_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_right_resultrightvaluemasklookuppositive + S (dst_positive_inverse_right_resultrightvaluemasklookup) = S ((S (dc_index_inverse_right_resultrightvaluemask)) * dst_positive_scale_inverse_right_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_right_resultrightvaluemasklookuppositive. dst_positive_code_inverse_right_resultrightvaluemasklookup = ff_q_pvs_inverse_right_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_right_resultrightvaluemask)) * dst_positive_scale_inverse_right_resultrightvaluemasklookup) + (dst_positive_inverse_right_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_right_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_right_resultrightvaluemasklookupnegative + S (dst_negative_inverse_right_resultrightvaluemasklookup) = S ((S (dc_index_inverse_right_resultrightvaluemask)) * dst_negative_scale_inverse_right_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_right_resultrightvaluemasklookupnegative. dst_negative_code_inverse_right_resultrightvaluemasklookup = ff_q_pvs_inverse_right_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_right_resultrightvaluemask)) * dst_negative_scale_inverse_right_resultrightvaluemasklookup) + (dst_negative_inverse_right_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_right_resultrightvaluemasklookupvalue ge_balance_negative_inverse_right_resultrightvaluemasklookupvalue. (((((dc_value_inverse_right_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_right_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_right_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_right_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_right_resultrightvaluemask) = 2 * ge_signed_half_inverse_right_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_right_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_right_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_right_resultrightvaluemasklookup) + ge_balance_negative_inverse_right_resultrightvaluemasklookupvalue = (dst_negative_inverse_right_resultrightvaluemasklookup) + ge_balance_positive_inverse_right_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_right_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_right_resultrightvaluemaskentry dc_left_inverse_right_resultrightvaluemaskentry dc_right_inverse_right_resultrightvaluemaskentry. (((dc_input_inverse_right_resultright)=(dc_index_inverse_right_resultrightvaluemask)*dc_quotient_inverse_right_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_right_resultrightvaluemaskentryleft dst_positive_scale_inverse_right_resultrightvaluemaskentryleft dst_negative_code_inverse_right_resultrightvaluemaskentryleft dst_negative_scale_inverse_right_resultrightvaluemaskentryleft dst_positive_inverse_right_resultrightvaluemaskentryleft dst_negative_inverse_right_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_right_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_right_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_right_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_right_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_right_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_right_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_right_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_right_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_right_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_right_resultrightvaluemask)) * dst_positive_scale_inverse_right_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_right_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_right_resultrightvaluemaskentryleft = ff_q_pvs_inverse_right_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_right_resultrightvaluemask)) * dst_positive_scale_inverse_right_resultrightvaluemaskentryleft) + (dst_positive_inverse_right_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_right_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_right_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_right_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_right_resultrightvaluemask)) * dst_negative_scale_inverse_right_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_right_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_right_resultrightvaluemaskentryleft = ff_q_pvs_inverse_right_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_right_resultrightvaluemask)) * dst_negative_scale_inverse_right_resultrightvaluemaskentryleft) + (dst_negative_inverse_right_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_right_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_right_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_right_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_right_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_right_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_right_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_right_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_right_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_right_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_right_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_right_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_right_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_right_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_right_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_right_resultrightvaluemaskentryright dst_positive_scale_inverse_right_resultrightvaluemaskentryright dst_negative_code_inverse_right_resultrightvaluemaskentryright dst_negative_scale_inverse_right_resultrightvaluemaskentryright dst_positive_inverse_right_resultrightvaluemaskentryright dst_negative_inverse_right_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_right_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_right_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_right_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_right_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_right_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_right_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_right_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_right_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_right_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_right_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_right_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_right_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_right_resultrightvaluemaskentry)) * dst_positive_scale_inverse_right_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_right_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_right_resultrightvaluemaskentryright = ff_q_pvs_inverse_right_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_right_resultrightvaluemaskentry)) * dst_positive_scale_inverse_right_resultrightvaluemaskentryright) + (dst_positive_inverse_right_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_right_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_right_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_right_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_right_resultrightvaluemaskentry)) * dst_negative_scale_inverse_right_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_right_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_right_resultrightvaluemaskentryright = ff_q_pvs_inverse_right_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_right_resultrightvaluemaskentry)) * dst_negative_scale_inverse_right_resultrightvaluemaskentryright) + (dst_negative_inverse_right_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_right_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_right_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_right_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_right_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_right_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_right_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_right_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_right_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_right_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_right_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_right_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_right_resultrightvaluemaskentryright) + ge_balance_negative_inverse_right_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_right_resultrightvaluemaskentryright) + ge_balance_positive_inverse_right_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_right_resultrightvaluemaskentryproduct sto_an_inverse_right_resultrightvaluemaskentryproduct sto_bp_inverse_right_resultrightvaluemaskentryproduct sto_bn_inverse_right_resultrightvaluemaskentryproduct sto_cp_inverse_right_resultrightvaluemaskentryproduct sto_cn_inverse_right_resultrightvaluemaskentryproduct. (((((dc_left_inverse_right_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_right_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_right_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_resultrightvaluemaskentryproductleft. (((dc_left_inverse_right_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_right_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_right_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_right_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_right_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_right_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_right_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_right_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_resultrightvaluemaskentryproductright. (((dc_right_inverse_right_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_right_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_right_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_right_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_right_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_right_resultrightvaluemask) = 2 * (sto_cp_inverse_right_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_right_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_right_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_right_resultrightvaluemask) = 2 * ge_signed_half_inverse_right_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_right_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_right_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_right_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_right_resultrightvaluemaskentryproduct * sto_bp_inverse_right_resultrightvaluemaskentryproduct + sto_an_inverse_right_resultrightvaluemaskentryproduct * sto_bn_inverse_right_resultrightvaluemaskentryproduct) + sto_cn_inverse_right_resultrightvaluemaskentryproduct = (sto_ap_inverse_right_resultrightvaluemaskentryproduct * sto_bn_inverse_right_resultrightvaluemaskentryproduct + sto_an_inverse_right_resultrightvaluemaskentryproduct * sto_bp_inverse_right_resultrightvaluemaskentryproduct) + sto_cp_inverse_right_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_right_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_right_resultrightvaluemaskentrynondivisor. (dc_input_inverse_right_resultright) = (dc_index_inverse_right_resultrightvaluemask) * pvs_factor_inverse_right_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_right_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_right_resultrightvaluefold dst_positive_scale_inverse_right_resultrightvaluefold dst_negative_code_inverse_right_resultrightvaluefold dst_negative_scale_inverse_right_resultrightvaluefold dst_positive_sum_inverse_right_resultrightvaluefold dst_negative_sum_inverse_right_resultrightvaluefold. (((dc_mask_inverse_right_resultrightvalue) = (((((dst_positive_code_inverse_right_resultrightvaluefold) + (dst_positive_scale_inverse_right_resultrightvaluefold)) * S ((dst_positive_code_inverse_right_resultrightvaluefold) + (dst_positive_scale_inverse_right_resultrightvaluefold)) + ((dst_positive_scale_inverse_right_resultrightvaluefold) + (dst_positive_scale_inverse_right_resultrightvaluefold))) + (((dst_negative_code_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)) * S ((dst_negative_code_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)) + ((dst_negative_scale_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_right_resultrightvaluefold) + (dst_positive_scale_inverse_right_resultrightvaluefold)) * S ((dst_positive_code_inverse_right_resultrightvaluefold) + (dst_positive_scale_inverse_right_resultrightvaluefold)) + ((dst_positive_scale_inverse_right_resultrightvaluefold) + (dst_positive_scale_inverse_right_resultrightvaluefold))) + (((dst_negative_code_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)) * S ((dst_negative_code_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)) + ((dst_negative_scale_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)))) + ((((dst_negative_code_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)) * S ((dst_negative_code_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)) + ((dst_negative_scale_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold))) + (((dst_negative_code_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)) * S ((dst_negative_code_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)) + ((dst_negative_scale_inverse_right_resultrightvaluefold) + (dst_negative_scale_inverse_right_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_right_resultrightvaluefoldpositive fs_v_dst_inverse_right_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_right_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_right_resultrightvaluefoldpositive = fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_right_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_right_resultrightvaluefold) = S ((S (S (dc_input_inverse_right_resultright))) * fs_v_dst_inverse_right_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_right_resultrightvaluefoldpositive = fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_right_resultright))) * fs_v_dst_inverse_right_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_right_resultrightvaluefold))) /\ forall fs_i_dst_inverse_right_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_right_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_right_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_right_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_right_resultright)) -> exists fs_a_dst_inverse_right_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_right_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_right_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_right_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_right_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_right_resultrightvaluefold)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_right_resultrightvaluefold = fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_right_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_right_resultrightvaluefold) + (fs_a_dst_inverse_right_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_right_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_right_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_right_resultrightvaluefoldpositive = fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_right_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_resultrightvaluefoldpositive) + (fs_r_dst_inverse_right_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_right_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_right_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_right_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_right_resultrightvaluefoldpositive = fs_q_dst_inverse_right_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_right_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_right_resultrightvaluefoldpositive) + (fs_s_dst_inverse_right_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_right_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_right_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_right_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_right_resultrightvaluefoldnegative fs_v_dst_inverse_right_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_right_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_right_resultrightvaluefoldnegative = fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_right_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_right_resultrightvaluefold) = S ((S (S (dc_input_inverse_right_resultright))) * fs_v_dst_inverse_right_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_right_resultrightvaluefoldnegative = fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_right_resultright))) * fs_v_dst_inverse_right_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_right_resultrightvaluefold))) /\ forall fs_i_dst_inverse_right_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_right_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_right_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_right_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_right_resultright)) -> exists fs_a_dst_inverse_right_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_right_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_right_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_right_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_right_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_right_resultrightvaluefold)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_right_resultrightvaluefold = fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_right_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_right_resultrightvaluefold) + (fs_a_dst_inverse_right_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_right_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_right_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_right_resultrightvaluefoldnegative = fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_right_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_resultrightvaluefoldnegative) + (fs_r_dst_inverse_right_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_right_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_right_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_right_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_right_resultrightvaluefoldnegative = fs_q_dst_inverse_right_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_right_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_right_resultrightvaluefoldnegative) + (fs_s_dst_inverse_right_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_right_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_right_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_right_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_right_resultrightvaluefoldresult ge_balance_negative_inverse_right_resultrightvaluefoldresult. (((((dc_output_inverse_right_resultright) = 2 * (ge_balance_positive_inverse_right_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_right_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_right_resultrightvaluefoldresultdecode. (((dc_output_inverse_right_resultright) = 2 * ge_signed_half_inverse_right_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_right_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_right_resultrightvaluefoldresult) = S ge_signed_half_inverse_right_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_right_resultrightvaluefold) + ge_balance_negative_inverse_right_resultrightvaluefoldresult = (dst_negative_sum_inverse_right_resultrightvaluefold) + ge_balance_positive_inverse_right_resultrightvaluefoldresult))))))))))))))))))))))))