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 F G. (exists dst_positive_code_inverse_zero_left dst_positive_scale_inverse_zero_left dst_negative_code_inverse_zero_left dst_negative_scale_inverse_zero_left. (((F) = (((((dst_positive_code_inverse_zero_left) + (dst_positive_scale_inverse_zero_left)) * S ((dst_positive_code_inverse_zero_left) + (dst_positive_scale_inverse_zero_left)) + ((dst_positive_scale_inverse_zero_left) + (dst_positive_scale_inverse_zero_left))) + (((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) * S ((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) + ((dst_negative_scale_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)))) * S ((((dst_positive_code_inverse_zero_left) + (dst_positive_scale_inverse_zero_left)) * S ((dst_positive_code_inverse_zero_left) + (dst_positive_scale_inverse_zero_left)) + ((dst_positive_scale_inverse_zero_left) + (dst_positive_scale_inverse_zero_left))) + (((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) * S ((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) + ((dst_negative_scale_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)))) + ((((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) * S ((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) + ((dst_negative_scale_inverse_zero_left) + (dst_negative_scale_inverse_zero_left))) + (((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) * S ((dst_negative_code_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)) + ((dst_negative_scale_inverse_zero_left) + (dst_negative_scale_inverse_zero_left)))))) /\ (forall dst_index_inverse_zero_left. (exists pvs_le_gap_inverse_zero_leftdomain. pvs_le_gap_inverse_zero_leftdomain + (dst_index_inverse_zero_left) = (0)) -> exists dst_positive_inverse_zero_left dst_negative_inverse_zero_left dst_value_inverse_zero_left. ((((exists ff_h_pvs_inverse_zero_leftentrypositive. ff_h_pvs_inverse_zero_leftentrypositive + S (dst_positive_inverse_zero_left) = S ((S (dst_index_inverse_zero_left)) * dst_positive_scale_inverse_zero_left)) /\ exists ff_q_pvs_inverse_zero_leftentrypositive. dst_positive_code_inverse_zero_left = ff_q_pvs_inverse_zero_leftentrypositive * S ((S (dst_index_inverse_zero_left)) * dst_positive_scale_inverse_zero_left) + (dst_positive_inverse_zero_left))) /\ (((((exists ff_h_pvs_inverse_zero_leftentrynegative. ff_h_pvs_inverse_zero_leftentrynegative + S (dst_negative_inverse_zero_left) = S ((S (dst_index_inverse_zero_left)) * dst_negative_scale_inverse_zero_left)) /\ exists ff_q_pvs_inverse_zero_leftentrynegative. dst_negative_code_inverse_zero_left = ff_q_pvs_inverse_zero_leftentrynegative * S ((S (dst_index_inverse_zero_left)) * dst_negative_scale_inverse_zero_left) + (dst_negative_inverse_zero_left))) /\ (exists ge_balance_positive_inverse_zero_leftentryvalue ge_balance_negative_inverse_zero_leftentryvalue. (((((dst_value_inverse_zero_left) = 2 * (ge_balance_positive_inverse_zero_leftentryvalue) /\ (ge_balance_negative_inverse_zero_leftentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_leftentryvaluedecode. (((dst_value_inverse_zero_left) = 2 * ge_signed_half_inverse_zero_leftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_leftentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_leftentryvalue) = S ge_signed_half_inverse_zero_leftentryvaluedecode))) /\ ((dst_positive_inverse_zero_left) + ge_balance_negative_inverse_zero_leftentryvalue = (dst_negative_inverse_zero_left) + ge_balance_positive_inverse_zero_leftentryvalue))))))))) -> (exists dst_positive_code_inverse_zero_right dst_positive_scale_inverse_zero_right dst_negative_code_inverse_zero_right dst_negative_scale_inverse_zero_right. (((G) = (((((dst_positive_code_inverse_zero_right) + (dst_positive_scale_inverse_zero_right)) * S ((dst_positive_code_inverse_zero_right) + (dst_positive_scale_inverse_zero_right)) + ((dst_positive_scale_inverse_zero_right) + (dst_positive_scale_inverse_zero_right))) + (((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) * S ((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) + ((dst_negative_scale_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)))) * S ((((dst_positive_code_inverse_zero_right) + (dst_positive_scale_inverse_zero_right)) * S ((dst_positive_code_inverse_zero_right) + (dst_positive_scale_inverse_zero_right)) + ((dst_positive_scale_inverse_zero_right) + (dst_positive_scale_inverse_zero_right))) + (((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) * S ((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) + ((dst_negative_scale_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)))) + ((((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) * S ((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) + ((dst_negative_scale_inverse_zero_right) + (dst_negative_scale_inverse_zero_right))) + (((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) * S ((dst_negative_code_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)) + ((dst_negative_scale_inverse_zero_right) + (dst_negative_scale_inverse_zero_right)))))) /\ (forall dst_index_inverse_zero_right. (exists pvs_le_gap_inverse_zero_rightdomain. pvs_le_gap_inverse_zero_rightdomain + (dst_index_inverse_zero_right) = (0)) -> exists dst_positive_inverse_zero_right dst_negative_inverse_zero_right dst_value_inverse_zero_right. ((((exists ff_h_pvs_inverse_zero_rightentrypositive. ff_h_pvs_inverse_zero_rightentrypositive + S (dst_positive_inverse_zero_right) = S ((S (dst_index_inverse_zero_right)) * dst_positive_scale_inverse_zero_right)) /\ exists ff_q_pvs_inverse_zero_rightentrypositive. dst_positive_code_inverse_zero_right = ff_q_pvs_inverse_zero_rightentrypositive * S ((S (dst_index_inverse_zero_right)) * dst_positive_scale_inverse_zero_right) + (dst_positive_inverse_zero_right))) /\ (((((exists ff_h_pvs_inverse_zero_rightentrynegative. ff_h_pvs_inverse_zero_rightentrynegative + S (dst_negative_inverse_zero_right) = S ((S (dst_index_inverse_zero_right)) * dst_negative_scale_inverse_zero_right)) /\ exists ff_q_pvs_inverse_zero_rightentrynegative. dst_negative_code_inverse_zero_right = ff_q_pvs_inverse_zero_rightentrynegative * S ((S (dst_index_inverse_zero_right)) * dst_negative_scale_inverse_zero_right) + (dst_negative_inverse_zero_right))) /\ (exists ge_balance_positive_inverse_zero_rightentryvalue ge_balance_negative_inverse_zero_rightentryvalue. (((((dst_value_inverse_zero_right) = 2 * (ge_balance_positive_inverse_zero_rightentryvalue) /\ (ge_balance_negative_inverse_zero_rightentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_rightentryvaluedecode. (((dst_value_inverse_zero_right) = 2 * ge_signed_half_inverse_zero_rightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_rightentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_rightentryvalue) = S ge_signed_half_inverse_zero_rightentryvaluedecode))) /\ ((dst_positive_inverse_zero_right) + ge_balance_negative_inverse_zero_rightentryvalue = (dst_negative_inverse_zero_right) + ge_balance_positive_inverse_zero_rightentryvalue))))))))) -> (exists di_delta_inverse_zero_result. ((((exists dst_positive_code_inverse_zero_resultdeltatable dst_positive_scale_inverse_zero_resultdeltatable dst_negative_code_inverse_zero_resultdeltatable dst_negative_scale_inverse_zero_resultdeltatable. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable)) * S ((dst_positive_code_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable)) + ((dst_positive_scale_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable))) + (((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) * S ((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) + ((dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)))) * S ((((dst_positive_code_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable)) * S ((dst_positive_code_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable)) + ((dst_positive_scale_inverse_zero_resultdeltatable) + (dst_positive_scale_inverse_zero_resultdeltatable))) + (((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) * S ((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) + ((dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)))) + ((((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) * S ((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) + ((dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable))) + (((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) * S ((dst_negative_code_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)) + ((dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_scale_inverse_zero_resultdeltatable)))))) /\ (forall dst_index_inverse_zero_resultdeltatable. (exists pvs_le_gap_inverse_zero_resultdeltatabledomain. pvs_le_gap_inverse_zero_resultdeltatabledomain + (dst_index_inverse_zero_resultdeltatable) = (0)) -> exists dst_positive_inverse_zero_resultdeltatable dst_negative_inverse_zero_resultdeltatable dst_value_inverse_zero_resultdeltatable. ((((exists ff_h_pvs_inverse_zero_resultdeltatableentrypositive. ff_h_pvs_inverse_zero_resultdeltatableentrypositive + S (dst_positive_inverse_zero_resultdeltatable) = S ((S (dst_index_inverse_zero_resultdeltatable)) * dst_positive_scale_inverse_zero_resultdeltatable)) /\ exists ff_q_pvs_inverse_zero_resultdeltatableentrypositive. dst_positive_code_inverse_zero_resultdeltatable = ff_q_pvs_inverse_zero_resultdeltatableentrypositive * S ((S (dst_index_inverse_zero_resultdeltatable)) * dst_positive_scale_inverse_zero_resultdeltatable) + (dst_positive_inverse_zero_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_zero_resultdeltatableentrynegative. ff_h_pvs_inverse_zero_resultdeltatableentrynegative + S (dst_negative_inverse_zero_resultdeltatable) = S ((S (dst_index_inverse_zero_resultdeltatable)) * dst_negative_scale_inverse_zero_resultdeltatable)) /\ exists ff_q_pvs_inverse_zero_resultdeltatableentrynegative. dst_negative_code_inverse_zero_resultdeltatable = ff_q_pvs_inverse_zero_resultdeltatableentrynegative * S ((S (dst_index_inverse_zero_resultdeltatable)) * dst_negative_scale_inverse_zero_resultdeltatable) + (dst_negative_inverse_zero_resultdeltatable))) /\ (exists ge_balance_positive_inverse_zero_resultdeltatableentryvalue ge_balance_negative_inverse_zero_resultdeltatableentryvalue. (((((dst_value_inverse_zero_resultdeltatable) = 2 * (ge_balance_positive_inverse_zero_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_zero_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultdeltatableentryvaluedecode. (((dst_value_inverse_zero_resultdeltatable) = 2 * ge_signed_half_inverse_zero_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultdeltatableentryvalue) = S ge_signed_half_inverse_zero_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultdeltatable) + ge_balance_negative_inverse_zero_resultdeltatableentryvalue = (dst_negative_inverse_zero_resultdeltatable) + ge_balance_positive_inverse_zero_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_zero_resultdelta du_value_inverse_zero_resultdelta. ~(du_index_inverse_zero_resultdelta=0) -> (exists pvs_le_gap_inverse_zero_resultdeltabound. pvs_le_gap_inverse_zero_resultdeltabound + (du_index_inverse_zero_resultdelta) = (0)) -> (exists dst_positive_code_inverse_zero_resultdeltaentry dst_positive_scale_inverse_zero_resultdeltaentry dst_negative_code_inverse_zero_resultdeltaentry dst_negative_scale_inverse_zero_resultdeltaentry dst_positive_inverse_zero_resultdeltaentry dst_negative_inverse_zero_resultdeltaentry. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry)) * S ((dst_positive_code_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry)) + ((dst_positive_scale_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry))) + (((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)))) * S ((((dst_positive_code_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry)) * S ((dst_positive_code_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry)) + ((dst_positive_scale_inverse_zero_resultdeltaentry) + (dst_positive_scale_inverse_zero_resultdeltaentry))) + (((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)))) + ((((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry))) + (((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) * S ((dst_negative_code_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)) + ((dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_scale_inverse_zero_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultdeltaentrypositive. ff_h_pvs_inverse_zero_resultdeltaentrypositive + S (dst_positive_inverse_zero_resultdeltaentry) = S ((S (du_index_inverse_zero_resultdelta)) * dst_positive_scale_inverse_zero_resultdeltaentry)) /\ exists ff_q_pvs_inverse_zero_resultdeltaentrypositive. dst_positive_code_inverse_zero_resultdeltaentry = ff_q_pvs_inverse_zero_resultdeltaentrypositive * S ((S (du_index_inverse_zero_resultdelta)) * dst_positive_scale_inverse_zero_resultdeltaentry) + (dst_positive_inverse_zero_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_zero_resultdeltaentrynegative. ff_h_pvs_inverse_zero_resultdeltaentrynegative + S (dst_negative_inverse_zero_resultdeltaentry) = S ((S (du_index_inverse_zero_resultdelta)) * dst_negative_scale_inverse_zero_resultdeltaentry)) /\ exists ff_q_pvs_inverse_zero_resultdeltaentrynegative. dst_negative_code_inverse_zero_resultdeltaentry = ff_q_pvs_inverse_zero_resultdeltaentrynegative * S ((S (du_index_inverse_zero_resultdelta)) * dst_negative_scale_inverse_zero_resultdeltaentry) + (dst_negative_inverse_zero_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_zero_resultdeltaentryvalue ge_balance_negative_inverse_zero_resultdeltaentryvalue. (((((du_value_inverse_zero_resultdelta) = 2 * (ge_balance_positive_inverse_zero_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_zero_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultdeltaentryvaluedecode. (((du_value_inverse_zero_resultdelta) = 2 * ge_signed_half_inverse_zero_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultdeltaentryvalue) = S ge_signed_half_inverse_zero_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultdeltaentry) + ge_balance_negative_inverse_zero_resultdeltaentryvalue = (dst_negative_inverse_zero_resultdeltaentry) + ge_balance_positive_inverse_zero_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_zero_resultdelta)=1 -> (du_value_inverse_zero_resultdelta)=2) /\ (~((du_index_inverse_zero_resultdelta)=1) -> (du_value_inverse_zero_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_zero_resultleftleft dst_positive_scale_inverse_zero_resultleftleft dst_negative_code_inverse_zero_resultleftleft dst_negative_scale_inverse_zero_resultleftleft. (((F) = (((((dst_positive_code_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft)) * S ((dst_positive_code_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft)) + ((dst_positive_scale_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft))) + (((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) * S ((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) + ((dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)))) * S ((((dst_positive_code_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft)) * S ((dst_positive_code_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft)) + ((dst_positive_scale_inverse_zero_resultleftleft) + (dst_positive_scale_inverse_zero_resultleftleft))) + (((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) * S ((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) + ((dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)))) + ((((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) * S ((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) + ((dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft))) + (((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) * S ((dst_negative_code_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)) + ((dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_scale_inverse_zero_resultleftleft)))))) /\ (forall dst_index_inverse_zero_resultleftleft. (exists pvs_le_gap_inverse_zero_resultleftleftdomain. pvs_le_gap_inverse_zero_resultleftleftdomain + (dst_index_inverse_zero_resultleftleft) = (0)) -> exists dst_positive_inverse_zero_resultleftleft dst_negative_inverse_zero_resultleftleft dst_value_inverse_zero_resultleftleft. ((((exists ff_h_pvs_inverse_zero_resultleftleftentrypositive. ff_h_pvs_inverse_zero_resultleftleftentrypositive + S (dst_positive_inverse_zero_resultleftleft) = S ((S (dst_index_inverse_zero_resultleftleft)) * dst_positive_scale_inverse_zero_resultleftleft)) /\ exists ff_q_pvs_inverse_zero_resultleftleftentrypositive. dst_positive_code_inverse_zero_resultleftleft = ff_q_pvs_inverse_zero_resultleftleftentrypositive * S ((S (dst_index_inverse_zero_resultleftleft)) * dst_positive_scale_inverse_zero_resultleftleft) + (dst_positive_inverse_zero_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftleftentrynegative. ff_h_pvs_inverse_zero_resultleftleftentrynegative + S (dst_negative_inverse_zero_resultleftleft) = S ((S (dst_index_inverse_zero_resultleftleft)) * dst_negative_scale_inverse_zero_resultleftleft)) /\ exists ff_q_pvs_inverse_zero_resultleftleftentrynegative. dst_negative_code_inverse_zero_resultleftleft = ff_q_pvs_inverse_zero_resultleftleftentrynegative * S ((S (dst_index_inverse_zero_resultleftleft)) * dst_negative_scale_inverse_zero_resultleftleft) + (dst_negative_inverse_zero_resultleftleft))) /\ (exists ge_balance_positive_inverse_zero_resultleftleftentryvalue ge_balance_negative_inverse_zero_resultleftleftentryvalue. (((((dst_value_inverse_zero_resultleftleft) = 2 * (ge_balance_positive_inverse_zero_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_zero_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftleftentryvaluedecode. (((dst_value_inverse_zero_resultleftleft) = 2 * ge_signed_half_inverse_zero_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftleftentryvalue) = S ge_signed_half_inverse_zero_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftleft) + ge_balance_negative_inverse_zero_resultleftleftentryvalue = (dst_negative_inverse_zero_resultleftleft) + ge_balance_positive_inverse_zero_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultleftright dst_positive_scale_inverse_zero_resultleftright dst_negative_code_inverse_zero_resultleftright dst_negative_scale_inverse_zero_resultleftright. (((G) = (((((dst_positive_code_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright)) * S ((dst_positive_code_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright)) + ((dst_positive_scale_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright))) + (((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) * S ((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) + ((dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)))) * S ((((dst_positive_code_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright)) * S ((dst_positive_code_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright)) + ((dst_positive_scale_inverse_zero_resultleftright) + (dst_positive_scale_inverse_zero_resultleftright))) + (((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) * S ((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) + ((dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)))) + ((((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) * S ((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) + ((dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright))) + (((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) * S ((dst_negative_code_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)) + ((dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_scale_inverse_zero_resultleftright)))))) /\ (forall dst_index_inverse_zero_resultleftright. (exists pvs_le_gap_inverse_zero_resultleftrightdomain. pvs_le_gap_inverse_zero_resultleftrightdomain + (dst_index_inverse_zero_resultleftright) = (0)) -> exists dst_positive_inverse_zero_resultleftright dst_negative_inverse_zero_resultleftright dst_value_inverse_zero_resultleftright. ((((exists ff_h_pvs_inverse_zero_resultleftrightentrypositive. ff_h_pvs_inverse_zero_resultleftrightentrypositive + S (dst_positive_inverse_zero_resultleftright) = S ((S (dst_index_inverse_zero_resultleftright)) * dst_positive_scale_inverse_zero_resultleftright)) /\ exists ff_q_pvs_inverse_zero_resultleftrightentrypositive. dst_positive_code_inverse_zero_resultleftright = ff_q_pvs_inverse_zero_resultleftrightentrypositive * S ((S (dst_index_inverse_zero_resultleftright)) * dst_positive_scale_inverse_zero_resultleftright) + (dst_positive_inverse_zero_resultleftright))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftrightentrynegative. ff_h_pvs_inverse_zero_resultleftrightentrynegative + S (dst_negative_inverse_zero_resultleftright) = S ((S (dst_index_inverse_zero_resultleftright)) * dst_negative_scale_inverse_zero_resultleftright)) /\ exists ff_q_pvs_inverse_zero_resultleftrightentrynegative. dst_negative_code_inverse_zero_resultleftright = ff_q_pvs_inverse_zero_resultleftrightentrynegative * S ((S (dst_index_inverse_zero_resultleftright)) * dst_negative_scale_inverse_zero_resultleftright) + (dst_negative_inverse_zero_resultleftright))) /\ (exists ge_balance_positive_inverse_zero_resultleftrightentryvalue ge_balance_negative_inverse_zero_resultleftrightentryvalue. (((((dst_value_inverse_zero_resultleftright) = 2 * (ge_balance_positive_inverse_zero_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_zero_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftrightentryvaluedecode. (((dst_value_inverse_zero_resultleftright) = 2 * ge_signed_half_inverse_zero_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftrightentryvalue) = S ge_signed_half_inverse_zero_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftright) + ge_balance_negative_inverse_zero_resultleftrightentryvalue = (dst_negative_inverse_zero_resultleftright) + ge_balance_positive_inverse_zero_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultlefttable dst_positive_scale_inverse_zero_resultlefttable dst_negative_code_inverse_zero_resultlefttable dst_negative_scale_inverse_zero_resultlefttable. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable)) * S ((dst_positive_code_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable)) + ((dst_positive_scale_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable))) + (((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) * S ((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) + ((dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)))) * S ((((dst_positive_code_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable)) * S ((dst_positive_code_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable)) + ((dst_positive_scale_inverse_zero_resultlefttable) + (dst_positive_scale_inverse_zero_resultlefttable))) + (((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) * S ((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) + ((dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)))) + ((((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) * S ((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) + ((dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable))) + (((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) * S ((dst_negative_code_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)) + ((dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_scale_inverse_zero_resultlefttable)))))) /\ (forall dst_index_inverse_zero_resultlefttable. (exists pvs_le_gap_inverse_zero_resultlefttabledomain. pvs_le_gap_inverse_zero_resultlefttabledomain + (dst_index_inverse_zero_resultlefttable) = (0)) -> exists dst_positive_inverse_zero_resultlefttable dst_negative_inverse_zero_resultlefttable dst_value_inverse_zero_resultlefttable. ((((exists ff_h_pvs_inverse_zero_resultlefttableentrypositive. ff_h_pvs_inverse_zero_resultlefttableentrypositive + S (dst_positive_inverse_zero_resultlefttable) = S ((S (dst_index_inverse_zero_resultlefttable)) * dst_positive_scale_inverse_zero_resultlefttable)) /\ exists ff_q_pvs_inverse_zero_resultlefttableentrypositive. dst_positive_code_inverse_zero_resultlefttable = ff_q_pvs_inverse_zero_resultlefttableentrypositive * S ((S (dst_index_inverse_zero_resultlefttable)) * dst_positive_scale_inverse_zero_resultlefttable) + (dst_positive_inverse_zero_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_zero_resultlefttableentrynegative. ff_h_pvs_inverse_zero_resultlefttableentrynegative + S (dst_negative_inverse_zero_resultlefttable) = S ((S (dst_index_inverse_zero_resultlefttable)) * dst_negative_scale_inverse_zero_resultlefttable)) /\ exists ff_q_pvs_inverse_zero_resultlefttableentrynegative. dst_negative_code_inverse_zero_resultlefttable = ff_q_pvs_inverse_zero_resultlefttableentrynegative * S ((S (dst_index_inverse_zero_resultlefttable)) * dst_negative_scale_inverse_zero_resultlefttable) + (dst_negative_inverse_zero_resultlefttable))) /\ (exists ge_balance_positive_inverse_zero_resultlefttableentryvalue ge_balance_negative_inverse_zero_resultlefttableentryvalue. (((((dst_value_inverse_zero_resultlefttable) = 2 * (ge_balance_positive_inverse_zero_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_zero_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultlefttableentryvaluedecode. (((dst_value_inverse_zero_resultlefttable) = 2 * ge_signed_half_inverse_zero_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultlefttableentryvalue) = S ge_signed_half_inverse_zero_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultlefttable) + ge_balance_negative_inverse_zero_resultlefttableentryvalue = (dst_negative_inverse_zero_resultlefttable) + ge_balance_positive_inverse_zero_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_zero_resultleft dc_output_inverse_zero_resultleft. ~(dc_input_inverse_zero_resultleft=0) -> (exists pvs_le_gap_inverse_zero_resultleftdomain. pvs_le_gap_inverse_zero_resultleftdomain + (dc_input_inverse_zero_resultleft) = (0)) -> (exists dst_positive_code_inverse_zero_resultleftlookup dst_positive_scale_inverse_zero_resultleftlookup dst_negative_code_inverse_zero_resultleftlookup dst_negative_scale_inverse_zero_resultleftlookup dst_positive_inverse_zero_resultleftlookup dst_negative_inverse_zero_resultleftlookup. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup)) * S ((dst_positive_code_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup)) + ((dst_positive_scale_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup))) + (((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) * S ((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) + ((dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)))) * S ((((dst_positive_code_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup)) * S ((dst_positive_code_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup)) + ((dst_positive_scale_inverse_zero_resultleftlookup) + (dst_positive_scale_inverse_zero_resultleftlookup))) + (((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) * S ((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) + ((dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)))) + ((((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) * S ((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) + ((dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup))) + (((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) * S ((dst_negative_code_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)) + ((dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_scale_inverse_zero_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftlookuppositive. ff_h_pvs_inverse_zero_resultleftlookuppositive + S (dst_positive_inverse_zero_resultleftlookup) = S ((S (dc_input_inverse_zero_resultleft)) * dst_positive_scale_inverse_zero_resultleftlookup)) /\ exists ff_q_pvs_inverse_zero_resultleftlookuppositive. dst_positive_code_inverse_zero_resultleftlookup = ff_q_pvs_inverse_zero_resultleftlookuppositive * S ((S (dc_input_inverse_zero_resultleft)) * dst_positive_scale_inverse_zero_resultleftlookup) + (dst_positive_inverse_zero_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftlookupnegative. ff_h_pvs_inverse_zero_resultleftlookupnegative + S (dst_negative_inverse_zero_resultleftlookup) = S ((S (dc_input_inverse_zero_resultleft)) * dst_negative_scale_inverse_zero_resultleftlookup)) /\ exists ff_q_pvs_inverse_zero_resultleftlookupnegative. dst_negative_code_inverse_zero_resultleftlookup = ff_q_pvs_inverse_zero_resultleftlookupnegative * S ((S (dc_input_inverse_zero_resultleft)) * dst_negative_scale_inverse_zero_resultleftlookup) + (dst_negative_inverse_zero_resultleftlookup))) /\ (exists ge_balance_positive_inverse_zero_resultleftlookupvalue ge_balance_negative_inverse_zero_resultleftlookupvalue. (((((dc_output_inverse_zero_resultleft) = 2 * (ge_balance_positive_inverse_zero_resultleftlookupvalue) /\ (ge_balance_negative_inverse_zero_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftlookupvaluedecode. (((dc_output_inverse_zero_resultleft) = 2 * ge_signed_half_inverse_zero_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftlookupvalue) = S ge_signed_half_inverse_zero_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftlookup) + ge_balance_negative_inverse_zero_resultleftlookupvalue = (dst_negative_inverse_zero_resultleftlookup) + ge_balance_positive_inverse_zero_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_zero_resultleft)=0)) /\ (exists dc_mask_inverse_zero_resultleftvalue. ((((exists dst_positive_code_inverse_zero_resultleftvaluemasktable dst_positive_scale_inverse_zero_resultleftvaluemasktable dst_negative_code_inverse_zero_resultleftvaluemasktable dst_negative_scale_inverse_zero_resultleftvaluemasktable. (((dc_mask_inverse_zero_resultleftvalue) = (((((dst_positive_code_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_zero_resultleftvaluemasktable) + (dst_positive_scale_inverse_zero_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable))) + (((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_scale_inverse_zero_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_zero_resultleftvaluemasktable. (exists pvs_le_gap_inverse_zero_resultleftvaluemasktabledomain. pvs_le_gap_inverse_zero_resultleftvaluemasktabledomain + (dst_index_inverse_zero_resultleftvaluemasktable) = (dc_input_inverse_zero_resultleft)) -> exists dst_positive_inverse_zero_resultleftvaluemasktable dst_negative_inverse_zero_resultleftvaluemasktable dst_value_inverse_zero_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_zero_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_zero_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_zero_resultleftvaluemasktable) = S ((S (dst_index_inverse_zero_resultleftvaluemasktable)) * dst_positive_scale_inverse_zero_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_zero_resultleftvaluemasktable = ff_q_pvs_inverse_zero_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_zero_resultleftvaluemasktable)) * dst_positive_scale_inverse_zero_resultleftvaluemasktable) + (dst_positive_inverse_zero_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_zero_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_zero_resultleftvaluemasktable) = S ((S (dst_index_inverse_zero_resultleftvaluemasktable)) * dst_negative_scale_inverse_zero_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_zero_resultleftvaluemasktable = ff_q_pvs_inverse_zero_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_zero_resultleftvaluemasktable)) * dst_negative_scale_inverse_zero_resultleftvaluemasktable) + (dst_negative_inverse_zero_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_zero_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_zero_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_zero_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_zero_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_zero_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_zero_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftvaluemasktable) + ge_balance_negative_inverse_zero_resultleftvaluemasktableentryvalue = (dst_negative_inverse_zero_resultleftvaluemasktable) + ge_balance_positive_inverse_zero_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_zero_resultleftvaluemask dc_value_inverse_zero_resultleftvaluemask. (exists pvs_le_gap_inverse_zero_resultleftvaluemaskdomain. pvs_le_gap_inverse_zero_resultleftvaluemaskdomain + (dc_index_inverse_zero_resultleftvaluemask) = (dc_input_inverse_zero_resultleft)) -> (exists dst_positive_code_inverse_zero_resultleftvaluemasklookup dst_positive_scale_inverse_zero_resultleftvaluemasklookup dst_negative_code_inverse_zero_resultleftvaluemasklookup dst_negative_scale_inverse_zero_resultleftvaluemasklookup dst_positive_inverse_zero_resultleftvaluemasklookup dst_negative_inverse_zero_resultleftvaluemasklookup. (((dc_mask_inverse_zero_resultleftvalue) = (((((dst_positive_code_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_zero_resultleftvaluemasklookup) + (dst_positive_scale_inverse_zero_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_scale_inverse_zero_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_zero_resultleftvaluemasklookuppositive + S (dst_positive_inverse_zero_resultleftvaluemasklookup) = S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_positive_scale_inverse_zero_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemasklookuppositive. dst_positive_code_inverse_zero_resultleftvaluemasklookup = ff_q_pvs_inverse_zero_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_positive_scale_inverse_zero_resultleftvaluemasklookup) + (dst_positive_inverse_zero_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_zero_resultleftvaluemasklookupnegative + S (dst_negative_inverse_zero_resultleftvaluemasklookup) = S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_negative_scale_inverse_zero_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemasklookupnegative. dst_negative_code_inverse_zero_resultleftvaluemasklookup = ff_q_pvs_inverse_zero_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_negative_scale_inverse_zero_resultleftvaluemasklookup) + (dst_negative_inverse_zero_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluemasklookupvalue ge_balance_negative_inverse_zero_resultleftvaluemasklookupvalue. (((((dc_value_inverse_zero_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_zero_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_zero_resultleftvaluemask) = 2 * ge_signed_half_inverse_zero_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_zero_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftvaluemasklookup) + ge_balance_negative_inverse_zero_resultleftvaluemasklookupvalue = (dst_negative_inverse_zero_resultleftvaluemasklookup) + ge_balance_positive_inverse_zero_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_zero_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_zero_resultleftvaluemaskentry dc_left_inverse_zero_resultleftvaluemaskentry dc_right_inverse_zero_resultleftvaluemaskentry. (((dc_input_inverse_zero_resultleft)=(dc_index_inverse_zero_resultleftvaluemask)*dc_quotient_inverse_zero_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_zero_resultleftvaluemaskentryleft dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft dst_negative_code_inverse_zero_resultleftvaluemaskentryleft dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft dst_positive_inverse_zero_resultleftvaluemaskentryleft dst_negative_inverse_zero_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_zero_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_zero_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_zero_resultleftvaluemaskentryleft = ff_q_pvs_inverse_zero_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_positive_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_positive_inverse_zero_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_zero_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_zero_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_zero_resultleftvaluemaskentryleft = ff_q_pvs_inverse_zero_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_zero_resultleftvaluemask)) * dst_negative_scale_inverse_zero_resultleftvaluemaskentryleft) + (dst_negative_inverse_zero_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_zero_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_zero_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_zero_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_zero_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_zero_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_zero_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_zero_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultleftvaluemaskentryright dst_positive_scale_inverse_zero_resultleftvaluemaskentryright dst_negative_code_inverse_zero_resultleftvaluemaskentryright dst_negative_scale_inverse_zero_resultleftvaluemaskentryright dst_positive_inverse_zero_resultleftvaluemaskentryright dst_negative_inverse_zero_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_zero_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_zero_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_resultleftvaluemaskentry)) * dst_positive_scale_inverse_zero_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_zero_resultleftvaluemaskentryright = ff_q_pvs_inverse_zero_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_zero_resultleftvaluemaskentry)) * dst_positive_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_positive_inverse_zero_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_zero_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_zero_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_zero_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_resultleftvaluemaskentry)) * dst_negative_scale_inverse_zero_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_zero_resultleftvaluemaskentryright = ff_q_pvs_inverse_zero_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_zero_resultleftvaluemaskentry)) * dst_negative_scale_inverse_zero_resultleftvaluemaskentryright) + (dst_negative_inverse_zero_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_zero_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_zero_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_zero_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_zero_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_zero_resultleftvaluemaskentryright) + ge_balance_negative_inverse_zero_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_zero_resultleftvaluemaskentryright) + ge_balance_positive_inverse_zero_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_zero_resultleftvaluemaskentryproduct sto_an_inverse_zero_resultleftvaluemaskentryproduct sto_bp_inverse_zero_resultleftvaluemaskentryproduct sto_bn_inverse_zero_resultleftvaluemaskentryproduct sto_cp_inverse_zero_resultleftvaluemaskentryproduct sto_cn_inverse_zero_resultleftvaluemaskentryproduct. (((((dc_left_inverse_zero_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_zero_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_zero_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryproductleft. (((dc_left_inverse_zero_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_zero_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_zero_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_zero_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_zero_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_zero_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryproductright. (((dc_right_inverse_zero_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_zero_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_zero_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_zero_resultleftvaluemask) = 2 * (sto_cp_inverse_zero_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_zero_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_zero_resultleftvaluemask) = 2 * ge_signed_half_inverse_zero_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_zero_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_zero_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_zero_resultleftvaluemaskentryproduct * sto_bp_inverse_zero_resultleftvaluemaskentryproduct + sto_an_inverse_zero_resultleftvaluemaskentryproduct * sto_bn_inverse_zero_resultleftvaluemaskentryproduct) + sto_cn_inverse_zero_resultleftvaluemaskentryproduct = (sto_ap_inverse_zero_resultleftvaluemaskentryproduct * sto_bn_inverse_zero_resultleftvaluemaskentryproduct + sto_an_inverse_zero_resultleftvaluemaskentryproduct * sto_bp_inverse_zero_resultleftvaluemaskentryproduct) + sto_cp_inverse_zero_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_zero_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_zero_resultleftvaluemaskentrynondivisor. (dc_input_inverse_zero_resultleft) = (dc_index_inverse_zero_resultleftvaluemask) * pvs_factor_inverse_zero_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_zero_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_zero_resultleftvaluefold dst_positive_scale_inverse_zero_resultleftvaluefold dst_negative_code_inverse_zero_resultleftvaluefold dst_negative_scale_inverse_zero_resultleftvaluefold dst_positive_sum_inverse_zero_resultleftvaluefold dst_negative_sum_inverse_zero_resultleftvaluefold. (((dc_mask_inverse_zero_resultleftvalue) = (((((dst_positive_code_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold)) * S ((dst_positive_code_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold)) + ((dst_positive_scale_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold)) * S ((dst_positive_code_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold)) + ((dst_positive_scale_inverse_zero_resultleftvaluefold) + (dst_positive_scale_inverse_zero_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)))) + ((((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold))) + (((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) * S ((dst_negative_code_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)) + ((dst_negative_scale_inverse_zero_resultleftvaluefold) + (dst_negative_scale_inverse_zero_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_zero_resultleftvaluefoldpositive fs_v_dst_inverse_zero_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_zero_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_zero_resultleftvaluefold) = S ((S (S (dc_input_inverse_zero_resultleft))) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_zero_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_zero_resultleft))) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_zero_resultleftvaluefold))) /\ forall fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_zero_resultleft)) -> exists fs_a_dst_inverse_zero_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_zero_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_zero_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_zero_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_resultleftvaluefold)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_zero_resultleftvaluefold = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_resultleftvaluefold) + (fs_a_dst_inverse_zero_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_zero_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_zero_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive) + (fs_r_dst_inverse_zero_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_zero_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_zero_resultleftvaluefoldpositive = fs_q_dst_inverse_zero_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldpositive) + (fs_s_dst_inverse_zero_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_zero_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_zero_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_zero_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_zero_resultleftvaluefoldnegative fs_v_dst_inverse_zero_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_zero_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_zero_resultleftvaluefold) = S ((S (S (dc_input_inverse_zero_resultleft))) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_zero_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_zero_resultleft))) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_zero_resultleftvaluefold))) /\ forall fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_zero_resultleft)) -> exists fs_a_dst_inverse_zero_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_zero_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_zero_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_zero_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_resultleftvaluefold)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_zero_resultleftvaluefold = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_resultleftvaluefold) + (fs_a_dst_inverse_zero_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_zero_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_zero_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative) + (fs_r_dst_inverse_zero_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_zero_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_zero_resultleftvaluefoldnegative = fs_q_dst_inverse_zero_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultleftvaluefoldnegative) + (fs_s_dst_inverse_zero_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_zero_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_zero_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_zero_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_zero_resultleftvaluefoldresult ge_balance_negative_inverse_zero_resultleftvaluefoldresult. (((((dc_output_inverse_zero_resultleft) = 2 * (ge_balance_positive_inverse_zero_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_zero_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_zero_resultleftvaluefoldresultdecode. (((dc_output_inverse_zero_resultleft) = 2 * ge_signed_half_inverse_zero_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_zero_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_zero_resultleftvaluefoldresult) = S ge_signed_half_inverse_zero_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_zero_resultleftvaluefold) + ge_balance_negative_inverse_zero_resultleftvaluefoldresult = (dst_negative_sum_inverse_zero_resultleftvaluefold) + ge_balance_positive_inverse_zero_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_zero_resultrightleft dst_positive_scale_inverse_zero_resultrightleft dst_negative_code_inverse_zero_resultrightleft dst_negative_scale_inverse_zero_resultrightleft. (((G) = (((((dst_positive_code_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft)) * S ((dst_positive_code_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft)) + ((dst_positive_scale_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft))) + (((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) * S ((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) + ((dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)))) * S ((((dst_positive_code_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft)) * S ((dst_positive_code_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft)) + ((dst_positive_scale_inverse_zero_resultrightleft) + (dst_positive_scale_inverse_zero_resultrightleft))) + (((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) * S ((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) + ((dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)))) + ((((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) * S ((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) + ((dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft))) + (((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) * S ((dst_negative_code_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)) + ((dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_scale_inverse_zero_resultrightleft)))))) /\ (forall dst_index_inverse_zero_resultrightleft. (exists pvs_le_gap_inverse_zero_resultrightleftdomain. pvs_le_gap_inverse_zero_resultrightleftdomain + (dst_index_inverse_zero_resultrightleft) = (0)) -> exists dst_positive_inverse_zero_resultrightleft dst_negative_inverse_zero_resultrightleft dst_value_inverse_zero_resultrightleft. ((((exists ff_h_pvs_inverse_zero_resultrightleftentrypositive. ff_h_pvs_inverse_zero_resultrightleftentrypositive + S (dst_positive_inverse_zero_resultrightleft) = S ((S (dst_index_inverse_zero_resultrightleft)) * dst_positive_scale_inverse_zero_resultrightleft)) /\ exists ff_q_pvs_inverse_zero_resultrightleftentrypositive. dst_positive_code_inverse_zero_resultrightleft = ff_q_pvs_inverse_zero_resultrightleftentrypositive * S ((S (dst_index_inverse_zero_resultrightleft)) * dst_positive_scale_inverse_zero_resultrightleft) + (dst_positive_inverse_zero_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightleftentrynegative. ff_h_pvs_inverse_zero_resultrightleftentrynegative + S (dst_negative_inverse_zero_resultrightleft) = S ((S (dst_index_inverse_zero_resultrightleft)) * dst_negative_scale_inverse_zero_resultrightleft)) /\ exists ff_q_pvs_inverse_zero_resultrightleftentrynegative. dst_negative_code_inverse_zero_resultrightleft = ff_q_pvs_inverse_zero_resultrightleftentrynegative * S ((S (dst_index_inverse_zero_resultrightleft)) * dst_negative_scale_inverse_zero_resultrightleft) + (dst_negative_inverse_zero_resultrightleft))) /\ (exists ge_balance_positive_inverse_zero_resultrightleftentryvalue ge_balance_negative_inverse_zero_resultrightleftentryvalue. (((((dst_value_inverse_zero_resultrightleft) = 2 * (ge_balance_positive_inverse_zero_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_zero_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightleftentryvaluedecode. (((dst_value_inverse_zero_resultrightleft) = 2 * ge_signed_half_inverse_zero_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightleftentryvalue) = S ge_signed_half_inverse_zero_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightleft) + ge_balance_negative_inverse_zero_resultrightleftentryvalue = (dst_negative_inverse_zero_resultrightleft) + ge_balance_positive_inverse_zero_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultrightright dst_positive_scale_inverse_zero_resultrightright dst_negative_code_inverse_zero_resultrightright dst_negative_scale_inverse_zero_resultrightright. (((F) = (((((dst_positive_code_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright)) * S ((dst_positive_code_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright)) + ((dst_positive_scale_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright))) + (((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) * S ((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) + ((dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)))) * S ((((dst_positive_code_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright)) * S ((dst_positive_code_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright)) + ((dst_positive_scale_inverse_zero_resultrightright) + (dst_positive_scale_inverse_zero_resultrightright))) + (((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) * S ((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) + ((dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)))) + ((((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) * S ((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) + ((dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright))) + (((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) * S ((dst_negative_code_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)) + ((dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_scale_inverse_zero_resultrightright)))))) /\ (forall dst_index_inverse_zero_resultrightright. (exists pvs_le_gap_inverse_zero_resultrightrightdomain. pvs_le_gap_inverse_zero_resultrightrightdomain + (dst_index_inverse_zero_resultrightright) = (0)) -> exists dst_positive_inverse_zero_resultrightright dst_negative_inverse_zero_resultrightright dst_value_inverse_zero_resultrightright. ((((exists ff_h_pvs_inverse_zero_resultrightrightentrypositive. ff_h_pvs_inverse_zero_resultrightrightentrypositive + S (dst_positive_inverse_zero_resultrightright) = S ((S (dst_index_inverse_zero_resultrightright)) * dst_positive_scale_inverse_zero_resultrightright)) /\ exists ff_q_pvs_inverse_zero_resultrightrightentrypositive. dst_positive_code_inverse_zero_resultrightright = ff_q_pvs_inverse_zero_resultrightrightentrypositive * S ((S (dst_index_inverse_zero_resultrightright)) * dst_positive_scale_inverse_zero_resultrightright) + (dst_positive_inverse_zero_resultrightright))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightrightentrynegative. ff_h_pvs_inverse_zero_resultrightrightentrynegative + S (dst_negative_inverse_zero_resultrightright) = S ((S (dst_index_inverse_zero_resultrightright)) * dst_negative_scale_inverse_zero_resultrightright)) /\ exists ff_q_pvs_inverse_zero_resultrightrightentrynegative. dst_negative_code_inverse_zero_resultrightright = ff_q_pvs_inverse_zero_resultrightrightentrynegative * S ((S (dst_index_inverse_zero_resultrightright)) * dst_negative_scale_inverse_zero_resultrightright) + (dst_negative_inverse_zero_resultrightright))) /\ (exists ge_balance_positive_inverse_zero_resultrightrightentryvalue ge_balance_negative_inverse_zero_resultrightrightentryvalue. (((((dst_value_inverse_zero_resultrightright) = 2 * (ge_balance_positive_inverse_zero_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_zero_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightrightentryvaluedecode. (((dst_value_inverse_zero_resultrightright) = 2 * ge_signed_half_inverse_zero_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightrightentryvalue) = S ge_signed_half_inverse_zero_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightright) + ge_balance_negative_inverse_zero_resultrightrightentryvalue = (dst_negative_inverse_zero_resultrightright) + ge_balance_positive_inverse_zero_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultrighttable dst_positive_scale_inverse_zero_resultrighttable dst_negative_code_inverse_zero_resultrighttable dst_negative_scale_inverse_zero_resultrighttable. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable)) * S ((dst_positive_code_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable)) + ((dst_positive_scale_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable))) + (((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) * S ((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) + ((dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)))) * S ((((dst_positive_code_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable)) * S ((dst_positive_code_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable)) + ((dst_positive_scale_inverse_zero_resultrighttable) + (dst_positive_scale_inverse_zero_resultrighttable))) + (((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) * S ((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) + ((dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)))) + ((((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) * S ((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) + ((dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable))) + (((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) * S ((dst_negative_code_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)) + ((dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_scale_inverse_zero_resultrighttable)))))) /\ (forall dst_index_inverse_zero_resultrighttable. (exists pvs_le_gap_inverse_zero_resultrighttabledomain. pvs_le_gap_inverse_zero_resultrighttabledomain + (dst_index_inverse_zero_resultrighttable) = (0)) -> exists dst_positive_inverse_zero_resultrighttable dst_negative_inverse_zero_resultrighttable dst_value_inverse_zero_resultrighttable. ((((exists ff_h_pvs_inverse_zero_resultrighttableentrypositive. ff_h_pvs_inverse_zero_resultrighttableentrypositive + S (dst_positive_inverse_zero_resultrighttable) = S ((S (dst_index_inverse_zero_resultrighttable)) * dst_positive_scale_inverse_zero_resultrighttable)) /\ exists ff_q_pvs_inverse_zero_resultrighttableentrypositive. dst_positive_code_inverse_zero_resultrighttable = ff_q_pvs_inverse_zero_resultrighttableentrypositive * S ((S (dst_index_inverse_zero_resultrighttable)) * dst_positive_scale_inverse_zero_resultrighttable) + (dst_positive_inverse_zero_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_zero_resultrighttableentrynegative. ff_h_pvs_inverse_zero_resultrighttableentrynegative + S (dst_negative_inverse_zero_resultrighttable) = S ((S (dst_index_inverse_zero_resultrighttable)) * dst_negative_scale_inverse_zero_resultrighttable)) /\ exists ff_q_pvs_inverse_zero_resultrighttableentrynegative. dst_negative_code_inverse_zero_resultrighttable = ff_q_pvs_inverse_zero_resultrighttableentrynegative * S ((S (dst_index_inverse_zero_resultrighttable)) * dst_negative_scale_inverse_zero_resultrighttable) + (dst_negative_inverse_zero_resultrighttable))) /\ (exists ge_balance_positive_inverse_zero_resultrighttableentryvalue ge_balance_negative_inverse_zero_resultrighttableentryvalue. (((((dst_value_inverse_zero_resultrighttable) = 2 * (ge_balance_positive_inverse_zero_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_zero_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrighttableentryvaluedecode. (((dst_value_inverse_zero_resultrighttable) = 2 * ge_signed_half_inverse_zero_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrighttableentryvalue) = S ge_signed_half_inverse_zero_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultrighttable) + ge_balance_negative_inverse_zero_resultrighttableentryvalue = (dst_negative_inverse_zero_resultrighttable) + ge_balance_positive_inverse_zero_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_zero_resultright dc_output_inverse_zero_resultright. ~(dc_input_inverse_zero_resultright=0) -> (exists pvs_le_gap_inverse_zero_resultrightdomain. pvs_le_gap_inverse_zero_resultrightdomain + (dc_input_inverse_zero_resultright) = (0)) -> (exists dst_positive_code_inverse_zero_resultrightlookup dst_positive_scale_inverse_zero_resultrightlookup dst_negative_code_inverse_zero_resultrightlookup dst_negative_scale_inverse_zero_resultrightlookup dst_positive_inverse_zero_resultrightlookup dst_negative_inverse_zero_resultrightlookup. (((di_delta_inverse_zero_result) = (((((dst_positive_code_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup)) * S ((dst_positive_code_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup)) + ((dst_positive_scale_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup))) + (((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) * S ((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) + ((dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)))) * S ((((dst_positive_code_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup)) * S ((dst_positive_code_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup)) + ((dst_positive_scale_inverse_zero_resultrightlookup) + (dst_positive_scale_inverse_zero_resultrightlookup))) + (((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) * S ((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) + ((dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)))) + ((((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) * S ((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) + ((dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup))) + (((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) * S ((dst_negative_code_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)) + ((dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_scale_inverse_zero_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightlookuppositive. ff_h_pvs_inverse_zero_resultrightlookuppositive + S (dst_positive_inverse_zero_resultrightlookup) = S ((S (dc_input_inverse_zero_resultright)) * dst_positive_scale_inverse_zero_resultrightlookup)) /\ exists ff_q_pvs_inverse_zero_resultrightlookuppositive. dst_positive_code_inverse_zero_resultrightlookup = ff_q_pvs_inverse_zero_resultrightlookuppositive * S ((S (dc_input_inverse_zero_resultright)) * dst_positive_scale_inverse_zero_resultrightlookup) + (dst_positive_inverse_zero_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightlookupnegative. ff_h_pvs_inverse_zero_resultrightlookupnegative + S (dst_negative_inverse_zero_resultrightlookup) = S ((S (dc_input_inverse_zero_resultright)) * dst_negative_scale_inverse_zero_resultrightlookup)) /\ exists ff_q_pvs_inverse_zero_resultrightlookupnegative. dst_negative_code_inverse_zero_resultrightlookup = ff_q_pvs_inverse_zero_resultrightlookupnegative * S ((S (dc_input_inverse_zero_resultright)) * dst_negative_scale_inverse_zero_resultrightlookup) + (dst_negative_inverse_zero_resultrightlookup))) /\ (exists ge_balance_positive_inverse_zero_resultrightlookupvalue ge_balance_negative_inverse_zero_resultrightlookupvalue. (((((dc_output_inverse_zero_resultright) = 2 * (ge_balance_positive_inverse_zero_resultrightlookupvalue) /\ (ge_balance_negative_inverse_zero_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightlookupvaluedecode. (((dc_output_inverse_zero_resultright) = 2 * ge_signed_half_inverse_zero_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightlookupvalue) = S ge_signed_half_inverse_zero_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightlookup) + ge_balance_negative_inverse_zero_resultrightlookupvalue = (dst_negative_inverse_zero_resultrightlookup) + ge_balance_positive_inverse_zero_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_zero_resultright)=0)) /\ (exists dc_mask_inverse_zero_resultrightvalue. ((((exists dst_positive_code_inverse_zero_resultrightvaluemasktable dst_positive_scale_inverse_zero_resultrightvaluemasktable dst_negative_code_inverse_zero_resultrightvaluemasktable dst_negative_scale_inverse_zero_resultrightvaluemasktable. (((dc_mask_inverse_zero_resultrightvalue) = (((((dst_positive_code_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_zero_resultrightvaluemasktable) + (dst_positive_scale_inverse_zero_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable))) + (((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_scale_inverse_zero_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_zero_resultrightvaluemasktable. (exists pvs_le_gap_inverse_zero_resultrightvaluemasktabledomain. pvs_le_gap_inverse_zero_resultrightvaluemasktabledomain + (dst_index_inverse_zero_resultrightvaluemasktable) = (dc_input_inverse_zero_resultright)) -> exists dst_positive_inverse_zero_resultrightvaluemasktable dst_negative_inverse_zero_resultrightvaluemasktable dst_value_inverse_zero_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_zero_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_zero_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_zero_resultrightvaluemasktable) = S ((S (dst_index_inverse_zero_resultrightvaluemasktable)) * dst_positive_scale_inverse_zero_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_zero_resultrightvaluemasktable = ff_q_pvs_inverse_zero_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_zero_resultrightvaluemasktable)) * dst_positive_scale_inverse_zero_resultrightvaluemasktable) + (dst_positive_inverse_zero_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_zero_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_zero_resultrightvaluemasktable) = S ((S (dst_index_inverse_zero_resultrightvaluemasktable)) * dst_negative_scale_inverse_zero_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_zero_resultrightvaluemasktable = ff_q_pvs_inverse_zero_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_zero_resultrightvaluemasktable)) * dst_negative_scale_inverse_zero_resultrightvaluemasktable) + (dst_negative_inverse_zero_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_zero_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_zero_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_zero_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_zero_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_zero_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_zero_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightvaluemasktable) + ge_balance_negative_inverse_zero_resultrightvaluemasktableentryvalue = (dst_negative_inverse_zero_resultrightvaluemasktable) + ge_balance_positive_inverse_zero_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_zero_resultrightvaluemask dc_value_inverse_zero_resultrightvaluemask. (exists pvs_le_gap_inverse_zero_resultrightvaluemaskdomain. pvs_le_gap_inverse_zero_resultrightvaluemaskdomain + (dc_index_inverse_zero_resultrightvaluemask) = (dc_input_inverse_zero_resultright)) -> (exists dst_positive_code_inverse_zero_resultrightvaluemasklookup dst_positive_scale_inverse_zero_resultrightvaluemasklookup dst_negative_code_inverse_zero_resultrightvaluemasklookup dst_negative_scale_inverse_zero_resultrightvaluemasklookup dst_positive_inverse_zero_resultrightvaluemasklookup dst_negative_inverse_zero_resultrightvaluemasklookup. (((dc_mask_inverse_zero_resultrightvalue) = (((((dst_positive_code_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_zero_resultrightvaluemasklookup) + (dst_positive_scale_inverse_zero_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_scale_inverse_zero_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_zero_resultrightvaluemasklookuppositive + S (dst_positive_inverse_zero_resultrightvaluemasklookup) = S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_positive_scale_inverse_zero_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemasklookuppositive. dst_positive_code_inverse_zero_resultrightvaluemasklookup = ff_q_pvs_inverse_zero_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_positive_scale_inverse_zero_resultrightvaluemasklookup) + (dst_positive_inverse_zero_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_zero_resultrightvaluemasklookupnegative + S (dst_negative_inverse_zero_resultrightvaluemasklookup) = S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_negative_scale_inverse_zero_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemasklookupnegative. dst_negative_code_inverse_zero_resultrightvaluemasklookup = ff_q_pvs_inverse_zero_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_negative_scale_inverse_zero_resultrightvaluemasklookup) + (dst_negative_inverse_zero_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluemasklookupvalue ge_balance_negative_inverse_zero_resultrightvaluemasklookupvalue. (((((dc_value_inverse_zero_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_zero_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_zero_resultrightvaluemask) = 2 * ge_signed_half_inverse_zero_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_zero_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightvaluemasklookup) + ge_balance_negative_inverse_zero_resultrightvaluemasklookupvalue = (dst_negative_inverse_zero_resultrightvaluemasklookup) + ge_balance_positive_inverse_zero_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_zero_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_zero_resultrightvaluemaskentry dc_left_inverse_zero_resultrightvaluemaskentry dc_right_inverse_zero_resultrightvaluemaskentry. (((dc_input_inverse_zero_resultright)=(dc_index_inverse_zero_resultrightvaluemask)*dc_quotient_inverse_zero_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_zero_resultrightvaluemaskentryleft dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft dst_negative_code_inverse_zero_resultrightvaluemaskentryleft dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft dst_positive_inverse_zero_resultrightvaluemaskentryleft dst_negative_inverse_zero_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_zero_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_zero_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_zero_resultrightvaluemaskentryleft = ff_q_pvs_inverse_zero_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_positive_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_positive_inverse_zero_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_zero_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_zero_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_zero_resultrightvaluemaskentryleft = ff_q_pvs_inverse_zero_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_zero_resultrightvaluemask)) * dst_negative_scale_inverse_zero_resultrightvaluemaskentryleft) + (dst_negative_inverse_zero_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_zero_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_zero_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_zero_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_zero_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_zero_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_zero_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_zero_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_zero_resultrightvaluemaskentryright dst_positive_scale_inverse_zero_resultrightvaluemaskentryright dst_negative_code_inverse_zero_resultrightvaluemaskentryright dst_negative_scale_inverse_zero_resultrightvaluemaskentryright dst_positive_inverse_zero_resultrightvaluemaskentryright dst_negative_inverse_zero_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_zero_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_zero_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_zero_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_resultrightvaluemaskentry)) * dst_positive_scale_inverse_zero_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_zero_resultrightvaluemaskentryright = ff_q_pvs_inverse_zero_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_zero_resultrightvaluemaskentry)) * dst_positive_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_positive_inverse_zero_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_zero_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_zero_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_zero_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_zero_resultrightvaluemaskentry)) * dst_negative_scale_inverse_zero_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_zero_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_zero_resultrightvaluemaskentryright = ff_q_pvs_inverse_zero_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_zero_resultrightvaluemaskentry)) * dst_negative_scale_inverse_zero_resultrightvaluemaskentryright) + (dst_negative_inverse_zero_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_zero_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_zero_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_zero_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_zero_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_zero_resultrightvaluemaskentryright) + ge_balance_negative_inverse_zero_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_zero_resultrightvaluemaskentryright) + ge_balance_positive_inverse_zero_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_zero_resultrightvaluemaskentryproduct sto_an_inverse_zero_resultrightvaluemaskentryproduct sto_bp_inverse_zero_resultrightvaluemaskentryproduct sto_bn_inverse_zero_resultrightvaluemaskentryproduct sto_cp_inverse_zero_resultrightvaluemaskentryproduct sto_cn_inverse_zero_resultrightvaluemaskentryproduct. (((((dc_left_inverse_zero_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_zero_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_zero_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryproductleft. (((dc_left_inverse_zero_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_zero_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_zero_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_zero_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_zero_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_zero_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryproductright. (((dc_right_inverse_zero_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_zero_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_zero_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_zero_resultrightvaluemask) = 2 * (sto_cp_inverse_zero_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_zero_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_zero_resultrightvaluemask) = 2 * ge_signed_half_inverse_zero_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_zero_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_zero_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_zero_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_zero_resultrightvaluemaskentryproduct * sto_bp_inverse_zero_resultrightvaluemaskentryproduct + sto_an_inverse_zero_resultrightvaluemaskentryproduct * sto_bn_inverse_zero_resultrightvaluemaskentryproduct) + sto_cn_inverse_zero_resultrightvaluemaskentryproduct = (sto_ap_inverse_zero_resultrightvaluemaskentryproduct * sto_bn_inverse_zero_resultrightvaluemaskentryproduct + sto_an_inverse_zero_resultrightvaluemaskentryproduct * sto_bp_inverse_zero_resultrightvaluemaskentryproduct) + sto_cp_inverse_zero_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_zero_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_zero_resultrightvaluemaskentrynondivisor. (dc_input_inverse_zero_resultright) = (dc_index_inverse_zero_resultrightvaluemask) * pvs_factor_inverse_zero_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_zero_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_zero_resultrightvaluefold dst_positive_scale_inverse_zero_resultrightvaluefold dst_negative_code_inverse_zero_resultrightvaluefold dst_negative_scale_inverse_zero_resultrightvaluefold dst_positive_sum_inverse_zero_resultrightvaluefold dst_negative_sum_inverse_zero_resultrightvaluefold. (((dc_mask_inverse_zero_resultrightvalue) = (((((dst_positive_code_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold)) * S ((dst_positive_code_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold)) + ((dst_positive_scale_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold)) * S ((dst_positive_code_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold)) + ((dst_positive_scale_inverse_zero_resultrightvaluefold) + (dst_positive_scale_inverse_zero_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)))) + ((((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold))) + (((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) * S ((dst_negative_code_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)) + ((dst_negative_scale_inverse_zero_resultrightvaluefold) + (dst_negative_scale_inverse_zero_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_zero_resultrightvaluefoldpositive fs_v_dst_inverse_zero_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_zero_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_zero_resultrightvaluefold) = S ((S (S (dc_input_inverse_zero_resultright))) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_zero_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_zero_resultright))) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_zero_resultrightvaluefold))) /\ forall fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_zero_resultright)) -> exists fs_a_dst_inverse_zero_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_zero_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_zero_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_zero_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_resultrightvaluefold)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_zero_resultrightvaluefold = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_zero_resultrightvaluefold) + (fs_a_dst_inverse_zero_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_zero_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_zero_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive) + (fs_r_dst_inverse_zero_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_zero_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_zero_resultrightvaluefoldpositive = fs_q_dst_inverse_zero_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldpositive) + (fs_s_dst_inverse_zero_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_zero_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_zero_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_zero_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_zero_resultrightvaluefoldnegative fs_v_dst_inverse_zero_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_zero_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_zero_resultrightvaluefold) = S ((S (S (dc_input_inverse_zero_resultright))) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_zero_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_zero_resultright))) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_zero_resultrightvaluefold))) /\ forall fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_zero_resultright)) -> exists fs_a_dst_inverse_zero_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_zero_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_zero_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_zero_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_resultrightvaluefold)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_zero_resultrightvaluefold = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_zero_resultrightvaluefold) + (fs_a_dst_inverse_zero_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_zero_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_zero_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative) + (fs_r_dst_inverse_zero_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_zero_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_zero_resultrightvaluefoldnegative = fs_q_dst_inverse_zero_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_zero_resultrightvaluefoldnegative) + (fs_s_dst_inverse_zero_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_zero_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_zero_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_zero_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_zero_resultrightvaluefoldresult ge_balance_negative_inverse_zero_resultrightvaluefoldresult. (((((dc_output_inverse_zero_resultright) = 2 * (ge_balance_positive_inverse_zero_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_zero_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_zero_resultrightvaluefoldresultdecode. (((dc_output_inverse_zero_resultright) = 2 * ge_signed_half_inverse_zero_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_zero_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_zero_resultrightvaluefoldresult) = S ge_signed_half_inverse_zero_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_zero_resultrightvaluefold) + ge_balance_negative_inverse_zero_resultrightvaluefoldresult = (dst_negative_sum_inverse_zero_resultrightvaluefold) + ge_balance_positive_inverse_zero_resultrightvaluefoldresult))))))))))))))))))))))))Constructive proof overview
Generated structural guide
Every pair of actual zero-window tables has a genuine delta witness and both empty positive-domain inverse identities, with no condition at one.
The unchanged tactic script uses 2 declared prerequisites and contains 29 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 dirichlet_convolution_table_zero_constructor Alpha theorem; checked-use authorizedDirect 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.
01Fix variables and assumptionsL1–4
02Establish hdL5–8
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 casesL9–11
04Construct an explicit witnessL12–12
Supply the displayed value, then prove that it has the required property.
- L12
exists x
05Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
split
06Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact hd_witness_left
07Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
split
08Use earlier factsL16–25
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
specialize dirichlet_convolution_table_zero_constructor (F) - L17
specialize dirichlet_convolution_table_zero_constructor (G) - L18
specialize dirichlet_convolution_table_zero_constructor (x) - L19
apply dirichlet_convolution_table_zero_constructor - L20
exact hF - L21
exact hG - L22
exact hd_witness_left_left - L23
specialize dirichlet_convolution_table_zero_constructor (G) - L24
specialize dirichlet_convolution_table_zero_constructor (F) - L25
specialize dirichlet_convolution_table_zero_constructor (x)
Original exact command ledger · 29 lines
- 0001
intro F - 0002
intro G - 0003
intro hF - 0004
intro hG - 0005
have hd : exists E. (((exists dst_positive_code_zero_actual_deltatable dst_positive_scale_zero_actual_deltatable dst_negative_code_zero_actual_deltatable dst_negative_scale_zero_actual_deltatable. (((E) = (((((dst_positive_code_zero_actual_deltatable) + (dst_positive_scale_zero_actual_deltatable)) * S ((dst_positive_code_zero_actual_deltatable) + (dst_positive_scale_zero_actual_deltatable)) + ((dst_positive_scale_zero_actual_deltatable) + (dst_positive_scale_zero_actual_deltatable))) + (((dst_negative_code_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)) * S ((dst_negative_code_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)) + ((dst_negative_scale_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)))) * S ((((dst_positive_code_zero_actual_deltatable) + (dst_positive_scale_zero_actual_deltatable)) * S ((dst_positive_code_zero_actual_deltatable) + (dst_positive_scale_zero_actual_deltatable)) + ((dst_positive_scale_zero_actual_deltatable) + (dst_positive_scale_zero_actual_deltatable))) + (((dst_negative_code_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)) * S ((dst_negative_code_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)) + ((dst_negative_scale_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)))) + ((((dst_negative_code_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)) * S ((dst_negative_code_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)) + ((dst_negative_scale_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable))) + (((dst_negative_code_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)) * S ((dst_negative_code_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)) + ((dst_negative_scale_zero_actual_deltatable) + (dst_negative_scale_zero_actual_deltatable)))))) /\ (forall dst_index_zero_actual_deltatable. (exists pvs_le_gap_zero_actual_deltatabledomain. pvs_le_gap_zero_actual_deltatabledomain + (dst_index_zero_actual_deltatable) = (0)) -> exists dst_positive_zero_actual_deltatable dst_negative_zero_actual_deltatable dst_value_zero_actual_deltatable. ((((exists ff_h_pvs_zero_actual_deltatableentrypositive. ff_h_pvs_zero_actual_deltatableentrypositive + S (dst_positive_zero_actual_deltatable) = S ((S (dst_index_zero_actual_deltatable)) * dst_positive_scale_zero_actual_deltatable)) /\ exists ff_q_pvs_zero_actual_deltatableentrypositive. dst_positive_code_zero_actual_deltatable = ff_q_pvs_zero_actual_deltatableentrypositive * S ((S (dst_index_zero_actual_deltatable)) * dst_positive_scale_zero_actual_deltatable) + (dst_positive_zero_actual_deltatable))) /\ (((((exists ff_h_pvs_zero_actual_deltatableentrynegative. ff_h_pvs_zero_actual_deltatableentrynegative + S (dst_negative_zero_actual_deltatable) = S ((S (dst_index_zero_actual_deltatable)) * dst_negative_scale_zero_actual_deltatable)) /\ exists ff_q_pvs_zero_actual_deltatableentrynegative. dst_negative_code_zero_actual_deltatable = ff_q_pvs_zero_actual_deltatableentrynegative * S ((S (dst_index_zero_actual_deltatable)) * dst_negative_scale_zero_actual_deltatable) + (dst_negative_zero_actual_deltatable))) /\ (exists ge_balance_positive_zero_actual_deltatableentryvalue ge_balance_negative_zero_actual_deltatableentryvalue. (((((dst_value_zero_actual_deltatable) = 2 * (ge_balance_positive_zero_actual_deltatableentryvalue) /\ (ge_balance_negative_zero_actual_deltatableentryvalue) = 0) \/ exists ge_signed_half_zero_actual_deltatableentryvaluedecode. (((dst_value_zero_actual_deltatable) = 2 * ge_signed_half_zero_actual_deltatableentryvaluedecode + 1 /\ (ge_balance_positive_zero_actual_deltatableentryvalue) = 0) /\ (ge_balance_negative_zero_actual_deltatableentryvalue) = S ge_signed_half_zero_actual_deltatableentryvaluedecode))) /\ ((dst_positive_zero_actual_deltatable) + ge_balance_negative_zero_actual_deltatableentryvalue = (dst_negative_zero_actual_deltatable) + ge_balance_positive_zero_actual_deltatableentryvalue))))))))) /\ (forall du_index_zero_actual_delta du_value_zero_actual_delta. ~(du_index_zero_actual_delta=0) -> (exists pvs_le_gap_zero_actual_deltabound. pvs_le_gap_zero_actual_deltabound + (du_index_zero_actual_delta) = (0)) -> (exists dst_positive_code_zero_actual_deltaentry dst_positive_scale_zero_actual_deltaentry dst_negative_code_zero_actual_deltaentry dst_negative_scale_zero_actual_deltaentry dst_positive_zero_actual_deltaentry dst_negative_zero_actual_deltaentry. (((E) = (((((dst_positive_code_zero_actual_deltaentry) + (dst_positive_scale_zero_actual_deltaentry)) * S ((dst_positive_code_zero_actual_deltaentry) + (dst_positive_scale_zero_actual_deltaentry)) + ((dst_positive_scale_zero_actual_deltaentry) + (dst_positive_scale_zero_actual_deltaentry))) + (((dst_negative_code_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)) * S ((dst_negative_code_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)) + ((dst_negative_scale_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)))) * S ((((dst_positive_code_zero_actual_deltaentry) + (dst_positive_scale_zero_actual_deltaentry)) * S ((dst_positive_code_zero_actual_deltaentry) + (dst_positive_scale_zero_actual_deltaentry)) + ((dst_positive_scale_zero_actual_deltaentry) + (dst_positive_scale_zero_actual_deltaentry))) + (((dst_negative_code_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)) * S ((dst_negative_code_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)) + ((dst_negative_scale_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)))) + ((((dst_negative_code_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)) * S ((dst_negative_code_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)) + ((dst_negative_scale_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry))) + (((dst_negative_code_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)) * S ((dst_negative_code_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)) + ((dst_negative_scale_zero_actual_deltaentry) + (dst_negative_scale_zero_actual_deltaentry)))))) /\ (((((exists ff_h_pvs_zero_actual_deltaentrypositive. ff_h_pvs_zero_actual_deltaentrypositive + S (dst_positive_zero_actual_deltaentry) = S ((S (du_index_zero_actual_delta)) * dst_positive_scale_zero_actual_deltaentry)) /\ exists ff_q_pvs_zero_actual_deltaentrypositive. dst_positive_code_zero_actual_deltaentry = ff_q_pvs_zero_actual_deltaentrypositive * S ((S (du_index_zero_actual_delta)) * dst_positive_scale_zero_actual_deltaentry) + (dst_positive_zero_actual_deltaentry))) /\ (((((exists ff_h_pvs_zero_actual_deltaentrynegative. ff_h_pvs_zero_actual_deltaentrynegative + S (dst_negative_zero_actual_deltaentry) = S ((S (du_index_zero_actual_delta)) * dst_negative_scale_zero_actual_deltaentry)) /\ exists ff_q_pvs_zero_actual_deltaentrynegative. dst_negative_code_zero_actual_deltaentry = ff_q_pvs_zero_actual_deltaentrynegative * S ((S (du_index_zero_actual_delta)) * dst_negative_scale_zero_actual_deltaentry) + (dst_negative_zero_actual_deltaentry))) /\ (exists ge_balance_positive_zero_actual_deltaentryvalue ge_balance_negative_zero_actual_deltaentryvalue. (((((du_value_zero_actual_delta) = 2 * (ge_balance_positive_zero_actual_deltaentryvalue) /\ (ge_balance_negative_zero_actual_deltaentryvalue) = 0) \/ exists ge_signed_half_zero_actual_deltaentryvaluedecode. (((du_value_zero_actual_delta) = 2 * ge_signed_half_zero_actual_deltaentryvaluedecode + 1 /\ (ge_balance_positive_zero_actual_deltaentryvalue) = 0) /\ (ge_balance_negative_zero_actual_deltaentryvalue) = S ge_signed_half_zero_actual_deltaentryvaluedecode))) /\ ((dst_positive_zero_actual_deltaentry) + ge_balance_negative_zero_actual_deltaentryvalue = (dst_negative_zero_actual_deltaentry) + ge_balance_positive_zero_actual_deltaentryvalue))))))))) -> ((((du_index_zero_actual_delta)=1 -> (du_value_zero_actual_delta)=2) /\ (~((du_index_zero_actual_delta)=1) -> (du_value_zero_actual_delta)=0)))))) /\ (exists dst_positive_code_zero_delta_value dst_positive_scale_zero_delta_value dst_negative_code_zero_delta_value dst_negative_scale_zero_delta_value dst_positive_zero_delta_value dst_negative_zero_delta_value. (((E) = (((((dst_positive_code_zero_delta_value) + (dst_positive_scale_zero_delta_value)) * S ((dst_positive_code_zero_delta_value) + (dst_positive_scale_zero_delta_value)) + ((dst_positive_scale_zero_delta_value) + (dst_positive_scale_zero_delta_value))) + (((dst_negative_code_zero_delta_value) + (dst_negative_scale_zero_delta_value)) * S ((dst_negative_code_zero_delta_value) + (dst_negative_scale_zero_delta_value)) + ((dst_negative_scale_zero_delta_value) + (dst_negative_scale_zero_delta_value)))) * S ((((dst_positive_code_zero_delta_value) + (dst_positive_scale_zero_delta_value)) * S ((dst_positive_code_zero_delta_value) + (dst_positive_scale_zero_delta_value)) + ((dst_positive_scale_zero_delta_value) + (dst_positive_scale_zero_delta_value))) + (((dst_negative_code_zero_delta_value) + (dst_negative_scale_zero_delta_value)) * S ((dst_negative_code_zero_delta_value) + (dst_negative_scale_zero_delta_value)) + ((dst_negative_scale_zero_delta_value) + (dst_negative_scale_zero_delta_value)))) + ((((dst_negative_code_zero_delta_value) + (dst_negative_scale_zero_delta_value)) * S ((dst_negative_code_zero_delta_value) + (dst_negative_scale_zero_delta_value)) + ((dst_negative_scale_zero_delta_value) + (dst_negative_scale_zero_delta_value))) + (((dst_negative_code_zero_delta_value) + (dst_negative_scale_zero_delta_value)) * S ((dst_negative_code_zero_delta_value) + (dst_negative_scale_zero_delta_value)) + ((dst_negative_scale_zero_delta_value) + (dst_negative_scale_zero_delta_value)))))) /\ (((((exists ff_h_pvs_zero_delta_valuepositive. ff_h_pvs_zero_delta_valuepositive + S (dst_positive_zero_delta_value) = S ((S (0)) * dst_positive_scale_zero_delta_value)) /\ exists ff_q_pvs_zero_delta_valuepositive. dst_positive_code_zero_delta_value = ff_q_pvs_zero_delta_valuepositive * S ((S (0)) * dst_positive_scale_zero_delta_value) + (dst_positive_zero_delta_value))) /\ (((((exists ff_h_pvs_zero_delta_valuenegative. ff_h_pvs_zero_delta_valuenegative + S (dst_negative_zero_delta_value) = S ((S (0)) * dst_negative_scale_zero_delta_value)) /\ exists ff_q_pvs_zero_delta_valuenegative. dst_negative_code_zero_delta_value = ff_q_pvs_zero_delta_valuenegative * S ((S (0)) * dst_negative_scale_zero_delta_value) + (dst_negative_zero_delta_value))) /\ (exists ge_balance_positive_zero_delta_valuevalue ge_balance_negative_zero_delta_valuevalue. (((((0) = 2 * (ge_balance_positive_zero_delta_valuevalue) /\ (ge_balance_negative_zero_delta_valuevalue) = 0) \/ exists ge_signed_half_zero_delta_valuevaluedecode. (((0) = 2 * ge_signed_half_zero_delta_valuevaluedecode + 1 /\ (ge_balance_positive_zero_delta_valuevalue) = 0) /\ (ge_balance_negative_zero_delta_valuevalue) = S ge_signed_half_zero_delta_valuevaluedecode))) /\ ((dst_positive_zero_delta_value) + ge_balance_negative_zero_delta_valuevalue = (dst_negative_zero_delta_value) + ge_balance_positive_zero_delta_valuevalue))))))))) - 0006
specialize dirichlet_kronecker_delta_table_exists (0) - 0007
specialize dirichlet_kronecker_delta_table_exists (0) - 0008
apply dirichlet_kronecker_delta_table_exists - 0009
cases hd - 0010
cases hd_witness - 0011
cases hd_witness_left - 0012
exists x - 0013
split - 0014
exact hd_witness_left - 0015
split - 0016
specialize dirichlet_convolution_table_zero_constructor (F) - 0017
specialize dirichlet_convolution_table_zero_constructor (G) - 0018
specialize dirichlet_convolution_table_zero_constructor (x) - 0019
apply dirichlet_convolution_table_zero_constructor - 0020
exact hF - 0021
exact hG - 0022
exact hd_witness_left_left - 0023
specialize dirichlet_convolution_table_zero_constructor (G) - 0024
specialize dirichlet_convolution_table_zero_constructor (F) - 0025
specialize dirichlet_convolution_table_zero_constructor (x) - 0026
apply dirichlet_convolution_table_zero_constructor - 0027
exact hG - 0028
exact hF - 0029
exact hd_witness_left_left