Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall N F u w. (exists dst_positive_code_inverse_unit_input dst_positive_scale_inverse_unit_input dst_negative_code_inverse_unit_input dst_negative_scale_inverse_unit_input. (((F) = (((((dst_positive_code_inverse_unit_input) + (dst_positive_scale_inverse_unit_input)) * S ((dst_positive_code_inverse_unit_input) + (dst_positive_scale_inverse_unit_input)) + ((dst_positive_scale_inverse_unit_input) + (dst_positive_scale_inverse_unit_input))) + (((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) * S ((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) + ((dst_negative_scale_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)))) * S ((((dst_positive_code_inverse_unit_input) + (dst_positive_scale_inverse_unit_input)) * S ((dst_positive_code_inverse_unit_input) + (dst_positive_scale_inverse_unit_input)) + ((dst_positive_scale_inverse_unit_input) + (dst_positive_scale_inverse_unit_input))) + (((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) * S ((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) + ((dst_negative_scale_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)))) + ((((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) * S ((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) + ((dst_negative_scale_inverse_unit_input) + (dst_negative_scale_inverse_unit_input))) + (((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) * S ((dst_negative_code_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)) + ((dst_negative_scale_inverse_unit_input) + (dst_negative_scale_inverse_unit_input)))))) /\ (forall dst_index_inverse_unit_input. (exists pvs_le_gap_inverse_unit_inputdomain. pvs_le_gap_inverse_unit_inputdomain + (dst_index_inverse_unit_input) = (N)) -> exists dst_positive_inverse_unit_input dst_negative_inverse_unit_input dst_value_inverse_unit_input. ((((exists ff_h_pvs_inverse_unit_inputentrypositive. ff_h_pvs_inverse_unit_inputentrypositive + S (dst_positive_inverse_unit_input) = S ((S (dst_index_inverse_unit_input)) * dst_positive_scale_inverse_unit_input)) /\ exists ff_q_pvs_inverse_unit_inputentrypositive. dst_positive_code_inverse_unit_input = ff_q_pvs_inverse_unit_inputentrypositive * S ((S (dst_index_inverse_unit_input)) * dst_positive_scale_inverse_unit_input) + (dst_positive_inverse_unit_input))) /\ (((((exists ff_h_pvs_inverse_unit_inputentrynegative. ff_h_pvs_inverse_unit_inputentrynegative + S (dst_negative_inverse_unit_input) = S ((S (dst_index_inverse_unit_input)) * dst_negative_scale_inverse_unit_input)) /\ exists ff_q_pvs_inverse_unit_inputentrynegative. dst_negative_code_inverse_unit_input = ff_q_pvs_inverse_unit_inputentrynegative * S ((S (dst_index_inverse_unit_input)) * dst_negative_scale_inverse_unit_input) + (dst_negative_inverse_unit_input))) /\ (exists ge_balance_positive_inverse_unit_inputentryvalue ge_balance_negative_inverse_unit_inputentryvalue. (((((dst_value_inverse_unit_input) = 2 * (ge_balance_positive_inverse_unit_inputentryvalue) /\ (ge_balance_negative_inverse_unit_inputentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_inputentryvaluedecode. (((dst_value_inverse_unit_input) = 2 * ge_signed_half_inverse_unit_inputentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_inputentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_inputentryvalue) = S ge_signed_half_inverse_unit_inputentryvaluedecode))) /\ ((dst_positive_inverse_unit_input) + ge_balance_negative_inverse_unit_inputentryvalue = (dst_negative_inverse_unit_input) + ge_balance_positive_inverse_unit_inputentryvalue))))))))) -> (exists dst_positive_code_inverse_unit_entry dst_positive_scale_inverse_unit_entry dst_negative_code_inverse_unit_entry dst_negative_scale_inverse_unit_entry dst_positive_inverse_unit_entry dst_negative_inverse_unit_entry. (((F) = (((((dst_positive_code_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry)) * S ((dst_positive_code_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry)) + ((dst_positive_scale_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry))) + (((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) * S ((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) + ((dst_negative_scale_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)))) * S ((((dst_positive_code_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry)) * S ((dst_positive_code_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry)) + ((dst_positive_scale_inverse_unit_entry) + (dst_positive_scale_inverse_unit_entry))) + (((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) * S ((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) + ((dst_negative_scale_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)))) + ((((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) * S ((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) + ((dst_negative_scale_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry))) + (((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) * S ((dst_negative_code_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)) + ((dst_negative_scale_inverse_unit_entry) + (dst_negative_scale_inverse_unit_entry)))))) /\ (((((exists ff_h_pvs_inverse_unit_entrypositive. ff_h_pvs_inverse_unit_entrypositive + S (dst_positive_inverse_unit_entry) = S ((S (1)) * dst_positive_scale_inverse_unit_entry)) /\ exists ff_q_pvs_inverse_unit_entrypositive. dst_positive_code_inverse_unit_entry = ff_q_pvs_inverse_unit_entrypositive * S ((S (1)) * dst_positive_scale_inverse_unit_entry) + (dst_positive_inverse_unit_entry))) /\ (((((exists ff_h_pvs_inverse_unit_entrynegative. ff_h_pvs_inverse_unit_entrynegative + S (dst_negative_inverse_unit_entry) = S ((S (1)) * dst_negative_scale_inverse_unit_entry)) /\ exists ff_q_pvs_inverse_unit_entrynegative. dst_negative_code_inverse_unit_entry = ff_q_pvs_inverse_unit_entrynegative * S ((S (1)) * dst_negative_scale_inverse_unit_entry) + (dst_negative_inverse_unit_entry))) /\ (exists ge_balance_positive_inverse_unit_entryvalue ge_balance_negative_inverse_unit_entryvalue. (((((u) = 2 * (ge_balance_positive_inverse_unit_entryvalue) /\ (ge_balance_negative_inverse_unit_entryvalue) = 0) \/ exists ge_signed_half_inverse_unit_entryvaluedecode. (((u) = 2 * ge_signed_half_inverse_unit_entryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_entryvalue) = 0) /\ (ge_balance_negative_inverse_unit_entryvalue) = S ge_signed_half_inverse_unit_entryvaluedecode))) /\ ((dst_positive_inverse_unit_entry) + ge_balance_negative_inverse_unit_entryvalue = (dst_negative_inverse_unit_entry) + ge_balance_positive_inverse_unit_entryvalue))))))))) -> (((u) = 2 \/ (u) = 1)) -> exists G. ((exists di_delta_inverse_unit_result. ((((exists dst_positive_code_inverse_unit_resultdeltatable dst_positive_scale_inverse_unit_resultdeltatable dst_negative_code_inverse_unit_resultdeltatable dst_negative_scale_inverse_unit_resultdeltatable. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable)) * S ((dst_positive_code_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable)) + ((dst_positive_scale_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable))) + (((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) * S ((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) + ((dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)))) * S ((((dst_positive_code_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable)) * S ((dst_positive_code_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable)) + ((dst_positive_scale_inverse_unit_resultdeltatable) + (dst_positive_scale_inverse_unit_resultdeltatable))) + (((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) * S ((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) + ((dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)))) + ((((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) * S ((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) + ((dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable))) + (((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) * S ((dst_negative_code_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)) + ((dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_scale_inverse_unit_resultdeltatable)))))) /\ (forall dst_index_inverse_unit_resultdeltatable. (exists pvs_le_gap_inverse_unit_resultdeltatabledomain. pvs_le_gap_inverse_unit_resultdeltatabledomain + (dst_index_inverse_unit_resultdeltatable) = (N)) -> exists dst_positive_inverse_unit_resultdeltatable dst_negative_inverse_unit_resultdeltatable dst_value_inverse_unit_resultdeltatable. ((((exists ff_h_pvs_inverse_unit_resultdeltatableentrypositive. ff_h_pvs_inverse_unit_resultdeltatableentrypositive + S (dst_positive_inverse_unit_resultdeltatable) = S ((S (dst_index_inverse_unit_resultdeltatable)) * dst_positive_scale_inverse_unit_resultdeltatable)) /\ exists ff_q_pvs_inverse_unit_resultdeltatableentrypositive. dst_positive_code_inverse_unit_resultdeltatable = ff_q_pvs_inverse_unit_resultdeltatableentrypositive * S ((S (dst_index_inverse_unit_resultdeltatable)) * dst_positive_scale_inverse_unit_resultdeltatable) + (dst_positive_inverse_unit_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_unit_resultdeltatableentrynegative. ff_h_pvs_inverse_unit_resultdeltatableentrynegative + S (dst_negative_inverse_unit_resultdeltatable) = S ((S (dst_index_inverse_unit_resultdeltatable)) * dst_negative_scale_inverse_unit_resultdeltatable)) /\ exists ff_q_pvs_inverse_unit_resultdeltatableentrynegative. dst_negative_code_inverse_unit_resultdeltatable = ff_q_pvs_inverse_unit_resultdeltatableentrynegative * S ((S (dst_index_inverse_unit_resultdeltatable)) * dst_negative_scale_inverse_unit_resultdeltatable) + (dst_negative_inverse_unit_resultdeltatable))) /\ (exists ge_balance_positive_inverse_unit_resultdeltatableentryvalue ge_balance_negative_inverse_unit_resultdeltatableentryvalue. (((((dst_value_inverse_unit_resultdeltatable) = 2 * (ge_balance_positive_inverse_unit_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_unit_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultdeltatableentryvaluedecode. (((dst_value_inverse_unit_resultdeltatable) = 2 * ge_signed_half_inverse_unit_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultdeltatableentryvalue) = S ge_signed_half_inverse_unit_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultdeltatable) + ge_balance_negative_inverse_unit_resultdeltatableentryvalue = (dst_negative_inverse_unit_resultdeltatable) + ge_balance_positive_inverse_unit_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_unit_resultdelta du_value_inverse_unit_resultdelta. ~(du_index_inverse_unit_resultdelta=0) -> (exists pvs_le_gap_inverse_unit_resultdeltabound. pvs_le_gap_inverse_unit_resultdeltabound + (du_index_inverse_unit_resultdelta) = (N)) -> (exists dst_positive_code_inverse_unit_resultdeltaentry dst_positive_scale_inverse_unit_resultdeltaentry dst_negative_code_inverse_unit_resultdeltaentry dst_negative_scale_inverse_unit_resultdeltaentry dst_positive_inverse_unit_resultdeltaentry dst_negative_inverse_unit_resultdeltaentry. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry)) * S ((dst_positive_code_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry)) + ((dst_positive_scale_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry))) + (((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) * S ((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) + ((dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)))) * S ((((dst_positive_code_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry)) * S ((dst_positive_code_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry)) + ((dst_positive_scale_inverse_unit_resultdeltaentry) + (dst_positive_scale_inverse_unit_resultdeltaentry))) + (((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) * S ((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) + ((dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)))) + ((((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) * S ((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) + ((dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry))) + (((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) * S ((dst_negative_code_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)) + ((dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_scale_inverse_unit_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultdeltaentrypositive. ff_h_pvs_inverse_unit_resultdeltaentrypositive + S (dst_positive_inverse_unit_resultdeltaentry) = S ((S (du_index_inverse_unit_resultdelta)) * dst_positive_scale_inverse_unit_resultdeltaentry)) /\ exists ff_q_pvs_inverse_unit_resultdeltaentrypositive. dst_positive_code_inverse_unit_resultdeltaentry = ff_q_pvs_inverse_unit_resultdeltaentrypositive * S ((S (du_index_inverse_unit_resultdelta)) * dst_positive_scale_inverse_unit_resultdeltaentry) + (dst_positive_inverse_unit_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_unit_resultdeltaentrynegative. ff_h_pvs_inverse_unit_resultdeltaentrynegative + S (dst_negative_inverse_unit_resultdeltaentry) = S ((S (du_index_inverse_unit_resultdelta)) * dst_negative_scale_inverse_unit_resultdeltaentry)) /\ exists ff_q_pvs_inverse_unit_resultdeltaentrynegative. dst_negative_code_inverse_unit_resultdeltaentry = ff_q_pvs_inverse_unit_resultdeltaentrynegative * S ((S (du_index_inverse_unit_resultdelta)) * dst_negative_scale_inverse_unit_resultdeltaentry) + (dst_negative_inverse_unit_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_unit_resultdeltaentryvalue ge_balance_negative_inverse_unit_resultdeltaentryvalue. (((((du_value_inverse_unit_resultdelta) = 2 * (ge_balance_positive_inverse_unit_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_unit_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultdeltaentryvaluedecode. (((du_value_inverse_unit_resultdelta) = 2 * ge_signed_half_inverse_unit_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultdeltaentryvalue) = S ge_signed_half_inverse_unit_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultdeltaentry) + ge_balance_negative_inverse_unit_resultdeltaentryvalue = (dst_negative_inverse_unit_resultdeltaentry) + ge_balance_positive_inverse_unit_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_unit_resultdelta)=1 -> (du_value_inverse_unit_resultdelta)=2) /\ (~((du_index_inverse_unit_resultdelta)=1) -> (du_value_inverse_unit_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_unit_resultleftleft dst_positive_scale_inverse_unit_resultleftleft dst_negative_code_inverse_unit_resultleftleft dst_negative_scale_inverse_unit_resultleftleft. (((F) = (((((dst_positive_code_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft)) * S ((dst_positive_code_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft)) + ((dst_positive_scale_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft))) + (((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) * S ((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) + ((dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)))) * S ((((dst_positive_code_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft)) * S ((dst_positive_code_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft)) + ((dst_positive_scale_inverse_unit_resultleftleft) + (dst_positive_scale_inverse_unit_resultleftleft))) + (((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) * S ((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) + ((dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)))) + ((((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) * S ((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) + ((dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft))) + (((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) * S ((dst_negative_code_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)) + ((dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_scale_inverse_unit_resultleftleft)))))) /\ (forall dst_index_inverse_unit_resultleftleft. (exists pvs_le_gap_inverse_unit_resultleftleftdomain. pvs_le_gap_inverse_unit_resultleftleftdomain + (dst_index_inverse_unit_resultleftleft) = (N)) -> exists dst_positive_inverse_unit_resultleftleft dst_negative_inverse_unit_resultleftleft dst_value_inverse_unit_resultleftleft. ((((exists ff_h_pvs_inverse_unit_resultleftleftentrypositive. ff_h_pvs_inverse_unit_resultleftleftentrypositive + S (dst_positive_inverse_unit_resultleftleft) = S ((S (dst_index_inverse_unit_resultleftleft)) * dst_positive_scale_inverse_unit_resultleftleft)) /\ exists ff_q_pvs_inverse_unit_resultleftleftentrypositive. dst_positive_code_inverse_unit_resultleftleft = ff_q_pvs_inverse_unit_resultleftleftentrypositive * S ((S (dst_index_inverse_unit_resultleftleft)) * dst_positive_scale_inverse_unit_resultleftleft) + (dst_positive_inverse_unit_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftleftentrynegative. ff_h_pvs_inverse_unit_resultleftleftentrynegative + S (dst_negative_inverse_unit_resultleftleft) = S ((S (dst_index_inverse_unit_resultleftleft)) * dst_negative_scale_inverse_unit_resultleftleft)) /\ exists ff_q_pvs_inverse_unit_resultleftleftentrynegative. dst_negative_code_inverse_unit_resultleftleft = ff_q_pvs_inverse_unit_resultleftleftentrynegative * S ((S (dst_index_inverse_unit_resultleftleft)) * dst_negative_scale_inverse_unit_resultleftleft) + (dst_negative_inverse_unit_resultleftleft))) /\ (exists ge_balance_positive_inverse_unit_resultleftleftentryvalue ge_balance_negative_inverse_unit_resultleftleftentryvalue. (((((dst_value_inverse_unit_resultleftleft) = 2 * (ge_balance_positive_inverse_unit_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_unit_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftleftentryvaluedecode. (((dst_value_inverse_unit_resultleftleft) = 2 * ge_signed_half_inverse_unit_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftleftentryvalue) = S ge_signed_half_inverse_unit_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftleft) + ge_balance_negative_inverse_unit_resultleftleftentryvalue = (dst_negative_inverse_unit_resultleftleft) + ge_balance_positive_inverse_unit_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultleftright dst_positive_scale_inverse_unit_resultleftright dst_negative_code_inverse_unit_resultleftright dst_negative_scale_inverse_unit_resultleftright. (((G) = (((((dst_positive_code_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright)) * S ((dst_positive_code_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright)) + ((dst_positive_scale_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright))) + (((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) * S ((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) + ((dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)))) * S ((((dst_positive_code_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright)) * S ((dst_positive_code_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright)) + ((dst_positive_scale_inverse_unit_resultleftright) + (dst_positive_scale_inverse_unit_resultleftright))) + (((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) * S ((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) + ((dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)))) + ((((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) * S ((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) + ((dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright))) + (((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) * S ((dst_negative_code_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)) + ((dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_scale_inverse_unit_resultleftright)))))) /\ (forall dst_index_inverse_unit_resultleftright. (exists pvs_le_gap_inverse_unit_resultleftrightdomain. pvs_le_gap_inverse_unit_resultleftrightdomain + (dst_index_inverse_unit_resultleftright) = (N)) -> exists dst_positive_inverse_unit_resultleftright dst_negative_inverse_unit_resultleftright dst_value_inverse_unit_resultleftright. ((((exists ff_h_pvs_inverse_unit_resultleftrightentrypositive. ff_h_pvs_inverse_unit_resultleftrightentrypositive + S (dst_positive_inverse_unit_resultleftright) = S ((S (dst_index_inverse_unit_resultleftright)) * dst_positive_scale_inverse_unit_resultleftright)) /\ exists ff_q_pvs_inverse_unit_resultleftrightentrypositive. dst_positive_code_inverse_unit_resultleftright = ff_q_pvs_inverse_unit_resultleftrightentrypositive * S ((S (dst_index_inverse_unit_resultleftright)) * dst_positive_scale_inverse_unit_resultleftright) + (dst_positive_inverse_unit_resultleftright))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftrightentrynegative. ff_h_pvs_inverse_unit_resultleftrightentrynegative + S (dst_negative_inverse_unit_resultleftright) = S ((S (dst_index_inverse_unit_resultleftright)) * dst_negative_scale_inverse_unit_resultleftright)) /\ exists ff_q_pvs_inverse_unit_resultleftrightentrynegative. dst_negative_code_inverse_unit_resultleftright = ff_q_pvs_inverse_unit_resultleftrightentrynegative * S ((S (dst_index_inverse_unit_resultleftright)) * dst_negative_scale_inverse_unit_resultleftright) + (dst_negative_inverse_unit_resultleftright))) /\ (exists ge_balance_positive_inverse_unit_resultleftrightentryvalue ge_balance_negative_inverse_unit_resultleftrightentryvalue. (((((dst_value_inverse_unit_resultleftright) = 2 * (ge_balance_positive_inverse_unit_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_unit_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftrightentryvaluedecode. (((dst_value_inverse_unit_resultleftright) = 2 * ge_signed_half_inverse_unit_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftrightentryvalue) = S ge_signed_half_inverse_unit_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftright) + ge_balance_negative_inverse_unit_resultleftrightentryvalue = (dst_negative_inverse_unit_resultleftright) + ge_balance_positive_inverse_unit_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultlefttable dst_positive_scale_inverse_unit_resultlefttable dst_negative_code_inverse_unit_resultlefttable dst_negative_scale_inverse_unit_resultlefttable. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable)) * S ((dst_positive_code_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable)) + ((dst_positive_scale_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable))) + (((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) * S ((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) + ((dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)))) * S ((((dst_positive_code_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable)) * S ((dst_positive_code_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable)) + ((dst_positive_scale_inverse_unit_resultlefttable) + (dst_positive_scale_inverse_unit_resultlefttable))) + (((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) * S ((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) + ((dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)))) + ((((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) * S ((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) + ((dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable))) + (((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) * S ((dst_negative_code_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)) + ((dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_scale_inverse_unit_resultlefttable)))))) /\ (forall dst_index_inverse_unit_resultlefttable. (exists pvs_le_gap_inverse_unit_resultlefttabledomain. pvs_le_gap_inverse_unit_resultlefttabledomain + (dst_index_inverse_unit_resultlefttable) = (N)) -> exists dst_positive_inverse_unit_resultlefttable dst_negative_inverse_unit_resultlefttable dst_value_inverse_unit_resultlefttable. ((((exists ff_h_pvs_inverse_unit_resultlefttableentrypositive. ff_h_pvs_inverse_unit_resultlefttableentrypositive + S (dst_positive_inverse_unit_resultlefttable) = S ((S (dst_index_inverse_unit_resultlefttable)) * dst_positive_scale_inverse_unit_resultlefttable)) /\ exists ff_q_pvs_inverse_unit_resultlefttableentrypositive. dst_positive_code_inverse_unit_resultlefttable = ff_q_pvs_inverse_unit_resultlefttableentrypositive * S ((S (dst_index_inverse_unit_resultlefttable)) * dst_positive_scale_inverse_unit_resultlefttable) + (dst_positive_inverse_unit_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_unit_resultlefttableentrynegative. ff_h_pvs_inverse_unit_resultlefttableentrynegative + S (dst_negative_inverse_unit_resultlefttable) = S ((S (dst_index_inverse_unit_resultlefttable)) * dst_negative_scale_inverse_unit_resultlefttable)) /\ exists ff_q_pvs_inverse_unit_resultlefttableentrynegative. dst_negative_code_inverse_unit_resultlefttable = ff_q_pvs_inverse_unit_resultlefttableentrynegative * S ((S (dst_index_inverse_unit_resultlefttable)) * dst_negative_scale_inverse_unit_resultlefttable) + (dst_negative_inverse_unit_resultlefttable))) /\ (exists ge_balance_positive_inverse_unit_resultlefttableentryvalue ge_balance_negative_inverse_unit_resultlefttableentryvalue. (((((dst_value_inverse_unit_resultlefttable) = 2 * (ge_balance_positive_inverse_unit_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_unit_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultlefttableentryvaluedecode. (((dst_value_inverse_unit_resultlefttable) = 2 * ge_signed_half_inverse_unit_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultlefttableentryvalue) = S ge_signed_half_inverse_unit_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultlefttable) + ge_balance_negative_inverse_unit_resultlefttableentryvalue = (dst_negative_inverse_unit_resultlefttable) + ge_balance_positive_inverse_unit_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_unit_resultleft dc_output_inverse_unit_resultleft. ~(dc_input_inverse_unit_resultleft=0) -> (exists pvs_le_gap_inverse_unit_resultleftdomain. pvs_le_gap_inverse_unit_resultleftdomain + (dc_input_inverse_unit_resultleft) = (N)) -> (exists dst_positive_code_inverse_unit_resultleftlookup dst_positive_scale_inverse_unit_resultleftlookup dst_negative_code_inverse_unit_resultleftlookup dst_negative_scale_inverse_unit_resultleftlookup dst_positive_inverse_unit_resultleftlookup dst_negative_inverse_unit_resultleftlookup. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup)) * S ((dst_positive_code_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup)) + ((dst_positive_scale_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup))) + (((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) * S ((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) + ((dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)))) * S ((((dst_positive_code_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup)) * S ((dst_positive_code_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup)) + ((dst_positive_scale_inverse_unit_resultleftlookup) + (dst_positive_scale_inverse_unit_resultleftlookup))) + (((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) * S ((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) + ((dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)))) + ((((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) * S ((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) + ((dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup))) + (((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) * S ((dst_negative_code_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)) + ((dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_scale_inverse_unit_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftlookuppositive. ff_h_pvs_inverse_unit_resultleftlookuppositive + S (dst_positive_inverse_unit_resultleftlookup) = S ((S (dc_input_inverse_unit_resultleft)) * dst_positive_scale_inverse_unit_resultleftlookup)) /\ exists ff_q_pvs_inverse_unit_resultleftlookuppositive. dst_positive_code_inverse_unit_resultleftlookup = ff_q_pvs_inverse_unit_resultleftlookuppositive * S ((S (dc_input_inverse_unit_resultleft)) * dst_positive_scale_inverse_unit_resultleftlookup) + (dst_positive_inverse_unit_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftlookupnegative. ff_h_pvs_inverse_unit_resultleftlookupnegative + S (dst_negative_inverse_unit_resultleftlookup) = S ((S (dc_input_inverse_unit_resultleft)) * dst_negative_scale_inverse_unit_resultleftlookup)) /\ exists ff_q_pvs_inverse_unit_resultleftlookupnegative. dst_negative_code_inverse_unit_resultleftlookup = ff_q_pvs_inverse_unit_resultleftlookupnegative * S ((S (dc_input_inverse_unit_resultleft)) * dst_negative_scale_inverse_unit_resultleftlookup) + (dst_negative_inverse_unit_resultleftlookup))) /\ (exists ge_balance_positive_inverse_unit_resultleftlookupvalue ge_balance_negative_inverse_unit_resultleftlookupvalue. (((((dc_output_inverse_unit_resultleft) = 2 * (ge_balance_positive_inverse_unit_resultleftlookupvalue) /\ (ge_balance_negative_inverse_unit_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftlookupvaluedecode. (((dc_output_inverse_unit_resultleft) = 2 * ge_signed_half_inverse_unit_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftlookupvalue) = S ge_signed_half_inverse_unit_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftlookup) + ge_balance_negative_inverse_unit_resultleftlookupvalue = (dst_negative_inverse_unit_resultleftlookup) + ge_balance_positive_inverse_unit_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_unit_resultleft)=0)) /\ (exists dc_mask_inverse_unit_resultleftvalue. ((((exists dst_positive_code_inverse_unit_resultleftvaluemasktable dst_positive_scale_inverse_unit_resultleftvaluemasktable dst_negative_code_inverse_unit_resultleftvaluemasktable dst_negative_scale_inverse_unit_resultleftvaluemasktable. (((dc_mask_inverse_unit_resultleftvalue) = (((((dst_positive_code_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable))) + (((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_unit_resultleftvaluemasktable) + (dst_positive_scale_inverse_unit_resultleftvaluemasktable))) + (((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable))) + (((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_scale_inverse_unit_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_unit_resultleftvaluemasktable. (exists pvs_le_gap_inverse_unit_resultleftvaluemasktabledomain. pvs_le_gap_inverse_unit_resultleftvaluemasktabledomain + (dst_index_inverse_unit_resultleftvaluemasktable) = (dc_input_inverse_unit_resultleft)) -> exists dst_positive_inverse_unit_resultleftvaluemasktable dst_negative_inverse_unit_resultleftvaluemasktable dst_value_inverse_unit_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_unit_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_unit_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_unit_resultleftvaluemasktable) = S ((S (dst_index_inverse_unit_resultleftvaluemasktable)) * dst_positive_scale_inverse_unit_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_unit_resultleftvaluemasktable = ff_q_pvs_inverse_unit_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_unit_resultleftvaluemasktable)) * dst_positive_scale_inverse_unit_resultleftvaluemasktable) + (dst_positive_inverse_unit_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_unit_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_unit_resultleftvaluemasktable) = S ((S (dst_index_inverse_unit_resultleftvaluemasktable)) * dst_negative_scale_inverse_unit_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_unit_resultleftvaluemasktable = ff_q_pvs_inverse_unit_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_unit_resultleftvaluemasktable)) * dst_negative_scale_inverse_unit_resultleftvaluemasktable) + (dst_negative_inverse_unit_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_unit_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_unit_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_unit_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_unit_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_unit_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_unit_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftvaluemasktable) + ge_balance_negative_inverse_unit_resultleftvaluemasktableentryvalue = (dst_negative_inverse_unit_resultleftvaluemasktable) + ge_balance_positive_inverse_unit_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_unit_resultleftvaluemask dc_value_inverse_unit_resultleftvaluemask. (exists pvs_le_gap_inverse_unit_resultleftvaluemaskdomain. pvs_le_gap_inverse_unit_resultleftvaluemaskdomain + (dc_index_inverse_unit_resultleftvaluemask) = (dc_input_inverse_unit_resultleft)) -> (exists dst_positive_code_inverse_unit_resultleftvaluemasklookup dst_positive_scale_inverse_unit_resultleftvaluemasklookup dst_negative_code_inverse_unit_resultleftvaluemasklookup dst_negative_scale_inverse_unit_resultleftvaluemasklookup dst_positive_inverse_unit_resultleftvaluemasklookup dst_negative_inverse_unit_resultleftvaluemasklookup. (((dc_mask_inverse_unit_resultleftvalue) = (((((dst_positive_code_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_unit_resultleftvaluemasklookup) + (dst_positive_scale_inverse_unit_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_scale_inverse_unit_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_unit_resultleftvaluemasklookuppositive + S (dst_positive_inverse_unit_resultleftvaluemasklookup) = S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_positive_scale_inverse_unit_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemasklookuppositive. dst_positive_code_inverse_unit_resultleftvaluemasklookup = ff_q_pvs_inverse_unit_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_positive_scale_inverse_unit_resultleftvaluemasklookup) + (dst_positive_inverse_unit_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_unit_resultleftvaluemasklookupnegative + S (dst_negative_inverse_unit_resultleftvaluemasklookup) = S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_negative_scale_inverse_unit_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemasklookupnegative. dst_negative_code_inverse_unit_resultleftvaluemasklookup = ff_q_pvs_inverse_unit_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_negative_scale_inverse_unit_resultleftvaluemasklookup) + (dst_negative_inverse_unit_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluemasklookupvalue ge_balance_negative_inverse_unit_resultleftvaluemasklookupvalue. (((((dc_value_inverse_unit_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_unit_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_unit_resultleftvaluemask) = 2 * ge_signed_half_inverse_unit_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_unit_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftvaluemasklookup) + ge_balance_negative_inverse_unit_resultleftvaluemasklookupvalue = (dst_negative_inverse_unit_resultleftvaluemasklookup) + ge_balance_positive_inverse_unit_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_unit_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_unit_resultleftvaluemaskentry dc_left_inverse_unit_resultleftvaluemaskentry dc_right_inverse_unit_resultleftvaluemaskentry. (((dc_input_inverse_unit_resultleft)=(dc_index_inverse_unit_resultleftvaluemask)*dc_quotient_inverse_unit_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_unit_resultleftvaluemaskentryleft dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft dst_negative_code_inverse_unit_resultleftvaluemaskentryleft dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft dst_positive_inverse_unit_resultleftvaluemaskentryleft dst_negative_inverse_unit_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_unit_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_unit_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_unit_resultleftvaluemaskentryleft = ff_q_pvs_inverse_unit_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_positive_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_positive_inverse_unit_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_unit_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_unit_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_unit_resultleftvaluemaskentryleft = ff_q_pvs_inverse_unit_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_unit_resultleftvaluemask)) * dst_negative_scale_inverse_unit_resultleftvaluemaskentryleft) + (dst_negative_inverse_unit_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_unit_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_unit_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_unit_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_unit_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_unit_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_unit_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_unit_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultleftvaluemaskentryright dst_positive_scale_inverse_unit_resultleftvaluemaskentryright dst_negative_code_inverse_unit_resultleftvaluemaskentryright dst_negative_scale_inverse_unit_resultleftvaluemaskentryright dst_positive_inverse_unit_resultleftvaluemaskentryright dst_negative_inverse_unit_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_unit_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_unit_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_unit_resultleftvaluemaskentry)) * dst_positive_scale_inverse_unit_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_unit_resultleftvaluemaskentryright = ff_q_pvs_inverse_unit_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_unit_resultleftvaluemaskentry)) * dst_positive_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_positive_inverse_unit_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_unit_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_unit_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_unit_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_unit_resultleftvaluemaskentry)) * dst_negative_scale_inverse_unit_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_unit_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_unit_resultleftvaluemaskentryright = ff_q_pvs_inverse_unit_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_unit_resultleftvaluemaskentry)) * dst_negative_scale_inverse_unit_resultleftvaluemaskentryright) + (dst_negative_inverse_unit_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_unit_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_unit_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_unit_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_unit_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_unit_resultleftvaluemaskentryright) + ge_balance_negative_inverse_unit_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_unit_resultleftvaluemaskentryright) + ge_balance_positive_inverse_unit_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_unit_resultleftvaluemaskentryproduct sto_an_inverse_unit_resultleftvaluemaskentryproduct sto_bp_inverse_unit_resultleftvaluemaskentryproduct sto_bn_inverse_unit_resultleftvaluemaskentryproduct sto_cp_inverse_unit_resultleftvaluemaskentryproduct sto_cn_inverse_unit_resultleftvaluemaskentryproduct. (((((dc_left_inverse_unit_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_unit_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_unit_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryproductleft. (((dc_left_inverse_unit_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_unit_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_unit_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_unit_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_unit_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_unit_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryproductright. (((dc_right_inverse_unit_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_unit_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_unit_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_unit_resultleftvaluemask) = 2 * (sto_cp_inverse_unit_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_unit_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_unit_resultleftvaluemask) = 2 * ge_signed_half_inverse_unit_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_unit_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_unit_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_unit_resultleftvaluemaskentryproduct * sto_bp_inverse_unit_resultleftvaluemaskentryproduct + sto_an_inverse_unit_resultleftvaluemaskentryproduct * sto_bn_inverse_unit_resultleftvaluemaskentryproduct) + sto_cn_inverse_unit_resultleftvaluemaskentryproduct = (sto_ap_inverse_unit_resultleftvaluemaskentryproduct * sto_bn_inverse_unit_resultleftvaluemaskentryproduct + sto_an_inverse_unit_resultleftvaluemaskentryproduct * sto_bp_inverse_unit_resultleftvaluemaskentryproduct) + sto_cp_inverse_unit_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_unit_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_unit_resultleftvaluemaskentrynondivisor. (dc_input_inverse_unit_resultleft) = (dc_index_inverse_unit_resultleftvaluemask) * pvs_factor_inverse_unit_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_unit_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_unit_resultleftvaluefold dst_positive_scale_inverse_unit_resultleftvaluefold dst_negative_code_inverse_unit_resultleftvaluefold dst_negative_scale_inverse_unit_resultleftvaluefold dst_positive_sum_inverse_unit_resultleftvaluefold dst_negative_sum_inverse_unit_resultleftvaluefold. (((dc_mask_inverse_unit_resultleftvalue) = (((((dst_positive_code_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold)) * S ((dst_positive_code_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold)) + ((dst_positive_scale_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold))) + (((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) * S ((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) + ((dst_negative_scale_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold)) * S ((dst_positive_code_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold)) + ((dst_positive_scale_inverse_unit_resultleftvaluefold) + (dst_positive_scale_inverse_unit_resultleftvaluefold))) + (((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) * S ((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) + ((dst_negative_scale_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)))) + ((((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) * S ((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) + ((dst_negative_scale_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold))) + (((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) * S ((dst_negative_code_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)) + ((dst_negative_scale_inverse_unit_resultleftvaluefold) + (dst_negative_scale_inverse_unit_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_unit_resultleftvaluefoldpositive fs_v_dst_inverse_unit_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_unit_resultleftvaluefoldpositive = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_unit_resultleftvaluefold) = S ((S (S (dc_input_inverse_unit_resultleft))) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_unit_resultleftvaluefoldpositive = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_unit_resultleft))) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_unit_resultleftvaluefold))) /\ forall fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_unit_resultleft)) -> exists fs_a_dst_inverse_unit_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_unit_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_unit_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_unit_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_unit_resultleftvaluefold)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_unit_resultleftvaluefold = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_unit_resultleftvaluefold) + (fs_a_dst_inverse_unit_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_unit_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_unit_resultleftvaluefoldpositive = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive) + (fs_r_dst_inverse_unit_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_unit_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_unit_resultleftvaluefoldpositive = fs_q_dst_inverse_unit_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldpositive) + (fs_s_dst_inverse_unit_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_unit_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_unit_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_unit_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_unit_resultleftvaluefoldnegative fs_v_dst_inverse_unit_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_unit_resultleftvaluefoldnegative = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_unit_resultleftvaluefold) = S ((S (S (dc_input_inverse_unit_resultleft))) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_unit_resultleftvaluefoldnegative = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_unit_resultleft))) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_unit_resultleftvaluefold))) /\ forall fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_unit_resultleft)) -> exists fs_a_dst_inverse_unit_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_unit_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_unit_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_unit_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_unit_resultleftvaluefold)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_unit_resultleftvaluefold = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_unit_resultleftvaluefold) + (fs_a_dst_inverse_unit_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_unit_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_unit_resultleftvaluefoldnegative = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative) + (fs_r_dst_inverse_unit_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_unit_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_unit_resultleftvaluefoldnegative = fs_q_dst_inverse_unit_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultleftvaluefoldnegative) + (fs_s_dst_inverse_unit_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_unit_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_unit_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_unit_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_unit_resultleftvaluefoldresult ge_balance_negative_inverse_unit_resultleftvaluefoldresult. (((((dc_output_inverse_unit_resultleft) = 2 * (ge_balance_positive_inverse_unit_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_unit_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_unit_resultleftvaluefoldresultdecode. (((dc_output_inverse_unit_resultleft) = 2 * ge_signed_half_inverse_unit_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_unit_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_unit_resultleftvaluefoldresult) = S ge_signed_half_inverse_unit_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_unit_resultleftvaluefold) + ge_balance_negative_inverse_unit_resultleftvaluefoldresult = (dst_negative_sum_inverse_unit_resultleftvaluefold) + ge_balance_positive_inverse_unit_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_unit_resultrightleft dst_positive_scale_inverse_unit_resultrightleft dst_negative_code_inverse_unit_resultrightleft dst_negative_scale_inverse_unit_resultrightleft. (((G) = (((((dst_positive_code_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft)) * S ((dst_positive_code_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft)) + ((dst_positive_scale_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft))) + (((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) * S ((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) + ((dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)))) * S ((((dst_positive_code_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft)) * S ((dst_positive_code_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft)) + ((dst_positive_scale_inverse_unit_resultrightleft) + (dst_positive_scale_inverse_unit_resultrightleft))) + (((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) * S ((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) + ((dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)))) + ((((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) * S ((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) + ((dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft))) + (((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) * S ((dst_negative_code_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)) + ((dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_scale_inverse_unit_resultrightleft)))))) /\ (forall dst_index_inverse_unit_resultrightleft. (exists pvs_le_gap_inverse_unit_resultrightleftdomain. pvs_le_gap_inverse_unit_resultrightleftdomain + (dst_index_inverse_unit_resultrightleft) = (N)) -> exists dst_positive_inverse_unit_resultrightleft dst_negative_inverse_unit_resultrightleft dst_value_inverse_unit_resultrightleft. ((((exists ff_h_pvs_inverse_unit_resultrightleftentrypositive. ff_h_pvs_inverse_unit_resultrightleftentrypositive + S (dst_positive_inverse_unit_resultrightleft) = S ((S (dst_index_inverse_unit_resultrightleft)) * dst_positive_scale_inverse_unit_resultrightleft)) /\ exists ff_q_pvs_inverse_unit_resultrightleftentrypositive. dst_positive_code_inverse_unit_resultrightleft = ff_q_pvs_inverse_unit_resultrightleftentrypositive * S ((S (dst_index_inverse_unit_resultrightleft)) * dst_positive_scale_inverse_unit_resultrightleft) + (dst_positive_inverse_unit_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightleftentrynegative. ff_h_pvs_inverse_unit_resultrightleftentrynegative + S (dst_negative_inverse_unit_resultrightleft) = S ((S (dst_index_inverse_unit_resultrightleft)) * dst_negative_scale_inverse_unit_resultrightleft)) /\ exists ff_q_pvs_inverse_unit_resultrightleftentrynegative. dst_negative_code_inverse_unit_resultrightleft = ff_q_pvs_inverse_unit_resultrightleftentrynegative * S ((S (dst_index_inverse_unit_resultrightleft)) * dst_negative_scale_inverse_unit_resultrightleft) + (dst_negative_inverse_unit_resultrightleft))) /\ (exists ge_balance_positive_inverse_unit_resultrightleftentryvalue ge_balance_negative_inverse_unit_resultrightleftentryvalue. (((((dst_value_inverse_unit_resultrightleft) = 2 * (ge_balance_positive_inverse_unit_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_unit_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightleftentryvaluedecode. (((dst_value_inverse_unit_resultrightleft) = 2 * ge_signed_half_inverse_unit_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightleftentryvalue) = S ge_signed_half_inverse_unit_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightleft) + ge_balance_negative_inverse_unit_resultrightleftentryvalue = (dst_negative_inverse_unit_resultrightleft) + ge_balance_positive_inverse_unit_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultrightright dst_positive_scale_inverse_unit_resultrightright dst_negative_code_inverse_unit_resultrightright dst_negative_scale_inverse_unit_resultrightright. (((F) = (((((dst_positive_code_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright)) * S ((dst_positive_code_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright)) + ((dst_positive_scale_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright))) + (((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) * S ((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) + ((dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)))) * S ((((dst_positive_code_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright)) * S ((dst_positive_code_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright)) + ((dst_positive_scale_inverse_unit_resultrightright) + (dst_positive_scale_inverse_unit_resultrightright))) + (((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) * S ((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) + ((dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)))) + ((((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) * S ((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) + ((dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright))) + (((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) * S ((dst_negative_code_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)) + ((dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_scale_inverse_unit_resultrightright)))))) /\ (forall dst_index_inverse_unit_resultrightright. (exists pvs_le_gap_inverse_unit_resultrightrightdomain. pvs_le_gap_inverse_unit_resultrightrightdomain + (dst_index_inverse_unit_resultrightright) = (N)) -> exists dst_positive_inverse_unit_resultrightright dst_negative_inverse_unit_resultrightright dst_value_inverse_unit_resultrightright. ((((exists ff_h_pvs_inverse_unit_resultrightrightentrypositive. ff_h_pvs_inverse_unit_resultrightrightentrypositive + S (dst_positive_inverse_unit_resultrightright) = S ((S (dst_index_inverse_unit_resultrightright)) * dst_positive_scale_inverse_unit_resultrightright)) /\ exists ff_q_pvs_inverse_unit_resultrightrightentrypositive. dst_positive_code_inverse_unit_resultrightright = ff_q_pvs_inverse_unit_resultrightrightentrypositive * S ((S (dst_index_inverse_unit_resultrightright)) * dst_positive_scale_inverse_unit_resultrightright) + (dst_positive_inverse_unit_resultrightright))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightrightentrynegative. ff_h_pvs_inverse_unit_resultrightrightentrynegative + S (dst_negative_inverse_unit_resultrightright) = S ((S (dst_index_inverse_unit_resultrightright)) * dst_negative_scale_inverse_unit_resultrightright)) /\ exists ff_q_pvs_inverse_unit_resultrightrightentrynegative. dst_negative_code_inverse_unit_resultrightright = ff_q_pvs_inverse_unit_resultrightrightentrynegative * S ((S (dst_index_inverse_unit_resultrightright)) * dst_negative_scale_inverse_unit_resultrightright) + (dst_negative_inverse_unit_resultrightright))) /\ (exists ge_balance_positive_inverse_unit_resultrightrightentryvalue ge_balance_negative_inverse_unit_resultrightrightentryvalue. (((((dst_value_inverse_unit_resultrightright) = 2 * (ge_balance_positive_inverse_unit_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_unit_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightrightentryvaluedecode. (((dst_value_inverse_unit_resultrightright) = 2 * ge_signed_half_inverse_unit_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightrightentryvalue) = S ge_signed_half_inverse_unit_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightright) + ge_balance_negative_inverse_unit_resultrightrightentryvalue = (dst_negative_inverse_unit_resultrightright) + ge_balance_positive_inverse_unit_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultrighttable dst_positive_scale_inverse_unit_resultrighttable dst_negative_code_inverse_unit_resultrighttable dst_negative_scale_inverse_unit_resultrighttable. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable)) * S ((dst_positive_code_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable)) + ((dst_positive_scale_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable))) + (((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) * S ((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) + ((dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)))) * S ((((dst_positive_code_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable)) * S ((dst_positive_code_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable)) + ((dst_positive_scale_inverse_unit_resultrighttable) + (dst_positive_scale_inverse_unit_resultrighttable))) + (((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) * S ((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) + ((dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)))) + ((((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) * S ((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) + ((dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable))) + (((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) * S ((dst_negative_code_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)) + ((dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_scale_inverse_unit_resultrighttable)))))) /\ (forall dst_index_inverse_unit_resultrighttable. (exists pvs_le_gap_inverse_unit_resultrighttabledomain. pvs_le_gap_inverse_unit_resultrighttabledomain + (dst_index_inverse_unit_resultrighttable) = (N)) -> exists dst_positive_inverse_unit_resultrighttable dst_negative_inverse_unit_resultrighttable dst_value_inverse_unit_resultrighttable. ((((exists ff_h_pvs_inverse_unit_resultrighttableentrypositive. ff_h_pvs_inverse_unit_resultrighttableentrypositive + S (dst_positive_inverse_unit_resultrighttable) = S ((S (dst_index_inverse_unit_resultrighttable)) * dst_positive_scale_inverse_unit_resultrighttable)) /\ exists ff_q_pvs_inverse_unit_resultrighttableentrypositive. dst_positive_code_inverse_unit_resultrighttable = ff_q_pvs_inverse_unit_resultrighttableentrypositive * S ((S (dst_index_inverse_unit_resultrighttable)) * dst_positive_scale_inverse_unit_resultrighttable) + (dst_positive_inverse_unit_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_unit_resultrighttableentrynegative. ff_h_pvs_inverse_unit_resultrighttableentrynegative + S (dst_negative_inverse_unit_resultrighttable) = S ((S (dst_index_inverse_unit_resultrighttable)) * dst_negative_scale_inverse_unit_resultrighttable)) /\ exists ff_q_pvs_inverse_unit_resultrighttableentrynegative. dst_negative_code_inverse_unit_resultrighttable = ff_q_pvs_inverse_unit_resultrighttableentrynegative * S ((S (dst_index_inverse_unit_resultrighttable)) * dst_negative_scale_inverse_unit_resultrighttable) + (dst_negative_inverse_unit_resultrighttable))) /\ (exists ge_balance_positive_inverse_unit_resultrighttableentryvalue ge_balance_negative_inverse_unit_resultrighttableentryvalue. (((((dst_value_inverse_unit_resultrighttable) = 2 * (ge_balance_positive_inverse_unit_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_unit_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrighttableentryvaluedecode. (((dst_value_inverse_unit_resultrighttable) = 2 * ge_signed_half_inverse_unit_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrighttableentryvalue) = S ge_signed_half_inverse_unit_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultrighttable) + ge_balance_negative_inverse_unit_resultrighttableentryvalue = (dst_negative_inverse_unit_resultrighttable) + ge_balance_positive_inverse_unit_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_unit_resultright dc_output_inverse_unit_resultright. ~(dc_input_inverse_unit_resultright=0) -> (exists pvs_le_gap_inverse_unit_resultrightdomain. pvs_le_gap_inverse_unit_resultrightdomain + (dc_input_inverse_unit_resultright) = (N)) -> (exists dst_positive_code_inverse_unit_resultrightlookup dst_positive_scale_inverse_unit_resultrightlookup dst_negative_code_inverse_unit_resultrightlookup dst_negative_scale_inverse_unit_resultrightlookup dst_positive_inverse_unit_resultrightlookup dst_negative_inverse_unit_resultrightlookup. (((di_delta_inverse_unit_result) = (((((dst_positive_code_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup)) * S ((dst_positive_code_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup)) + ((dst_positive_scale_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup))) + (((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) * S ((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) + ((dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)))) * S ((((dst_positive_code_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup)) * S ((dst_positive_code_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup)) + ((dst_positive_scale_inverse_unit_resultrightlookup) + (dst_positive_scale_inverse_unit_resultrightlookup))) + (((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) * S ((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) + ((dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)))) + ((((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) * S ((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) + ((dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup))) + (((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) * S ((dst_negative_code_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)) + ((dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_scale_inverse_unit_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightlookuppositive. ff_h_pvs_inverse_unit_resultrightlookuppositive + S (dst_positive_inverse_unit_resultrightlookup) = S ((S (dc_input_inverse_unit_resultright)) * dst_positive_scale_inverse_unit_resultrightlookup)) /\ exists ff_q_pvs_inverse_unit_resultrightlookuppositive. dst_positive_code_inverse_unit_resultrightlookup = ff_q_pvs_inverse_unit_resultrightlookuppositive * S ((S (dc_input_inverse_unit_resultright)) * dst_positive_scale_inverse_unit_resultrightlookup) + (dst_positive_inverse_unit_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightlookupnegative. ff_h_pvs_inverse_unit_resultrightlookupnegative + S (dst_negative_inverse_unit_resultrightlookup) = S ((S (dc_input_inverse_unit_resultright)) * dst_negative_scale_inverse_unit_resultrightlookup)) /\ exists ff_q_pvs_inverse_unit_resultrightlookupnegative. dst_negative_code_inverse_unit_resultrightlookup = ff_q_pvs_inverse_unit_resultrightlookupnegative * S ((S (dc_input_inverse_unit_resultright)) * dst_negative_scale_inverse_unit_resultrightlookup) + (dst_negative_inverse_unit_resultrightlookup))) /\ (exists ge_balance_positive_inverse_unit_resultrightlookupvalue ge_balance_negative_inverse_unit_resultrightlookupvalue. (((((dc_output_inverse_unit_resultright) = 2 * (ge_balance_positive_inverse_unit_resultrightlookupvalue) /\ (ge_balance_negative_inverse_unit_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightlookupvaluedecode. (((dc_output_inverse_unit_resultright) = 2 * ge_signed_half_inverse_unit_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightlookupvalue) = S ge_signed_half_inverse_unit_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightlookup) + ge_balance_negative_inverse_unit_resultrightlookupvalue = (dst_negative_inverse_unit_resultrightlookup) + ge_balance_positive_inverse_unit_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_unit_resultright)=0)) /\ (exists dc_mask_inverse_unit_resultrightvalue. ((((exists dst_positive_code_inverse_unit_resultrightvaluemasktable dst_positive_scale_inverse_unit_resultrightvaluemasktable dst_negative_code_inverse_unit_resultrightvaluemasktable dst_negative_scale_inverse_unit_resultrightvaluemasktable. (((dc_mask_inverse_unit_resultrightvalue) = (((((dst_positive_code_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable))) + (((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_unit_resultrightvaluemasktable) + (dst_positive_scale_inverse_unit_resultrightvaluemasktable))) + (((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable))) + (((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_scale_inverse_unit_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_unit_resultrightvaluemasktable. (exists pvs_le_gap_inverse_unit_resultrightvaluemasktabledomain. pvs_le_gap_inverse_unit_resultrightvaluemasktabledomain + (dst_index_inverse_unit_resultrightvaluemasktable) = (dc_input_inverse_unit_resultright)) -> exists dst_positive_inverse_unit_resultrightvaluemasktable dst_negative_inverse_unit_resultrightvaluemasktable dst_value_inverse_unit_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_unit_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_unit_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_unit_resultrightvaluemasktable) = S ((S (dst_index_inverse_unit_resultrightvaluemasktable)) * dst_positive_scale_inverse_unit_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_unit_resultrightvaluemasktable = ff_q_pvs_inverse_unit_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_unit_resultrightvaluemasktable)) * dst_positive_scale_inverse_unit_resultrightvaluemasktable) + (dst_positive_inverse_unit_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_unit_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_unit_resultrightvaluemasktable) = S ((S (dst_index_inverse_unit_resultrightvaluemasktable)) * dst_negative_scale_inverse_unit_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_unit_resultrightvaluemasktable = ff_q_pvs_inverse_unit_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_unit_resultrightvaluemasktable)) * dst_negative_scale_inverse_unit_resultrightvaluemasktable) + (dst_negative_inverse_unit_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_unit_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_unit_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_unit_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_unit_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_unit_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_unit_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightvaluemasktable) + ge_balance_negative_inverse_unit_resultrightvaluemasktableentryvalue = (dst_negative_inverse_unit_resultrightvaluemasktable) + ge_balance_positive_inverse_unit_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_unit_resultrightvaluemask dc_value_inverse_unit_resultrightvaluemask. (exists pvs_le_gap_inverse_unit_resultrightvaluemaskdomain. pvs_le_gap_inverse_unit_resultrightvaluemaskdomain + (dc_index_inverse_unit_resultrightvaluemask) = (dc_input_inverse_unit_resultright)) -> (exists dst_positive_code_inverse_unit_resultrightvaluemasklookup dst_positive_scale_inverse_unit_resultrightvaluemasklookup dst_negative_code_inverse_unit_resultrightvaluemasklookup dst_negative_scale_inverse_unit_resultrightvaluemasklookup dst_positive_inverse_unit_resultrightvaluemasklookup dst_negative_inverse_unit_resultrightvaluemasklookup. (((dc_mask_inverse_unit_resultrightvalue) = (((((dst_positive_code_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_unit_resultrightvaluemasklookup) + (dst_positive_scale_inverse_unit_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_scale_inverse_unit_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_unit_resultrightvaluemasklookuppositive + S (dst_positive_inverse_unit_resultrightvaluemasklookup) = S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_positive_scale_inverse_unit_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemasklookuppositive. dst_positive_code_inverse_unit_resultrightvaluemasklookup = ff_q_pvs_inverse_unit_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_positive_scale_inverse_unit_resultrightvaluemasklookup) + (dst_positive_inverse_unit_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_unit_resultrightvaluemasklookupnegative + S (dst_negative_inverse_unit_resultrightvaluemasklookup) = S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_negative_scale_inverse_unit_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemasklookupnegative. dst_negative_code_inverse_unit_resultrightvaluemasklookup = ff_q_pvs_inverse_unit_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_negative_scale_inverse_unit_resultrightvaluemasklookup) + (dst_negative_inverse_unit_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluemasklookupvalue ge_balance_negative_inverse_unit_resultrightvaluemasklookupvalue. (((((dc_value_inverse_unit_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_unit_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_unit_resultrightvaluemask) = 2 * ge_signed_half_inverse_unit_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_unit_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightvaluemasklookup) + ge_balance_negative_inverse_unit_resultrightvaluemasklookupvalue = (dst_negative_inverse_unit_resultrightvaluemasklookup) + ge_balance_positive_inverse_unit_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_unit_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_unit_resultrightvaluemaskentry dc_left_inverse_unit_resultrightvaluemaskentry dc_right_inverse_unit_resultrightvaluemaskentry. (((dc_input_inverse_unit_resultright)=(dc_index_inverse_unit_resultrightvaluemask)*dc_quotient_inverse_unit_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_unit_resultrightvaluemaskentryleft dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft dst_negative_code_inverse_unit_resultrightvaluemaskentryleft dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft dst_positive_inverse_unit_resultrightvaluemaskentryleft dst_negative_inverse_unit_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_unit_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_unit_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_unit_resultrightvaluemaskentryleft = ff_q_pvs_inverse_unit_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_positive_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_positive_inverse_unit_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_unit_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_unit_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_unit_resultrightvaluemaskentryleft = ff_q_pvs_inverse_unit_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_unit_resultrightvaluemask)) * dst_negative_scale_inverse_unit_resultrightvaluemaskentryleft) + (dst_negative_inverse_unit_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_unit_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_unit_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_unit_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_unit_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_unit_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_unit_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_unit_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_unit_resultrightvaluemaskentryright dst_positive_scale_inverse_unit_resultrightvaluemaskentryright dst_negative_code_inverse_unit_resultrightvaluemaskentryright dst_negative_scale_inverse_unit_resultrightvaluemaskentryright dst_positive_inverse_unit_resultrightvaluemaskentryright dst_negative_inverse_unit_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_unit_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_unit_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_unit_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_unit_resultrightvaluemaskentry)) * dst_positive_scale_inverse_unit_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_unit_resultrightvaluemaskentryright = ff_q_pvs_inverse_unit_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_unit_resultrightvaluemaskentry)) * dst_positive_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_positive_inverse_unit_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_unit_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_unit_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_unit_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_unit_resultrightvaluemaskentry)) * dst_negative_scale_inverse_unit_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_unit_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_unit_resultrightvaluemaskentryright = ff_q_pvs_inverse_unit_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_unit_resultrightvaluemaskentry)) * dst_negative_scale_inverse_unit_resultrightvaluemaskentryright) + (dst_negative_inverse_unit_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_unit_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_unit_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_unit_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_unit_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_unit_resultrightvaluemaskentryright) + ge_balance_negative_inverse_unit_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_unit_resultrightvaluemaskentryright) + ge_balance_positive_inverse_unit_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_unit_resultrightvaluemaskentryproduct sto_an_inverse_unit_resultrightvaluemaskentryproduct sto_bp_inverse_unit_resultrightvaluemaskentryproduct sto_bn_inverse_unit_resultrightvaluemaskentryproduct sto_cp_inverse_unit_resultrightvaluemaskentryproduct sto_cn_inverse_unit_resultrightvaluemaskentryproduct. (((((dc_left_inverse_unit_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_unit_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_unit_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryproductleft. (((dc_left_inverse_unit_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_unit_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_unit_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_unit_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_unit_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_unit_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryproductright. (((dc_right_inverse_unit_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_unit_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_unit_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_unit_resultrightvaluemask) = 2 * (sto_cp_inverse_unit_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_unit_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_unit_resultrightvaluemask) = 2 * ge_signed_half_inverse_unit_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_unit_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_unit_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_unit_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_unit_resultrightvaluemaskentryproduct * sto_bp_inverse_unit_resultrightvaluemaskentryproduct + sto_an_inverse_unit_resultrightvaluemaskentryproduct * sto_bn_inverse_unit_resultrightvaluemaskentryproduct) + sto_cn_inverse_unit_resultrightvaluemaskentryproduct = (sto_ap_inverse_unit_resultrightvaluemaskentryproduct * sto_bn_inverse_unit_resultrightvaluemaskentryproduct + sto_an_inverse_unit_resultrightvaluemaskentryproduct * sto_bp_inverse_unit_resultrightvaluemaskentryproduct) + sto_cp_inverse_unit_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_unit_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_unit_resultrightvaluemaskentrynondivisor. (dc_input_inverse_unit_resultright) = (dc_index_inverse_unit_resultrightvaluemask) * pvs_factor_inverse_unit_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_unit_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_unit_resultrightvaluefold dst_positive_scale_inverse_unit_resultrightvaluefold dst_negative_code_inverse_unit_resultrightvaluefold dst_negative_scale_inverse_unit_resultrightvaluefold dst_positive_sum_inverse_unit_resultrightvaluefold dst_negative_sum_inverse_unit_resultrightvaluefold. (((dc_mask_inverse_unit_resultrightvalue) = (((((dst_positive_code_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold)) * S ((dst_positive_code_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold)) + ((dst_positive_scale_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold))) + (((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) * S ((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) + ((dst_negative_scale_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold)) * S ((dst_positive_code_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold)) + ((dst_positive_scale_inverse_unit_resultrightvaluefold) + (dst_positive_scale_inverse_unit_resultrightvaluefold))) + (((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) * S ((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) + ((dst_negative_scale_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)))) + ((((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) * S ((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) + ((dst_negative_scale_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold))) + (((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) * S ((dst_negative_code_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)) + ((dst_negative_scale_inverse_unit_resultrightvaluefold) + (dst_negative_scale_inverse_unit_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_unit_resultrightvaluefoldpositive fs_v_dst_inverse_unit_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_unit_resultrightvaluefoldpositive = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_unit_resultrightvaluefold) = S ((S (S (dc_input_inverse_unit_resultright))) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_unit_resultrightvaluefoldpositive = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_unit_resultright))) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_unit_resultrightvaluefold))) /\ forall fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_unit_resultright)) -> exists fs_a_dst_inverse_unit_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_unit_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_unit_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_unit_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_unit_resultrightvaluefold)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_unit_resultrightvaluefold = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_unit_resultrightvaluefold) + (fs_a_dst_inverse_unit_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_unit_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_unit_resultrightvaluefoldpositive = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive) + (fs_r_dst_inverse_unit_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_unit_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_unit_resultrightvaluefoldpositive = fs_q_dst_inverse_unit_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldpositive) + (fs_s_dst_inverse_unit_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_unit_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_unit_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_unit_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_unit_resultrightvaluefoldnegative fs_v_dst_inverse_unit_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_unit_resultrightvaluefoldnegative = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_unit_resultrightvaluefold) = S ((S (S (dc_input_inverse_unit_resultright))) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_unit_resultrightvaluefoldnegative = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_unit_resultright))) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_unit_resultrightvaluefold))) /\ forall fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_unit_resultright)) -> exists fs_a_dst_inverse_unit_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_unit_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_unit_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_unit_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_unit_resultrightvaluefold)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_unit_resultrightvaluefold = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_unit_resultrightvaluefold) + (fs_a_dst_inverse_unit_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_unit_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_unit_resultrightvaluefoldnegative = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative) + (fs_r_dst_inverse_unit_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_unit_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_unit_resultrightvaluefoldnegative = fs_q_dst_inverse_unit_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_unit_resultrightvaluefoldnegative) + (fs_s_dst_inverse_unit_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_unit_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_unit_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_unit_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_unit_resultrightvaluefoldresult ge_balance_negative_inverse_unit_resultrightvaluefoldresult. (((((dc_output_inverse_unit_resultright) = 2 * (ge_balance_positive_inverse_unit_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_unit_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_unit_resultrightvaluefoldresultdecode. (((dc_output_inverse_unit_resultright) = 2 * ge_signed_half_inverse_unit_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_unit_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_unit_resultrightvaluefoldresult) = S ge_signed_half_inverse_unit_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_unit_resultrightvaluefold) + ge_balance_negative_inverse_unit_resultrightvaluefoldresult = (dst_negative_sum_inverse_unit_resultrightvaluefold) + ge_balance_positive_inverse_unit_resultrightvaluefoldresult)))))))))))))))))))))))) /\ (exists dst_positive_code_inverse_unit_zero dst_positive_scale_inverse_unit_zero dst_negative_code_inverse_unit_zero dst_negative_scale_inverse_unit_zero dst_positive_inverse_unit_zero dst_negative_inverse_unit_zero. (((G) = (((((dst_positive_code_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero)) * S ((dst_positive_code_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero)) + ((dst_positive_scale_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero))) + (((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) * S ((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) + ((dst_negative_scale_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)))) * S ((((dst_positive_code_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero)) * S ((dst_positive_code_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero)) + ((dst_positive_scale_inverse_unit_zero) + (dst_positive_scale_inverse_unit_zero))) + (((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) * S ((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) + ((dst_negative_scale_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)))) + ((((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) * S ((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) + ((dst_negative_scale_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero))) + (((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) * S ((dst_negative_code_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)) + ((dst_negative_scale_inverse_unit_zero) + (dst_negative_scale_inverse_unit_zero)))))) /\ (((((exists ff_h_pvs_inverse_unit_zeropositive. ff_h_pvs_inverse_unit_zeropositive + S (dst_positive_inverse_unit_zero) = S ((S (0)) * dst_positive_scale_inverse_unit_zero)) /\ exists ff_q_pvs_inverse_unit_zeropositive. dst_positive_code_inverse_unit_zero = ff_q_pvs_inverse_unit_zeropositive * S ((S (0)) * dst_positive_scale_inverse_unit_zero) + (dst_positive_inverse_unit_zero))) /\ (((((exists ff_h_pvs_inverse_unit_zeronegative. ff_h_pvs_inverse_unit_zeronegative + S (dst_negative_inverse_unit_zero) = S ((S (0)) * dst_negative_scale_inverse_unit_zero)) /\ exists ff_q_pvs_inverse_unit_zeronegative. dst_negative_code_inverse_unit_zero = ff_q_pvs_inverse_unit_zeronegative * S ((S (0)) * dst_negative_scale_inverse_unit_zero) + (dst_negative_inverse_unit_zero))) /\ (exists ge_balance_positive_inverse_unit_zerovalue ge_balance_negative_inverse_unit_zerovalue. (((((w) = 2 * (ge_balance_positive_inverse_unit_zerovalue) /\ (ge_balance_negative_inverse_unit_zerovalue) = 0) \/ exists ge_signed_half_inverse_unit_zerovaluedecode. (((w) = 2 * ge_signed_half_inverse_unit_zerovaluedecode + 1 /\ (ge_balance_positive_inverse_unit_zerovalue) = 0) /\ (ge_balance_negative_inverse_unit_zerovalue) = S ge_signed_half_inverse_unit_zerovaluedecode))) /\ ((dst_positive_inverse_unit_zero) + ge_balance_negative_inverse_unit_zerovalue = (dst_negative_inverse_unit_zero) + ge_balance_positive_inverse_unit_zerovalue))))))))))Constructive proof overview
Generated structural guide
Construct an actual delta target and solve the genuine triangular convolution equation; both inverse laws and the independently prescribed zeroth value follow.
The unchanged tactic script uses 3 declared prerequisites and contains 37 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
dirichlet_kronecker_delta_table_exists Alpha theorem; checked-use authorized IV0009 dirichlet_unit_equation_construct IV0004 dirichlet_inverse_from_right_deltaDirect dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–7
02Establish hdL8–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet kronecker delta table exists.
03Separate the logical casesL12–14
04Establish hgL15–24
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply dirichlet unit equation construct.
- L15
have hg : ∃ G. DirichletTable(N,G,F,x) ∧ ArithAt(G,0,w)Definitions: ArithAtDirichletTable - L16
specialize dirichlet_unit_equation_construct (N) - L17
specialize dirichlet_unit_equation_construct (F) - L18
specialize dirichlet_unit_equation_construct (x) - L19
specialize dirichlet_unit_equation_construct (u) - L20
specialize dirichlet_unit_equation_construct (w) - L21
apply dirichlet_unit_equation_construct - L22
exact hF - L23
exact hd_witness_left_left - L24
exact hu
05Use earlier factsL25–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L25
exact hunit
06Separate the logical casesL26–27
07Construct an explicit witnessL28–28
Supply the displayed value, then prove that it has the required property.
- L28
exists x1
08Separate the logical casesL29–29
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L29
split
09Use earlier factsL30–37
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L30
specialize dirichlet_inverse_from_right_delta (N) - L31
specialize dirichlet_inverse_from_right_delta (F) - L32
specialize dirichlet_inverse_from_right_delta (x1) - L33
specialize dirichlet_inverse_from_right_delta (x) - L34
apply dirichlet_inverse_from_right_delta - L35
exact hd_witness_left - L36
exact hg_witness_left - L37
exact hg_witness_right
Original exact command ledger · 37 lines
- 0001
intro N - 0002
intro F - 0003
intro u - 0004
intro w - 0005
intro hF - 0006
intro hu - 0007
intro hunit - 0008
have hd : exists E. ((((exists dst_positive_code_construct_deltatable dst_positive_scale_construct_deltatable dst_negative_code_construct_deltatable dst_negative_scale_construct_deltatable. (((E) = (((((dst_positive_code_construct_deltatable) + (dst_positive_scale_construct_deltatable)) * S ((dst_positive_code_construct_deltatable) + (dst_positive_scale_construct_deltatable)) + ((dst_positive_scale_construct_deltatable) + (dst_positive_scale_construct_deltatable))) + (((dst_negative_code_construct_deltatable) + (dst_negative_scale_construct_deltatable)) * S ((dst_negative_code_construct_deltatable) + (dst_negative_scale_construct_deltatable)) + ((dst_negative_scale_construct_deltatable) + (dst_negative_scale_construct_deltatable)))) * S ((((dst_positive_code_construct_deltatable) + (dst_positive_scale_construct_deltatable)) * S ((dst_positive_code_construct_deltatable) + (dst_positive_scale_construct_deltatable)) + ((dst_positive_scale_construct_deltatable) + (dst_positive_scale_construct_deltatable))) + (((dst_negative_code_construct_deltatable) + (dst_negative_scale_construct_deltatable)) * S ((dst_negative_code_construct_deltatable) + (dst_negative_scale_construct_deltatable)) + ((dst_negative_scale_construct_deltatable) + (dst_negative_scale_construct_deltatable)))) + ((((dst_negative_code_construct_deltatable) + (dst_negative_scale_construct_deltatable)) * S ((dst_negative_code_construct_deltatable) + (dst_negative_scale_construct_deltatable)) + ((dst_negative_scale_construct_deltatable) + (dst_negative_scale_construct_deltatable))) + (((dst_negative_code_construct_deltatable) + (dst_negative_scale_construct_deltatable)) * S ((dst_negative_code_construct_deltatable) + (dst_negative_scale_construct_deltatable)) + ((dst_negative_scale_construct_deltatable) + (dst_negative_scale_construct_deltatable)))))) /\ (forall dst_index_construct_deltatable. (exists pvs_le_gap_construct_deltatabledomain. pvs_le_gap_construct_deltatabledomain + (dst_index_construct_deltatable) = (N)) -> exists dst_positive_construct_deltatable dst_negative_construct_deltatable dst_value_construct_deltatable. ((((exists ff_h_pvs_construct_deltatableentrypositive. ff_h_pvs_construct_deltatableentrypositive + S (dst_positive_construct_deltatable) = S ((S (dst_index_construct_deltatable)) * dst_positive_scale_construct_deltatable)) /\ exists ff_q_pvs_construct_deltatableentrypositive. dst_positive_code_construct_deltatable = ff_q_pvs_construct_deltatableentrypositive * S ((S (dst_index_construct_deltatable)) * dst_positive_scale_construct_deltatable) + (dst_positive_construct_deltatable))) /\ (((((exists ff_h_pvs_construct_deltatableentrynegative. ff_h_pvs_construct_deltatableentrynegative + S (dst_negative_construct_deltatable) = S ((S (dst_index_construct_deltatable)) * dst_negative_scale_construct_deltatable)) /\ exists ff_q_pvs_construct_deltatableentrynegative. dst_negative_code_construct_deltatable = ff_q_pvs_construct_deltatableentrynegative * S ((S (dst_index_construct_deltatable)) * dst_negative_scale_construct_deltatable) + (dst_negative_construct_deltatable))) /\ (exists ge_balance_positive_construct_deltatableentryvalue ge_balance_negative_construct_deltatableentryvalue. (((((dst_value_construct_deltatable) = 2 * (ge_balance_positive_construct_deltatableentryvalue) /\ (ge_balance_negative_construct_deltatableentryvalue) = 0) \/ exists ge_signed_half_construct_deltatableentryvaluedecode. (((dst_value_construct_deltatable) = 2 * ge_signed_half_construct_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_construct_deltatableentryvalue) = 0) /\ (ge_balance_negative_construct_deltatableentryvalue) = S ge_signed_half_construct_deltatableentryvaluedecode))) /\ ((dst_positive_construct_deltatable) + ge_balance_negative_construct_deltatableentryvalue = (dst_negative_construct_deltatable) + ge_balance_positive_construct_deltatableentryvalue))))))))) /\ (forall du_index_construct_delta du_value_construct_delta. ~(du_index_construct_delta=0) -> (exists pvs_le_gap_construct_deltabound. pvs_le_gap_construct_deltabound + (du_index_construct_delta) = (N)) -> (exists dst_positive_code_construct_deltaentry dst_positive_scale_construct_deltaentry dst_negative_code_construct_deltaentry dst_negative_scale_construct_deltaentry dst_positive_construct_deltaentry dst_negative_construct_deltaentry. (((E) = (((((dst_positive_code_construct_deltaentry) + (dst_positive_scale_construct_deltaentry)) * S ((dst_positive_code_construct_deltaentry) + (dst_positive_scale_construct_deltaentry)) + ((dst_positive_scale_construct_deltaentry) + (dst_positive_scale_construct_deltaentry))) + (((dst_negative_code_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)) * S ((dst_negative_code_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)) + ((dst_negative_scale_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)))) * S ((((dst_positive_code_construct_deltaentry) + (dst_positive_scale_construct_deltaentry)) * S ((dst_positive_code_construct_deltaentry) + (dst_positive_scale_construct_deltaentry)) + ((dst_positive_scale_construct_deltaentry) + (dst_positive_scale_construct_deltaentry))) + (((dst_negative_code_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)) * S ((dst_negative_code_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)) + ((dst_negative_scale_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)))) + ((((dst_negative_code_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)) * S ((dst_negative_code_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)) + ((dst_negative_scale_construct_deltaentry) + (dst_negative_scale_construct_deltaentry))) + (((dst_negative_code_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)) * S ((dst_negative_code_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)) + ((dst_negative_scale_construct_deltaentry) + (dst_negative_scale_construct_deltaentry)))))) /\ (((((exists ff_h_pvs_construct_deltaentrypositive. ff_h_pvs_construct_deltaentrypositive + S (dst_positive_construct_deltaentry) = S ((S (du_index_construct_delta)) * dst_positive_scale_construct_deltaentry)) /\ exists ff_q_pvs_construct_deltaentrypositive. dst_positive_code_construct_deltaentry = ff_q_pvs_construct_deltaentrypositive * S ((S (du_index_construct_delta)) * dst_positive_scale_construct_deltaentry) + (dst_positive_construct_deltaentry))) /\ (((((exists ff_h_pvs_construct_deltaentrynegative. ff_h_pvs_construct_deltaentrynegative + S (dst_negative_construct_deltaentry) = S ((S (du_index_construct_delta)) * dst_negative_scale_construct_deltaentry)) /\ exists ff_q_pvs_construct_deltaentrynegative. dst_negative_code_construct_deltaentry = ff_q_pvs_construct_deltaentrynegative * S ((S (du_index_construct_delta)) * dst_negative_scale_construct_deltaentry) + (dst_negative_construct_deltaentry))) /\ (exists ge_balance_positive_construct_deltaentryvalue ge_balance_negative_construct_deltaentryvalue. (((((du_value_construct_delta) = 2 * (ge_balance_positive_construct_deltaentryvalue) /\ (ge_balance_negative_construct_deltaentryvalue) = 0) \/ exists ge_signed_half_construct_deltaentryvaluedecode. (((du_value_construct_delta) = 2 * ge_signed_half_construct_deltaentryvaluedecode + 1 /\ (ge_balance_positive_construct_deltaentryvalue) = 0) /\ (ge_balance_negative_construct_deltaentryvalue) = S ge_signed_half_construct_deltaentryvaluedecode))) /\ ((dst_positive_construct_deltaentry) + ge_balance_negative_construct_deltaentryvalue = (dst_negative_construct_deltaentry) + ge_balance_positive_construct_deltaentryvalue))))))))) -> ((((du_index_construct_delta)=1 -> (du_value_construct_delta)=2) /\ (~((du_index_construct_delta)=1) -> (du_value_construct_delta)=0)))))) /\ (exists dst_positive_code_construct_delta_zero dst_positive_scale_construct_delta_zero dst_negative_code_construct_delta_zero dst_negative_scale_construct_delta_zero dst_positive_construct_delta_zero dst_negative_construct_delta_zero. (((E) = (((((dst_positive_code_construct_delta_zero) + (dst_positive_scale_construct_delta_zero)) * S ((dst_positive_code_construct_delta_zero) + (dst_positive_scale_construct_delta_zero)) + ((dst_positive_scale_construct_delta_zero) + (dst_positive_scale_construct_delta_zero))) + (((dst_negative_code_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)) * S ((dst_negative_code_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)) + ((dst_negative_scale_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)))) * S ((((dst_positive_code_construct_delta_zero) + (dst_positive_scale_construct_delta_zero)) * S ((dst_positive_code_construct_delta_zero) + (dst_positive_scale_construct_delta_zero)) + ((dst_positive_scale_construct_delta_zero) + (dst_positive_scale_construct_delta_zero))) + (((dst_negative_code_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)) * S ((dst_negative_code_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)) + ((dst_negative_scale_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)))) + ((((dst_negative_code_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)) * S ((dst_negative_code_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)) + ((dst_negative_scale_construct_delta_zero) + (dst_negative_scale_construct_delta_zero))) + (((dst_negative_code_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)) * S ((dst_negative_code_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)) + ((dst_negative_scale_construct_delta_zero) + (dst_negative_scale_construct_delta_zero)))))) /\ (((((exists ff_h_pvs_construct_delta_zeropositive. ff_h_pvs_construct_delta_zeropositive + S (dst_positive_construct_delta_zero) = S ((S (0)) * dst_positive_scale_construct_delta_zero)) /\ exists ff_q_pvs_construct_delta_zeropositive. dst_positive_code_construct_delta_zero = ff_q_pvs_construct_delta_zeropositive * S ((S (0)) * dst_positive_scale_construct_delta_zero) + (dst_positive_construct_delta_zero))) /\ (((((exists ff_h_pvs_construct_delta_zeronegative. ff_h_pvs_construct_delta_zeronegative + S (dst_negative_construct_delta_zero) = S ((S (0)) * dst_negative_scale_construct_delta_zero)) /\ exists ff_q_pvs_construct_delta_zeronegative. dst_negative_code_construct_delta_zero = ff_q_pvs_construct_delta_zeronegative * S ((S (0)) * dst_negative_scale_construct_delta_zero) + (dst_negative_construct_delta_zero))) /\ (exists ge_balance_positive_construct_delta_zerovalue ge_balance_negative_construct_delta_zerovalue. (((((0) = 2 * (ge_balance_positive_construct_delta_zerovalue) /\ (ge_balance_negative_construct_delta_zerovalue) = 0) \/ exists ge_signed_half_construct_delta_zerovaluedecode. (((0) = 2 * ge_signed_half_construct_delta_zerovaluedecode + 1 /\ (ge_balance_positive_construct_delta_zerovalue) = 0) /\ (ge_balance_negative_construct_delta_zerovalue) = S ge_signed_half_construct_delta_zerovaluedecode))) /\ ((dst_positive_construct_delta_zero) + ge_balance_negative_construct_delta_zerovalue = (dst_negative_construct_delta_zero) + ge_balance_positive_construct_delta_zerovalue)))))))))) - 0009
specialize dirichlet_kronecker_delta_table_exists (N) - 0010
specialize dirichlet_kronecker_delta_table_exists (0) - 0011
apply dirichlet_kronecker_delta_table_exists - 0012
cases hd - 0013
cases hd_witness - 0014
cases hd_witness_left - 0015
have hg : exists G. ((((exists dst_positive_code_construct_inverse_equationleft dst_positive_scale_construct_inverse_equationleft dst_negative_code_construct_inverse_equationleft dst_negative_scale_construct_inverse_equationleft. (((G) = (((((dst_positive_code_construct_inverse_equationleft) + (dst_positive_scale_construct_inverse_equationleft)) * S ((dst_positive_code_construct_inverse_equationleft) + (dst_positive_scale_construct_inverse_equationleft)) + ((dst_positive_scale_construct_inverse_equationleft) + (dst_positive_scale_construct_inverse_equationleft))) + (((dst_negative_code_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)) * S ((dst_negative_code_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)) + ((dst_negative_scale_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)))) * S ((((dst_positive_code_construct_inverse_equationleft) + (dst_positive_scale_construct_inverse_equationleft)) * S ((dst_positive_code_construct_inverse_equationleft) + (dst_positive_scale_construct_inverse_equationleft)) + ((dst_positive_scale_construct_inverse_equationleft) + (dst_positive_scale_construct_inverse_equationleft))) + (((dst_negative_code_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)) * S ((dst_negative_code_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)) + ((dst_negative_scale_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)))) + ((((dst_negative_code_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)) * S ((dst_negative_code_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)) + ((dst_negative_scale_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft))) + (((dst_negative_code_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)) * S ((dst_negative_code_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)) + ((dst_negative_scale_construct_inverse_equationleft) + (dst_negative_scale_construct_inverse_equationleft)))))) /\ (forall dst_index_construct_inverse_equationleft. (exists pvs_le_gap_construct_inverse_equationleftdomain. pvs_le_gap_construct_inverse_equationleftdomain + (dst_index_construct_inverse_equationleft) = (N)) -> exists dst_positive_construct_inverse_equationleft dst_negative_construct_inverse_equationleft dst_value_construct_inverse_equationleft. ((((exists ff_h_pvs_construct_inverse_equationleftentrypositive. ff_h_pvs_construct_inverse_equationleftentrypositive + S (dst_positive_construct_inverse_equationleft) = S ((S (dst_index_construct_inverse_equationleft)) * dst_positive_scale_construct_inverse_equationleft)) /\ exists ff_q_pvs_construct_inverse_equationleftentrypositive. dst_positive_code_construct_inverse_equationleft = ff_q_pvs_construct_inverse_equationleftentrypositive * S ((S (dst_index_construct_inverse_equationleft)) * dst_positive_scale_construct_inverse_equationleft) + (dst_positive_construct_inverse_equationleft))) /\ (((((exists ff_h_pvs_construct_inverse_equationleftentrynegative. ff_h_pvs_construct_inverse_equationleftentrynegative + S (dst_negative_construct_inverse_equationleft) = S ((S (dst_index_construct_inverse_equationleft)) * dst_negative_scale_construct_inverse_equationleft)) /\ exists ff_q_pvs_construct_inverse_equationleftentrynegative. dst_negative_code_construct_inverse_equationleft = ff_q_pvs_construct_inverse_equationleftentrynegative * S ((S (dst_index_construct_inverse_equationleft)) * dst_negative_scale_construct_inverse_equationleft) + (dst_negative_construct_inverse_equationleft))) /\ (exists ge_balance_positive_construct_inverse_equationleftentryvalue ge_balance_negative_construct_inverse_equationleftentryvalue. (((((dst_value_construct_inverse_equationleft) = 2 * (ge_balance_positive_construct_inverse_equationleftentryvalue) /\ (ge_balance_negative_construct_inverse_equationleftentryvalue) = 0) \/ exists ge_signed_half_construct_inverse_equationleftentryvaluedecode. (((dst_value_construct_inverse_equationleft) = 2 * ge_signed_half_construct_inverse_equationleftentryvaluedecode + 1 /\ (ge_balance_positive_construct_inverse_equationleftentryvalue) = 0) /\ (ge_balance_negative_construct_inverse_equationleftentryvalue) = S ge_signed_half_construct_inverse_equationleftentryvaluedecode))) /\ ((dst_positive_construct_inverse_equationleft) + ge_balance_negative_construct_inverse_equationleftentryvalue = (dst_negative_construct_inverse_equationleft) + ge_balance_positive_construct_inverse_equationleftentryvalue))))))))) /\ (((exists dst_positive_code_construct_inverse_equationright dst_positive_scale_construct_inverse_equationright dst_negative_code_construct_inverse_equationright dst_negative_scale_construct_inverse_equationright. (((F) = (((((dst_positive_code_construct_inverse_equationright) + (dst_positive_scale_construct_inverse_equationright)) * S ((dst_positive_code_construct_inverse_equationright) + (dst_positive_scale_construct_inverse_equationright)) + ((dst_positive_scale_construct_inverse_equationright) + (dst_positive_scale_construct_inverse_equationright))) + (((dst_negative_code_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)) * S ((dst_negative_code_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)) + ((dst_negative_scale_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)))) * S ((((dst_positive_code_construct_inverse_equationright) + (dst_positive_scale_construct_inverse_equationright)) * S ((dst_positive_code_construct_inverse_equationright) + (dst_positive_scale_construct_inverse_equationright)) + ((dst_positive_scale_construct_inverse_equationright) + (dst_positive_scale_construct_inverse_equationright))) + (((dst_negative_code_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)) * S ((dst_negative_code_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)) + ((dst_negative_scale_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)))) + ((((dst_negative_code_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)) * S ((dst_negative_code_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)) + ((dst_negative_scale_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright))) + (((dst_negative_code_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)) * S ((dst_negative_code_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)) + ((dst_negative_scale_construct_inverse_equationright) + (dst_negative_scale_construct_inverse_equationright)))))) /\ (forall dst_index_construct_inverse_equationright. (exists pvs_le_gap_construct_inverse_equationrightdomain. pvs_le_gap_construct_inverse_equationrightdomain + (dst_index_construct_inverse_equationright) = (N)) -> exists dst_positive_construct_inverse_equationright dst_negative_construct_inverse_equationright dst_value_construct_inverse_equationright. ((((exists ff_h_pvs_construct_inverse_equationrightentrypositive. ff_h_pvs_construct_inverse_equationrightentrypositive + S (dst_positive_construct_inverse_equationright) = S ((S (dst_index_construct_inverse_equationright)) * dst_positive_scale_construct_inverse_equationright)) /\ exists ff_q_pvs_construct_inverse_equationrightentrypositive. dst_positive_code_construct_inverse_equationright = ff_q_pvs_construct_inverse_equationrightentrypositive * S ((S (dst_index_construct_inverse_equationright)) * dst_positive_scale_construct_inverse_equationright) + (dst_positive_construct_inverse_equationright))) /\ (((((exists ff_h_pvs_construct_inverse_equationrightentrynegative. ff_h_pvs_construct_inverse_equationrightentrynegative + S (dst_negative_construct_inverse_equationright) = S ((S (dst_index_construct_inverse_equationright)) * dst_negative_scale_construct_inverse_equationright)) /\ exists ff_q_pvs_construct_inverse_equationrightentrynegative. dst_negative_code_construct_inverse_equationright = ff_q_pvs_construct_inverse_equationrightentrynegative * S ((S (dst_index_construct_inverse_equationright)) * dst_negative_scale_construct_inverse_equationright) + (dst_negative_construct_inverse_equationright))) /\ (exists ge_balance_positive_construct_inverse_equationrightentryvalue ge_balance_negative_construct_inverse_equationrightentryvalue. (((((dst_value_construct_inverse_equationright) = 2 * (ge_balance_positive_construct_inverse_equationrightentryvalue) /\ (ge_balance_negative_construct_inverse_equationrightentryvalue) = 0) \/ exists ge_signed_half_construct_inverse_equationrightentryvaluedecode. (((dst_value_construct_inverse_equationright) = 2 * ge_signed_half_construct_inverse_equationrightentryvaluedecode + 1 /\ (ge_balance_positive_construct_inverse_equationrightentryvalue) = 0) /\ (ge_balance_negative_construct_inverse_equationrightentryvalue) = S ge_signed_half_construct_inverse_equationrightentryvaluedecode))) /\ ((dst_positive_construct_inverse_equationright) + ge_balance_negative_construct_inverse_equationrightentryvalue = (dst_negative_construct_inverse_equationright) + ge_balance_positive_construct_inverse_equationrightentryvalue))))))))) /\ (((exists dst_positive_code_construct_inverse_equationtable dst_positive_scale_construct_inverse_equationtable dst_negative_code_construct_inverse_equationtable dst_negative_scale_construct_inverse_equationtable. (((x) = (((((dst_positive_code_construct_inverse_equationtable) + (dst_positive_scale_construct_inverse_equationtable)) * S ((dst_positive_code_construct_inverse_equationtable) + (dst_positive_scale_construct_inverse_equationtable)) + ((dst_positive_scale_construct_inverse_equationtable) + (dst_positive_scale_construct_inverse_equationtable))) + (((dst_negative_code_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)) * S ((dst_negative_code_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)) + ((dst_negative_scale_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)))) * S ((((dst_positive_code_construct_inverse_equationtable) + (dst_positive_scale_construct_inverse_equationtable)) * S ((dst_positive_code_construct_inverse_equationtable) + (dst_positive_scale_construct_inverse_equationtable)) + ((dst_positive_scale_construct_inverse_equationtable) + (dst_positive_scale_construct_inverse_equationtable))) + (((dst_negative_code_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)) * S ((dst_negative_code_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)) + ((dst_negative_scale_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)))) + ((((dst_negative_code_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)) * S ((dst_negative_code_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)) + ((dst_negative_scale_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable))) + (((dst_negative_code_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)) * S ((dst_negative_code_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)) + ((dst_negative_scale_construct_inverse_equationtable) + (dst_negative_scale_construct_inverse_equationtable)))))) /\ (forall dst_index_construct_inverse_equationtable. (exists pvs_le_gap_construct_inverse_equationtabledomain. pvs_le_gap_construct_inverse_equationtabledomain + (dst_index_construct_inverse_equationtable) = (N)) -> exists dst_positive_construct_inverse_equationtable dst_negative_construct_inverse_equationtable dst_value_construct_inverse_equationtable. ((((exists ff_h_pvs_construct_inverse_equationtableentrypositive. ff_h_pvs_construct_inverse_equationtableentrypositive + S (dst_positive_construct_inverse_equationtable) = S ((S (dst_index_construct_inverse_equationtable)) * dst_positive_scale_construct_inverse_equationtable)) /\ exists ff_q_pvs_construct_inverse_equationtableentrypositive. dst_positive_code_construct_inverse_equationtable = ff_q_pvs_construct_inverse_equationtableentrypositive * S ((S (dst_index_construct_inverse_equationtable)) * dst_positive_scale_construct_inverse_equationtable) + (dst_positive_construct_inverse_equationtable))) /\ (((((exists ff_h_pvs_construct_inverse_equationtableentrynegative. ff_h_pvs_construct_inverse_equationtableentrynegative + S (dst_negative_construct_inverse_equationtable) = S ((S (dst_index_construct_inverse_equationtable)) * dst_negative_scale_construct_inverse_equationtable)) /\ exists ff_q_pvs_construct_inverse_equationtableentrynegative. dst_negative_code_construct_inverse_equationtable = ff_q_pvs_construct_inverse_equationtableentrynegative * S ((S (dst_index_construct_inverse_equationtable)) * dst_negative_scale_construct_inverse_equationtable) + (dst_negative_construct_inverse_equationtable))) /\ (exists ge_balance_positive_construct_inverse_equationtableentryvalue ge_balance_negative_construct_inverse_equationtableentryvalue. (((((dst_value_construct_inverse_equationtable) = 2 * (ge_balance_positive_construct_inverse_equationtableentryvalue) /\ (ge_balance_negative_construct_inverse_equationtableentryvalue) = 0) \/ exists ge_signed_half_construct_inverse_equationtableentryvaluedecode. (((dst_value_construct_inverse_equationtable) = 2 * ge_signed_half_construct_inverse_equationtableentryvaluedecode + 1 /\ (ge_balance_positive_construct_inverse_equationtableentryvalue) = 0) /\ (ge_balance_negative_construct_inverse_equationtableentryvalue) = S ge_signed_half_construct_inverse_equationtableentryvaluedecode))) /\ ((dst_positive_construct_inverse_equationtable) + ge_balance_negative_construct_inverse_equationtableentryvalue = (dst_negative_construct_inverse_equationtable) + ge_balance_positive_construct_inverse_equationtableentryvalue))))))))) /\ (forall dc_input_construct_inverse_equation dc_output_construct_inverse_equation. ~(dc_input_construct_inverse_equation=0) -> (exists pvs_le_gap_construct_inverse_equationdomain. pvs_le_gap_construct_inverse_equationdomain + (dc_input_construct_inverse_equation) = (N)) -> (exists dst_positive_code_construct_inverse_equationlookup dst_positive_scale_construct_inverse_equationlookup dst_negative_code_construct_inverse_equationlookup dst_negative_scale_construct_inverse_equationlookup dst_positive_construct_inverse_equationlookup dst_negative_construct_inverse_equationlookup. (((x) = (((((dst_positive_code_construct_inverse_equationlookup) + (dst_positive_scale_construct_inverse_equationlookup)) * S ((dst_positive_code_construct_inverse_equationlookup) + (dst_positive_scale_construct_inverse_equationlookup)) + ((dst_positive_scale_construct_inverse_equationlookup) + (dst_positive_scale_construct_inverse_equationlookup))) + (((dst_negative_code_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)) * S ((dst_negative_code_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)) + ((dst_negative_scale_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)))) * S ((((dst_positive_code_construct_inverse_equationlookup) + (dst_positive_scale_construct_inverse_equationlookup)) * S ((dst_positive_code_construct_inverse_equationlookup) + (dst_positive_scale_construct_inverse_equationlookup)) + ((dst_positive_scale_construct_inverse_equationlookup) + (dst_positive_scale_construct_inverse_equationlookup))) + (((dst_negative_code_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)) * S ((dst_negative_code_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)) + ((dst_negative_scale_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)))) + ((((dst_negative_code_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)) * S ((dst_negative_code_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)) + ((dst_negative_scale_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup))) + (((dst_negative_code_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)) * S ((dst_negative_code_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)) + ((dst_negative_scale_construct_inverse_equationlookup) + (dst_negative_scale_construct_inverse_equationlookup)))))) /\ (((((exists ff_h_pvs_construct_inverse_equationlookuppositive. ff_h_pvs_construct_inverse_equationlookuppositive + S (dst_positive_construct_inverse_equationlookup) = S ((S (dc_input_construct_inverse_equation)) * dst_positive_scale_construct_inverse_equationlookup)) /\ exists ff_q_pvs_construct_inverse_equationlookuppositive. dst_positive_code_construct_inverse_equationlookup = ff_q_pvs_construct_inverse_equationlookuppositive * S ((S (dc_input_construct_inverse_equation)) * dst_positive_scale_construct_inverse_equationlookup) + (dst_positive_construct_inverse_equationlookup))) /\ (((((exists ff_h_pvs_construct_inverse_equationlookupnegative. ff_h_pvs_construct_inverse_equationlookupnegative + S (dst_negative_construct_inverse_equationlookup) = S ((S (dc_input_construct_inverse_equation)) * dst_negative_scale_construct_inverse_equationlookup)) /\ exists ff_q_pvs_construct_inverse_equationlookupnegative. dst_negative_code_construct_inverse_equationlookup = ff_q_pvs_construct_inverse_equationlookupnegative * S ((S (dc_input_construct_inverse_equation)) * dst_negative_scale_construct_inverse_equationlookup) + (dst_negative_construct_inverse_equationlookup))) /\ (exists ge_balance_positive_construct_inverse_equationlookupvalue ge_balance_negative_construct_inverse_equationlookupvalue. (((((dc_output_construct_inverse_equation) = 2 * (ge_balance_positive_construct_inverse_equationlookupvalue) /\ (ge_balance_negative_construct_inverse_equationlookupvalue) = 0) \/ exists ge_signed_half_construct_inverse_equationlookupvaluedecode. (((dc_output_construct_inverse_equation) = 2 * ge_signed_half_construct_inverse_equationlookupvaluedecode + 1 /\ (ge_balance_positive_construct_inverse_equationlookupvalue) = 0) /\ (ge_balance_negative_construct_inverse_equationlookupvalue) = S ge_signed_half_construct_inverse_equationlookupvaluedecode))) /\ ((dst_positive_construct_inverse_equationlookup) + ge_balance_negative_construct_inverse_equationlookupvalue = (dst_negative_construct_inverse_equationlookup) + ge_balance_positive_construct_inverse_equationlookupvalue))))))))) -> (((~((dc_input_construct_inverse_equation)=0)) /\ (exists dc_mask_construct_inverse_equationvalue. ((((exists dst_positive_code_construct_inverse_equationvaluemasktable dst_positive_scale_construct_inverse_equationvaluemasktable dst_negative_code_construct_inverse_equationvaluemasktable dst_negative_scale_construct_inverse_equationvaluemasktable. (((dc_mask_construct_inverse_equationvalue) = (((((dst_positive_code_construct_inverse_equationvaluemasktable) + (dst_positive_scale_construct_inverse_equationvaluemasktable)) * S ((dst_positive_code_construct_inverse_equationvaluemasktable) + (dst_positive_scale_construct_inverse_equationvaluemasktable)) + ((dst_positive_scale_construct_inverse_equationvaluemasktable) + (dst_positive_scale_construct_inverse_equationvaluemasktable))) + (((dst_negative_code_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)) * S ((dst_negative_code_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)) + ((dst_negative_scale_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)))) * S ((((dst_positive_code_construct_inverse_equationvaluemasktable) + (dst_positive_scale_construct_inverse_equationvaluemasktable)) * S ((dst_positive_code_construct_inverse_equationvaluemasktable) + (dst_positive_scale_construct_inverse_equationvaluemasktable)) + ((dst_positive_scale_construct_inverse_equationvaluemasktable) + (dst_positive_scale_construct_inverse_equationvaluemasktable))) + (((dst_negative_code_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)) * S ((dst_negative_code_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)) + ((dst_negative_scale_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)))) + ((((dst_negative_code_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)) * S ((dst_negative_code_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)) + ((dst_negative_scale_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable))) + (((dst_negative_code_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)) * S ((dst_negative_code_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)) + ((dst_negative_scale_construct_inverse_equationvaluemasktable) + (dst_negative_scale_construct_inverse_equationvaluemasktable)))))) /\ (forall dst_index_construct_inverse_equationvaluemasktable. (exists pvs_le_gap_construct_inverse_equationvaluemasktabledomain. pvs_le_gap_construct_inverse_equationvaluemasktabledomain + (dst_index_construct_inverse_equationvaluemasktable) = (dc_input_construct_inverse_equation)) -> exists dst_positive_construct_inverse_equationvaluemasktable dst_negative_construct_inverse_equationvaluemasktable dst_value_construct_inverse_equationvaluemasktable. ((((exists ff_h_pvs_construct_inverse_equationvaluemasktableentrypositive. ff_h_pvs_construct_inverse_equationvaluemasktableentrypositive + S (dst_positive_construct_inverse_equationvaluemasktable) = S ((S (dst_index_construct_inverse_equationvaluemasktable)) * dst_positive_scale_construct_inverse_equationvaluemasktable)) /\ exists ff_q_pvs_construct_inverse_equationvaluemasktableentrypositive. dst_positive_code_construct_inverse_equationvaluemasktable = ff_q_pvs_construct_inverse_equationvaluemasktableentrypositive * S ((S (dst_index_construct_inverse_equationvaluemasktable)) * dst_positive_scale_construct_inverse_equationvaluemasktable) + (dst_positive_construct_inverse_equationvaluemasktable))) /\ (((((exists ff_h_pvs_construct_inverse_equationvaluemasktableentrynegative. ff_h_pvs_construct_inverse_equationvaluemasktableentrynegative + S (dst_negative_construct_inverse_equationvaluemasktable) = S ((S (dst_index_construct_inverse_equationvaluemasktable)) * dst_negative_scale_construct_inverse_equationvaluemasktable)) /\ exists ff_q_pvs_construct_inverse_equationvaluemasktableentrynegative. dst_negative_code_construct_inverse_equationvaluemasktable = ff_q_pvs_construct_inverse_equationvaluemasktableentrynegative * S ((S (dst_index_construct_inverse_equationvaluemasktable)) * dst_negative_scale_construct_inverse_equationvaluemasktable) + (dst_negative_construct_inverse_equationvaluemasktable))) /\ (exists ge_balance_positive_construct_inverse_equationvaluemasktableentryvalue ge_balance_negative_construct_inverse_equationvaluemasktableentryvalue. (((((dst_value_construct_inverse_equationvaluemasktable) = 2 * (ge_balance_positive_construct_inverse_equationvaluemasktableentryvalue) /\ (ge_balance_negative_construct_inverse_equationvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_construct_inverse_equationvaluemasktableentryvaluedecode. (((dst_value_construct_inverse_equationvaluemasktable) = 2 * ge_signed_half_construct_inverse_equationvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_construct_inverse_equationvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_construct_inverse_equationvaluemasktableentryvalue) = S ge_signed_half_construct_inverse_equationvaluemasktableentryvaluedecode))) /\ ((dst_positive_construct_inverse_equationvaluemasktable) + ge_balance_negative_construct_inverse_equationvaluemasktableentryvalue = (dst_negative_construct_inverse_equationvaluemasktable) + ge_balance_positive_construct_inverse_equationvaluemasktableentryvalue))))))))) /\ (forall dc_index_construct_inverse_equationvaluemask dc_value_construct_inverse_equationvaluemask. (exists pvs_le_gap_construct_inverse_equationvaluemaskdomain. pvs_le_gap_construct_inverse_equationvaluemaskdomain + (dc_index_construct_inverse_equationvaluemask) = (dc_input_construct_inverse_equation)) -> (exists dst_positive_code_construct_inverse_equationvaluemasklookup dst_positive_scale_construct_inverse_equationvaluemasklookup dst_negative_code_construct_inverse_equationvaluemasklookup dst_negative_scale_construct_inverse_equationvaluemasklookup dst_positive_construct_inverse_equationvaluemasklookup dst_negative_construct_inverse_equationvaluemasklookup. (((dc_mask_construct_inverse_equationvalue) = (((((dst_positive_code_construct_inverse_equationvaluemasklookup) + (dst_positive_scale_construct_inverse_equationvaluemasklookup)) * S ((dst_positive_code_construct_inverse_equationvaluemasklookup) + (dst_positive_scale_construct_inverse_equationvaluemasklookup)) + ((dst_positive_scale_construct_inverse_equationvaluemasklookup) + (dst_positive_scale_construct_inverse_equationvaluemasklookup))) + (((dst_negative_code_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)) * S ((dst_negative_code_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)) + ((dst_negative_scale_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)))) * S ((((dst_positive_code_construct_inverse_equationvaluemasklookup) + (dst_positive_scale_construct_inverse_equationvaluemasklookup)) * S ((dst_positive_code_construct_inverse_equationvaluemasklookup) + (dst_positive_scale_construct_inverse_equationvaluemasklookup)) + ((dst_positive_scale_construct_inverse_equationvaluemasklookup) + (dst_positive_scale_construct_inverse_equationvaluemasklookup))) + (((dst_negative_code_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)) * S ((dst_negative_code_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)) + ((dst_negative_scale_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)))) + ((((dst_negative_code_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)) * S ((dst_negative_code_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)) + ((dst_negative_scale_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup))) + (((dst_negative_code_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)) * S ((dst_negative_code_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)) + ((dst_negative_scale_construct_inverse_equationvaluemasklookup) + (dst_negative_scale_construct_inverse_equationvaluemasklookup)))))) /\ (((((exists ff_h_pvs_construct_inverse_equationvaluemasklookuppositive. ff_h_pvs_construct_inverse_equationvaluemasklookuppositive + S (dst_positive_construct_inverse_equationvaluemasklookup) = S ((S (dc_index_construct_inverse_equationvaluemask)) * dst_positive_scale_construct_inverse_equationvaluemasklookup)) /\ exists ff_q_pvs_construct_inverse_equationvaluemasklookuppositive. dst_positive_code_construct_inverse_equationvaluemasklookup = ff_q_pvs_construct_inverse_equationvaluemasklookuppositive * S ((S (dc_index_construct_inverse_equationvaluemask)) * dst_positive_scale_construct_inverse_equationvaluemasklookup) + (dst_positive_construct_inverse_equationvaluemasklookup))) /\ (((((exists ff_h_pvs_construct_inverse_equationvaluemasklookupnegative. ff_h_pvs_construct_inverse_equationvaluemasklookupnegative + S (dst_negative_construct_inverse_equationvaluemasklookup) = S ((S (dc_index_construct_inverse_equationvaluemask)) * dst_negative_scale_construct_inverse_equationvaluemasklookup)) /\ exists ff_q_pvs_construct_inverse_equationvaluemasklookupnegative. dst_negative_code_construct_inverse_equationvaluemasklookup = ff_q_pvs_construct_inverse_equationvaluemasklookupnegative * S ((S (dc_index_construct_inverse_equationvaluemask)) * dst_negative_scale_construct_inverse_equationvaluemasklookup) + (dst_negative_construct_inverse_equationvaluemasklookup))) /\ (exists ge_balance_positive_construct_inverse_equationvaluemasklookupvalue ge_balance_negative_construct_inverse_equationvaluemasklookupvalue. (((((dc_value_construct_inverse_equationvaluemask) = 2 * (ge_balance_positive_construct_inverse_equationvaluemasklookupvalue) /\ (ge_balance_negative_construct_inverse_equationvaluemasklookupvalue) = 0) \/ exists ge_signed_half_construct_inverse_equationvaluemasklookupvaluedecode. (((dc_value_construct_inverse_equationvaluemask) = 2 * ge_signed_half_construct_inverse_equationvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_construct_inverse_equationvaluemasklookupvalue) = 0) /\ (ge_balance_negative_construct_inverse_equationvaluemasklookupvalue) = S ge_signed_half_construct_inverse_equationvaluemasklookupvaluedecode))) /\ ((dst_positive_construct_inverse_equationvaluemasklookup) + ge_balance_negative_construct_inverse_equationvaluemasklookupvalue = (dst_negative_construct_inverse_equationvaluemasklookup) + ge_balance_positive_construct_inverse_equationvaluemasklookupvalue))))))))) -> ((((~((dc_index_construct_inverse_equationvaluemask)=0)) /\ (exists dc_quotient_construct_inverse_equationvaluemaskentry dc_left_construct_inverse_equationvaluemaskentry dc_right_construct_inverse_equationvaluemaskentry. (((dc_input_construct_inverse_equation)=(dc_index_construct_inverse_equationvaluemask)*dc_quotient_construct_inverse_equationvaluemaskentry) /\ (((exists dst_positive_code_construct_inverse_equationvaluemaskentryleft dst_positive_scale_construct_inverse_equationvaluemaskentryleft dst_negative_code_construct_inverse_equationvaluemaskentryleft dst_negative_scale_construct_inverse_equationvaluemaskentryleft dst_positive_construct_inverse_equationvaluemaskentryleft dst_negative_construct_inverse_equationvaluemaskentryleft. (((G) = (((((dst_positive_code_construct_inverse_equationvaluemaskentryleft) + (dst_positive_scale_construct_inverse_equationvaluemaskentryleft)) * S ((dst_positive_code_construct_inverse_equationvaluemaskentryleft) + (dst_positive_scale_construct_inverse_equationvaluemaskentryleft)) + ((dst_positive_scale_construct_inverse_equationvaluemaskentryleft) + (dst_positive_scale_construct_inverse_equationvaluemaskentryleft))) + (((dst_negative_code_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) * S ((dst_negative_code_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) + ((dst_negative_scale_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)))) * S ((((dst_positive_code_construct_inverse_equationvaluemaskentryleft) + (dst_positive_scale_construct_inverse_equationvaluemaskentryleft)) * S ((dst_positive_code_construct_inverse_equationvaluemaskentryleft) + (dst_positive_scale_construct_inverse_equationvaluemaskentryleft)) + ((dst_positive_scale_construct_inverse_equationvaluemaskentryleft) + (dst_positive_scale_construct_inverse_equationvaluemaskentryleft))) + (((dst_negative_code_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) * S ((dst_negative_code_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) + ((dst_negative_scale_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)))) + ((((dst_negative_code_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) * S ((dst_negative_code_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) + ((dst_negative_scale_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft))) + (((dst_negative_code_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) * S ((dst_negative_code_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) + ((dst_negative_scale_construct_inverse_equationvaluemaskentryleft) + (dst_negative_scale_construct_inverse_equationvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_construct_inverse_equationvaluemaskentryleftpositive. ff_h_pvs_construct_inverse_equationvaluemaskentryleftpositive + S (dst_positive_construct_inverse_equationvaluemaskentryleft) = S ((S (dc_index_construct_inverse_equationvaluemask)) * dst_positive_scale_construct_inverse_equationvaluemaskentryleft)) /\ exists ff_q_pvs_construct_inverse_equationvaluemaskentryleftpositive. dst_positive_code_construct_inverse_equationvaluemaskentryleft = ff_q_pvs_construct_inverse_equationvaluemaskentryleftpositive * S ((S (dc_index_construct_inverse_equationvaluemask)) * dst_positive_scale_construct_inverse_equationvaluemaskentryleft) + (dst_positive_construct_inverse_equationvaluemaskentryleft))) /\ (((((exists ff_h_pvs_construct_inverse_equationvaluemaskentryleftnegative. ff_h_pvs_construct_inverse_equationvaluemaskentryleftnegative + S (dst_negative_construct_inverse_equationvaluemaskentryleft) = S ((S (dc_index_construct_inverse_equationvaluemask)) * dst_negative_scale_construct_inverse_equationvaluemaskentryleft)) /\ exists ff_q_pvs_construct_inverse_equationvaluemaskentryleftnegative. dst_negative_code_construct_inverse_equationvaluemaskentryleft = ff_q_pvs_construct_inverse_equationvaluemaskentryleftnegative * S ((S (dc_index_construct_inverse_equationvaluemask)) * dst_negative_scale_construct_inverse_equationvaluemaskentryleft) + (dst_negative_construct_inverse_equationvaluemaskentryleft))) /\ (exists ge_balance_positive_construct_inverse_equationvaluemaskentryleftvalue ge_balance_negative_construct_inverse_equationvaluemaskentryleftvalue. (((((dc_left_construct_inverse_equationvaluemaskentry) = 2 * (ge_balance_positive_construct_inverse_equationvaluemaskentryleftvalue) /\ (ge_balance_negative_construct_inverse_equationvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_construct_inverse_equationvaluemaskentryleftvaluedecode. (((dc_left_construct_inverse_equationvaluemaskentry) = 2 * ge_signed_half_construct_inverse_equationvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_construct_inverse_equationvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_construct_inverse_equationvaluemaskentryleftvalue) = S ge_signed_half_construct_inverse_equationvaluemaskentryleftvaluedecode))) /\ ((dst_positive_construct_inverse_equationvaluemaskentryleft) + ge_balance_negative_construct_inverse_equationvaluemaskentryleftvalue = (dst_negative_construct_inverse_equationvaluemaskentryleft) + ge_balance_positive_construct_inverse_equationvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_construct_inverse_equationvaluemaskentryright dst_positive_scale_construct_inverse_equationvaluemaskentryright dst_negative_code_construct_inverse_equationvaluemaskentryright dst_negative_scale_construct_inverse_equationvaluemaskentryright dst_positive_construct_inverse_equationvaluemaskentryright dst_negative_construct_inverse_equationvaluemaskentryright. (((F) = (((((dst_positive_code_construct_inverse_equationvaluemaskentryright) + (dst_positive_scale_construct_inverse_equationvaluemaskentryright)) * S ((dst_positive_code_construct_inverse_equationvaluemaskentryright) + (dst_positive_scale_construct_inverse_equationvaluemaskentryright)) + ((dst_positive_scale_construct_inverse_equationvaluemaskentryright) + (dst_positive_scale_construct_inverse_equationvaluemaskentryright))) + (((dst_negative_code_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)) * S ((dst_negative_code_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)) + ((dst_negative_scale_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)))) * S ((((dst_positive_code_construct_inverse_equationvaluemaskentryright) + (dst_positive_scale_construct_inverse_equationvaluemaskentryright)) * S ((dst_positive_code_construct_inverse_equationvaluemaskentryright) + (dst_positive_scale_construct_inverse_equationvaluemaskentryright)) + ((dst_positive_scale_construct_inverse_equationvaluemaskentryright) + (dst_positive_scale_construct_inverse_equationvaluemaskentryright))) + (((dst_negative_code_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)) * S ((dst_negative_code_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)) + ((dst_negative_scale_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)))) + ((((dst_negative_code_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)) * S ((dst_negative_code_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)) + ((dst_negative_scale_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright))) + (((dst_negative_code_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)) * S ((dst_negative_code_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)) + ((dst_negative_scale_construct_inverse_equationvaluemaskentryright) + (dst_negative_scale_construct_inverse_equationvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_construct_inverse_equationvaluemaskentryrightpositive. ff_h_pvs_construct_inverse_equationvaluemaskentryrightpositive + S (dst_positive_construct_inverse_equationvaluemaskentryright) = S ((S (dc_quotient_construct_inverse_equationvaluemaskentry)) * dst_positive_scale_construct_inverse_equationvaluemaskentryright)) /\ exists ff_q_pvs_construct_inverse_equationvaluemaskentryrightpositive. dst_positive_code_construct_inverse_equationvaluemaskentryright = ff_q_pvs_construct_inverse_equationvaluemaskentryrightpositive * S ((S (dc_quotient_construct_inverse_equationvaluemaskentry)) * dst_positive_scale_construct_inverse_equationvaluemaskentryright) + (dst_positive_construct_inverse_equationvaluemaskentryright))) /\ (((((exists ff_h_pvs_construct_inverse_equationvaluemaskentryrightnegative. ff_h_pvs_construct_inverse_equationvaluemaskentryrightnegative + S (dst_negative_construct_inverse_equationvaluemaskentryright) = S ((S (dc_quotient_construct_inverse_equationvaluemaskentry)) * dst_negative_scale_construct_inverse_equationvaluemaskentryright)) /\ exists ff_q_pvs_construct_inverse_equationvaluemaskentryrightnegative. dst_negative_code_construct_inverse_equationvaluemaskentryright = ff_q_pvs_construct_inverse_equationvaluemaskentryrightnegative * S ((S (dc_quotient_construct_inverse_equationvaluemaskentry)) * dst_negative_scale_construct_inverse_equationvaluemaskentryright) + (dst_negative_construct_inverse_equationvaluemaskentryright))) /\ (exists ge_balance_positive_construct_inverse_equationvaluemaskentryrightvalue ge_balance_negative_construct_inverse_equationvaluemaskentryrightvalue. (((((dc_right_construct_inverse_equationvaluemaskentry) = 2 * (ge_balance_positive_construct_inverse_equationvaluemaskentryrightvalue) /\ (ge_balance_negative_construct_inverse_equationvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_construct_inverse_equationvaluemaskentryrightvaluedecode. (((dc_right_construct_inverse_equationvaluemaskentry) = 2 * ge_signed_half_construct_inverse_equationvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_construct_inverse_equationvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_construct_inverse_equationvaluemaskentryrightvalue) = S ge_signed_half_construct_inverse_equationvaluemaskentryrightvaluedecode))) /\ ((dst_positive_construct_inverse_equationvaluemaskentryright) + ge_balance_negative_construct_inverse_equationvaluemaskentryrightvalue = (dst_negative_construct_inverse_equationvaluemaskentryright) + ge_balance_positive_construct_inverse_equationvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_construct_inverse_equationvaluemaskentryproduct sto_an_construct_inverse_equationvaluemaskentryproduct sto_bp_construct_inverse_equationvaluemaskentryproduct sto_bn_construct_inverse_equationvaluemaskentryproduct sto_cp_construct_inverse_equationvaluemaskentryproduct sto_cn_construct_inverse_equationvaluemaskentryproduct. (((((dc_left_construct_inverse_equationvaluemaskentry) = 2 * (sto_ap_construct_inverse_equationvaluemaskentryproduct) /\ (sto_an_construct_inverse_equationvaluemaskentryproduct) = 0) \/ exists ge_signed_half_construct_inverse_equationvaluemaskentryproductleft. (((dc_left_construct_inverse_equationvaluemaskentry) = 2 * ge_signed_half_construct_inverse_equationvaluemaskentryproductleft + 1 /\ (sto_ap_construct_inverse_equationvaluemaskentryproduct) = 0) /\ (sto_an_construct_inverse_equationvaluemaskentryproduct) = S ge_signed_half_construct_inverse_equationvaluemaskentryproductleft))) /\ ((((((dc_right_construct_inverse_equationvaluemaskentry) = 2 * (sto_bp_construct_inverse_equationvaluemaskentryproduct) /\ (sto_bn_construct_inverse_equationvaluemaskentryproduct) = 0) \/ exists ge_signed_half_construct_inverse_equationvaluemaskentryproductright. (((dc_right_construct_inverse_equationvaluemaskentry) = 2 * ge_signed_half_construct_inverse_equationvaluemaskentryproductright + 1 /\ (sto_bp_construct_inverse_equationvaluemaskentryproduct) = 0) /\ (sto_bn_construct_inverse_equationvaluemaskentryproduct) = S ge_signed_half_construct_inverse_equationvaluemaskentryproductright))) /\ ((((((dc_value_construct_inverse_equationvaluemask) = 2 * (sto_cp_construct_inverse_equationvaluemaskentryproduct) /\ (sto_cn_construct_inverse_equationvaluemaskentryproduct) = 0) \/ exists ge_signed_half_construct_inverse_equationvaluemaskentryproductoutput. (((dc_value_construct_inverse_equationvaluemask) = 2 * ge_signed_half_construct_inverse_equationvaluemaskentryproductoutput + 1 /\ (sto_cp_construct_inverse_equationvaluemaskentryproduct) = 0) /\ (sto_cn_construct_inverse_equationvaluemaskentryproduct) = S ge_signed_half_construct_inverse_equationvaluemaskentryproductoutput))) /\ ((sto_ap_construct_inverse_equationvaluemaskentryproduct * sto_bp_construct_inverse_equationvaluemaskentryproduct + sto_an_construct_inverse_equationvaluemaskentryproduct * sto_bn_construct_inverse_equationvaluemaskentryproduct) + sto_cn_construct_inverse_equationvaluemaskentryproduct = (sto_ap_construct_inverse_equationvaluemaskentryproduct * sto_bn_construct_inverse_equationvaluemaskentryproduct + sto_an_construct_inverse_equationvaluemaskentryproduct * sto_bp_construct_inverse_equationvaluemaskentryproduct) + sto_cp_construct_inverse_equationvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_construct_inverse_equationvaluemask)=0 \/ ~(exists pvs_factor_construct_inverse_equationvaluemaskentrynondivisor. (dc_input_construct_inverse_equation) = (dc_index_construct_inverse_equationvaluemask) * pvs_factor_construct_inverse_equationvaluemaskentrynondivisor)) /\ ((dc_value_construct_inverse_equationvaluemask)=0))))))) /\ (exists dst_positive_code_construct_inverse_equationvaluefold dst_positive_scale_construct_inverse_equationvaluefold dst_negative_code_construct_inverse_equationvaluefold dst_negative_scale_construct_inverse_equationvaluefold dst_positive_sum_construct_inverse_equationvaluefold dst_negative_sum_construct_inverse_equationvaluefold. (((dc_mask_construct_inverse_equationvalue) = (((((dst_positive_code_construct_inverse_equationvaluefold) + (dst_positive_scale_construct_inverse_equationvaluefold)) * S ((dst_positive_code_construct_inverse_equationvaluefold) + (dst_positive_scale_construct_inverse_equationvaluefold)) + ((dst_positive_scale_construct_inverse_equationvaluefold) + (dst_positive_scale_construct_inverse_equationvaluefold))) + (((dst_negative_code_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)) * S ((dst_negative_code_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)) + ((dst_negative_scale_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)))) * S ((((dst_positive_code_construct_inverse_equationvaluefold) + (dst_positive_scale_construct_inverse_equationvaluefold)) * S ((dst_positive_code_construct_inverse_equationvaluefold) + (dst_positive_scale_construct_inverse_equationvaluefold)) + ((dst_positive_scale_construct_inverse_equationvaluefold) + (dst_positive_scale_construct_inverse_equationvaluefold))) + (((dst_negative_code_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)) * S ((dst_negative_code_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)) + ((dst_negative_scale_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)))) + ((((dst_negative_code_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)) * S ((dst_negative_code_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)) + ((dst_negative_scale_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold))) + (((dst_negative_code_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)) * S ((dst_negative_code_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)) + ((dst_negative_scale_construct_inverse_equationvaluefold) + (dst_negative_scale_construct_inverse_equationvaluefold)))))) /\ (((exists fs_u_dst_construct_inverse_equationvaluefoldpositive fs_v_dst_construct_inverse_equationvaluefoldpositive. ((((exists fs_h_dst_construct_inverse_equationvaluefoldpositive_body_start. fs_h_dst_construct_inverse_equationvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_construct_inverse_equationvaluefoldpositive)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldpositive_body_start. fs_u_dst_construct_inverse_equationvaluefoldpositive = fs_q_dst_construct_inverse_equationvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_construct_inverse_equationvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_construct_inverse_equationvaluefoldpositive_body_terminal. fs_h_dst_construct_inverse_equationvaluefoldpositive_body_terminal + S (dst_positive_sum_construct_inverse_equationvaluefold) = S ((S (S (dc_input_construct_inverse_equation))) * fs_v_dst_construct_inverse_equationvaluefoldpositive)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldpositive_body_terminal. fs_u_dst_construct_inverse_equationvaluefoldpositive = fs_q_dst_construct_inverse_equationvaluefoldpositive_body_terminal * S ((S (S (dc_input_construct_inverse_equation))) * fs_v_dst_construct_inverse_equationvaluefoldpositive) + (dst_positive_sum_construct_inverse_equationvaluefold))) /\ forall fs_i_dst_construct_inverse_equationvaluefoldpositive_body_steps. (exists fs_lt_dst_construct_inverse_equationvaluefoldpositive_body_steps_bound. fs_lt_dst_construct_inverse_equationvaluefoldpositive_body_steps_bound + S fs_i_dst_construct_inverse_equationvaluefoldpositive_body_steps = S (dc_input_construct_inverse_equation)) -> exists fs_a_dst_construct_inverse_equationvaluefoldpositive_body_steps fs_r_dst_construct_inverse_equationvaluefoldpositive_body_steps fs_s_dst_construct_inverse_equationvaluefoldpositive_body_steps. ((((exists fs_h_dst_construct_inverse_equationvaluefoldpositive_body_steps_summand. fs_h_dst_construct_inverse_equationvaluefoldpositive_body_steps_summand + S (fs_a_dst_construct_inverse_equationvaluefoldpositive_body_steps) = S ((S (fs_i_dst_construct_inverse_equationvaluefoldpositive_body_steps)) * dst_positive_scale_construct_inverse_equationvaluefold)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldpositive_body_steps_summand. dst_positive_code_construct_inverse_equationvaluefold = fs_q_dst_construct_inverse_equationvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_construct_inverse_equationvaluefoldpositive_body_steps)) * dst_positive_scale_construct_inverse_equationvaluefold) + (fs_a_dst_construct_inverse_equationvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_construct_inverse_equationvaluefoldpositive_body_steps_partial. fs_h_dst_construct_inverse_equationvaluefoldpositive_body_steps_partial + S (fs_r_dst_construct_inverse_equationvaluefoldpositive_body_steps) = S ((S (fs_i_dst_construct_inverse_equationvaluefoldpositive_body_steps)) * fs_v_dst_construct_inverse_equationvaluefoldpositive)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldpositive_body_steps_partial. fs_u_dst_construct_inverse_equationvaluefoldpositive = fs_q_dst_construct_inverse_equationvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_construct_inverse_equationvaluefoldpositive_body_steps)) * fs_v_dst_construct_inverse_equationvaluefoldpositive) + (fs_r_dst_construct_inverse_equationvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_construct_inverse_equationvaluefoldpositive_body_steps_successor. fs_h_dst_construct_inverse_equationvaluefoldpositive_body_steps_successor + S (fs_s_dst_construct_inverse_equationvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_construct_inverse_equationvaluefoldpositive_body_steps)) * fs_v_dst_construct_inverse_equationvaluefoldpositive)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldpositive_body_steps_successor. fs_u_dst_construct_inverse_equationvaluefoldpositive = fs_q_dst_construct_inverse_equationvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_construct_inverse_equationvaluefoldpositive_body_steps)) * fs_v_dst_construct_inverse_equationvaluefoldpositive) + (fs_s_dst_construct_inverse_equationvaluefoldpositive_body_steps))) /\ fs_s_dst_construct_inverse_equationvaluefoldpositive_body_steps = fs_r_dst_construct_inverse_equationvaluefoldpositive_body_steps + fs_a_dst_construct_inverse_equationvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_construct_inverse_equationvaluefoldnegative fs_v_dst_construct_inverse_equationvaluefoldnegative. ((((exists fs_h_dst_construct_inverse_equationvaluefoldnegative_body_start. fs_h_dst_construct_inverse_equationvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_construct_inverse_equationvaluefoldnegative)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldnegative_body_start. fs_u_dst_construct_inverse_equationvaluefoldnegative = fs_q_dst_construct_inverse_equationvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_construct_inverse_equationvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_construct_inverse_equationvaluefoldnegative_body_terminal. fs_h_dst_construct_inverse_equationvaluefoldnegative_body_terminal + S (dst_negative_sum_construct_inverse_equationvaluefold) = S ((S (S (dc_input_construct_inverse_equation))) * fs_v_dst_construct_inverse_equationvaluefoldnegative)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldnegative_body_terminal. fs_u_dst_construct_inverse_equationvaluefoldnegative = fs_q_dst_construct_inverse_equationvaluefoldnegative_body_terminal * S ((S (S (dc_input_construct_inverse_equation))) * fs_v_dst_construct_inverse_equationvaluefoldnegative) + (dst_negative_sum_construct_inverse_equationvaluefold))) /\ forall fs_i_dst_construct_inverse_equationvaluefoldnegative_body_steps. (exists fs_lt_dst_construct_inverse_equationvaluefoldnegative_body_steps_bound. fs_lt_dst_construct_inverse_equationvaluefoldnegative_body_steps_bound + S fs_i_dst_construct_inverse_equationvaluefoldnegative_body_steps = S (dc_input_construct_inverse_equation)) -> exists fs_a_dst_construct_inverse_equationvaluefoldnegative_body_steps fs_r_dst_construct_inverse_equationvaluefoldnegative_body_steps fs_s_dst_construct_inverse_equationvaluefoldnegative_body_steps. ((((exists fs_h_dst_construct_inverse_equationvaluefoldnegative_body_steps_summand. fs_h_dst_construct_inverse_equationvaluefoldnegative_body_steps_summand + S (fs_a_dst_construct_inverse_equationvaluefoldnegative_body_steps) = S ((S (fs_i_dst_construct_inverse_equationvaluefoldnegative_body_steps)) * dst_negative_scale_construct_inverse_equationvaluefold)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldnegative_body_steps_summand. dst_negative_code_construct_inverse_equationvaluefold = fs_q_dst_construct_inverse_equationvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_construct_inverse_equationvaluefoldnegative_body_steps)) * dst_negative_scale_construct_inverse_equationvaluefold) + (fs_a_dst_construct_inverse_equationvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_construct_inverse_equationvaluefoldnegative_body_steps_partial. fs_h_dst_construct_inverse_equationvaluefoldnegative_body_steps_partial + S (fs_r_dst_construct_inverse_equationvaluefoldnegative_body_steps) = S ((S (fs_i_dst_construct_inverse_equationvaluefoldnegative_body_steps)) * fs_v_dst_construct_inverse_equationvaluefoldnegative)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldnegative_body_steps_partial. fs_u_dst_construct_inverse_equationvaluefoldnegative = fs_q_dst_construct_inverse_equationvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_construct_inverse_equationvaluefoldnegative_body_steps)) * fs_v_dst_construct_inverse_equationvaluefoldnegative) + (fs_r_dst_construct_inverse_equationvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_construct_inverse_equationvaluefoldnegative_body_steps_successor. fs_h_dst_construct_inverse_equationvaluefoldnegative_body_steps_successor + S (fs_s_dst_construct_inverse_equationvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_construct_inverse_equationvaluefoldnegative_body_steps)) * fs_v_dst_construct_inverse_equationvaluefoldnegative)) /\ exists fs_q_dst_construct_inverse_equationvaluefoldnegative_body_steps_successor. fs_u_dst_construct_inverse_equationvaluefoldnegative = fs_q_dst_construct_inverse_equationvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_construct_inverse_equationvaluefoldnegative_body_steps)) * fs_v_dst_construct_inverse_equationvaluefoldnegative) + (fs_s_dst_construct_inverse_equationvaluefoldnegative_body_steps))) /\ fs_s_dst_construct_inverse_equationvaluefoldnegative_body_steps = fs_r_dst_construct_inverse_equationvaluefoldnegative_body_steps + fs_a_dst_construct_inverse_equationvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_construct_inverse_equationvaluefoldresult ge_balance_negative_construct_inverse_equationvaluefoldresult. (((((dc_output_construct_inverse_equation) = 2 * (ge_balance_positive_construct_inverse_equationvaluefoldresult) /\ (ge_balance_negative_construct_inverse_equationvaluefoldresult) = 0) \/ exists ge_signed_half_construct_inverse_equationvaluefoldresultdecode. (((dc_output_construct_inverse_equation) = 2 * ge_signed_half_construct_inverse_equationvaluefoldresultdecode + 1 /\ (ge_balance_positive_construct_inverse_equationvaluefoldresult) = 0) /\ (ge_balance_negative_construct_inverse_equationvaluefoldresult) = S ge_signed_half_construct_inverse_equationvaluefoldresultdecode))) /\ ((dst_positive_sum_construct_inverse_equationvaluefold) + ge_balance_negative_construct_inverse_equationvaluefoldresult = (dst_negative_sum_construct_inverse_equationvaluefold) + ge_balance_positive_construct_inverse_equationvaluefoldresult)))))))))))))))))))) /\ (exists dst_positive_code_construct_inverse_zero dst_positive_scale_construct_inverse_zero dst_negative_code_construct_inverse_zero dst_negative_scale_construct_inverse_zero dst_positive_construct_inverse_zero dst_negative_construct_inverse_zero. (((G) = (((((dst_positive_code_construct_inverse_zero) + (dst_positive_scale_construct_inverse_zero)) * S ((dst_positive_code_construct_inverse_zero) + (dst_positive_scale_construct_inverse_zero)) + ((dst_positive_scale_construct_inverse_zero) + (dst_positive_scale_construct_inverse_zero))) + (((dst_negative_code_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)) * S ((dst_negative_code_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)) + ((dst_negative_scale_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)))) * S ((((dst_positive_code_construct_inverse_zero) + (dst_positive_scale_construct_inverse_zero)) * S ((dst_positive_code_construct_inverse_zero) + (dst_positive_scale_construct_inverse_zero)) + ((dst_positive_scale_construct_inverse_zero) + (dst_positive_scale_construct_inverse_zero))) + (((dst_negative_code_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)) * S ((dst_negative_code_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)) + ((dst_negative_scale_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)))) + ((((dst_negative_code_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)) * S ((dst_negative_code_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)) + ((dst_negative_scale_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero))) + (((dst_negative_code_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)) * S ((dst_negative_code_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)) + ((dst_negative_scale_construct_inverse_zero) + (dst_negative_scale_construct_inverse_zero)))))) /\ (((((exists ff_h_pvs_construct_inverse_zeropositive. ff_h_pvs_construct_inverse_zeropositive + S (dst_positive_construct_inverse_zero) = S ((S (0)) * dst_positive_scale_construct_inverse_zero)) /\ exists ff_q_pvs_construct_inverse_zeropositive. dst_positive_code_construct_inverse_zero = ff_q_pvs_construct_inverse_zeropositive * S ((S (0)) * dst_positive_scale_construct_inverse_zero) + (dst_positive_construct_inverse_zero))) /\ (((((exists ff_h_pvs_construct_inverse_zeronegative. ff_h_pvs_construct_inverse_zeronegative + S (dst_negative_construct_inverse_zero) = S ((S (0)) * dst_negative_scale_construct_inverse_zero)) /\ exists ff_q_pvs_construct_inverse_zeronegative. dst_negative_code_construct_inverse_zero = ff_q_pvs_construct_inverse_zeronegative * S ((S (0)) * dst_negative_scale_construct_inverse_zero) + (dst_negative_construct_inverse_zero))) /\ (exists ge_balance_positive_construct_inverse_zerovalue ge_balance_negative_construct_inverse_zerovalue. (((((w) = 2 * (ge_balance_positive_construct_inverse_zerovalue) /\ (ge_balance_negative_construct_inverse_zerovalue) = 0) \/ exists ge_signed_half_construct_inverse_zerovaluedecode. (((w) = 2 * ge_signed_half_construct_inverse_zerovaluedecode + 1 /\ (ge_balance_positive_construct_inverse_zerovalue) = 0) /\ (ge_balance_negative_construct_inverse_zerovalue) = S ge_signed_half_construct_inverse_zerovaluedecode))) /\ ((dst_positive_construct_inverse_zero) + ge_balance_negative_construct_inverse_zerovalue = (dst_negative_construct_inverse_zero) + ge_balance_positive_construct_inverse_zerovalue)))))))))) - 0016
specialize dirichlet_unit_equation_construct (N) - 0017
specialize dirichlet_unit_equation_construct (F) - 0018
specialize dirichlet_unit_equation_construct (x) - 0019
specialize dirichlet_unit_equation_construct (u) - 0020
specialize dirichlet_unit_equation_construct (w) - 0021
apply dirichlet_unit_equation_construct - 0022
exact hF - 0023
exact hd_witness_left_left - 0024
exact hu - 0025
exact hunit - 0026
cases hg - 0027
cases hg_witness - 0028
exists x1 - 0029
split - 0030
specialize dirichlet_inverse_from_right_delta (N) - 0031
specialize dirichlet_inverse_from_right_delta (F) - 0032
specialize dirichlet_inverse_from_right_delta (x1) - 0033
specialize dirichlet_inverse_from_right_delta (x) - 0034
apply dirichlet_inverse_from_right_delta - 0035
exact hd_witness_left - 0036
exact hg_witness_left - 0037
exact hg_witness_right