dirichlet_delta_left_table

Exact expanded first-order arithmetic statement

forall N F E. (exists dst_positive_code_left_unit_input dst_positive_scale_left_unit_input dst_negative_code_left_unit_input dst_negative_scale_left_unit_input. (((F) = (((((dst_positive_code_left_unit_input) + (dst_positive_scale_left_unit_input)) * S ((dst_positive_code_left_unit_input) + (dst_positive_scale_left_unit_input)) + ((dst_positive_scale_left_unit_input) + (dst_positive_scale_left_unit_input))) + (((dst_negative_code_left_unit_input) + (dst_negative_scale_left_unit_input)) * S ((dst_negative_code_left_unit_input) + (dst_negative_scale_left_unit_input)) + ((dst_negative_scale_left_unit_input) + (dst_negative_scale_left_unit_input)))) * S ((((dst_positive_code_left_unit_input) + (dst_positive_scale_left_unit_input)) * S ((dst_positive_code_left_unit_input) + (dst_positive_scale_left_unit_input)) + ((dst_positive_scale_left_unit_input) + (dst_positive_scale_left_unit_input))) + (((dst_negative_code_left_unit_input) + (dst_negative_scale_left_unit_input)) * S ((dst_negative_code_left_unit_input) + (dst_negative_scale_left_unit_input)) + ((dst_negative_scale_left_unit_input) + (dst_negative_scale_left_unit_input)))) + ((((dst_negative_code_left_unit_input) + (dst_negative_scale_left_unit_input)) * S ((dst_negative_code_left_unit_input) + (dst_negative_scale_left_unit_input)) + ((dst_negative_scale_left_unit_input) + (dst_negative_scale_left_unit_input))) + (((dst_negative_code_left_unit_input) + (dst_negative_scale_left_unit_input)) * S ((dst_negative_code_left_unit_input) + (dst_negative_scale_left_unit_input)) + ((dst_negative_scale_left_unit_input) + (dst_negative_scale_left_unit_input)))))) /\ (forall dst_index_left_unit_input. (exists pvs_le_gap_left_unit_inputdomain. pvs_le_gap_left_unit_inputdomain + (dst_index_left_unit_input) = (N)) -> exists dst_positive_left_unit_input dst_negative_left_unit_input dst_value_left_unit_input. ((((exists ff_h_pvs_left_unit_inputentrypositive. ff_h_pvs_left_unit_inputentrypositive + S (dst_positive_left_unit_input) = S ((S (dst_index_left_unit_input)) * dst_positive_scale_left_unit_input)) /\ exists ff_q_pvs_left_unit_inputentrypositive. dst_positive_code_left_unit_input = ff_q_pvs_left_unit_inputentrypositive * S ((S (dst_index_left_unit_input)) * dst_positive_scale_left_unit_input) + (dst_positive_left_unit_input))) /\ (((((exists ff_h_pvs_left_unit_inputentrynegative. ff_h_pvs_left_unit_inputentrynegative + S (dst_negative_left_unit_input) = S ((S (dst_index_left_unit_input)) * dst_negative_scale_left_unit_input)) /\ exists ff_q_pvs_left_unit_inputentrynegative. dst_negative_code_left_unit_input = ff_q_pvs_left_unit_inputentrynegative * S ((S (dst_index_left_unit_input)) * dst_negative_scale_left_unit_input) + (dst_negative_left_unit_input))) /\ (exists ge_balance_positive_left_unit_inputentryvalue ge_balance_negative_left_unit_inputentryvalue. (((((dst_value_left_unit_input) = 2 * (ge_balance_positive_left_unit_inputentryvalue) /\ (ge_balance_negative_left_unit_inputentryvalue) = 0) \/ exists ge_signed_half_left_unit_inputentryvaluedecode. (((dst_value_left_unit_input) = 2 * ge_signed_half_left_unit_inputentryvaluedecode + 1 /\ (ge_balance_positive_left_unit_inputentryvalue) = 0) /\ (ge_balance_negative_left_unit_inputentryvalue) = S ge_signed_half_left_unit_inputentryvaluedecode))) /\ ((dst_positive_left_unit_input) + ge_balance_negative_left_unit_inputentryvalue = (dst_negative_left_unit_input) + ge_balance_positive_left_unit_inputentryvalue))))))))) -> (((exists dst_positive_code_left_unit_deltatable dst_positive_scale_left_unit_deltatable dst_negative_code_left_unit_deltatable dst_negative_scale_left_unit_deltatable. (((E) = (((((dst_positive_code_left_unit_deltatable) + (dst_positive_scale_left_unit_deltatable)) * S ((dst_positive_code_left_unit_deltatable) + (dst_positive_scale_left_unit_deltatable)) + ((dst_positive_scale_left_unit_deltatable) + (dst_positive_scale_left_unit_deltatable))) + (((dst_negative_code_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)) * S ((dst_negative_code_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)) + ((dst_negative_scale_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)))) * S ((((dst_positive_code_left_unit_deltatable) + (dst_positive_scale_left_unit_deltatable)) * S ((dst_positive_code_left_unit_deltatable) + (dst_positive_scale_left_unit_deltatable)) + ((dst_positive_scale_left_unit_deltatable) + (dst_positive_scale_left_unit_deltatable))) + (((dst_negative_code_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)) * S ((dst_negative_code_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)) + ((dst_negative_scale_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)))) + ((((dst_negative_code_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)) * S ((dst_negative_code_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)) + ((dst_negative_scale_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable))) + (((dst_negative_code_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)) * S ((dst_negative_code_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)) + ((dst_negative_scale_left_unit_deltatable) + (dst_negative_scale_left_unit_deltatable)))))) /\ (forall dst_index_left_unit_deltatable. (exists pvs_le_gap_left_unit_deltatabledomain. pvs_le_gap_left_unit_deltatabledomain + (dst_index_left_unit_deltatable) = (N)) -> exists dst_positive_left_unit_deltatable dst_negative_left_unit_deltatable dst_value_left_unit_deltatable. ((((exists ff_h_pvs_left_unit_deltatableentrypositive. ff_h_pvs_left_unit_deltatableentrypositive + S (dst_positive_left_unit_deltatable) = S ((S (dst_index_left_unit_deltatable)) * dst_positive_scale_left_unit_deltatable)) /\ exists ff_q_pvs_left_unit_deltatableentrypositive. dst_positive_code_left_unit_deltatable = ff_q_pvs_left_unit_deltatableentrypositive * S ((S (dst_index_left_unit_deltatable)) * dst_positive_scale_left_unit_deltatable) + (dst_positive_left_unit_deltatable))) /\ (((((exists ff_h_pvs_left_unit_deltatableentrynegative. ff_h_pvs_left_unit_deltatableentrynegative + S (dst_negative_left_unit_deltatable) = S ((S (dst_index_left_unit_deltatable)) * dst_negative_scale_left_unit_deltatable)) /\ exists ff_q_pvs_left_unit_deltatableentrynegative. dst_negative_code_left_unit_deltatable = ff_q_pvs_left_unit_deltatableentrynegative * S ((S (dst_index_left_unit_deltatable)) * dst_negative_scale_left_unit_deltatable) + (dst_negative_left_unit_deltatable))) /\ (exists ge_balance_positive_left_unit_deltatableentryvalue ge_balance_negative_left_unit_deltatableentryvalue. (((((dst_value_left_unit_deltatable) = 2 * (ge_balance_positive_left_unit_deltatableentryvalue) /\ (ge_balance_negative_left_unit_deltatableentryvalue) = 0) \/ exists ge_signed_half_left_unit_deltatableentryvaluedecode. (((dst_value_left_unit_deltatable) = 2 * ge_signed_half_left_unit_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_left_unit_deltatableentryvalue) = 0) /\ (ge_balance_negative_left_unit_deltatableentryvalue) = S ge_signed_half_left_unit_deltatableentryvaluedecode))) /\ ((dst_positive_left_unit_deltatable) + ge_balance_negative_left_unit_deltatableentryvalue = (dst_negative_left_unit_deltatable) + ge_balance_positive_left_unit_deltatableentryvalue))))))))) /\ (forall du_index_left_unit_delta du_value_left_unit_delta. ~(du_index_left_unit_delta=0) -> (exists pvs_le_gap_left_unit_deltabound. pvs_le_gap_left_unit_deltabound + (du_index_left_unit_delta) = (N)) -> (exists dst_positive_code_left_unit_deltaentry dst_positive_scale_left_unit_deltaentry dst_negative_code_left_unit_deltaentry dst_negative_scale_left_unit_deltaentry dst_positive_left_unit_deltaentry dst_negative_left_unit_deltaentry. (((E) = (((((dst_positive_code_left_unit_deltaentry) + (dst_positive_scale_left_unit_deltaentry)) * S ((dst_positive_code_left_unit_deltaentry) + (dst_positive_scale_left_unit_deltaentry)) + ((dst_positive_scale_left_unit_deltaentry) + (dst_positive_scale_left_unit_deltaentry))) + (((dst_negative_code_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)) * S ((dst_negative_code_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)) + ((dst_negative_scale_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)))) * S ((((dst_positive_code_left_unit_deltaentry) + (dst_positive_scale_left_unit_deltaentry)) * S ((dst_positive_code_left_unit_deltaentry) + (dst_positive_scale_left_unit_deltaentry)) + ((dst_positive_scale_left_unit_deltaentry) + (dst_positive_scale_left_unit_deltaentry))) + (((dst_negative_code_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)) * S ((dst_negative_code_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)) + ((dst_negative_scale_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)))) + ((((dst_negative_code_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)) * S ((dst_negative_code_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)) + ((dst_negative_scale_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry))) + (((dst_negative_code_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)) * S ((dst_negative_code_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)) + ((dst_negative_scale_left_unit_deltaentry) + (dst_negative_scale_left_unit_deltaentry)))))) /\ (((((exists ff_h_pvs_left_unit_deltaentrypositive. ff_h_pvs_left_unit_deltaentrypositive + S (dst_positive_left_unit_deltaentry) = S ((S (du_index_left_unit_delta)) * dst_positive_scale_left_unit_deltaentry)) /\ exists ff_q_pvs_left_unit_deltaentrypositive. dst_positive_code_left_unit_deltaentry = ff_q_pvs_left_unit_deltaentrypositive * S ((S (du_index_left_unit_delta)) * dst_positive_scale_left_unit_deltaentry) + (dst_positive_left_unit_deltaentry))) /\ (((((exists ff_h_pvs_left_unit_deltaentrynegative. ff_h_pvs_left_unit_deltaentrynegative + S (dst_negative_left_unit_deltaentry) = S ((S (du_index_left_unit_delta)) * dst_negative_scale_left_unit_deltaentry)) /\ exists ff_q_pvs_left_unit_deltaentrynegative. dst_negative_code_left_unit_deltaentry = ff_q_pvs_left_unit_deltaentrynegative * S ((S (du_index_left_unit_delta)) * dst_negative_scale_left_unit_deltaentry) + (dst_negative_left_unit_deltaentry))) /\ (exists ge_balance_positive_left_unit_deltaentryvalue ge_balance_negative_left_unit_deltaentryvalue. (((((du_value_left_unit_delta) = 2 * (ge_balance_positive_left_unit_deltaentryvalue) /\ (ge_balance_negative_left_unit_deltaentryvalue) = 0) \/ exists ge_signed_half_left_unit_deltaentryvaluedecode. (((du_value_left_unit_delta) = 2 * ge_signed_half_left_unit_deltaentryvaluedecode + 1 /\ (ge_balance_positive_left_unit_deltaentryvalue) = 0) /\ (ge_balance_negative_left_unit_deltaentryvalue) = S ge_signed_half_left_unit_deltaentryvaluedecode))) /\ ((dst_positive_left_unit_deltaentry) + ge_balance_negative_left_unit_deltaentryvalue = (dst_negative_left_unit_deltaentry) + ge_balance_positive_left_unit_deltaentryvalue))))))))) -> ((((du_index_left_unit_delta)=1 -> (du_value_left_unit_delta)=2) /\ (~((du_index_left_unit_delta)=1) -> (du_value_left_unit_delta)=0)))))) -> (((exists dst_positive_code_left_unit_resultleft dst_positive_scale_left_unit_resultleft dst_negative_code_left_unit_resultleft dst_negative_scale_left_unit_resultleft. (((E) = (((((dst_positive_code_left_unit_resultleft) + (dst_positive_scale_left_unit_resultleft)) * S ((dst_positive_code_left_unit_resultleft) + (dst_positive_scale_left_unit_resultleft)) + ((dst_positive_scale_left_unit_resultleft) + (dst_positive_scale_left_unit_resultleft))) + (((dst_negative_code_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)) * S ((dst_negative_code_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)) + ((dst_negative_scale_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)))) * S ((((dst_positive_code_left_unit_resultleft) + (dst_positive_scale_left_unit_resultleft)) * S ((dst_positive_code_left_unit_resultleft) + (dst_positive_scale_left_unit_resultleft)) + ((dst_positive_scale_left_unit_resultleft) + (dst_positive_scale_left_unit_resultleft))) + (((dst_negative_code_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)) * S ((dst_negative_code_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)) + ((dst_negative_scale_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)))) + ((((dst_negative_code_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)) * S ((dst_negative_code_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)) + ((dst_negative_scale_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft))) + (((dst_negative_code_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)) * S ((dst_negative_code_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)) + ((dst_negative_scale_left_unit_resultleft) + (dst_negative_scale_left_unit_resultleft)))))) /\ (forall dst_index_left_unit_resultleft. (exists pvs_le_gap_left_unit_resultleftdomain. pvs_le_gap_left_unit_resultleftdomain + (dst_index_left_unit_resultleft) = (N)) -> exists dst_positive_left_unit_resultleft dst_negative_left_unit_resultleft dst_value_left_unit_resultleft. ((((exists ff_h_pvs_left_unit_resultleftentrypositive. ff_h_pvs_left_unit_resultleftentrypositive + S (dst_positive_left_unit_resultleft) = S ((S (dst_index_left_unit_resultleft)) * dst_positive_scale_left_unit_resultleft)) /\ exists ff_q_pvs_left_unit_resultleftentrypositive. dst_positive_code_left_unit_resultleft = ff_q_pvs_left_unit_resultleftentrypositive * S ((S (dst_index_left_unit_resultleft)) * dst_positive_scale_left_unit_resultleft) + (dst_positive_left_unit_resultleft))) /\ (((((exists ff_h_pvs_left_unit_resultleftentrynegative. ff_h_pvs_left_unit_resultleftentrynegative + S (dst_negative_left_unit_resultleft) = S ((S (dst_index_left_unit_resultleft)) * dst_negative_scale_left_unit_resultleft)) /\ exists ff_q_pvs_left_unit_resultleftentrynegative. dst_negative_code_left_unit_resultleft = ff_q_pvs_left_unit_resultleftentrynegative * S ((S (dst_index_left_unit_resultleft)) * dst_negative_scale_left_unit_resultleft) + (dst_negative_left_unit_resultleft))) /\ (exists ge_balance_positive_left_unit_resultleftentryvalue ge_balance_negative_left_unit_resultleftentryvalue. (((((dst_value_left_unit_resultleft) = 2 * (ge_balance_positive_left_unit_resultleftentryvalue) /\ (ge_balance_negative_left_unit_resultleftentryvalue) = 0) \/ exists ge_signed_half_left_unit_resultleftentryvaluedecode. (((dst_value_left_unit_resultleft) = 2 * ge_signed_half_left_unit_resultleftentryvaluedecode + 1 /\ (ge_balance_positive_left_unit_resultleftentryvalue) = 0) /\ (ge_balance_negative_left_unit_resultleftentryvalue) = S ge_signed_half_left_unit_resultleftentryvaluedecode))) /\ ((dst_positive_left_unit_resultleft) + ge_balance_negative_left_unit_resultleftentryvalue = (dst_negative_left_unit_resultleft) + ge_balance_positive_left_unit_resultleftentryvalue))))))))) /\ (((exists dst_positive_code_left_unit_resultright dst_positive_scale_left_unit_resultright dst_negative_code_left_unit_resultright dst_negative_scale_left_unit_resultright. (((F) = (((((dst_positive_code_left_unit_resultright) + (dst_positive_scale_left_unit_resultright)) * S ((dst_positive_code_left_unit_resultright) + (dst_positive_scale_left_unit_resultright)) + ((dst_positive_scale_left_unit_resultright) + (dst_positive_scale_left_unit_resultright))) + (((dst_negative_code_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)) * S ((dst_negative_code_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)) + ((dst_negative_scale_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)))) * S ((((dst_positive_code_left_unit_resultright) + (dst_positive_scale_left_unit_resultright)) * S ((dst_positive_code_left_unit_resultright) + (dst_positive_scale_left_unit_resultright)) + ((dst_positive_scale_left_unit_resultright) + (dst_positive_scale_left_unit_resultright))) + (((dst_negative_code_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)) * S ((dst_negative_code_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)) + ((dst_negative_scale_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)))) + ((((dst_negative_code_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)) * S ((dst_negative_code_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)) + ((dst_negative_scale_left_unit_resultright) + (dst_negative_scale_left_unit_resultright))) + (((dst_negative_code_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)) * S ((dst_negative_code_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)) + ((dst_negative_scale_left_unit_resultright) + (dst_negative_scale_left_unit_resultright)))))) /\ (forall dst_index_left_unit_resultright. (exists pvs_le_gap_left_unit_resultrightdomain. pvs_le_gap_left_unit_resultrightdomain + (dst_index_left_unit_resultright) = (N)) -> exists dst_positive_left_unit_resultright dst_negative_left_unit_resultright dst_value_left_unit_resultright. ((((exists ff_h_pvs_left_unit_resultrightentrypositive. ff_h_pvs_left_unit_resultrightentrypositive + S (dst_positive_left_unit_resultright) = S ((S (dst_index_left_unit_resultright)) * dst_positive_scale_left_unit_resultright)) /\ exists ff_q_pvs_left_unit_resultrightentrypositive. dst_positive_code_left_unit_resultright = ff_q_pvs_left_unit_resultrightentrypositive * S ((S (dst_index_left_unit_resultright)) * dst_positive_scale_left_unit_resultright) + (dst_positive_left_unit_resultright))) /\ (((((exists ff_h_pvs_left_unit_resultrightentrynegative. ff_h_pvs_left_unit_resultrightentrynegative + S (dst_negative_left_unit_resultright) = S ((S (dst_index_left_unit_resultright)) * dst_negative_scale_left_unit_resultright)) /\ exists ff_q_pvs_left_unit_resultrightentrynegative. dst_negative_code_left_unit_resultright = ff_q_pvs_left_unit_resultrightentrynegative * S ((S (dst_index_left_unit_resultright)) * dst_negative_scale_left_unit_resultright) + (dst_negative_left_unit_resultright))) /\ (exists ge_balance_positive_left_unit_resultrightentryvalue ge_balance_negative_left_unit_resultrightentryvalue. (((((dst_value_left_unit_resultright) = 2 * (ge_balance_positive_left_unit_resultrightentryvalue) /\ (ge_balance_negative_left_unit_resultrightentryvalue) = 0) \/ exists ge_signed_half_left_unit_resultrightentryvaluedecode. (((dst_value_left_unit_resultright) = 2 * ge_signed_half_left_unit_resultrightentryvaluedecode + 1 /\ (ge_balance_positive_left_unit_resultrightentryvalue) = 0) /\ (ge_balance_negative_left_unit_resultrightentryvalue) = S ge_signed_half_left_unit_resultrightentryvaluedecode))) /\ ((dst_positive_left_unit_resultright) + ge_balance_negative_left_unit_resultrightentryvalue = (dst_negative_left_unit_resultright) + ge_balance_positive_left_unit_resultrightentryvalue))))))))) /\ (((exists dst_positive_code_left_unit_resulttable dst_positive_scale_left_unit_resulttable dst_negative_code_left_unit_resulttable dst_negative_scale_left_unit_resulttable. (((F) = (((((dst_positive_code_left_unit_resulttable) + (dst_positive_scale_left_unit_resulttable)) * S ((dst_positive_code_left_unit_resulttable) + (dst_positive_scale_left_unit_resulttable)) + ((dst_positive_scale_left_unit_resulttable) + (dst_positive_scale_left_unit_resulttable))) + (((dst_negative_code_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)) * S ((dst_negative_code_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)) + ((dst_negative_scale_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)))) * S ((((dst_positive_code_left_unit_resulttable) + (dst_positive_scale_left_unit_resulttable)) * S ((dst_positive_code_left_unit_resulttable) + (dst_positive_scale_left_unit_resulttable)) + ((dst_positive_scale_left_unit_resulttable) + (dst_positive_scale_left_unit_resulttable))) + (((dst_negative_code_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)) * S ((dst_negative_code_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)) + ((dst_negative_scale_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)))) + ((((dst_negative_code_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)) * S ((dst_negative_code_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)) + ((dst_negative_scale_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable))) + (((dst_negative_code_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)) * S ((dst_negative_code_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)) + ((dst_negative_scale_left_unit_resulttable) + (dst_negative_scale_left_unit_resulttable)))))) /\ (forall dst_index_left_unit_resulttable. (exists pvs_le_gap_left_unit_resulttabledomain. pvs_le_gap_left_unit_resulttabledomain + (dst_index_left_unit_resulttable) = (N)) -> exists dst_positive_left_unit_resulttable dst_negative_left_unit_resulttable dst_value_left_unit_resulttable. ((((exists ff_h_pvs_left_unit_resulttableentrypositive. ff_h_pvs_left_unit_resulttableentrypositive + S (dst_positive_left_unit_resulttable) = S ((S (dst_index_left_unit_resulttable)) * dst_positive_scale_left_unit_resulttable)) /\ exists ff_q_pvs_left_unit_resulttableentrypositive. dst_positive_code_left_unit_resulttable = ff_q_pvs_left_unit_resulttableentrypositive * S ((S (dst_index_left_unit_resulttable)) * dst_positive_scale_left_unit_resulttable) + (dst_positive_left_unit_resulttable))) /\ (((((exists ff_h_pvs_left_unit_resulttableentrynegative. ff_h_pvs_left_unit_resulttableentrynegative + S (dst_negative_left_unit_resulttable) = S ((S (dst_index_left_unit_resulttable)) * dst_negative_scale_left_unit_resulttable)) /\ exists ff_q_pvs_left_unit_resulttableentrynegative. dst_negative_code_left_unit_resulttable = ff_q_pvs_left_unit_resulttableentrynegative * S ((S (dst_index_left_unit_resulttable)) * dst_negative_scale_left_unit_resulttable) + (dst_negative_left_unit_resulttable))) /\ (exists ge_balance_positive_left_unit_resulttableentryvalue ge_balance_negative_left_unit_resulttableentryvalue. (((((dst_value_left_unit_resulttable) = 2 * (ge_balance_positive_left_unit_resulttableentryvalue) /\ (ge_balance_negative_left_unit_resulttableentryvalue) = 0) \/ exists ge_signed_half_left_unit_resulttableentryvaluedecode. (((dst_value_left_unit_resulttable) = 2 * ge_signed_half_left_unit_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_left_unit_resulttableentryvalue) = 0) /\ (ge_balance_negative_left_unit_resulttableentryvalue) = S ge_signed_half_left_unit_resulttableentryvaluedecode))) /\ ((dst_positive_left_unit_resulttable) + ge_balance_negative_left_unit_resulttableentryvalue = (dst_negative_left_unit_resulttable) + ge_balance_positive_left_unit_resulttableentryvalue))))))))) /\ (forall dc_input_left_unit_result dc_output_left_unit_result. ~(dc_input_left_unit_result=0) -> (exists pvs_le_gap_left_unit_resultdomain. pvs_le_gap_left_unit_resultdomain + (dc_input_left_unit_result) = (N)) -> (exists dst_positive_code_left_unit_resultlookup dst_positive_scale_left_unit_resultlookup dst_negative_code_left_unit_resultlookup dst_negative_scale_left_unit_resultlookup dst_positive_left_unit_resultlookup dst_negative_left_unit_resultlookup. (((F) = (((((dst_positive_code_left_unit_resultlookup) + (dst_positive_scale_left_unit_resultlookup)) * S ((dst_positive_code_left_unit_resultlookup) + (dst_positive_scale_left_unit_resultlookup)) + ((dst_positive_scale_left_unit_resultlookup) + (dst_positive_scale_left_unit_resultlookup))) + (((dst_negative_code_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)) * S ((dst_negative_code_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)) + ((dst_negative_scale_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)))) * S ((((dst_positive_code_left_unit_resultlookup) + (dst_positive_scale_left_unit_resultlookup)) * S ((dst_positive_code_left_unit_resultlookup) + (dst_positive_scale_left_unit_resultlookup)) + ((dst_positive_scale_left_unit_resultlookup) + (dst_positive_scale_left_unit_resultlookup))) + (((dst_negative_code_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)) * S ((dst_negative_code_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)) + ((dst_negative_scale_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)))) + ((((dst_negative_code_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)) * S ((dst_negative_code_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)) + ((dst_negative_scale_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup))) + (((dst_negative_code_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)) * S ((dst_negative_code_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)) + ((dst_negative_scale_left_unit_resultlookup) + (dst_negative_scale_left_unit_resultlookup)))))) /\ (((((exists ff_h_pvs_left_unit_resultlookuppositive. ff_h_pvs_left_unit_resultlookuppositive + S (dst_positive_left_unit_resultlookup) = S ((S (dc_input_left_unit_result)) * dst_positive_scale_left_unit_resultlookup)) /\ exists ff_q_pvs_left_unit_resultlookuppositive. dst_positive_code_left_unit_resultlookup = ff_q_pvs_left_unit_resultlookuppositive * S ((S (dc_input_left_unit_result)) * dst_positive_scale_left_unit_resultlookup) + (dst_positive_left_unit_resultlookup))) /\ (((((exists ff_h_pvs_left_unit_resultlookupnegative. ff_h_pvs_left_unit_resultlookupnegative + S (dst_negative_left_unit_resultlookup) = S ((S (dc_input_left_unit_result)) * dst_negative_scale_left_unit_resultlookup)) /\ exists ff_q_pvs_left_unit_resultlookupnegative. dst_negative_code_left_unit_resultlookup = ff_q_pvs_left_unit_resultlookupnegative * S ((S (dc_input_left_unit_result)) * dst_negative_scale_left_unit_resultlookup) + (dst_negative_left_unit_resultlookup))) /\ (exists ge_balance_positive_left_unit_resultlookupvalue ge_balance_negative_left_unit_resultlookupvalue. (((((dc_output_left_unit_result) = 2 * (ge_balance_positive_left_unit_resultlookupvalue) /\ (ge_balance_negative_left_unit_resultlookupvalue) = 0) \/ exists ge_signed_half_left_unit_resultlookupvaluedecode. (((dc_output_left_unit_result) = 2 * ge_signed_half_left_unit_resultlookupvaluedecode + 1 /\ (ge_balance_positive_left_unit_resultlookupvalue) = 0) /\ (ge_balance_negative_left_unit_resultlookupvalue) = S ge_signed_half_left_unit_resultlookupvaluedecode))) /\ ((dst_positive_left_unit_resultlookup) + ge_balance_negative_left_unit_resultlookupvalue = (dst_negative_left_unit_resultlookup) + ge_balance_positive_left_unit_resultlookupvalue))))))))) -> (((~((dc_input_left_unit_result)=0)) /\ (exists dc_mask_left_unit_resultvalue. ((((exists dst_positive_code_left_unit_resultvaluemasktable dst_positive_scale_left_unit_resultvaluemasktable dst_negative_code_left_unit_resultvaluemasktable dst_negative_scale_left_unit_resultvaluemasktable. (((dc_mask_left_unit_resultvalue) = (((((dst_positive_code_left_unit_resultvaluemasktable) + (dst_positive_scale_left_unit_resultvaluemasktable)) * S ((dst_positive_code_left_unit_resultvaluemasktable) + (dst_positive_scale_left_unit_resultvaluemasktable)) + ((dst_positive_scale_left_unit_resultvaluemasktable) + (dst_positive_scale_left_unit_resultvaluemasktable))) + (((dst_negative_code_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)) * S ((dst_negative_code_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)) + ((dst_negative_scale_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)))) * S ((((dst_positive_code_left_unit_resultvaluemasktable) + (dst_positive_scale_left_unit_resultvaluemasktable)) * S ((dst_positive_code_left_unit_resultvaluemasktable) + (dst_positive_scale_left_unit_resultvaluemasktable)) + ((dst_positive_scale_left_unit_resultvaluemasktable) + (dst_positive_scale_left_unit_resultvaluemasktable))) + (((dst_negative_code_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)) * S ((dst_negative_code_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)) + ((dst_negative_scale_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)))) + ((((dst_negative_code_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)) * S ((dst_negative_code_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)) + ((dst_negative_scale_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable))) + (((dst_negative_code_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)) * S ((dst_negative_code_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)) + ((dst_negative_scale_left_unit_resultvaluemasktable) + (dst_negative_scale_left_unit_resultvaluemasktable)))))) /\ (forall dst_index_left_unit_resultvaluemasktable. (exists pvs_le_gap_left_unit_resultvaluemasktabledomain. pvs_le_gap_left_unit_resultvaluemasktabledomain + (dst_index_left_unit_resultvaluemasktable) = (dc_input_left_unit_result)) -> exists dst_positive_left_unit_resultvaluemasktable dst_negative_left_unit_resultvaluemasktable dst_value_left_unit_resultvaluemasktable. ((((exists ff_h_pvs_left_unit_resultvaluemasktableentrypositive. ff_h_pvs_left_unit_resultvaluemasktableentrypositive + S (dst_positive_left_unit_resultvaluemasktable) = S ((S (dst_index_left_unit_resultvaluemasktable)) * dst_positive_scale_left_unit_resultvaluemasktable)) /\ exists ff_q_pvs_left_unit_resultvaluemasktableentrypositive. dst_positive_code_left_unit_resultvaluemasktable = ff_q_pvs_left_unit_resultvaluemasktableentrypositive * S ((S (dst_index_left_unit_resultvaluemasktable)) * dst_positive_scale_left_unit_resultvaluemasktable) + (dst_positive_left_unit_resultvaluemasktable))) /\ (((((exists ff_h_pvs_left_unit_resultvaluemasktableentrynegative. ff_h_pvs_left_unit_resultvaluemasktableentrynegative + S (dst_negative_left_unit_resultvaluemasktable) = S ((S (dst_index_left_unit_resultvaluemasktable)) * dst_negative_scale_left_unit_resultvaluemasktable)) /\ exists ff_q_pvs_left_unit_resultvaluemasktableentrynegative. dst_negative_code_left_unit_resultvaluemasktable = ff_q_pvs_left_unit_resultvaluemasktableentrynegative * S ((S (dst_index_left_unit_resultvaluemasktable)) * dst_negative_scale_left_unit_resultvaluemasktable) + (dst_negative_left_unit_resultvaluemasktable))) /\ (exists ge_balance_positive_left_unit_resultvaluemasktableentryvalue ge_balance_negative_left_unit_resultvaluemasktableentryvalue. (((((dst_value_left_unit_resultvaluemasktable) = 2 * (ge_balance_positive_left_unit_resultvaluemasktableentryvalue) /\ (ge_balance_negative_left_unit_resultvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_left_unit_resultvaluemasktableentryvaluedecode. (((dst_value_left_unit_resultvaluemasktable) = 2 * ge_signed_half_left_unit_resultvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_left_unit_resultvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_left_unit_resultvaluemasktableentryvalue) = S ge_signed_half_left_unit_resultvaluemasktableentryvaluedecode))) /\ ((dst_positive_left_unit_resultvaluemasktable) + ge_balance_negative_left_unit_resultvaluemasktableentryvalue = (dst_negative_left_unit_resultvaluemasktable) + ge_balance_positive_left_unit_resultvaluemasktableentryvalue))))))))) /\ (forall dc_index_left_unit_resultvaluemask dc_value_left_unit_resultvaluemask. (exists pvs_le_gap_left_unit_resultvaluemaskdomain. pvs_le_gap_left_unit_resultvaluemaskdomain + (dc_index_left_unit_resultvaluemask) = (dc_input_left_unit_result)) -> (exists dst_positive_code_left_unit_resultvaluemasklookup dst_positive_scale_left_unit_resultvaluemasklookup dst_negative_code_left_unit_resultvaluemasklookup dst_negative_scale_left_unit_resultvaluemasklookup dst_positive_left_unit_resultvaluemasklookup dst_negative_left_unit_resultvaluemasklookup. (((dc_mask_left_unit_resultvalue) = (((((dst_positive_code_left_unit_resultvaluemasklookup) + (dst_positive_scale_left_unit_resultvaluemasklookup)) * S ((dst_positive_code_left_unit_resultvaluemasklookup) + (dst_positive_scale_left_unit_resultvaluemasklookup)) + ((dst_positive_scale_left_unit_resultvaluemasklookup) + (dst_positive_scale_left_unit_resultvaluemasklookup))) + (((dst_negative_code_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)) * S ((dst_negative_code_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)) + ((dst_negative_scale_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)))) * S ((((dst_positive_code_left_unit_resultvaluemasklookup) + (dst_positive_scale_left_unit_resultvaluemasklookup)) * S ((dst_positive_code_left_unit_resultvaluemasklookup) + (dst_positive_scale_left_unit_resultvaluemasklookup)) + ((dst_positive_scale_left_unit_resultvaluemasklookup) + (dst_positive_scale_left_unit_resultvaluemasklookup))) + (((dst_negative_code_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)) * S ((dst_negative_code_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)) + ((dst_negative_scale_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)))) + ((((dst_negative_code_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)) * S ((dst_negative_code_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)) + ((dst_negative_scale_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup))) + (((dst_negative_code_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)) * S ((dst_negative_code_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)) + ((dst_negative_scale_left_unit_resultvaluemasklookup) + (dst_negative_scale_left_unit_resultvaluemasklookup)))))) /\ (((((exists ff_h_pvs_left_unit_resultvaluemasklookuppositive. ff_h_pvs_left_unit_resultvaluemasklookuppositive + S (dst_positive_left_unit_resultvaluemasklookup) = S ((S (dc_index_left_unit_resultvaluemask)) * dst_positive_scale_left_unit_resultvaluemasklookup)) /\ exists ff_q_pvs_left_unit_resultvaluemasklookuppositive. dst_positive_code_left_unit_resultvaluemasklookup = ff_q_pvs_left_unit_resultvaluemasklookuppositive * S ((S (dc_index_left_unit_resultvaluemask)) * dst_positive_scale_left_unit_resultvaluemasklookup) + (dst_positive_left_unit_resultvaluemasklookup))) /\ (((((exists ff_h_pvs_left_unit_resultvaluemasklookupnegative. ff_h_pvs_left_unit_resultvaluemasklookupnegative + S (dst_negative_left_unit_resultvaluemasklookup) = S ((S (dc_index_left_unit_resultvaluemask)) * dst_negative_scale_left_unit_resultvaluemasklookup)) /\ exists ff_q_pvs_left_unit_resultvaluemasklookupnegative. dst_negative_code_left_unit_resultvaluemasklookup = ff_q_pvs_left_unit_resultvaluemasklookupnegative * S ((S (dc_index_left_unit_resultvaluemask)) * dst_negative_scale_left_unit_resultvaluemasklookup) + (dst_negative_left_unit_resultvaluemasklookup))) /\ (exists ge_balance_positive_left_unit_resultvaluemasklookupvalue ge_balance_negative_left_unit_resultvaluemasklookupvalue. (((((dc_value_left_unit_resultvaluemask) = 2 * (ge_balance_positive_left_unit_resultvaluemasklookupvalue) /\ (ge_balance_negative_left_unit_resultvaluemasklookupvalue) = 0) \/ exists ge_signed_half_left_unit_resultvaluemasklookupvaluedecode. (((dc_value_left_unit_resultvaluemask) = 2 * ge_signed_half_left_unit_resultvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_left_unit_resultvaluemasklookupvalue) = 0) /\ (ge_balance_negative_left_unit_resultvaluemasklookupvalue) = S ge_signed_half_left_unit_resultvaluemasklookupvaluedecode))) /\ ((dst_positive_left_unit_resultvaluemasklookup) + ge_balance_negative_left_unit_resultvaluemasklookupvalue = (dst_negative_left_unit_resultvaluemasklookup) + ge_balance_positive_left_unit_resultvaluemasklookupvalue))))))))) -> ((((~((dc_index_left_unit_resultvaluemask)=0)) /\ (exists dc_quotient_left_unit_resultvaluemaskentry dc_left_left_unit_resultvaluemaskentry dc_right_left_unit_resultvaluemaskentry. (((dc_input_left_unit_result)=(dc_index_left_unit_resultvaluemask)*dc_quotient_left_unit_resultvaluemaskentry) /\ (((exists dst_positive_code_left_unit_resultvaluemaskentryleft dst_positive_scale_left_unit_resultvaluemaskentryleft dst_negative_code_left_unit_resultvaluemaskentryleft dst_negative_scale_left_unit_resultvaluemaskentryleft dst_positive_left_unit_resultvaluemaskentryleft dst_negative_left_unit_resultvaluemaskentryleft. (((E) = (((((dst_positive_code_left_unit_resultvaluemaskentryleft) + (dst_positive_scale_left_unit_resultvaluemaskentryleft)) * S ((dst_positive_code_left_unit_resultvaluemaskentryleft) + (dst_positive_scale_left_unit_resultvaluemaskentryleft)) + ((dst_positive_scale_left_unit_resultvaluemaskentryleft) + (dst_positive_scale_left_unit_resultvaluemaskentryleft))) + (((dst_negative_code_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)) * S ((dst_negative_code_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)) + ((dst_negative_scale_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)))) * S ((((dst_positive_code_left_unit_resultvaluemaskentryleft) + (dst_positive_scale_left_unit_resultvaluemaskentryleft)) * S ((dst_positive_code_left_unit_resultvaluemaskentryleft) + (dst_positive_scale_left_unit_resultvaluemaskentryleft)) + ((dst_positive_scale_left_unit_resultvaluemaskentryleft) + (dst_positive_scale_left_unit_resultvaluemaskentryleft))) + (((dst_negative_code_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)) * S ((dst_negative_code_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)) + ((dst_negative_scale_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)))) + ((((dst_negative_code_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)) * S ((dst_negative_code_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)) + ((dst_negative_scale_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft))) + (((dst_negative_code_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)) * S ((dst_negative_code_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)) + ((dst_negative_scale_left_unit_resultvaluemaskentryleft) + (dst_negative_scale_left_unit_resultvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_left_unit_resultvaluemaskentryleftpositive. ff_h_pvs_left_unit_resultvaluemaskentryleftpositive + S (dst_positive_left_unit_resultvaluemaskentryleft) = S ((S (dc_index_left_unit_resultvaluemask)) * dst_positive_scale_left_unit_resultvaluemaskentryleft)) /\ exists ff_q_pvs_left_unit_resultvaluemaskentryleftpositive. dst_positive_code_left_unit_resultvaluemaskentryleft = ff_q_pvs_left_unit_resultvaluemaskentryleftpositive * S ((S (dc_index_left_unit_resultvaluemask)) * dst_positive_scale_left_unit_resultvaluemaskentryleft) + (dst_positive_left_unit_resultvaluemaskentryleft))) /\ (((((exists ff_h_pvs_left_unit_resultvaluemaskentryleftnegative. ff_h_pvs_left_unit_resultvaluemaskentryleftnegative + S (dst_negative_left_unit_resultvaluemaskentryleft) = S ((S (dc_index_left_unit_resultvaluemask)) * dst_negative_scale_left_unit_resultvaluemaskentryleft)) /\ exists ff_q_pvs_left_unit_resultvaluemaskentryleftnegative. dst_negative_code_left_unit_resultvaluemaskentryleft = ff_q_pvs_left_unit_resultvaluemaskentryleftnegative * S ((S (dc_index_left_unit_resultvaluemask)) * dst_negative_scale_left_unit_resultvaluemaskentryleft) + (dst_negative_left_unit_resultvaluemaskentryleft))) /\ (exists ge_balance_positive_left_unit_resultvaluemaskentryleftvalue ge_balance_negative_left_unit_resultvaluemaskentryleftvalue. (((((dc_left_left_unit_resultvaluemaskentry) = 2 * (ge_balance_positive_left_unit_resultvaluemaskentryleftvalue) /\ (ge_balance_negative_left_unit_resultvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_left_unit_resultvaluemaskentryleftvaluedecode. (((dc_left_left_unit_resultvaluemaskentry) = 2 * ge_signed_half_left_unit_resultvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_left_unit_resultvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_left_unit_resultvaluemaskentryleftvalue) = S ge_signed_half_left_unit_resultvaluemaskentryleftvaluedecode))) /\ ((dst_positive_left_unit_resultvaluemaskentryleft) + ge_balance_negative_left_unit_resultvaluemaskentryleftvalue = (dst_negative_left_unit_resultvaluemaskentryleft) + ge_balance_positive_left_unit_resultvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_left_unit_resultvaluemaskentryright dst_positive_scale_left_unit_resultvaluemaskentryright dst_negative_code_left_unit_resultvaluemaskentryright dst_negative_scale_left_unit_resultvaluemaskentryright dst_positive_left_unit_resultvaluemaskentryright dst_negative_left_unit_resultvaluemaskentryright. (((F) = (((((dst_positive_code_left_unit_resultvaluemaskentryright) + (dst_positive_scale_left_unit_resultvaluemaskentryright)) * S ((dst_positive_code_left_unit_resultvaluemaskentryright) + (dst_positive_scale_left_unit_resultvaluemaskentryright)) + ((dst_positive_scale_left_unit_resultvaluemaskentryright) + (dst_positive_scale_left_unit_resultvaluemaskentryright))) + (((dst_negative_code_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)) * S ((dst_negative_code_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)) + ((dst_negative_scale_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)))) * S ((((dst_positive_code_left_unit_resultvaluemaskentryright) + (dst_positive_scale_left_unit_resultvaluemaskentryright)) * S ((dst_positive_code_left_unit_resultvaluemaskentryright) + (dst_positive_scale_left_unit_resultvaluemaskentryright)) + ((dst_positive_scale_left_unit_resultvaluemaskentryright) + (dst_positive_scale_left_unit_resultvaluemaskentryright))) + (((dst_negative_code_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)) * S ((dst_negative_code_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)) + ((dst_negative_scale_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)))) + ((((dst_negative_code_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)) * S ((dst_negative_code_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)) + ((dst_negative_scale_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright))) + (((dst_negative_code_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)) * S ((dst_negative_code_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)) + ((dst_negative_scale_left_unit_resultvaluemaskentryright) + (dst_negative_scale_left_unit_resultvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_left_unit_resultvaluemaskentryrightpositive. ff_h_pvs_left_unit_resultvaluemaskentryrightpositive + S (dst_positive_left_unit_resultvaluemaskentryright) = S ((S (dc_quotient_left_unit_resultvaluemaskentry)) * dst_positive_scale_left_unit_resultvaluemaskentryright)) /\ exists ff_q_pvs_left_unit_resultvaluemaskentryrightpositive. dst_positive_code_left_unit_resultvaluemaskentryright = ff_q_pvs_left_unit_resultvaluemaskentryrightpositive * S ((S (dc_quotient_left_unit_resultvaluemaskentry)) * dst_positive_scale_left_unit_resultvaluemaskentryright) + (dst_positive_left_unit_resultvaluemaskentryright))) /\ (((((exists ff_h_pvs_left_unit_resultvaluemaskentryrightnegative. ff_h_pvs_left_unit_resultvaluemaskentryrightnegative + S (dst_negative_left_unit_resultvaluemaskentryright) = S ((S (dc_quotient_left_unit_resultvaluemaskentry)) * dst_negative_scale_left_unit_resultvaluemaskentryright)) /\ exists ff_q_pvs_left_unit_resultvaluemaskentryrightnegative. dst_negative_code_left_unit_resultvaluemaskentryright = ff_q_pvs_left_unit_resultvaluemaskentryrightnegative * S ((S (dc_quotient_left_unit_resultvaluemaskentry)) * dst_negative_scale_left_unit_resultvaluemaskentryright) + (dst_negative_left_unit_resultvaluemaskentryright))) /\ (exists ge_balance_positive_left_unit_resultvaluemaskentryrightvalue ge_balance_negative_left_unit_resultvaluemaskentryrightvalue. (((((dc_right_left_unit_resultvaluemaskentry) = 2 * (ge_balance_positive_left_unit_resultvaluemaskentryrightvalue) /\ (ge_balance_negative_left_unit_resultvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_left_unit_resultvaluemaskentryrightvaluedecode. (((dc_right_left_unit_resultvaluemaskentry) = 2 * ge_signed_half_left_unit_resultvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_left_unit_resultvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_left_unit_resultvaluemaskentryrightvalue) = S ge_signed_half_left_unit_resultvaluemaskentryrightvaluedecode))) /\ ((dst_positive_left_unit_resultvaluemaskentryright) + ge_balance_negative_left_unit_resultvaluemaskentryrightvalue = (dst_negative_left_unit_resultvaluemaskentryright) + ge_balance_positive_left_unit_resultvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_left_unit_resultvaluemaskentryproduct sto_an_left_unit_resultvaluemaskentryproduct sto_bp_left_unit_resultvaluemaskentryproduct sto_bn_left_unit_resultvaluemaskentryproduct sto_cp_left_unit_resultvaluemaskentryproduct sto_cn_left_unit_resultvaluemaskentryproduct. (((((dc_left_left_unit_resultvaluemaskentry) = 2 * (sto_ap_left_unit_resultvaluemaskentryproduct) /\ (sto_an_left_unit_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_left_unit_resultvaluemaskentryproductleft. (((dc_left_left_unit_resultvaluemaskentry) = 2 * ge_signed_half_left_unit_resultvaluemaskentryproductleft + 1 /\ (sto_ap_left_unit_resultvaluemaskentryproduct) = 0) /\ (sto_an_left_unit_resultvaluemaskentryproduct) = S ge_signed_half_left_unit_resultvaluemaskentryproductleft))) /\ ((((((dc_right_left_unit_resultvaluemaskentry) = 2 * (sto_bp_left_unit_resultvaluemaskentryproduct) /\ (sto_bn_left_unit_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_left_unit_resultvaluemaskentryproductright. (((dc_right_left_unit_resultvaluemaskentry) = 2 * ge_signed_half_left_unit_resultvaluemaskentryproductright + 1 /\ (sto_bp_left_unit_resultvaluemaskentryproduct) = 0) /\ (sto_bn_left_unit_resultvaluemaskentryproduct) = S ge_signed_half_left_unit_resultvaluemaskentryproductright))) /\ ((((((dc_value_left_unit_resultvaluemask) = 2 * (sto_cp_left_unit_resultvaluemaskentryproduct) /\ (sto_cn_left_unit_resultvaluemaskentryproduct) = 0) \/ exists ge_signed_half_left_unit_resultvaluemaskentryproductoutput. (((dc_value_left_unit_resultvaluemask) = 2 * ge_signed_half_left_unit_resultvaluemaskentryproductoutput + 1 /\ (sto_cp_left_unit_resultvaluemaskentryproduct) = 0) /\ (sto_cn_left_unit_resultvaluemaskentryproduct) = S ge_signed_half_left_unit_resultvaluemaskentryproductoutput))) /\ ((sto_ap_left_unit_resultvaluemaskentryproduct * sto_bp_left_unit_resultvaluemaskentryproduct + sto_an_left_unit_resultvaluemaskentryproduct * sto_bn_left_unit_resultvaluemaskentryproduct) + sto_cn_left_unit_resultvaluemaskentryproduct = (sto_ap_left_unit_resultvaluemaskentryproduct * sto_bn_left_unit_resultvaluemaskentryproduct + sto_an_left_unit_resultvaluemaskentryproduct * sto_bp_left_unit_resultvaluemaskentryproduct) + sto_cp_left_unit_resultvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_left_unit_resultvaluemask)=0 \/ ~(exists pvs_factor_left_unit_resultvaluemaskentrynondivisor. (dc_input_left_unit_result) = (dc_index_left_unit_resultvaluemask) * pvs_factor_left_unit_resultvaluemaskentrynondivisor)) /\ ((dc_value_left_unit_resultvaluemask)=0))))))) /\ (exists dst_positive_code_left_unit_resultvaluefold dst_positive_scale_left_unit_resultvaluefold dst_negative_code_left_unit_resultvaluefold dst_negative_scale_left_unit_resultvaluefold dst_positive_sum_left_unit_resultvaluefold dst_negative_sum_left_unit_resultvaluefold. (((dc_mask_left_unit_resultvalue) = (((((dst_positive_code_left_unit_resultvaluefold) + (dst_positive_scale_left_unit_resultvaluefold)) * S ((dst_positive_code_left_unit_resultvaluefold) + (dst_positive_scale_left_unit_resultvaluefold)) + ((dst_positive_scale_left_unit_resultvaluefold) + (dst_positive_scale_left_unit_resultvaluefold))) + (((dst_negative_code_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)) * S ((dst_negative_code_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)) + ((dst_negative_scale_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)))) * S ((((dst_positive_code_left_unit_resultvaluefold) + (dst_positive_scale_left_unit_resultvaluefold)) * S ((dst_positive_code_left_unit_resultvaluefold) + (dst_positive_scale_left_unit_resultvaluefold)) + ((dst_positive_scale_left_unit_resultvaluefold) + (dst_positive_scale_left_unit_resultvaluefold))) + (((dst_negative_code_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)) * S ((dst_negative_code_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)) + ((dst_negative_scale_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)))) + ((((dst_negative_code_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)) * S ((dst_negative_code_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)) + ((dst_negative_scale_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold))) + (((dst_negative_code_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)) * S ((dst_negative_code_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)) + ((dst_negative_scale_left_unit_resultvaluefold) + (dst_negative_scale_left_unit_resultvaluefold)))))) /\ (((exists fs_u_dst_left_unit_resultvaluefoldpositive fs_v_dst_left_unit_resultvaluefoldpositive. ((((exists fs_h_dst_left_unit_resultvaluefoldpositive_body_start. fs_h_dst_left_unit_resultvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_left_unit_resultvaluefoldpositive)) /\ exists fs_q_dst_left_unit_resultvaluefoldpositive_body_start. fs_u_dst_left_unit_resultvaluefoldpositive = fs_q_dst_left_unit_resultvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_left_unit_resultvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_left_unit_resultvaluefoldpositive_body_terminal. fs_h_dst_left_unit_resultvaluefoldpositive_body_terminal + S (dst_positive_sum_left_unit_resultvaluefold) = S ((S (S (dc_input_left_unit_result))) * fs_v_dst_left_unit_resultvaluefoldpositive)) /\ exists fs_q_dst_left_unit_resultvaluefoldpositive_body_terminal. fs_u_dst_left_unit_resultvaluefoldpositive = fs_q_dst_left_unit_resultvaluefoldpositive_body_terminal * S ((S (S (dc_input_left_unit_result))) * fs_v_dst_left_unit_resultvaluefoldpositive) + (dst_positive_sum_left_unit_resultvaluefold))) /\ forall fs_i_dst_left_unit_resultvaluefoldpositive_body_steps. (exists fs_lt_dst_left_unit_resultvaluefoldpositive_body_steps_bound. fs_lt_dst_left_unit_resultvaluefoldpositive_body_steps_bound + S fs_i_dst_left_unit_resultvaluefoldpositive_body_steps = S (dc_input_left_unit_result)) -> exists fs_a_dst_left_unit_resultvaluefoldpositive_body_steps fs_r_dst_left_unit_resultvaluefoldpositive_body_steps fs_s_dst_left_unit_resultvaluefoldpositive_body_steps. ((((exists fs_h_dst_left_unit_resultvaluefoldpositive_body_steps_summand. fs_h_dst_left_unit_resultvaluefoldpositive_body_steps_summand + S (fs_a_dst_left_unit_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_left_unit_resultvaluefoldpositive_body_steps)) * dst_positive_scale_left_unit_resultvaluefold)) /\ exists fs_q_dst_left_unit_resultvaluefoldpositive_body_steps_summand. dst_positive_code_left_unit_resultvaluefold = fs_q_dst_left_unit_resultvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_left_unit_resultvaluefoldpositive_body_steps)) * dst_positive_scale_left_unit_resultvaluefold) + (fs_a_dst_left_unit_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_left_unit_resultvaluefoldpositive_body_steps_partial. fs_h_dst_left_unit_resultvaluefoldpositive_body_steps_partial + S (fs_r_dst_left_unit_resultvaluefoldpositive_body_steps) = S ((S (fs_i_dst_left_unit_resultvaluefoldpositive_body_steps)) * fs_v_dst_left_unit_resultvaluefoldpositive)) /\ exists fs_q_dst_left_unit_resultvaluefoldpositive_body_steps_partial. fs_u_dst_left_unit_resultvaluefoldpositive = fs_q_dst_left_unit_resultvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_left_unit_resultvaluefoldpositive_body_steps)) * fs_v_dst_left_unit_resultvaluefoldpositive) + (fs_r_dst_left_unit_resultvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_left_unit_resultvaluefoldpositive_body_steps_successor. fs_h_dst_left_unit_resultvaluefoldpositive_body_steps_successor + S (fs_s_dst_left_unit_resultvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_left_unit_resultvaluefoldpositive_body_steps)) * fs_v_dst_left_unit_resultvaluefoldpositive)) /\ exists fs_q_dst_left_unit_resultvaluefoldpositive_body_steps_successor. fs_u_dst_left_unit_resultvaluefoldpositive = fs_q_dst_left_unit_resultvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_left_unit_resultvaluefoldpositive_body_steps)) * fs_v_dst_left_unit_resultvaluefoldpositive) + (fs_s_dst_left_unit_resultvaluefoldpositive_body_steps))) /\ fs_s_dst_left_unit_resultvaluefoldpositive_body_steps = fs_r_dst_left_unit_resultvaluefoldpositive_body_steps + fs_a_dst_left_unit_resultvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_left_unit_resultvaluefoldnegative fs_v_dst_left_unit_resultvaluefoldnegative. ((((exists fs_h_dst_left_unit_resultvaluefoldnegative_body_start. fs_h_dst_left_unit_resultvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_left_unit_resultvaluefoldnegative)) /\ exists fs_q_dst_left_unit_resultvaluefoldnegative_body_start. fs_u_dst_left_unit_resultvaluefoldnegative = fs_q_dst_left_unit_resultvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_left_unit_resultvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_left_unit_resultvaluefoldnegative_body_terminal. fs_h_dst_left_unit_resultvaluefoldnegative_body_terminal + S (dst_negative_sum_left_unit_resultvaluefold) = S ((S (S (dc_input_left_unit_result))) * fs_v_dst_left_unit_resultvaluefoldnegative)) /\ exists fs_q_dst_left_unit_resultvaluefoldnegative_body_terminal. fs_u_dst_left_unit_resultvaluefoldnegative = fs_q_dst_left_unit_resultvaluefoldnegative_body_terminal * S ((S (S (dc_input_left_unit_result))) * fs_v_dst_left_unit_resultvaluefoldnegative) + (dst_negative_sum_left_unit_resultvaluefold))) /\ forall fs_i_dst_left_unit_resultvaluefoldnegative_body_steps. (exists fs_lt_dst_left_unit_resultvaluefoldnegative_body_steps_bound. fs_lt_dst_left_unit_resultvaluefoldnegative_body_steps_bound + S fs_i_dst_left_unit_resultvaluefoldnegative_body_steps = S (dc_input_left_unit_result)) -> exists fs_a_dst_left_unit_resultvaluefoldnegative_body_steps fs_r_dst_left_unit_resultvaluefoldnegative_body_steps fs_s_dst_left_unit_resultvaluefoldnegative_body_steps. ((((exists fs_h_dst_left_unit_resultvaluefoldnegative_body_steps_summand. fs_h_dst_left_unit_resultvaluefoldnegative_body_steps_summand + S (fs_a_dst_left_unit_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_left_unit_resultvaluefoldnegative_body_steps)) * dst_negative_scale_left_unit_resultvaluefold)) /\ exists fs_q_dst_left_unit_resultvaluefoldnegative_body_steps_summand. dst_negative_code_left_unit_resultvaluefold = fs_q_dst_left_unit_resultvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_left_unit_resultvaluefoldnegative_body_steps)) * dst_negative_scale_left_unit_resultvaluefold) + (fs_a_dst_left_unit_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_left_unit_resultvaluefoldnegative_body_steps_partial. fs_h_dst_left_unit_resultvaluefoldnegative_body_steps_partial + S (fs_r_dst_left_unit_resultvaluefoldnegative_body_steps) = S ((S (fs_i_dst_left_unit_resultvaluefoldnegative_body_steps)) * fs_v_dst_left_unit_resultvaluefoldnegative)) /\ exists fs_q_dst_left_unit_resultvaluefoldnegative_body_steps_partial. fs_u_dst_left_unit_resultvaluefoldnegative = fs_q_dst_left_unit_resultvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_left_unit_resultvaluefoldnegative_body_steps)) * fs_v_dst_left_unit_resultvaluefoldnegative) + (fs_r_dst_left_unit_resultvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_left_unit_resultvaluefoldnegative_body_steps_successor. fs_h_dst_left_unit_resultvaluefoldnegative_body_steps_successor + S (fs_s_dst_left_unit_resultvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_left_unit_resultvaluefoldnegative_body_steps)) * fs_v_dst_left_unit_resultvaluefoldnegative)) /\ exists fs_q_dst_left_unit_resultvaluefoldnegative_body_steps_successor. fs_u_dst_left_unit_resultvaluefoldnegative = fs_q_dst_left_unit_resultvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_left_unit_resultvaluefoldnegative_body_steps)) * fs_v_dst_left_unit_resultvaluefoldnegative) + (fs_s_dst_left_unit_resultvaluefoldnegative_body_steps))) /\ fs_s_dst_left_unit_resultvaluefoldnegative_body_steps = fs_r_dst_left_unit_resultvaluefoldnegative_body_steps + fs_a_dst_left_unit_resultvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_left_unit_resultvaluefoldresult ge_balance_negative_left_unit_resultvaluefoldresult. (((((dc_output_left_unit_result) = 2 * (ge_balance_positive_left_unit_resultvaluefoldresult) /\ (ge_balance_negative_left_unit_resultvaluefoldresult) = 0) \/ exists ge_signed_half_left_unit_resultvaluefoldresultdecode. (((dc_output_left_unit_result) = 2 * ge_signed_half_left_unit_resultvaluefoldresultdecode + 1 /\ (ge_balance_positive_left_unit_resultvaluefoldresult) = 0) /\ (ge_balance_negative_left_unit_resultvaluefoldresult) = S ge_signed_half_left_unit_resultvaluefoldresultdecode))) /\ ((dst_positive_sum_left_unit_resultvaluefold) + ge_balance_negative_left_unit_resultvaluefoldresult = (dst_negative_sum_left_unit_resultvaluefold) + ge_balance_positive_left_unit_resultvaluefoldresult))))))))))))))))))))