dirichlet_delta_right_table

forall N F E. (exists dst_positive_code_unit_table_input dst_positive_scale_unit_table_input dst_negative_code_unit_table_input dst_negative_scale_unit_table_input. (((F) = (((((dst_positive_code_unit_table_input) + (dst_positive_scale_unit_table_input)) * S ((dst_positive_code_unit_table_input) + (dst_positive_scale_unit_table_input)) + ((dst_positive_scale_unit_table_input) + (dst_positive_scale_unit_table_input))) + (((dst_negative_code_unit_table_input) + (dst_negative_scale_unit_table_input)) * S ((dst_negative_code_unit_table_input) + (dst_negative_scale_unit_table_input)) + ((dst_negative_scale_unit_table_input) + (dst_negative_scale_unit_table_input)))) * S ((((dst_positive_code_unit_table_input) + (dst_positive_scale_unit_table_input)) * S ((dst_positive_code_unit_table_input) + (dst_positive_scale_unit_table_input)) + ((dst_positive_scale_unit_table_input) + (dst_positive_scale_unit_table_input))) + (((dst_negative_code_unit_table_input) + (dst_negative_scale_unit_table_input)) * S ((dst_negative_code_unit_table_input) + (dst_negative_scale_unit_table_input)) + ((dst_negative_scale_unit_table_input) + (dst_negative_scale_unit_table_input)))) + ((((dst_negative_code_unit_table_input) + (dst_negative_scale_unit_table_input)) * S ((dst_negative_code_unit_table_input) + (dst_negative_scale_unit_table_input)) + ((dst_negative_scale_unit_table_input) + (dst_negative_scale_unit_table_input))) + (((dst_negative_code_unit_table_input) + (dst_negative_scale_unit_table_input)) * S ((dst_negative_code_unit_table_input) + (dst_negative_scale_unit_table_input)) + ((dst_negative_scale_unit_table_input) + (dst_negative_scale_unit_table_input)))))) /\ (forall dst_index_unit_table_input. (exists pvs_le_gap_unit_table_inputdomain. pvs_le_gap_unit_table_inputdomain + (dst_index_unit_table_input) = (N)) -> exists dst_positive_unit_table_input dst_negative_unit_table_input dst_value_unit_table_input. ((((exists ff_h_pvs_unit_table_inputentrypositive. ff_h_pvs_unit_table_inputentrypositive + S (dst_positive_unit_table_input) = S ((S (dst_index_unit_table_input)) * dst_positive_scale_unit_table_input)) /\ exists ff_q_pvs_unit_table_inputentrypositive. dst_positive_code_unit_table_input = ff_q_pvs_unit_table_inputentrypositive * S ((S (dst_index_unit_table_input)) * dst_positive_scale_unit_table_input) + (dst_positive_unit_table_input))) /\ (((((exists ff_h_pvs_unit_table_inputentrynegative. ff_h_pvs_unit_table_inputentrynegative + S (dst_negative_unit_table_input) = S ((S (dst_index_unit_table_input)) * dst_negative_scale_unit_table_input)) /\ exists ff_q_pvs_unit_table_inputentrynegative. dst_negative_code_unit_table_input = ff_q_pvs_unit_table_inputentrynegative * S ((S (dst_index_unit_table_input)) * dst_negative_scale_unit_table_input) + (dst_negative_unit_table_input))) /\ (exists ge_balance_positive_unit_table_inputentryvalue ge_balance_negative_unit_table_inputentryvalue. (((((dst_value_unit_table_input) = 2 * (ge_balance_positive_unit_table_inputentryvalue) /\ (ge_balance_negative_unit_table_inputentryvalue) = 0) \/ exists ge_signed_half_unit_table_inputentryvaluedecode. (((dst_value_unit_table_input) = 2 * ge_signed_half_unit_table_inputentryvaluedecode + 1 /\ (ge_balance_positive_unit_table_inputentryvalue) = 0) /\ (ge_balance_negative_unit_table_inputentryvalue) = S ge_signed_half_unit_table_inputentryvaluedecode))) /\ ((dst_positive_unit_table_input) + ge_balance_negative_unit_table_inputentryvalue = (dst_negative_unit_table_input) + ge_balance_positive_unit_table_inputentryvalue))))))))) -> (((exists dst_positive_code_unit_table_deltatable dst_positive_scale_unit_table_deltatable dst_negative_code_unit_table_deltatable dst_negative_scale_unit_table_deltatable. (((E) = (((((dst_positive_code_unit_table_deltatable) + (dst_positive_scale_unit_table_deltatable)) * S ((dst_positive_code_unit_table_deltatable) + (dst_positive_scale_unit_table_deltatable)) + ((dst_positive_scale_unit_table_deltatable) + (dst_positive_scale_unit_table_deltatable))) + (((dst_negative_code_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)) * S ((dst_negative_code_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)) + ((dst_negative_scale_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)))) * S ((((dst_positive_code_unit_table_deltatable) + (dst_positive_scale_unit_table_deltatable)) * S ((dst_positive_code_unit_table_deltatable) + (dst_positive_scale_unit_table_deltatable)) + ((dst_positive_scale_unit_table_deltatable) + (dst_positive_scale_unit_table_deltatable))) + (((dst_negative_code_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)) * S ((dst_negative_code_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)) + ((dst_negative_scale_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)))) + ((((dst_negative_code_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)) * S ((dst_negative_code_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)) + ((dst_negative_scale_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable))) + (((dst_negative_code_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)) * S ((dst_negative_code_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)) + ((dst_negative_scale_unit_table_deltatable) + (dst_negative_scale_unit_table_deltatable)))))) /\ (forall dst_index_unit_table_deltatable. (exists pvs_le_gap_unit_table_deltatabledomain. pvs_le_gap_unit_table_deltatabledomain + (dst_index_unit_table_deltatable) = (N)) -> exists dst_positive_unit_table_deltatable dst_negative_unit_table_deltatable dst_value_unit_table_deltatable. ((((exists ff_h_pvs_unit_table_deltatableentrypositive. ff_h_pvs_unit_table_deltatableentrypositive + S (dst_positive_unit_table_deltatable) = S ((S (dst_index_unit_table_deltatable)) * dst_positive_scale_unit_table_deltatable)) /\ exists ff_q_pvs_unit_table_deltatableentrypositive. dst_positive_code_unit_table_deltatable = ff_q_pvs_unit_table_deltatableentrypositive * S ((S (dst_index_unit_table_deltatable)) * dst_positive_scale_unit_table_deltatable) + (dst_positive_unit_table_deltatable))) /\ (((((exists ff_h_pvs_unit_table_deltatableentrynegative. ff_h_pvs_unit_table_deltatableentrynegative + S (dst_negative_unit_table_deltatable) = S ((S (dst_index_unit_table_deltatable)) * dst_negative_scale_unit_table_deltatable)) /\ exists ff_q_pvs_unit_table_deltatableentrynegative. dst_negative_code_unit_table_deltatable = ff_q_pvs_unit_table_deltatableentrynegative * S ((S (dst_index_unit_table_deltatable)) * dst_negative_scale_unit_table_deltatable) + (dst_negative_unit_table_deltatable))) /\ (exists ge_balance_positive_unit_table_deltatableentryvalue ge_balance_negative_unit_table_deltatableentryvalue. (((((dst_value_unit_table_deltatable) = 2 * (ge_balance_positive_unit_table_deltatableentryvalue) /\ (ge_balance_negative_unit_table_deltatableentryvalue) = 0) \/ exists ge_signed_half_unit_table_deltatableentryvaluedecode. (((dst_value_unit_table_deltatable) = 2 * ge_signed_half_unit_table_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_unit_table_deltatableentryvalue) = 0) /\ (ge_balance_negative_unit_table_deltatableentryvalue) = S ge_signed_half_unit_table_deltatableentryvaluedecode))) /\ ((dst_positive_unit_table_deltatable) + ge_balance_negative_unit_table_deltatableentryvalue = (dst_negative_unit_table_deltatable) + ge_balance_positive_unit_table_deltatableentryvalue))))))))) /\ (forall du_index_unit_table_delta du_value_unit_table_delta. ~(du_index_unit_table_delta=0) -> (exists pvs_le_gap_unit_table_deltabound. pvs_le_gap_unit_table_deltabound + (du_index_unit_table_delta) = (N)) -> (exists dst_positive_code_unit_table_deltaentry dst_positive_scale_unit_table_deltaentry dst_negative_code_unit_table_deltaentry dst_negative_scale_unit_table_deltaentry dst_positive_unit_table_deltaentry dst_negative_unit_table_deltaentry. (((E) = (((((dst_positive_code_unit_table_deltaentry) + (dst_positive_scale_unit_table_deltaentry)) * S ((dst_positive_code_unit_table_deltaentry) + (dst_positive_scale_unit_table_deltaentry)) + ((dst_positive_scale_unit_table_deltaentry) + (dst_positive_scale_unit_table_deltaentry))) + (((dst_negative_code_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)) * S ((dst_negative_code_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)) + ((dst_negative_scale_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)))) * S ((((dst_positive_code_unit_table_deltaentry) + (dst_positive_scale_unit_table_deltaentry)) * S ((dst_positive_code_unit_table_deltaentry) + (dst_positive_scale_unit_table_deltaentry)) + ((dst_positive_scale_unit_table_deltaentry) + (dst_positive_scale_unit_table_deltaentry))) + (((dst_negative_code_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)) * S ((dst_negative_code_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)) + ((dst_negative_scale_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)))) + ((((dst_negative_code_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)) * S ((dst_negative_code_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)) + ((dst_negative_scale_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry))) + (((dst_negative_code_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)) * S ((dst_negative_code_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)) + ((dst_negative_scale_unit_table_deltaentry) + (dst_negative_scale_unit_table_deltaentry)))))) /\ (((((exists ff_h_pvs_unit_table_deltaentrypositive. ff_h_pvs_unit_table_deltaentrypositive + S (dst_positive_unit_table_deltaentry) = S ((S (du_index_unit_table_delta)) * dst_positive_scale_unit_table_deltaentry)) /\ exists ff_q_pvs_unit_table_deltaentrypositive. dst_positive_code_unit_table_deltaentry = ff_q_pvs_unit_table_deltaentrypositive * S ((S (du_index_unit_table_delta)) * dst_positive_scale_unit_table_deltaentry) + (dst_positive_unit_table_deltaentry))) /\ (((((exists ff_h_pvs_unit_table_deltaentrynegative. ff_h_pvs_unit_table_deltaentrynegative + S (dst_negative_unit_table_deltaentry) = S ((S (du_index_unit_table_delta)) * dst_negative_scale_unit_table_deltaentry)) /\ exists ff_q_pvs_unit_table_deltaentrynegative. dst_negative_code_unit_table_deltaentry = ff_q_pvs_unit_table_deltaentrynegative * S ((S (du_index_unit_table_delta)) * dst_negative_scale_unit_table_deltaentry) + (dst_negative_unit_table_deltaentry))) /\ (exists ge_balance_positive_unit_table_deltaentryvalue ge_balance_negative_unit_table_deltaentryvalue. (((((du_value_unit_table_delta) = 2 * (ge_balance_positive_unit_table_deltaentryvalue) /\ (ge_balance_negative_unit_table_deltaentryvalue) = 0) \/ exists ge_signed_half_unit_table_deltaentryvaluedecode. (((du_value_unit_table_delta) = 2 * ge_signed_half_unit_table_deltaentryvaluedecode + 1 /\ (ge_balance_positive_unit_table_deltaentryvalue) = 0) /\ (ge_balance_negative_unit_table_deltaentryvalue) = S ge_signed_half_unit_table_deltaentryvaluedecode))) /\ ((dst_positive_unit_table_deltaentry) + ge_balance_negative_unit_table_deltaentryvalue = (dst_negative_unit_table_deltaentry) + ge_balance_positive_unit_table_deltaentryvalue))))))))) -> ((((du_index_unit_table_delta)=1 -> (du_value_unit_table_delta)=2) /\ (~((du_index_unit_table_delta)=1) -> (du_value_unit_table_delta)=0)))))) -> (((exists dst_positive_code_unit_table_resultleft dst_positive_scale_unit_table_resultleft dst_negative_code_unit_table_resultleft dst_negative_scale_unit_table_resultleft. (((F) = (((((dst_positive_code_unit_table_resultleft) + (dst_positive_scale_unit_table_resultleft)) * S ((dst_positive_code_unit_table_resultleft) + (dst_positive_scale_unit_table_resultleft)) + ((dst_positive_scale_unit_table_resultleft) + (dst_positive_scale_unit_table_resultleft))) + (((dst_negative_code_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)) * S ((dst_negative_code_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)) + ((dst_negative_scale_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)))) * S ((((dst_positive_code_unit_table_resultleft) + (dst_positive_scale_unit_table_resultleft)) * S ((dst_positive_code_unit_table_resultleft) + (dst_positive_scale_unit_table_resultleft)) + ((dst_positive_scale_unit_table_resultleft) + (dst_positive_scale_unit_table_resultleft))) + (((dst_negative_code_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)) * S ((dst_negative_code_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)) + ((dst_negative_scale_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)))) + ((((dst_negative_code_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)) * S ((dst_negative_code_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)) + ((dst_negative_scale_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft))) + (((dst_negative_code_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)) * S ((dst_negative_code_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)) + ((dst_negative_scale_unit_table_resultleft) + (dst_negative_scale_unit_table_resultleft)))))) /\ (forall dst_index_unit_table_resultleft. (exists pvs_le_gap_unit_table_resultleftdomain. pvs_le_gap_unit_table_resultleftdomain + (dst_index_unit_table_resultleft) = (N)) -> exists dst_positive_unit_table_resultleft dst_negative_unit_table_resultleft dst_value_unit_table_resultleft. ((((exists ff_h_pvs_unit_table_resultleftentrypositive. ff_h_pvs_unit_table_resultleftentrypositive + S (dst_positive_unit_table_resultleft) = S ((S (dst_index_unit_table_resultleft)) * dst_positive_scale_unit_table_resultleft)) /\ exists ff_q_pvs_unit_table_resultleftentrypositive. dst_positive_code_unit_table_resultleft = ff_q_pvs_unit_table_resultleftentrypositive * S ((S (dst_index_unit_table_resultleft)) * dst_positive_scale_unit_table_resultleft) + (dst_positive_unit_table_resultleft))) /\ (((((exists ff_h_pvs_unit_table_resultleftentrynegative. ff_h_pvs_unit_table_resultleftentrynegative + S (dst_negative_unit_table_resultleft) = S ((S (dst_index_unit_table_resultleft)) * dst_negative_scale_unit_table_resultleft)) /\ exists ff_q_pvs_unit_table_resultleftentrynegative. dst_negative_code_unit_table_resultleft = ff_q_pvs_unit_table_resultleftentrynegative * S ((S (dst_index_unit_table_resultleft)) * dst_negative_scale_unit_table_resultleft) + (dst_negative_unit_table_resultleft))) /\ (exists ge_balance_positive_unit_table_resultleftentryvalue ge_balance_negative_unit_table_resultleftentryvalue. (((((dst_value_unit_table_resultleft) = 2 * (ge_balance_positive_unit_table_resultleftentryvalue) /\ (ge_balance_negative_unit_table_resultleftentryvalue) = 0) \/ exists ge_signed_half_unit_table_resultleftentryvaluedecode. (((dst_value_unit_table_resultleft) = 2 * ge_signed_half_unit_table_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_unit_table_resultleftentryvalue) = 0) /\ (ge_balance_negative_unit_table_resultleftentryvalue) = S ge_signed_half_unit_table_resultleftentryvaluedecode))) /\ ((dst_positive_unit_table_resultleft) + ge_balance_negative_unit_table_resultleftentryvalue = (dst_negative_unit_table_resultleft) + ge_balance_positive_unit_table_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_unit_table_resultright dst_positive_scale_unit_table_resultright dst_negative_code_unit_table_resultright dst_negative_scale_unit_table_resultright. (((E) = (((((dst_positive_code_unit_table_resultright) + (dst_positive_scale_unit_table_resultright)) * S ((dst_positive_code_unit_table_resultright) + (dst_positive_scale_unit_table_resultright)) + ((dst_positive_scale_unit_table_resultright) + (dst_positive_scale_unit_table_resultright))) + (((dst_negative_code_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)) * S ((dst_negative_code_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)) + ((dst_negative_scale_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)))) * S ((((dst_positive_code_unit_table_resultright) + (dst_positive_scale_unit_table_resultright)) * S ((dst_positive_code_unit_table_resultright) + (dst_positive_scale_unit_table_resultright)) + ((dst_positive_scale_unit_table_resultright) + (dst_positive_scale_unit_table_resultright))) + (((dst_negative_code_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)) * S ((dst_negative_code_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)) + ((dst_negative_scale_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)))) + ((((dst_negative_code_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)) * S ((dst_negative_code_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)) + ((dst_negative_scale_unit_table_resultright) + (dst_negative_scale_unit_table_resultright))) + (((dst_negative_code_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)) * S ((dst_negative_code_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)) + ((dst_negative_scale_unit_table_resultright) + (dst_negative_scale_unit_table_resultright)))))) /\ (forall dst_index_unit_table_resultright. (exists pvs_le_gap_unit_table_resultrightdomain. pvs_le_gap_unit_table_resultrightdomain + (dst_index_unit_table_resultright) = (N)) -> exists dst_positive_unit_table_resultright dst_negative_unit_table_resultright dst_value_unit_table_resultright. ((((exists ff_h_pvs_unit_table_resultrightentrypositive. ff_h_pvs_unit_table_resultrightentrypositive + S (dst_positive_unit_table_resultright) = S ((S (dst_index_unit_table_resultright)) * dst_positive_scale_unit_table_resultright)) /\ exists ff_q_pvs_unit_table_resultrightentrypositive. dst_positive_code_unit_table_resultright = ff_q_pvs_unit_table_resultrightentrypositive * S ((S (dst_index_unit_table_resultright)) * dst_positive_scale_unit_table_resultright) + (dst_positive_unit_table_resultright))) /\ (((((exists ff_h_pvs_unit_table_resultrightentrynegative. ff_h_pvs_unit_table_resultrightentrynegative + S (dst_negative_unit_table_resultright) = S ((S (dst_index_unit_table_resultright)) * dst_negative_scale_unit_table_resultright)) /\ exists ff_q_pvs_unit_table_resultrightentrynegative. dst_negative_code_unit_table_resultright = ff_q_pvs_unit_table_resultrightentrynegative * S ((S (dst_index_unit_table_resultright)) * dst_negative_scale_unit_table_resultright) + (dst_negative_unit_table_resultright))) /\ (exists ge_balance_positive_unit_table_resultrightentryvalue ge_balance_negative_unit_table_resultrightentryvalue. (((((dst_value_unit_table_resultright) = 2 * (ge_balance_positive_unit_table_resultrightentryvalue) /\ (ge_balance_negative_unit_table_resultrightentryvalue) = 0) \/ exists ge_signed_half_unit_table_resultrightentryvaluedecode. (((dst_value_unit_table_resultright) = 2 * ge_signed_half_unit_table_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_unit_table_resultrightentryvalue) = 0) /\ (ge_balance_negative_unit_table_resultrightentryvalue) = S ge_signed_half_unit_table_resultrightentryvaluedecode))) /\ ((dst_positive_unit_table_resultright) + ge_balance_negative_unit_table_resultrightentryvalue = (dst_negative_unit_table_resultright) + ge_balance_positive_unit_table_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_unit_table_resulttable dst_positive_scale_unit_table_resulttable dst_negative_code_unit_table_resulttable dst_negative_scale_unit_table_resulttable. (((F) = (((((dst_positive_code_unit_table_resulttable) + (dst_positive_scale_unit_table_resulttable)) * S ((dst_positive_code_unit_table_resulttable) + (dst_positive_scale_unit_table_resulttable)) + ((dst_positive_scale_unit_table_resulttable) + (dst_positive_scale_unit_table_resulttable))) + (((dst_negative_code_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)) * S ((dst_negative_code_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)) + ((dst_negative_scale_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)))) * S ((((dst_positive_code_unit_table_resulttable) + (dst_positive_scale_unit_table_resulttable)) * S ((dst_positive_code_unit_table_resulttable) + (dst_positive_scale_unit_table_resulttable)) + ((dst_positive_scale_unit_table_resulttable) + (dst_positive_scale_unit_table_resulttable))) + (((dst_negative_code_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)) * S ((dst_negative_code_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)) + ((dst_negative_scale_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)))) + ((((dst_negative_code_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)) * S ((dst_negative_code_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)) + ((dst_negative_scale_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable))) + (((dst_negative_code_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)) * S ((dst_negative_code_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)) + ((dst_negative_scale_unit_table_resulttable) + (dst_negative_scale_unit_table_resulttable)))))) /\ (forall dst_index_unit_table_resulttable. (exists pvs_le_gap_unit_table_resulttabledomain. pvs_le_gap_unit_table_resulttabledomain + (dst_index_unit_table_resulttable) = (N)) -> exists dst_positive_unit_table_resulttable dst_negative_unit_table_resulttable dst_value_unit_table_resulttable. ((((exists ff_h_pvs_unit_table_resulttableentrypositive. ff_h_pvs_unit_table_resulttableentrypositive + S (dst_positive_unit_table_resulttable) = S ((S (dst_index_unit_table_resulttable)) * dst_positive_scale_unit_table_resulttable)) /\ exists ff_q_pvs_unit_table_resulttableentrypositive. dst_positive_code_unit_table_resulttable = ff_q_pvs_unit_table_resulttableentrypositive * S ((S (dst_index_unit_table_resulttable)) * dst_positive_scale_unit_table_resulttable) + (dst_positive_unit_table_resulttable))) /\ (((((exists ff_h_pvs_unit_table_resulttableentrynegative. ff_h_pvs_unit_table_resulttableentrynegative + S (dst_negative_unit_table_resulttable) = S ((S (dst_index_unit_table_resulttable)) * dst_negative_scale_unit_table_resulttable)) /\ exists ff_q_pvs_unit_table_resulttableentrynegative. dst_negative_code_unit_table_resulttable = ff_q_pvs_unit_table_resulttableentrynegative * S ((S (dst_index_unit_table_resulttable)) * dst_negative_scale_unit_table_resulttable) + (dst_negative_unit_table_resulttable))) /\ (exists ge_balance_positive_unit_table_resulttableentryvalue ge_balance_negative_unit_table_resulttableentryvalue. (((((dst_value_unit_table_resulttable) = 2 * (ge_balance_positive_unit_table_resulttableentryvalue) /\ (ge_balance_negative_unit_table_resulttableentryvalue) = 0) \/ exists ge_signed_half_unit_table_resulttableentryvaluedecode. (((dst_value_unit_table_resulttable) = 2 * ge_signed_half_unit_table_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_unit_table_resulttableentryvalue) = 0) /\ (ge_balance_negative_unit_table_resulttableentryvalue) = S ge_signed_half_unit_table_resulttableentryvaluedecode))) /\ ((dst_positive_unit_table_resulttable) + ge_balance_negative_unit_table_resulttableentryvalue = (dst_negative_unit_table_resulttable) + ge_balance_positive_unit_table_resulttableentryvalue))))))))) /\ (forall dc_input_unit_table_result dc_output_unit_table_result. ~(dc_input_unit_table_result=0) -> (exists pvs_le_gap_unit_table_resultdomain. pvs_le_gap_unit_table_resultdomain + (dc_input_unit_table_result) = (N)) -> (exists dst_positive_code_unit_table_resultlookup dst_positive_scale_unit_table_resultlookup dst_negative_code_unit_table_resultlookup dst_negative_scale_unit_table_resultlookup dst_positive_unit_table_resultlookup dst_negative_unit_table_resultlookup. (((F) = (((((dst_positive_code_unit_table_resultlookup) + (dst_positive_scale_unit_table_resultlookup)) * S ((dst_positive_code_unit_table_resultlookup) + (dst_positive_scale_unit_table_resultlookup)) + ((dst_positive_scale_unit_table_resultlookup) + (dst_positive_scale_unit_table_resultlookup))) + (((dst_negative_code_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)) * S ((dst_negative_code_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)) + ((dst_negative_scale_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)))) * S ((((dst_positive_code_unit_table_resultlookup) + (dst_positive_scale_unit_table_resultlookup)) * S ((dst_positive_code_unit_table_resultlookup) + (dst_positive_scale_unit_table_resultlookup)) + ((dst_positive_scale_unit_table_resultlookup) + (dst_positive_scale_unit_table_resultlookup))) + (((dst_negative_code_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)) * S ((dst_negative_code_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)) + ((dst_negative_scale_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)))) + ((((dst_negative_code_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)) * S ((dst_negative_code_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)) + ((dst_negative_scale_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup))) + (((dst_negative_code_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)) * S ((dst_negative_code_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)) + ((dst_negative_scale_unit_table_resultlookup) + (dst_negative_scale_unit_table_resultlookup)))))) /\ (((((exists ff_h_pvs_unit_table_resultlookuppositive. ff_h_pvs_unit_table_resultlookuppositive + S (dst_positive_unit_table_resultlookup) = S ((S (dc_input_unit_table_result)) * dst_positive_scale_unit_table_resultlookup)) /\ exists ff_q_pvs_unit_table_resultlookuppositive. dst_positive_code_unit_table_resultlookup = ff_q_pvs_unit_table_resultlookuppositive * S ((S (dc_input_unit_table_result)) * dst_positive_scale_unit_table_resultlookup) + (dst_positive_unit_table_resultlookup))) /\ (((((exists ff_h_pvs_unit_table_resultlookupnegative. ff_h_pvs_unit_table_resultlookupnegative + S (dst_negative_unit_table_resultlookup) = S ((S (dc_input_unit_table_result)) * dst_negative_scale_unit_table_resultlookup)) /\ exists ff_q_pvs_unit_table_resultlookupnegative. dst_negative_code_unit_table_resultlookup = ff_q_pvs_unit_table_resultlookupnegative * S ((S (dc_input_unit_table_result)) * dst_negative_scale_unit_table_resultlookup) + (dst_negative_unit_table_resultlookup))) /\ (exists ge_balance_positive_unit_table_resultlookupvalue ge_balance_negative_unit_table_resultlookupvalue. (((((dc_output_unit_table_result) = 2 * (ge_balance_positive_unit_table_resultlookupvalue) /\ (ge_balance_negative_unit_table_resultlookupvalue) = 0) \/ exists ge_signed_half_unit_table_resultlookupvaluedecode. (((dc_output_unit_table_result) = 2 * ge_signed_half_unit_table_resultlookupvaluedecode + 1 /\ (ge_balance_positive_unit_table_resultlookupvalue) = 0) /\ (ge_balance_negative_unit_table_resultlookupvalue) = S ge_signed_half_unit_table_resultlookupvaluedecode))) /\ ((dst_positive_unit_table_resultlookup) + ge_balance_negative_unit_table_resultlookupvalue = (dst_negative_unit_table_resultlookup) + ge_balance_positive_unit_table_resultlookupvalue))))))))) -> (((~((dc_input_unit_table_result)=0)) /\ (exists dc_mask_unit_table_resultvalue. ((((exists dst_positive_code_unit_table_resultvaluemasktable dst_positive_scale_unit_table_resultvaluemasktable dst_negative_code_unit_table_resultvaluemasktable dst_negative_scale_unit_table_resultvaluemasktable. (((dc_mask_unit_table_resultvalue) = (((((dst_positive_code_unit_table_resultvaluemasktable) + (dst_positive_scale_unit_table_resultvaluemasktable)) * S ((dst_positive_code_unit_table_resultvaluemasktable) + (dst_positive_scale_unit_table_resultvaluemasktable)) + ((dst_positive_scale_unit_table_resultvaluemasktable) + (dst_positive_scale_unit_table_resultvaluemasktable))) + (((dst_negative_code_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)) * S ((dst_negative_code_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)) + ((dst_negative_scale_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)))) * S ((((dst_positive_code_unit_table_resultvaluemasktable) + (dst_positive_scale_unit_table_resultvaluemasktable)) * S ((dst_positive_code_unit_table_resultvaluemasktable) + (dst_positive_scale_unit_table_resultvaluemasktable)) + ((dst_positive_scale_unit_table_resultvaluemasktable) + (dst_positive_scale_unit_table_resultvaluemasktable))) + (((dst_negative_code_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)) * S ((dst_negative_code_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)) + ((dst_negative_scale_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)))) + ((((dst_negative_code_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)) * S ((dst_negative_code_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)) + ((dst_negative_scale_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable))) + (((dst_negative_code_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)) * S ((dst_negative_code_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)) + ((dst_negative_scale_unit_table_resultvaluemasktable) + (dst_negative_scale_unit_table_resultvaluemasktable)))))) /\ (forall dst_index_unit_table_resultvaluemasktable. (exists pvs_le_gap_unit_table_resultvaluemasktabledomain. pvs_le_gap_unit_table_resultvaluemasktabledomain + (dst_index_unit_table_resultvaluemasktable) = (dc_input_unit_table_result)) -> exists dst_positive_unit_table_resultvaluemasktable dst_negative_unit_table_resultvaluemasktable dst_value_unit_table_resultvaluemasktable. ((((exists ff_h_pvs_unit_table_resultvaluemasktableentrypositive. ff_h_pvs_unit_table_resultvaluemasktableentrypositive + S (dst_positive_unit_table_resultvaluemasktable) = S ((S (dst_index_unit_table_resultvaluemasktable)) * dst_positive_scale_unit_table_resultvaluemasktable)) /\ exists ff_q_pvs_unit_table_resultvaluemasktableentrypositive. dst_positive_code_unit_table_resultvaluemasktable = ff_q_pvs_unit_table_resultvaluemasktableentrypositive * S ((S (dst_index_unit_table_resultvaluemasktable)) * dst_positive_scale_unit_table_resultvaluemasktable) + (dst_positive_unit_table_resultvaluemasktable))) /\ (((((exists ff_h_pvs_unit_table_resultvaluemasktableentrynegative. ff_h_pvs_unit_table_resultvaluemasktableentrynegative + S (dst_negative_unit_table_resultvaluemasktable) = S ((S (dst_index_unit_table_resultvaluemasktable)) * dst_negative_scale_unit_table_resultvaluemasktable)) /\ exists ff_q_pvs_unit_table_resultvaluemasktableentrynegative. dst_negative_code_unit_table_resultvaluemasktable = ff_q_pvs_unit_table_resultvaluemasktableentrynegative * S ((S (dst_index_unit_table_resultvaluemasktable)) * dst_negative_scale_unit_table_resultvaluemasktable) + (dst_negative_unit_table_resultvaluemasktable))) /\ (exists ge_balance_positive_unit_table_resultvaluemasktableentryvalue ge_balance_negative_unit_table_resultvaluemasktableentryvalue. (((((dst_value_unit_table_resultvaluemasktable) = 2 * (ge_balance_positive_unit_table_resultvaluemasktableentryvalue) /\ (ge_balance_negative_unit_table_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_unit_table_resultvaluemasktableentryvaluedecode. (((dst_value_unit_table_resultvaluemasktable) = 2 * ge_signed_half_unit_table_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_unit_table_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_unit_table_resultvaluemasktableentryvalue) = S ge_signed_half_unit_table_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_unit_table_resultvaluemasktable) + ge_balance_negative_unit_table_resultvaluemasktableentryvalue = (dst_negative_unit_table_resultvaluemasktable) + ge_balance_positive_unit_table_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_unit_table_resultvaluemask dc_value_unit_table_resultvaluemask. (exists pvs_le_gap_unit_table_resultvaluemaskdomain. pvs_le_gap_unit_table_resultvaluemaskdomain + (dc_index_unit_table_resultvaluemask) = (dc_input_unit_table_result)) -> (exists dst_positive_code_unit_table_resultvaluemasklookup dst_positive_scale_unit_table_resultvaluemasklookup dst_negative_code_unit_table_resultvaluemasklookup dst_negative_scale_unit_table_resultvaluemasklookup dst_positive_unit_table_resultvaluemasklookup dst_negative_unit_table_resultvaluemasklookup. (((dc_mask_unit_table_resultvalue) = (((((dst_positive_code_unit_table_resultvaluemasklookup) + (dst_positive_scale_unit_table_resultvaluemasklookup)) * S ((dst_positive_code_unit_table_resultvaluemasklookup) + (dst_positive_scale_unit_table_resultvaluemasklookup)) + ((dst_positive_scale_unit_table_resultvaluemasklookup) + (dst_positive_scale_unit_table_resultvaluemasklookup))) + (((dst_negative_code_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)) * S ((dst_negative_code_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)) + ((dst_negative_scale_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)))) * S ((((dst_positive_code_unit_table_resultvaluemasklookup) + (dst_positive_scale_unit_table_resultvaluemasklookup)) * S ((dst_positive_code_unit_table_resultvaluemasklookup) + (dst_positive_scale_unit_table_resultvaluemasklookup)) + ((dst_positive_scale_unit_table_resultvaluemasklookup) + (dst_positive_scale_unit_table_resultvaluemasklookup))) + (((dst_negative_code_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)) * S ((dst_negative_code_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)) + ((dst_negative_scale_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)))) + ((((dst_negative_code_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)) * S ((dst_negative_code_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)) + ((dst_negative_scale_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup))) + (((dst_negative_code_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)) * S ((dst_negative_code_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)) + ((dst_negative_scale_unit_table_resultvaluemasklookup) + (dst_negative_scale_unit_table_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_unit_table_resultvaluemasklookuppositive. ff_h_pvs_unit_table_resultvaluemasklookuppositive + S (dst_positive_unit_table_resultvaluemasklookup) = S ((S (dc_index_unit_table_resultvaluemask)) * dst_positive_scale_unit_table_resultvaluemasklookup)) /\ exists ff_q_pvs_unit_table_resultvaluemasklookuppositive. dst_positive_code_unit_table_resultvaluemasklookup = ff_q_pvs_unit_table_resultvaluemasklookuppositive * S ((S (dc_index_unit_table_resultvaluemask)) * dst_positive_scale_unit_table_resultvaluemasklookup) + (dst_positive_unit_table_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_unit_table_resultvaluemasklookupnegative. ff_h_pvs_unit_table_resultvaluemasklookupnegative + S (dst_negative_unit_table_resultvaluemasklookup) = S ((S (dc_index_unit_table_resultvaluemask)) * dst_negative_scale_unit_table_resultvaluemasklookup)) /\ exists ff_q_pvs_unit_table_resultvaluemasklookupnegative. dst_negative_code_unit_table_resultvaluemasklookup = ff_q_pvs_unit_table_resultvaluemasklookupnegative * S ((S (dc_index_unit_table_resultvaluemask)) * dst_negative_scale_unit_table_resultvaluemasklookup) + (dst_negative_unit_table_resultvaluemasklookup))) /\ (exists ge_balance_positive_unit_table_resultvaluemasklookupvalue ge_balance_negative_unit_table_resultvaluemasklookupvalue. (((((dc_value_unit_table_resultvaluemask) = 2 * (ge_balance_positive_unit_table_resultvaluemasklookupvalue) /\ (ge_balance_negative_unit_table_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_unit_table_resultvaluemasklookupvaluedecode. (((dc_value_unit_table_resultvaluemask) = 2 * ge_signed_half_unit_table_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_unit_table_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_unit_table_resultvaluemasklookupvalue) = S ge_signed_half_unit_table_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_unit_table_resultvaluemasklookup) + ge_balance_negative_unit_table_resultvaluemasklookupvalue = (dst_negative_unit_table_resultvaluemasklookup) + ge_balance_positive_unit_table_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_unit_table_resultvaluemask)=0)) /\ (exists dc_quotient_unit_table_resultvaluemaskentry dc_left_unit_table_resultvaluemaskentry dc_right_unit_table_resultvaluemaskentry. (((dc_input_unit_table_result)=(dc_index_unit_table_resultvaluemask)*dc_quotient_unit_table_resultvaluemaskentry) /\ (((exists dst_positive_code_unit_table_resultvaluemaskentryleft dst_positive_scale_unit_table_resultvaluemaskentryleft dst_negative_code_unit_table_resultvaluemaskentryleft dst_negative_scale_unit_table_resultvaluemaskentryleft dst_positive_unit_table_resultvaluemaskentryleft dst_negative_unit_table_resultvaluemaskentryleft. (((F) = (((((dst_positive_code_unit_table_resultvaluemaskentryleft) + (dst_positive_scale_unit_table_resultvaluemaskentryleft)) * S ((dst_positive_code_unit_table_resultvaluemaskentryleft) + (dst_positive_scale_unit_table_resultvaluemaskentryleft)) + ((dst_positive_scale_unit_table_resultvaluemaskentryleft) + (dst_positive_scale_unit_table_resultvaluemaskentryleft))) + (((dst_negative_code_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)) * S ((dst_negative_code_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)) + ((dst_negative_scale_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)))) * S ((((dst_positive_code_unit_table_resultvaluemaskentryleft) + (dst_positive_scale_unit_table_resultvaluemaskentryleft)) * S ((dst_positive_code_unit_table_resultvaluemaskentryleft) + (dst_positive_scale_unit_table_resultvaluemaskentryleft)) + ((dst_positive_scale_unit_table_resultvaluemaskentryleft) + (dst_positive_scale_unit_table_resultvaluemaskentryleft))) + (((dst_negative_code_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)) * S ((dst_negative_code_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)) + ((dst_negative_scale_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)))) + ((((dst_negative_code_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)) * S ((dst_negative_code_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)) + ((dst_negative_scale_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft))) + (((dst_negative_code_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)) * S ((dst_negative_code_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)) + ((dst_negative_scale_unit_table_resultvaluemaskentryleft) + (dst_negative_scale_unit_table_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_unit_table_resultvaluemaskentryleftpositive. ff_h_pvs_unit_table_resultvaluemaskentryleftpositive + S (dst_positive_unit_table_resultvaluemaskentryleft) = S ((S (dc_index_unit_table_resultvaluemask)) * dst_positive_scale_unit_table_resultvaluemaskentryleft)) /\ exists ff_q_pvs_unit_table_resultvaluemaskentryleftpositive. dst_positive_code_unit_table_resultvaluemaskentryleft = ff_q_pvs_unit_table_resultvaluemaskentryleftpositive * S ((S (dc_index_unit_table_resultvaluemask)) * dst_positive_scale_unit_table_resultvaluemaskentryleft) + (dst_positive_unit_table_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_unit_table_resultvaluemaskentryleftnegative. ff_h_pvs_unit_table_resultvaluemaskentryleftnegative + S (dst_negative_unit_table_resultvaluemaskentryleft) = S ((S (dc_index_unit_table_resultvaluemask)) * dst_negative_scale_unit_table_resultvaluemaskentryleft)) /\ exists ff_q_pvs_unit_table_resultvaluemaskentryleftnegative. dst_negative_code_unit_table_resultvaluemaskentryleft = ff_q_pvs_unit_table_resultvaluemaskentryleftnegative * S ((S (dc_index_unit_table_resultvaluemask)) * dst_negative_scale_unit_table_resultvaluemaskentryleft) + (dst_negative_unit_table_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_unit_table_resultvaluemaskentryleftvalue ge_balance_negative_unit_table_resultvaluemaskentryleftvalue. (((((dc_left_unit_table_resultvaluemaskentry) = 2 * (ge_balance_positive_unit_table_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_unit_table_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_unit_table_resultvaluemaskentryleftvaluedecode. (((dc_left_unit_table_resultvaluemaskentry) = 2 * ge_signed_half_unit_table_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_unit_table_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_unit_table_resultvaluemaskentryleftvalue) = S ge_signed_half_unit_table_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_unit_table_resultvaluemaskentryleft) + ge_balance_negative_unit_table_resultvaluemaskentryleftvalue = (dst_negative_unit_table_resultvaluemaskentryleft) + ge_balance_positive_unit_table_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_unit_table_resultvaluemaskentryright dst_positive_scale_unit_table_resultvaluemaskentryright dst_negative_code_unit_table_resultvaluemaskentryright dst_negative_scale_unit_table_resultvaluemaskentryright dst_positive_unit_table_resultvaluemaskentryright dst_negative_unit_table_resultvaluemaskentryright. (((E) = (((((dst_positive_code_unit_table_resultvaluemaskentryright) + (dst_positive_scale_unit_table_resultvaluemaskentryright)) * S ((dst_positive_code_unit_table_resultvaluemaskentryright) + (dst_positive_scale_unit_table_resultvaluemaskentryright)) + ((dst_positive_scale_unit_table_resultvaluemaskentryright) + (dst_positive_scale_unit_table_resultvaluemaskentryright))) + (((dst_negative_code_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)) * S ((dst_negative_code_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)) + ((dst_negative_scale_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)))) * S ((((dst_positive_code_unit_table_resultvaluemaskentryright) + (dst_positive_scale_unit_table_resultvaluemaskentryright)) * S ((dst_positive_code_unit_table_resultvaluemaskentryright) + (dst_positive_scale_unit_table_resultvaluemaskentryright)) + ((dst_positive_scale_unit_table_resultvaluemaskentryright) + (dst_positive_scale_unit_table_resultvaluemaskentryright))) + (((dst_negative_code_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)) * S ((dst_negative_code_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)) + ((dst_negative_scale_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)))) + ((((dst_negative_code_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)) * S ((dst_negative_code_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)) + ((dst_negative_scale_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright))) + (((dst_negative_code_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)) * S ((dst_negative_code_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)) + ((dst_negative_scale_unit_table_resultvaluemaskentryright) + (dst_negative_scale_unit_table_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_unit_table_resultvaluemaskentryrightpositive. ff_h_pvs_unit_table_resultvaluemaskentryrightpositive + S (dst_positive_unit_table_resultvaluemaskentryright) = S ((S (dc_quotient_unit_table_resultvaluemaskentry)) * dst_positive_scale_unit_table_resultvaluemaskentryright)) /\ exists ff_q_pvs_unit_table_resultvaluemaskentryrightpositive. dst_positive_code_unit_table_resultvaluemaskentryright = ff_q_pvs_unit_table_resultvaluemaskentryrightpositive * S ((S (dc_quotient_unit_table_resultvaluemaskentry)) * dst_positive_scale_unit_table_resultvaluemaskentryright) + (dst_positive_unit_table_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_unit_table_resultvaluemaskentryrightnegative. ff_h_pvs_unit_table_resultvaluemaskentryrightnegative + S (dst_negative_unit_table_resultvaluemaskentryright) = S ((S (dc_quotient_unit_table_resultvaluemaskentry)) * dst_negative_scale_unit_table_resultvaluemaskentryright)) /\ exists ff_q_pvs_unit_table_resultvaluemaskentryrightnegative. dst_negative_code_unit_table_resultvaluemaskentryright = ff_q_pvs_unit_table_resultvaluemaskentryrightnegative * S ((S (dc_quotient_unit_table_resultvaluemaskentry)) * dst_negative_scale_unit_table_resultvaluemaskentryright) + (dst_negative_unit_table_resultvaluemaskentryright))) /\ (exists ge_balance_positive_unit_table_resultvaluemaskentryrightvalue ge_balance_negative_unit_table_resultvaluemaskentryrightvalue. (((((dc_right_unit_table_resultvaluemaskentry) = 2 * (ge_balance_positive_unit_table_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_unit_table_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_unit_table_resultvaluemaskentryrightvaluedecode. (((dc_right_unit_table_resultvaluemaskentry) = 2 * ge_signed_half_unit_table_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_unit_table_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_unit_table_resultvaluemaskentryrightvalue) = S ge_signed_half_unit_table_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_unit_table_resultvaluemaskentryright) + ge_balance_negative_unit_table_resultvaluemaskentryrightvalue = (dst_negative_unit_table_resultvaluemaskentryright) + ge_balance_positive_unit_table_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_unit_table_resultvaluemaskentryproduct sto_an_unit_table_resultvaluemaskentryproduct sto_bp_unit_table_resultvaluemaskentryproduct sto_bn_unit_table_resultvaluemaskentryproduct sto_cp_unit_table_resultvaluemaskentryproduct sto_cn_unit_table_resultvaluemaskentryproduct. (((((dc_left_unit_table_resultvaluemaskentry) = 2 * (sto_ap_unit_table_resultvaluemaskentryproduct) /\ (sto_an_unit_table_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_table_resultvaluemaskentryproductleft. (((dc_left_unit_table_resultvaluemaskentry) = 2 * ge_signed_half_unit_table_resultvaluemaskentryproductleft + 1 /\ (sto_ap_unit_table_resultvaluemaskentryproduct) = 0) /\ (sto_an_unit_table_resultvaluemaskentryproduct) = S ge_signed_half_unit_table_resultvaluemaskentryproductleft))) /\ ((((((dc_right_unit_table_resultvaluemaskentry) = 2 * (sto_bp_unit_table_resultvaluemaskentryproduct) /\ (sto_bn_unit_table_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_table_resultvaluemaskentryproductright. (((dc_right_unit_table_resultvaluemaskentry) = 2 * ge_signed_half_unit_table_resultvaluemaskentryproductright + 1 /\ (sto_bp_unit_table_resultvaluemaskentryproduct) = 0) /\ (sto_bn_unit_table_resultvaluemaskentryproduct) = S ge_signed_half_unit_table_resultvaluemaskentryproductright))) /\ ((((((dc_value_unit_table_resultvaluemask) = 2 * (sto_cp_unit_table_resultvaluemaskentryproduct) /\ (sto_cn_unit_table_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_unit_table_resultvaluemaskentryproductoutput. (((dc_value_unit_table_resultvaluemask) = 2 * ge_signed_half_unit_table_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_unit_table_resultvaluemaskentryproduct) = 0) /\ (sto_cn_unit_table_resultvaluemaskentryproduct) = S ge_signed_half_unit_table_resultvaluemaskentryproductoutput))) /\ ((sto_ap_unit_table_resultvaluemaskentryproduct * sto_bp_unit_table_resultvaluemaskentryproduct + sto_an_unit_table_resultvaluemaskentryproduct * sto_bn_unit_table_resultvaluemaskentryproduct) + sto_cn_unit_table_resultvaluemaskentryproduct = (sto_ap_unit_table_resultvaluemaskentryproduct * sto_bn_unit_table_resultvaluemaskentryproduct + sto_an_unit_table_resultvaluemaskentryproduct * sto_bp_unit_table_resultvaluemaskentryproduct) + sto_cp_unit_table_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_unit_table_resultvaluemask)=0 \/ ~(exists pvs_factor_unit_table_resultvaluemaskentrynondivisor. (dc_input_unit_table_result) = (dc_index_unit_table_resultvaluemask) * pvs_factor_unit_table_resultvaluemaskentrynondivisor)) /\ ((dc_value_unit_table_resultvaluemask)=0))))))) /\ (exists dst_positive_code_unit_table_resultvaluefold dst_positive_scale_unit_table_resultvaluefold dst_negative_code_unit_table_resultvaluefold dst_negative_scale_unit_table_resultvaluefold dst_positive_sum_unit_table_resultvaluefold dst_negative_sum_unit_table_resultvaluefold. (((dc_mask_unit_table_resultvalue) = (((((dst_positive_code_unit_table_resultvaluefold) + (dst_positive_scale_unit_table_resultvaluefold)) * S ((dst_positive_code_unit_table_resultvaluefold) + (dst_positive_scale_unit_table_resultvaluefold)) + ((dst_positive_scale_unit_table_resultvaluefold) + (dst_positive_scale_unit_table_resultvaluefold))) + (((dst_negative_code_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)) * S ((dst_negative_code_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)) + ((dst_negative_scale_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)))) * S ((((dst_positive_code_unit_table_resultvaluefold) + (dst_positive_scale_unit_table_resultvaluefold)) * S ((dst_positive_code_unit_table_resultvaluefold) + (dst_positive_scale_unit_table_resultvaluefold)) + ((dst_positive_scale_unit_table_resultvaluefold) + (dst_positive_scale_unit_table_resultvaluefold))) + (((dst_negative_code_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)) * S ((dst_negative_code_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)) + ((dst_negative_scale_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)))) + ((((dst_negative_code_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)) * S ((dst_negative_code_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)) + ((dst_negative_scale_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold))) + (((dst_negative_code_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)) * S ((dst_negative_code_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)) + ((dst_negative_scale_unit_table_resultvaluefold) + (dst_negative_scale_unit_table_resultvaluefold)))))) /\ (((exists fs_u_dst_unit_table_resultvaluefoldpositive fs_v_dst_unit_table_resultvaluefoldpositive. ((((exists fs_h_dst_unit_table_resultvaluefoldpositive_body_start. fs_h_dst_unit_table_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_table_resultvaluefoldpositive)) /\ exists fs_q_dst_unit_table_resultvaluefoldpositive_body_start. fs_u_dst_unit_table_resultvaluefoldpositive = fs_q_dst_unit_table_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_unit_table_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_unit_table_resultvaluefoldpositive_body_terminal. fs_h_dst_unit_table_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_unit_table_resultvaluefold) = S ((S (S (dc_input_unit_table_result))) * fs_v_dst_unit_table_resultvaluefoldpositive)) /\ exists fs_q_dst_unit_table_resultvaluefoldpositive_body_terminal. fs_u_dst_unit_table_resultvaluefoldpositive = fs_q_dst_unit_table_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_unit_table_result))) * fs_v_dst_unit_table_resultvaluefoldpositive) + (dst_positive_sum_unit_table_resultvaluefold))) /\ forall fs_i_dst_unit_table_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_unit_table_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_unit_table_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_unit_table_resultvaluefoldpositive_body_steps = S (dc_input_unit_table_result)) -> exists fs_a_dst_unit_table_resultvaluefoldpositive_body_steps fs_r_dst_unit_table_resultvaluefoldpositive_body_steps fs_s_dst_unit_table_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_unit_table_resultvaluefoldpositive_body_steps_summand. fs_h_dst_unit_table_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_unit_table_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_unit_table_resultvaluefoldpositive_body_steps)) * dst_positive_scale_unit_table_resultvaluefold)) /\ exists fs_q_dst_unit_table_resultvaluefoldpositive_body_steps_summand. dst_positive_code_unit_table_resultvaluefold = fs_q_dst_unit_table_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_unit_table_resultvaluefoldpositive_body_steps)) * dst_positive_scale_unit_table_resultvaluefold) + (fs_a_dst_unit_table_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_table_resultvaluefoldpositive_body_steps_partial. fs_h_dst_unit_table_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_unit_table_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_unit_table_resultvaluefoldpositive_body_steps)) * fs_v_dst_unit_table_resultvaluefoldpositive)) /\ exists fs_q_dst_unit_table_resultvaluefoldpositive_body_steps_partial. fs_u_dst_unit_table_resultvaluefoldpositive = fs_q_dst_unit_table_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_unit_table_resultvaluefoldpositive_body_steps)) * fs_v_dst_unit_table_resultvaluefoldpositive) + (fs_r_dst_unit_table_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_unit_table_resultvaluefoldpositive_body_steps_successor. fs_h_dst_unit_table_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_unit_table_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_unit_table_resultvaluefoldpositive_body_steps)) * fs_v_dst_unit_table_resultvaluefoldpositive)) /\ exists fs_q_dst_unit_table_resultvaluefoldpositive_body_steps_successor. fs_u_dst_unit_table_resultvaluefoldpositive = fs_q_dst_unit_table_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_unit_table_resultvaluefoldpositive_body_steps)) * fs_v_dst_unit_table_resultvaluefoldpositive) + (fs_s_dst_unit_table_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_unit_table_resultvaluefoldpositive_body_steps = fs_r_dst_unit_table_resultvaluefoldpositive_body_steps + fs_a_dst_unit_table_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_unit_table_resultvaluefoldnegative fs_v_dst_unit_table_resultvaluefoldnegative. ((((exists fs_h_dst_unit_table_resultvaluefoldnegative_body_start. fs_h_dst_unit_table_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_unit_table_resultvaluefoldnegative)) /\ exists fs_q_dst_unit_table_resultvaluefoldnegative_body_start. fs_u_dst_unit_table_resultvaluefoldnegative = fs_q_dst_unit_table_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_unit_table_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_unit_table_resultvaluefoldnegative_body_terminal. fs_h_dst_unit_table_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_unit_table_resultvaluefold) = S ((S (S (dc_input_unit_table_result))) * fs_v_dst_unit_table_resultvaluefoldnegative)) /\ exists fs_q_dst_unit_table_resultvaluefoldnegative_body_terminal. fs_u_dst_unit_table_resultvaluefoldnegative = fs_q_dst_unit_table_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_unit_table_result))) * fs_v_dst_unit_table_resultvaluefoldnegative) + (dst_negative_sum_unit_table_resultvaluefold))) /\ forall fs_i_dst_unit_table_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_unit_table_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_unit_table_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_unit_table_resultvaluefoldnegative_body_steps = S (dc_input_unit_table_result)) -> exists fs_a_dst_unit_table_resultvaluefoldnegative_body_steps fs_r_dst_unit_table_resultvaluefoldnegative_body_steps fs_s_dst_unit_table_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_unit_table_resultvaluefoldnegative_body_steps_summand. fs_h_dst_unit_table_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_unit_table_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_unit_table_resultvaluefoldnegative_body_steps)) * dst_negative_scale_unit_table_resultvaluefold)) /\ exists fs_q_dst_unit_table_resultvaluefoldnegative_body_steps_summand. dst_negative_code_unit_table_resultvaluefold = fs_q_dst_unit_table_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_unit_table_resultvaluefoldnegative_body_steps)) * dst_negative_scale_unit_table_resultvaluefold) + (fs_a_dst_unit_table_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_table_resultvaluefoldnegative_body_steps_partial. fs_h_dst_unit_table_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_unit_table_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_unit_table_resultvaluefoldnegative_body_steps)) * fs_v_dst_unit_table_resultvaluefoldnegative)) /\ exists fs_q_dst_unit_table_resultvaluefoldnegative_body_steps_partial. fs_u_dst_unit_table_resultvaluefoldnegative = fs_q_dst_unit_table_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_unit_table_resultvaluefoldnegative_body_steps)) * fs_v_dst_unit_table_resultvaluefoldnegative) + (fs_r_dst_unit_table_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_unit_table_resultvaluefoldnegative_body_steps_successor. fs_h_dst_unit_table_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_unit_table_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_unit_table_resultvaluefoldnegative_body_steps)) * fs_v_dst_unit_table_resultvaluefoldnegative)) /\ exists fs_q_dst_unit_table_resultvaluefoldnegative_body_steps_successor. fs_u_dst_unit_table_resultvaluefoldnegative = fs_q_dst_unit_table_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_unit_table_resultvaluefoldnegative_body_steps)) * fs_v_dst_unit_table_resultvaluefoldnegative) + (fs_s_dst_unit_table_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_unit_table_resultvaluefoldnegative_body_steps = fs_r_dst_unit_table_resultvaluefoldnegative_body_steps + fs_a_dst_unit_table_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_unit_table_resultvaluefoldresult ge_balance_negative_unit_table_resultvaluefoldresult. (((((dc_output_unit_table_result) = 2 * (ge_balance_positive_unit_table_resultvaluefoldresult) /\ (ge_balance_negative_unit_table_resultvaluefoldresult) = 0) \/ exists ge_signed_half_unit_table_resultvaluefoldresultdecode. (((dc_output_unit_table_result) = 2 * ge_signed_half_unit_table_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_unit_table_resultvaluefoldresult) = 0) /\ (ge_balance_negative_unit_table_resultvaluefoldresult) = S ge_signed_half_unit_table_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_unit_table_resultvaluefold) + ge_balance_negative_unit_table_resultvaluefoldresult = (dst_negative_sum_unit_table_resultvaluefold) + ge_balance_positive_unit_table_resultvaluefoldresult))))))))))))))))))))