Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
Exact expanded first-order arithmetic statement
forall N F w. (exists dst_positive_code_inverse_construct_input dst_positive_scale_inverse_construct_input dst_negative_code_inverse_construct_input dst_negative_scale_inverse_construct_input. (((F) = (((((dst_positive_code_inverse_construct_input) + (dst_positive_scale_inverse_construct_input)) * S ((dst_positive_code_inverse_construct_input) + (dst_positive_scale_inverse_construct_input)) + ((dst_positive_scale_inverse_construct_input) + (dst_positive_scale_inverse_construct_input))) + (((dst_negative_code_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)) * S ((dst_negative_code_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)) + ((dst_negative_scale_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)))) * S ((((dst_positive_code_inverse_construct_input) + (dst_positive_scale_inverse_construct_input)) * S ((dst_positive_code_inverse_construct_input) + (dst_positive_scale_inverse_construct_input)) + ((dst_positive_scale_inverse_construct_input) + (dst_positive_scale_inverse_construct_input))) + (((dst_negative_code_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)) * S ((dst_negative_code_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)) + ((dst_negative_scale_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)))) + ((((dst_negative_code_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)) * S ((dst_negative_code_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)) + ((dst_negative_scale_inverse_construct_input) + (dst_negative_scale_inverse_construct_input))) + (((dst_negative_code_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)) * S ((dst_negative_code_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)) + ((dst_negative_scale_inverse_construct_input) + (dst_negative_scale_inverse_construct_input)))))) /\ (forall dst_index_inverse_construct_input. (exists pvs_le_gap_inverse_construct_inputdomain. pvs_le_gap_inverse_construct_inputdomain + (dst_index_inverse_construct_input) = (N)) -> exists dst_positive_inverse_construct_input dst_negative_inverse_construct_input dst_value_inverse_construct_input. ((((exists ff_h_pvs_inverse_construct_inputentrypositive. ff_h_pvs_inverse_construct_inputentrypositive + S (dst_positive_inverse_construct_input) = S ((S (dst_index_inverse_construct_input)) * dst_positive_scale_inverse_construct_input)) /\ exists ff_q_pvs_inverse_construct_inputentrypositive. dst_positive_code_inverse_construct_input = ff_q_pvs_inverse_construct_inputentrypositive * S ((S (dst_index_inverse_construct_input)) * dst_positive_scale_inverse_construct_input) + (dst_positive_inverse_construct_input))) /\ (((((exists ff_h_pvs_inverse_construct_inputentrynegative. ff_h_pvs_inverse_construct_inputentrynegative + S (dst_negative_inverse_construct_input) = S ((S (dst_index_inverse_construct_input)) * dst_negative_scale_inverse_construct_input)) /\ exists ff_q_pvs_inverse_construct_inputentrynegative. dst_negative_code_inverse_construct_input = ff_q_pvs_inverse_construct_inputentrynegative * S ((S (dst_index_inverse_construct_input)) * dst_negative_scale_inverse_construct_input) + (dst_negative_inverse_construct_input))) /\ (exists ge_balance_positive_inverse_construct_inputentryvalue ge_balance_negative_inverse_construct_inputentryvalue. (((((dst_value_inverse_construct_input) = 2 * (ge_balance_positive_inverse_construct_inputentryvalue) /\ (ge_balance_negative_inverse_construct_inputentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_inputentryvaluedecode. (((dst_value_inverse_construct_input) = 2 * ge_signed_half_inverse_construct_inputentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_inputentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_inputentryvalue) = S ge_signed_half_inverse_construct_inputentryvaluedecode))) /\ ((dst_positive_inverse_construct_input) + ge_balance_negative_inverse_construct_inputentryvalue = (dst_negative_inverse_construct_input) + ge_balance_positive_inverse_construct_inputentryvalue))))))))) -> (N=0 \/ ((exists dst_positive_code_inverse_construct_conditionpositive dst_positive_scale_inverse_construct_conditionpositive dst_negative_code_inverse_construct_conditionpositive dst_negative_scale_inverse_construct_conditionpositive dst_positive_inverse_construct_conditionpositive dst_negative_inverse_construct_conditionpositive. (((F) = (((((dst_positive_code_inverse_construct_conditionpositive) + (dst_positive_scale_inverse_construct_conditionpositive)) * S ((dst_positive_code_inverse_construct_conditionpositive) + (dst_positive_scale_inverse_construct_conditionpositive)) + ((dst_positive_scale_inverse_construct_conditionpositive) + (dst_positive_scale_inverse_construct_conditionpositive))) + (((dst_negative_code_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)) * S ((dst_negative_code_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)) + ((dst_negative_scale_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)))) * S ((((dst_positive_code_inverse_construct_conditionpositive) + (dst_positive_scale_inverse_construct_conditionpositive)) * S ((dst_positive_code_inverse_construct_conditionpositive) + (dst_positive_scale_inverse_construct_conditionpositive)) + ((dst_positive_scale_inverse_construct_conditionpositive) + (dst_positive_scale_inverse_construct_conditionpositive))) + (((dst_negative_code_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)) * S ((dst_negative_code_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)) + ((dst_negative_scale_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)))) + ((((dst_negative_code_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)) * S ((dst_negative_code_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)) + ((dst_negative_scale_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive))) + (((dst_negative_code_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)) * S ((dst_negative_code_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)) + ((dst_negative_scale_inverse_construct_conditionpositive) + (dst_negative_scale_inverse_construct_conditionpositive)))))) /\ (((((exists ff_h_pvs_inverse_construct_conditionpositivepositive. ff_h_pvs_inverse_construct_conditionpositivepositive + S (dst_positive_inverse_construct_conditionpositive) = S ((S (1)) * dst_positive_scale_inverse_construct_conditionpositive)) /\ exists ff_q_pvs_inverse_construct_conditionpositivepositive. dst_positive_code_inverse_construct_conditionpositive = ff_q_pvs_inverse_construct_conditionpositivepositive * S ((S (1)) * dst_positive_scale_inverse_construct_conditionpositive) + (dst_positive_inverse_construct_conditionpositive))) /\ (((((exists ff_h_pvs_inverse_construct_conditionpositivenegative. ff_h_pvs_inverse_construct_conditionpositivenegative + S (dst_negative_inverse_construct_conditionpositive) = S ((S (1)) * dst_negative_scale_inverse_construct_conditionpositive)) /\ exists ff_q_pvs_inverse_construct_conditionpositivenegative. dst_negative_code_inverse_construct_conditionpositive = ff_q_pvs_inverse_construct_conditionpositivenegative * S ((S (1)) * dst_negative_scale_inverse_construct_conditionpositive) + (dst_negative_inverse_construct_conditionpositive))) /\ (exists ge_balance_positive_inverse_construct_conditionpositivevalue ge_balance_negative_inverse_construct_conditionpositivevalue. (((((2) = 2 * (ge_balance_positive_inverse_construct_conditionpositivevalue) /\ (ge_balance_negative_inverse_construct_conditionpositivevalue) = 0) \/ exists ge_signed_half_inverse_construct_conditionpositivevaluedecode. (((2) = 2 * ge_signed_half_inverse_construct_conditionpositivevaluedecode + 1 /\ (ge_balance_positive_inverse_construct_conditionpositivevalue) = 0) /\ (ge_balance_negative_inverse_construct_conditionpositivevalue) = S ge_signed_half_inverse_construct_conditionpositivevaluedecode))) /\ ((dst_positive_inverse_construct_conditionpositive) + ge_balance_negative_inverse_construct_conditionpositivevalue = (dst_negative_inverse_construct_conditionpositive) + ge_balance_positive_inverse_construct_conditionpositivevalue))))))))) \/ (exists dst_positive_code_inverse_construct_conditionnegative dst_positive_scale_inverse_construct_conditionnegative dst_negative_code_inverse_construct_conditionnegative dst_negative_scale_inverse_construct_conditionnegative dst_positive_inverse_construct_conditionnegative dst_negative_inverse_construct_conditionnegative. (((F) = (((((dst_positive_code_inverse_construct_conditionnegative) + (dst_positive_scale_inverse_construct_conditionnegative)) * S ((dst_positive_code_inverse_construct_conditionnegative) + (dst_positive_scale_inverse_construct_conditionnegative)) + ((dst_positive_scale_inverse_construct_conditionnegative) + (dst_positive_scale_inverse_construct_conditionnegative))) + (((dst_negative_code_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)) * S ((dst_negative_code_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)) + ((dst_negative_scale_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)))) * S ((((dst_positive_code_inverse_construct_conditionnegative) + (dst_positive_scale_inverse_construct_conditionnegative)) * S ((dst_positive_code_inverse_construct_conditionnegative) + (dst_positive_scale_inverse_construct_conditionnegative)) + ((dst_positive_scale_inverse_construct_conditionnegative) + (dst_positive_scale_inverse_construct_conditionnegative))) + (((dst_negative_code_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)) * S ((dst_negative_code_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)) + ((dst_negative_scale_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)))) + ((((dst_negative_code_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)) * S ((dst_negative_code_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)) + ((dst_negative_scale_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative))) + (((dst_negative_code_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)) * S ((dst_negative_code_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)) + ((dst_negative_scale_inverse_construct_conditionnegative) + (dst_negative_scale_inverse_construct_conditionnegative)))))) /\ (((((exists ff_h_pvs_inverse_construct_conditionnegativepositive. ff_h_pvs_inverse_construct_conditionnegativepositive + S (dst_positive_inverse_construct_conditionnegative) = S ((S (1)) * dst_positive_scale_inverse_construct_conditionnegative)) /\ exists ff_q_pvs_inverse_construct_conditionnegativepositive. dst_positive_code_inverse_construct_conditionnegative = ff_q_pvs_inverse_construct_conditionnegativepositive * S ((S (1)) * dst_positive_scale_inverse_construct_conditionnegative) + (dst_positive_inverse_construct_conditionnegative))) /\ (((((exists ff_h_pvs_inverse_construct_conditionnegativenegative. ff_h_pvs_inverse_construct_conditionnegativenegative + S (dst_negative_inverse_construct_conditionnegative) = S ((S (1)) * dst_negative_scale_inverse_construct_conditionnegative)) /\ exists ff_q_pvs_inverse_construct_conditionnegativenegative. dst_negative_code_inverse_construct_conditionnegative = ff_q_pvs_inverse_construct_conditionnegativenegative * S ((S (1)) * dst_negative_scale_inverse_construct_conditionnegative) + (dst_negative_inverse_construct_conditionnegative))) /\ (exists ge_balance_positive_inverse_construct_conditionnegativevalue ge_balance_negative_inverse_construct_conditionnegativevalue. (((((1) = 2 * (ge_balance_positive_inverse_construct_conditionnegativevalue) /\ (ge_balance_negative_inverse_construct_conditionnegativevalue) = 0) \/ exists ge_signed_half_inverse_construct_conditionnegativevaluedecode. (((1) = 2 * ge_signed_half_inverse_construct_conditionnegativevaluedecode + 1 /\ (ge_balance_positive_inverse_construct_conditionnegativevalue) = 0) /\ (ge_balance_negative_inverse_construct_conditionnegativevalue) = S ge_signed_half_inverse_construct_conditionnegativevaluedecode))) /\ ((dst_positive_inverse_construct_conditionnegative) + ge_balance_negative_inverse_construct_conditionnegativevalue = (dst_negative_inverse_construct_conditionnegative) + ge_balance_positive_inverse_construct_conditionnegativevalue))))))))))) -> exists G. ((exists di_delta_inverse_construct_result. ((((exists dst_positive_code_inverse_construct_resultdeltatable dst_positive_scale_inverse_construct_resultdeltatable dst_negative_code_inverse_construct_resultdeltatable dst_negative_scale_inverse_construct_resultdeltatable. (((di_delta_inverse_construct_result) = (((((dst_positive_code_inverse_construct_resultdeltatable) + (dst_positive_scale_inverse_construct_resultdeltatable)) * S ((dst_positive_code_inverse_construct_resultdeltatable) + (dst_positive_scale_inverse_construct_resultdeltatable)) + ((dst_positive_scale_inverse_construct_resultdeltatable) + (dst_positive_scale_inverse_construct_resultdeltatable))) + (((dst_negative_code_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)) * S ((dst_negative_code_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)) + ((dst_negative_scale_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)))) * S ((((dst_positive_code_inverse_construct_resultdeltatable) + (dst_positive_scale_inverse_construct_resultdeltatable)) * S ((dst_positive_code_inverse_construct_resultdeltatable) + (dst_positive_scale_inverse_construct_resultdeltatable)) + ((dst_positive_scale_inverse_construct_resultdeltatable) + (dst_positive_scale_inverse_construct_resultdeltatable))) + (((dst_negative_code_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)) * S ((dst_negative_code_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)) + ((dst_negative_scale_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)))) + ((((dst_negative_code_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)) * S ((dst_negative_code_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)) + ((dst_negative_scale_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable))) + (((dst_negative_code_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)) * S ((dst_negative_code_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)) + ((dst_negative_scale_inverse_construct_resultdeltatable) + (dst_negative_scale_inverse_construct_resultdeltatable)))))) /\ (forall dst_index_inverse_construct_resultdeltatable. (exists pvs_le_gap_inverse_construct_resultdeltatabledomain. pvs_le_gap_inverse_construct_resultdeltatabledomain + (dst_index_inverse_construct_resultdeltatable) = (N)) -> exists dst_positive_inverse_construct_resultdeltatable dst_negative_inverse_construct_resultdeltatable dst_value_inverse_construct_resultdeltatable. ((((exists ff_h_pvs_inverse_construct_resultdeltatableentrypositive. ff_h_pvs_inverse_construct_resultdeltatableentrypositive + S (dst_positive_inverse_construct_resultdeltatable) = S ((S (dst_index_inverse_construct_resultdeltatable)) * dst_positive_scale_inverse_construct_resultdeltatable)) /\ exists ff_q_pvs_inverse_construct_resultdeltatableentrypositive. dst_positive_code_inverse_construct_resultdeltatable = ff_q_pvs_inverse_construct_resultdeltatableentrypositive * S ((S (dst_index_inverse_construct_resultdeltatable)) * dst_positive_scale_inverse_construct_resultdeltatable) + (dst_positive_inverse_construct_resultdeltatable))) /\ (((((exists ff_h_pvs_inverse_construct_resultdeltatableentrynegative. ff_h_pvs_inverse_construct_resultdeltatableentrynegative + S (dst_negative_inverse_construct_resultdeltatable) = S ((S (dst_index_inverse_construct_resultdeltatable)) * dst_negative_scale_inverse_construct_resultdeltatable)) /\ exists ff_q_pvs_inverse_construct_resultdeltatableentrynegative. dst_negative_code_inverse_construct_resultdeltatable = ff_q_pvs_inverse_construct_resultdeltatableentrynegative * S ((S (dst_index_inverse_construct_resultdeltatable)) * dst_negative_scale_inverse_construct_resultdeltatable) + (dst_negative_inverse_construct_resultdeltatable))) /\ (exists ge_balance_positive_inverse_construct_resultdeltatableentryvalue ge_balance_negative_inverse_construct_resultdeltatableentryvalue. (((((dst_value_inverse_construct_resultdeltatable) = 2 * (ge_balance_positive_inverse_construct_resultdeltatableentryvalue) /\ (ge_balance_negative_inverse_construct_resultdeltatableentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultdeltatableentryvaluedecode. (((dst_value_inverse_construct_resultdeltatable) = 2 * ge_signed_half_inverse_construct_resultdeltatableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultdeltatableentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultdeltatableentryvalue) = S ge_signed_half_inverse_construct_resultdeltatableentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultdeltatable) + ge_balance_negative_inverse_construct_resultdeltatableentryvalue = (dst_negative_inverse_construct_resultdeltatable) + ge_balance_positive_inverse_construct_resultdeltatableentryvalue))))))))) /\ (forall du_index_inverse_construct_resultdelta du_value_inverse_construct_resultdelta. ~(du_index_inverse_construct_resultdelta=0) -> (exists pvs_le_gap_inverse_construct_resultdeltabound. pvs_le_gap_inverse_construct_resultdeltabound + (du_index_inverse_construct_resultdelta) = (N)) -> (exists dst_positive_code_inverse_construct_resultdeltaentry dst_positive_scale_inverse_construct_resultdeltaentry dst_negative_code_inverse_construct_resultdeltaentry dst_negative_scale_inverse_construct_resultdeltaentry dst_positive_inverse_construct_resultdeltaentry dst_negative_inverse_construct_resultdeltaentry. (((di_delta_inverse_construct_result) = (((((dst_positive_code_inverse_construct_resultdeltaentry) + (dst_positive_scale_inverse_construct_resultdeltaentry)) * S ((dst_positive_code_inverse_construct_resultdeltaentry) + (dst_positive_scale_inverse_construct_resultdeltaentry)) + ((dst_positive_scale_inverse_construct_resultdeltaentry) + (dst_positive_scale_inverse_construct_resultdeltaentry))) + (((dst_negative_code_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)) * S ((dst_negative_code_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)) + ((dst_negative_scale_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)))) * S ((((dst_positive_code_inverse_construct_resultdeltaentry) + (dst_positive_scale_inverse_construct_resultdeltaentry)) * S ((dst_positive_code_inverse_construct_resultdeltaentry) + (dst_positive_scale_inverse_construct_resultdeltaentry)) + ((dst_positive_scale_inverse_construct_resultdeltaentry) + (dst_positive_scale_inverse_construct_resultdeltaentry))) + (((dst_negative_code_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)) * S ((dst_negative_code_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)) + ((dst_negative_scale_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)))) + ((((dst_negative_code_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)) * S ((dst_negative_code_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)) + ((dst_negative_scale_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry))) + (((dst_negative_code_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)) * S ((dst_negative_code_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)) + ((dst_negative_scale_inverse_construct_resultdeltaentry) + (dst_negative_scale_inverse_construct_resultdeltaentry)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultdeltaentrypositive. ff_h_pvs_inverse_construct_resultdeltaentrypositive + S (dst_positive_inverse_construct_resultdeltaentry) = S ((S (du_index_inverse_construct_resultdelta)) * dst_positive_scale_inverse_construct_resultdeltaentry)) /\ exists ff_q_pvs_inverse_construct_resultdeltaentrypositive. dst_positive_code_inverse_construct_resultdeltaentry = ff_q_pvs_inverse_construct_resultdeltaentrypositive * S ((S (du_index_inverse_construct_resultdelta)) * dst_positive_scale_inverse_construct_resultdeltaentry) + (dst_positive_inverse_construct_resultdeltaentry))) /\ (((((exists ff_h_pvs_inverse_construct_resultdeltaentrynegative. ff_h_pvs_inverse_construct_resultdeltaentrynegative + S (dst_negative_inverse_construct_resultdeltaentry) = S ((S (du_index_inverse_construct_resultdelta)) * dst_negative_scale_inverse_construct_resultdeltaentry)) /\ exists ff_q_pvs_inverse_construct_resultdeltaentrynegative. dst_negative_code_inverse_construct_resultdeltaentry = ff_q_pvs_inverse_construct_resultdeltaentrynegative * S ((S (du_index_inverse_construct_resultdelta)) * dst_negative_scale_inverse_construct_resultdeltaentry) + (dst_negative_inverse_construct_resultdeltaentry))) /\ (exists ge_balance_positive_inverse_construct_resultdeltaentryvalue ge_balance_negative_inverse_construct_resultdeltaentryvalue. (((((du_value_inverse_construct_resultdelta) = 2 * (ge_balance_positive_inverse_construct_resultdeltaentryvalue) /\ (ge_balance_negative_inverse_construct_resultdeltaentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultdeltaentryvaluedecode. (((du_value_inverse_construct_resultdelta) = 2 * ge_signed_half_inverse_construct_resultdeltaentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultdeltaentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultdeltaentryvalue) = S ge_signed_half_inverse_construct_resultdeltaentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultdeltaentry) + ge_balance_negative_inverse_construct_resultdeltaentryvalue = (dst_negative_inverse_construct_resultdeltaentry) + ge_balance_positive_inverse_construct_resultdeltaentryvalue))))))))) -> ((((du_index_inverse_construct_resultdelta)=1 -> (du_value_inverse_construct_resultdelta)=2) /\ (~((du_index_inverse_construct_resultdelta)=1) -> (du_value_inverse_construct_resultdelta)=0)))))) /\ (((((exists dst_positive_code_inverse_construct_resultleftleft dst_positive_scale_inverse_construct_resultleftleft dst_negative_code_inverse_construct_resultleftleft dst_negative_scale_inverse_construct_resultleftleft. (((F) = (((((dst_positive_code_inverse_construct_resultleftleft) + (dst_positive_scale_inverse_construct_resultleftleft)) * S ((dst_positive_code_inverse_construct_resultleftleft) + (dst_positive_scale_inverse_construct_resultleftleft)) + ((dst_positive_scale_inverse_construct_resultleftleft) + (dst_positive_scale_inverse_construct_resultleftleft))) + (((dst_negative_code_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)) * S ((dst_negative_code_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)) + ((dst_negative_scale_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)))) * S ((((dst_positive_code_inverse_construct_resultleftleft) + (dst_positive_scale_inverse_construct_resultleftleft)) * S ((dst_positive_code_inverse_construct_resultleftleft) + (dst_positive_scale_inverse_construct_resultleftleft)) + ((dst_positive_scale_inverse_construct_resultleftleft) + (dst_positive_scale_inverse_construct_resultleftleft))) + (((dst_negative_code_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)) * S ((dst_negative_code_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)) + ((dst_negative_scale_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)))) + ((((dst_negative_code_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)) * S ((dst_negative_code_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)) + ((dst_negative_scale_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft))) + (((dst_negative_code_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)) * S ((dst_negative_code_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)) + ((dst_negative_scale_inverse_construct_resultleftleft) + (dst_negative_scale_inverse_construct_resultleftleft)))))) /\ (forall dst_index_inverse_construct_resultleftleft. (exists pvs_le_gap_inverse_construct_resultleftleftdomain. pvs_le_gap_inverse_construct_resultleftleftdomain + (dst_index_inverse_construct_resultleftleft) = (N)) -> exists dst_positive_inverse_construct_resultleftleft dst_negative_inverse_construct_resultleftleft dst_value_inverse_construct_resultleftleft. ((((exists ff_h_pvs_inverse_construct_resultleftleftentrypositive. ff_h_pvs_inverse_construct_resultleftleftentrypositive + S (dst_positive_inverse_construct_resultleftleft) = S ((S (dst_index_inverse_construct_resultleftleft)) * dst_positive_scale_inverse_construct_resultleftleft)) /\ exists ff_q_pvs_inverse_construct_resultleftleftentrypositive. dst_positive_code_inverse_construct_resultleftleft = ff_q_pvs_inverse_construct_resultleftleftentrypositive * S ((S (dst_index_inverse_construct_resultleftleft)) * dst_positive_scale_inverse_construct_resultleftleft) + (dst_positive_inverse_construct_resultleftleft))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftleftentrynegative. ff_h_pvs_inverse_construct_resultleftleftentrynegative + S (dst_negative_inverse_construct_resultleftleft) = S ((S (dst_index_inverse_construct_resultleftleft)) * dst_negative_scale_inverse_construct_resultleftleft)) /\ exists ff_q_pvs_inverse_construct_resultleftleftentrynegative. dst_negative_code_inverse_construct_resultleftleft = ff_q_pvs_inverse_construct_resultleftleftentrynegative * S ((S (dst_index_inverse_construct_resultleftleft)) * dst_negative_scale_inverse_construct_resultleftleft) + (dst_negative_inverse_construct_resultleftleft))) /\ (exists ge_balance_positive_inverse_construct_resultleftleftentryvalue ge_balance_negative_inverse_construct_resultleftleftentryvalue. (((((dst_value_inverse_construct_resultleftleft) = 2 * (ge_balance_positive_inverse_construct_resultleftleftentryvalue) /\ (ge_balance_negative_inverse_construct_resultleftleftentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultleftleftentryvaluedecode. (((dst_value_inverse_construct_resultleftleft) = 2 * ge_signed_half_inverse_construct_resultleftleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultleftleftentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultleftleftentryvalue) = S ge_signed_half_inverse_construct_resultleftleftentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultleftleft) + ge_balance_negative_inverse_construct_resultleftleftentryvalue = (dst_negative_inverse_construct_resultleftleft) + ge_balance_positive_inverse_construct_resultleftleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_construct_resultleftright dst_positive_scale_inverse_construct_resultleftright dst_negative_code_inverse_construct_resultleftright dst_negative_scale_inverse_construct_resultleftright. (((G) = (((((dst_positive_code_inverse_construct_resultleftright) + (dst_positive_scale_inverse_construct_resultleftright)) * S ((dst_positive_code_inverse_construct_resultleftright) + (dst_positive_scale_inverse_construct_resultleftright)) + ((dst_positive_scale_inverse_construct_resultleftright) + (dst_positive_scale_inverse_construct_resultleftright))) + (((dst_negative_code_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)) * S ((dst_negative_code_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)) + ((dst_negative_scale_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)))) * S ((((dst_positive_code_inverse_construct_resultleftright) + (dst_positive_scale_inverse_construct_resultleftright)) * S ((dst_positive_code_inverse_construct_resultleftright) + (dst_positive_scale_inverse_construct_resultleftright)) + ((dst_positive_scale_inverse_construct_resultleftright) + (dst_positive_scale_inverse_construct_resultleftright))) + (((dst_negative_code_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)) * S ((dst_negative_code_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)) + ((dst_negative_scale_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)))) + ((((dst_negative_code_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)) * S ((dst_negative_code_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)) + ((dst_negative_scale_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright))) + (((dst_negative_code_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)) * S ((dst_negative_code_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)) + ((dst_negative_scale_inverse_construct_resultleftright) + (dst_negative_scale_inverse_construct_resultleftright)))))) /\ (forall dst_index_inverse_construct_resultleftright. (exists pvs_le_gap_inverse_construct_resultleftrightdomain. pvs_le_gap_inverse_construct_resultleftrightdomain + (dst_index_inverse_construct_resultleftright) = (N)) -> exists dst_positive_inverse_construct_resultleftright dst_negative_inverse_construct_resultleftright dst_value_inverse_construct_resultleftright. ((((exists ff_h_pvs_inverse_construct_resultleftrightentrypositive. ff_h_pvs_inverse_construct_resultleftrightentrypositive + S (dst_positive_inverse_construct_resultleftright) = S ((S (dst_index_inverse_construct_resultleftright)) * dst_positive_scale_inverse_construct_resultleftright)) /\ exists ff_q_pvs_inverse_construct_resultleftrightentrypositive. dst_positive_code_inverse_construct_resultleftright = ff_q_pvs_inverse_construct_resultleftrightentrypositive * S ((S (dst_index_inverse_construct_resultleftright)) * dst_positive_scale_inverse_construct_resultleftright) + (dst_positive_inverse_construct_resultleftright))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftrightentrynegative. ff_h_pvs_inverse_construct_resultleftrightentrynegative + S (dst_negative_inverse_construct_resultleftright) = S ((S (dst_index_inverse_construct_resultleftright)) * dst_negative_scale_inverse_construct_resultleftright)) /\ exists ff_q_pvs_inverse_construct_resultleftrightentrynegative. dst_negative_code_inverse_construct_resultleftright = ff_q_pvs_inverse_construct_resultleftrightentrynegative * S ((S (dst_index_inverse_construct_resultleftright)) * dst_negative_scale_inverse_construct_resultleftright) + (dst_negative_inverse_construct_resultleftright))) /\ (exists ge_balance_positive_inverse_construct_resultleftrightentryvalue ge_balance_negative_inverse_construct_resultleftrightentryvalue. (((((dst_value_inverse_construct_resultleftright) = 2 * (ge_balance_positive_inverse_construct_resultleftrightentryvalue) /\ (ge_balance_negative_inverse_construct_resultleftrightentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultleftrightentryvaluedecode. (((dst_value_inverse_construct_resultleftright) = 2 * ge_signed_half_inverse_construct_resultleftrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultleftrightentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultleftrightentryvalue) = S ge_signed_half_inverse_construct_resultleftrightentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultleftright) + ge_balance_negative_inverse_construct_resultleftrightentryvalue = (dst_negative_inverse_construct_resultleftright) + ge_balance_positive_inverse_construct_resultleftrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_construct_resultlefttable dst_positive_scale_inverse_construct_resultlefttable dst_negative_code_inverse_construct_resultlefttable dst_negative_scale_inverse_construct_resultlefttable. (((di_delta_inverse_construct_result) = (((((dst_positive_code_inverse_construct_resultlefttable) + (dst_positive_scale_inverse_construct_resultlefttable)) * S ((dst_positive_code_inverse_construct_resultlefttable) + (dst_positive_scale_inverse_construct_resultlefttable)) + ((dst_positive_scale_inverse_construct_resultlefttable) + (dst_positive_scale_inverse_construct_resultlefttable))) + (((dst_negative_code_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)) * S ((dst_negative_code_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)) + ((dst_negative_scale_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)))) * S ((((dst_positive_code_inverse_construct_resultlefttable) + (dst_positive_scale_inverse_construct_resultlefttable)) * S ((dst_positive_code_inverse_construct_resultlefttable) + (dst_positive_scale_inverse_construct_resultlefttable)) + ((dst_positive_scale_inverse_construct_resultlefttable) + (dst_positive_scale_inverse_construct_resultlefttable))) + (((dst_negative_code_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)) * S ((dst_negative_code_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)) + ((dst_negative_scale_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)))) + ((((dst_negative_code_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)) * S ((dst_negative_code_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)) + ((dst_negative_scale_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable))) + (((dst_negative_code_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)) * S ((dst_negative_code_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)) + ((dst_negative_scale_inverse_construct_resultlefttable) + (dst_negative_scale_inverse_construct_resultlefttable)))))) /\ (forall dst_index_inverse_construct_resultlefttable. (exists pvs_le_gap_inverse_construct_resultlefttabledomain. pvs_le_gap_inverse_construct_resultlefttabledomain + (dst_index_inverse_construct_resultlefttable) = (N)) -> exists dst_positive_inverse_construct_resultlefttable dst_negative_inverse_construct_resultlefttable dst_value_inverse_construct_resultlefttable. ((((exists ff_h_pvs_inverse_construct_resultlefttableentrypositive. ff_h_pvs_inverse_construct_resultlefttableentrypositive + S (dst_positive_inverse_construct_resultlefttable) = S ((S (dst_index_inverse_construct_resultlefttable)) * dst_positive_scale_inverse_construct_resultlefttable)) /\ exists ff_q_pvs_inverse_construct_resultlefttableentrypositive. dst_positive_code_inverse_construct_resultlefttable = ff_q_pvs_inverse_construct_resultlefttableentrypositive * S ((S (dst_index_inverse_construct_resultlefttable)) * dst_positive_scale_inverse_construct_resultlefttable) + (dst_positive_inverse_construct_resultlefttable))) /\ (((((exists ff_h_pvs_inverse_construct_resultlefttableentrynegative. ff_h_pvs_inverse_construct_resultlefttableentrynegative + S (dst_negative_inverse_construct_resultlefttable) = S ((S (dst_index_inverse_construct_resultlefttable)) * dst_negative_scale_inverse_construct_resultlefttable)) /\ exists ff_q_pvs_inverse_construct_resultlefttableentrynegative. dst_negative_code_inverse_construct_resultlefttable = ff_q_pvs_inverse_construct_resultlefttableentrynegative * S ((S (dst_index_inverse_construct_resultlefttable)) * dst_negative_scale_inverse_construct_resultlefttable) + (dst_negative_inverse_construct_resultlefttable))) /\ (exists ge_balance_positive_inverse_construct_resultlefttableentryvalue ge_balance_negative_inverse_construct_resultlefttableentryvalue. (((((dst_value_inverse_construct_resultlefttable) = 2 * (ge_balance_positive_inverse_construct_resultlefttableentryvalue) /\ (ge_balance_negative_inverse_construct_resultlefttableentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultlefttableentryvaluedecode. (((dst_value_inverse_construct_resultlefttable) = 2 * ge_signed_half_inverse_construct_resultlefttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultlefttableentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultlefttableentryvalue) = S ge_signed_half_inverse_construct_resultlefttableentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultlefttable) + ge_balance_negative_inverse_construct_resultlefttableentryvalue = (dst_negative_inverse_construct_resultlefttable) + ge_balance_positive_inverse_construct_resultlefttableentryvalue))))))))) /\ (forall dc_input_inverse_construct_resultleft dc_output_inverse_construct_resultleft. ~(dc_input_inverse_construct_resultleft=0) -> (exists pvs_le_gap_inverse_construct_resultleftdomain. pvs_le_gap_inverse_construct_resultleftdomain + (dc_input_inverse_construct_resultleft) = (N)) -> (exists dst_positive_code_inverse_construct_resultleftlookup dst_positive_scale_inverse_construct_resultleftlookup dst_negative_code_inverse_construct_resultleftlookup dst_negative_scale_inverse_construct_resultleftlookup dst_positive_inverse_construct_resultleftlookup dst_negative_inverse_construct_resultleftlookup. (((di_delta_inverse_construct_result) = (((((dst_positive_code_inverse_construct_resultleftlookup) + (dst_positive_scale_inverse_construct_resultleftlookup)) * S ((dst_positive_code_inverse_construct_resultleftlookup) + (dst_positive_scale_inverse_construct_resultleftlookup)) + ((dst_positive_scale_inverse_construct_resultleftlookup) + (dst_positive_scale_inverse_construct_resultleftlookup))) + (((dst_negative_code_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)) * S ((dst_negative_code_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)) + ((dst_negative_scale_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)))) * S ((((dst_positive_code_inverse_construct_resultleftlookup) + (dst_positive_scale_inverse_construct_resultleftlookup)) * S ((dst_positive_code_inverse_construct_resultleftlookup) + (dst_positive_scale_inverse_construct_resultleftlookup)) + ((dst_positive_scale_inverse_construct_resultleftlookup) + (dst_positive_scale_inverse_construct_resultleftlookup))) + (((dst_negative_code_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)) * S ((dst_negative_code_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)) + ((dst_negative_scale_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)))) + ((((dst_negative_code_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)) * S ((dst_negative_code_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)) + ((dst_negative_scale_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup))) + (((dst_negative_code_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)) * S ((dst_negative_code_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)) + ((dst_negative_scale_inverse_construct_resultleftlookup) + (dst_negative_scale_inverse_construct_resultleftlookup)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftlookuppositive. ff_h_pvs_inverse_construct_resultleftlookuppositive + S (dst_positive_inverse_construct_resultleftlookup) = S ((S (dc_input_inverse_construct_resultleft)) * dst_positive_scale_inverse_construct_resultleftlookup)) /\ exists ff_q_pvs_inverse_construct_resultleftlookuppositive. dst_positive_code_inverse_construct_resultleftlookup = ff_q_pvs_inverse_construct_resultleftlookuppositive * S ((S (dc_input_inverse_construct_resultleft)) * dst_positive_scale_inverse_construct_resultleftlookup) + (dst_positive_inverse_construct_resultleftlookup))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftlookupnegative. ff_h_pvs_inverse_construct_resultleftlookupnegative + S (dst_negative_inverse_construct_resultleftlookup) = S ((S (dc_input_inverse_construct_resultleft)) * dst_negative_scale_inverse_construct_resultleftlookup)) /\ exists ff_q_pvs_inverse_construct_resultleftlookupnegative. dst_negative_code_inverse_construct_resultleftlookup = ff_q_pvs_inverse_construct_resultleftlookupnegative * S ((S (dc_input_inverse_construct_resultleft)) * dst_negative_scale_inverse_construct_resultleftlookup) + (dst_negative_inverse_construct_resultleftlookup))) /\ (exists ge_balance_positive_inverse_construct_resultleftlookupvalue ge_balance_negative_inverse_construct_resultleftlookupvalue. (((((dc_output_inverse_construct_resultleft) = 2 * (ge_balance_positive_inverse_construct_resultleftlookupvalue) /\ (ge_balance_negative_inverse_construct_resultleftlookupvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultleftlookupvaluedecode. (((dc_output_inverse_construct_resultleft) = 2 * ge_signed_half_inverse_construct_resultleftlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultleftlookupvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultleftlookupvalue) = S ge_signed_half_inverse_construct_resultleftlookupvaluedecode))) /\ ((dst_positive_inverse_construct_resultleftlookup) + ge_balance_negative_inverse_construct_resultleftlookupvalue = (dst_negative_inverse_construct_resultleftlookup) + ge_balance_positive_inverse_construct_resultleftlookupvalue))))))))) -> (((~((dc_input_inverse_construct_resultleft)=0)) /\ (exists dc_mask_inverse_construct_resultleftvalue. ((((exists dst_positive_code_inverse_construct_resultleftvaluemasktable dst_positive_scale_inverse_construct_resultleftvaluemasktable dst_negative_code_inverse_construct_resultleftvaluemasktable dst_negative_scale_inverse_construct_resultleftvaluemasktable. (((dc_mask_inverse_construct_resultleftvalue) = (((((dst_positive_code_inverse_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_construct_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_construct_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_construct_resultleftvaluemasktable))) + (((dst_negative_code_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)))) * S ((((dst_positive_code_inverse_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_construct_resultleftvaluemasktable)) * S ((dst_positive_code_inverse_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_construct_resultleftvaluemasktable)) + ((dst_positive_scale_inverse_construct_resultleftvaluemasktable) + (dst_positive_scale_inverse_construct_resultleftvaluemasktable))) + (((dst_negative_code_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)))) + ((((dst_negative_code_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable))) + (((dst_negative_code_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)) * S ((dst_negative_code_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)) + ((dst_negative_scale_inverse_construct_resultleftvaluemasktable) + (dst_negative_scale_inverse_construct_resultleftvaluemasktable)))))) /\ (forall dst_index_inverse_construct_resultleftvaluemasktable. (exists pvs_le_gap_inverse_construct_resultleftvaluemasktabledomain. pvs_le_gap_inverse_construct_resultleftvaluemasktabledomain + (dst_index_inverse_construct_resultleftvaluemasktable) = (dc_input_inverse_construct_resultleft)) -> exists dst_positive_inverse_construct_resultleftvaluemasktable dst_negative_inverse_construct_resultleftvaluemasktable dst_value_inverse_construct_resultleftvaluemasktable. ((((exists ff_h_pvs_inverse_construct_resultleftvaluemasktableentrypositive. ff_h_pvs_inverse_construct_resultleftvaluemasktableentrypositive + S (dst_positive_inverse_construct_resultleftvaluemasktable) = S ((S (dst_index_inverse_construct_resultleftvaluemasktable)) * dst_positive_scale_inverse_construct_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_construct_resultleftvaluemasktableentrypositive. dst_positive_code_inverse_construct_resultleftvaluemasktable = ff_q_pvs_inverse_construct_resultleftvaluemasktableentrypositive * S ((S (dst_index_inverse_construct_resultleftvaluemasktable)) * dst_positive_scale_inverse_construct_resultleftvaluemasktable) + (dst_positive_inverse_construct_resultleftvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftvaluemasktableentrynegative. ff_h_pvs_inverse_construct_resultleftvaluemasktableentrynegative + S (dst_negative_inverse_construct_resultleftvaluemasktable) = S ((S (dst_index_inverse_construct_resultleftvaluemasktable)) * dst_negative_scale_inverse_construct_resultleftvaluemasktable)) /\ exists ff_q_pvs_inverse_construct_resultleftvaluemasktableentrynegative. dst_negative_code_inverse_construct_resultleftvaluemasktable = ff_q_pvs_inverse_construct_resultleftvaluemasktableentrynegative * S ((S (dst_index_inverse_construct_resultleftvaluemasktable)) * dst_negative_scale_inverse_construct_resultleftvaluemasktable) + (dst_negative_inverse_construct_resultleftvaluemasktable))) /\ (exists ge_balance_positive_inverse_construct_resultleftvaluemasktableentryvalue ge_balance_negative_inverse_construct_resultleftvaluemasktableentryvalue. (((((dst_value_inverse_construct_resultleftvaluemasktable) = 2 * (ge_balance_positive_inverse_construct_resultleftvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_construct_resultleftvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultleftvaluemasktableentryvaluedecode. (((dst_value_inverse_construct_resultleftvaluemasktable) = 2 * ge_signed_half_inverse_construct_resultleftvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultleftvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultleftvaluemasktableentryvalue) = S ge_signed_half_inverse_construct_resultleftvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultleftvaluemasktable) + ge_balance_negative_inverse_construct_resultleftvaluemasktableentryvalue = (dst_negative_inverse_construct_resultleftvaluemasktable) + ge_balance_positive_inverse_construct_resultleftvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_construct_resultleftvaluemask dc_value_inverse_construct_resultleftvaluemask. (exists pvs_le_gap_inverse_construct_resultleftvaluemaskdomain. pvs_le_gap_inverse_construct_resultleftvaluemaskdomain + (dc_index_inverse_construct_resultleftvaluemask) = (dc_input_inverse_construct_resultleft)) -> (exists dst_positive_code_inverse_construct_resultleftvaluemasklookup dst_positive_scale_inverse_construct_resultleftvaluemasklookup dst_negative_code_inverse_construct_resultleftvaluemasklookup dst_negative_scale_inverse_construct_resultleftvaluemasklookup dst_positive_inverse_construct_resultleftvaluemasklookup dst_negative_inverse_construct_resultleftvaluemasklookup. (((dc_mask_inverse_construct_resultleftvalue) = (((((dst_positive_code_inverse_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_construct_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_construct_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_construct_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)))) * S ((((dst_positive_code_inverse_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_construct_resultleftvaluemasklookup)) * S ((dst_positive_code_inverse_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_construct_resultleftvaluemasklookup)) + ((dst_positive_scale_inverse_construct_resultleftvaluemasklookup) + (dst_positive_scale_inverse_construct_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)))) + ((((dst_negative_code_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup))) + (((dst_negative_code_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) * S ((dst_negative_code_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) + ((dst_negative_scale_inverse_construct_resultleftvaluemasklookup) + (dst_negative_scale_inverse_construct_resultleftvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftvaluemasklookuppositive. ff_h_pvs_inverse_construct_resultleftvaluemasklookuppositive + S (dst_positive_inverse_construct_resultleftvaluemasklookup) = S ((S (dc_index_inverse_construct_resultleftvaluemask)) * dst_positive_scale_inverse_construct_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_construct_resultleftvaluemasklookuppositive. dst_positive_code_inverse_construct_resultleftvaluemasklookup = ff_q_pvs_inverse_construct_resultleftvaluemasklookuppositive * S ((S (dc_index_inverse_construct_resultleftvaluemask)) * dst_positive_scale_inverse_construct_resultleftvaluemasklookup) + (dst_positive_inverse_construct_resultleftvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftvaluemasklookupnegative. ff_h_pvs_inverse_construct_resultleftvaluemasklookupnegative + S (dst_negative_inverse_construct_resultleftvaluemasklookup) = S ((S (dc_index_inverse_construct_resultleftvaluemask)) * dst_negative_scale_inverse_construct_resultleftvaluemasklookup)) /\ exists ff_q_pvs_inverse_construct_resultleftvaluemasklookupnegative. dst_negative_code_inverse_construct_resultleftvaluemasklookup = ff_q_pvs_inverse_construct_resultleftvaluemasklookupnegative * S ((S (dc_index_inverse_construct_resultleftvaluemask)) * dst_negative_scale_inverse_construct_resultleftvaluemasklookup) + (dst_negative_inverse_construct_resultleftvaluemasklookup))) /\ (exists ge_balance_positive_inverse_construct_resultleftvaluemasklookupvalue ge_balance_negative_inverse_construct_resultleftvaluemasklookupvalue. (((((dc_value_inverse_construct_resultleftvaluemask) = 2 * (ge_balance_positive_inverse_construct_resultleftvaluemasklookupvalue) /\ (ge_balance_negative_inverse_construct_resultleftvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultleftvaluemasklookupvaluedecode. (((dc_value_inverse_construct_resultleftvaluemask) = 2 * ge_signed_half_inverse_construct_resultleftvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultleftvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultleftvaluemasklookupvalue) = S ge_signed_half_inverse_construct_resultleftvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_construct_resultleftvaluemasklookup) + ge_balance_negative_inverse_construct_resultleftvaluemasklookupvalue = (dst_negative_inverse_construct_resultleftvaluemasklookup) + ge_balance_positive_inverse_construct_resultleftvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_construct_resultleftvaluemask)=0)) /\ (exists dc_quotient_inverse_construct_resultleftvaluemaskentry dc_left_inverse_construct_resultleftvaluemaskentry dc_right_inverse_construct_resultleftvaluemaskentry. (((dc_input_inverse_construct_resultleft)=(dc_index_inverse_construct_resultleftvaluemask)*dc_quotient_inverse_construct_resultleftvaluemaskentry) /\ (((exists dst_positive_code_inverse_construct_resultleftvaluemaskentryleft dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft dst_negative_code_inverse_construct_resultleftvaluemaskentryleft dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft dst_positive_inverse_construct_resultleftvaluemaskentryleft dst_negative_inverse_construct_resultleftvaluemaskentryleft. (((F) = (((((dst_positive_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft)) * S ((dst_positive_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft)) + ((dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)))) + ((((dst_negative_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft))) + (((dst_negative_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) * S ((dst_negative_code_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) + ((dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftvaluemaskentryleftpositive. ff_h_pvs_inverse_construct_resultleftvaluemaskentryleftpositive + S (dst_positive_inverse_construct_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_construct_resultleftvaluemask)) * dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_construct_resultleftvaluemaskentryleftpositive. dst_positive_code_inverse_construct_resultleftvaluemaskentryleft = ff_q_pvs_inverse_construct_resultleftvaluemaskentryleftpositive * S ((S (dc_index_inverse_construct_resultleftvaluemask)) * dst_positive_scale_inverse_construct_resultleftvaluemaskentryleft) + (dst_positive_inverse_construct_resultleftvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftvaluemaskentryleftnegative. ff_h_pvs_inverse_construct_resultleftvaluemaskentryleftnegative + S (dst_negative_inverse_construct_resultleftvaluemaskentryleft) = S ((S (dc_index_inverse_construct_resultleftvaluemask)) * dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_construct_resultleftvaluemaskentryleftnegative. dst_negative_code_inverse_construct_resultleftvaluemaskentryleft = ff_q_pvs_inverse_construct_resultleftvaluemaskentryleftnegative * S ((S (dc_index_inverse_construct_resultleftvaluemask)) * dst_negative_scale_inverse_construct_resultleftvaluemaskentryleft) + (dst_negative_inverse_construct_resultleftvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_construct_resultleftvaluemaskentryleftvalue ge_balance_negative_inverse_construct_resultleftvaluemaskentryleftvalue. (((((dc_left_inverse_construct_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_construct_resultleftvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_construct_resultleftvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultleftvaluemaskentryleftvaluedecode. (((dc_left_inverse_construct_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_construct_resultleftvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultleftvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultleftvaluemaskentryleftvalue) = S ge_signed_half_inverse_construct_resultleftvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_construct_resultleftvaluemaskentryleft) + ge_balance_negative_inverse_construct_resultleftvaluemaskentryleftvalue = (dst_negative_inverse_construct_resultleftvaluemaskentryleft) + ge_balance_positive_inverse_construct_resultleftvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_construct_resultleftvaluemaskentryright dst_positive_scale_inverse_construct_resultleftvaluemaskentryright dst_negative_code_inverse_construct_resultleftvaluemaskentryright dst_negative_scale_inverse_construct_resultleftvaluemaskentryright dst_positive_inverse_construct_resultleftvaluemaskentryright dst_negative_inverse_construct_resultleftvaluemaskentryright. (((G) = (((((dst_positive_code_inverse_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)))) * S ((((dst_positive_code_inverse_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryright)) * S ((dst_positive_code_inverse_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryright)) + ((dst_positive_scale_inverse_construct_resultleftvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)))) + ((((dst_negative_code_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright))) + (((dst_negative_code_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) * S ((dst_negative_code_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) + ((dst_negative_scale_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftvaluemaskentryrightpositive. ff_h_pvs_inverse_construct_resultleftvaluemaskentryrightpositive + S (dst_positive_inverse_construct_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_construct_resultleftvaluemaskentry)) * dst_positive_scale_inverse_construct_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_construct_resultleftvaluemaskentryrightpositive. dst_positive_code_inverse_construct_resultleftvaluemaskentryright = ff_q_pvs_inverse_construct_resultleftvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_construct_resultleftvaluemaskentry)) * dst_positive_scale_inverse_construct_resultleftvaluemaskentryright) + (dst_positive_inverse_construct_resultleftvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_construct_resultleftvaluemaskentryrightnegative. ff_h_pvs_inverse_construct_resultleftvaluemaskentryrightnegative + S (dst_negative_inverse_construct_resultleftvaluemaskentryright) = S ((S (dc_quotient_inverse_construct_resultleftvaluemaskentry)) * dst_negative_scale_inverse_construct_resultleftvaluemaskentryright)) /\ exists ff_q_pvs_inverse_construct_resultleftvaluemaskentryrightnegative. dst_negative_code_inverse_construct_resultleftvaluemaskentryright = ff_q_pvs_inverse_construct_resultleftvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_construct_resultleftvaluemaskentry)) * dst_negative_scale_inverse_construct_resultleftvaluemaskentryright) + (dst_negative_inverse_construct_resultleftvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_construct_resultleftvaluemaskentryrightvalue ge_balance_negative_inverse_construct_resultleftvaluemaskentryrightvalue. (((((dc_right_inverse_construct_resultleftvaluemaskentry) = 2 * (ge_balance_positive_inverse_construct_resultleftvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_construct_resultleftvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultleftvaluemaskentryrightvaluedecode. (((dc_right_inverse_construct_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_construct_resultleftvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultleftvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultleftvaluemaskentryrightvalue) = S ge_signed_half_inverse_construct_resultleftvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_construct_resultleftvaluemaskentryright) + ge_balance_negative_inverse_construct_resultleftvaluemaskentryrightvalue = (dst_negative_inverse_construct_resultleftvaluemaskentryright) + ge_balance_positive_inverse_construct_resultleftvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_construct_resultleftvaluemaskentryproduct sto_an_inverse_construct_resultleftvaluemaskentryproduct sto_bp_inverse_construct_resultleftvaluemaskentryproduct sto_bn_inverse_construct_resultleftvaluemaskentryproduct sto_cp_inverse_construct_resultleftvaluemaskentryproduct sto_cn_inverse_construct_resultleftvaluemaskentryproduct. (((((dc_left_inverse_construct_resultleftvaluemaskentry) = 2 * (sto_ap_inverse_construct_resultleftvaluemaskentryproduct) /\ (sto_an_inverse_construct_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_construct_resultleftvaluemaskentryproductleft. (((dc_left_inverse_construct_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_construct_resultleftvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_construct_resultleftvaluemaskentryproduct) = 0) /\ (sto_an_inverse_construct_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_construct_resultleftvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_construct_resultleftvaluemaskentry) = 2 * (sto_bp_inverse_construct_resultleftvaluemaskentryproduct) /\ (sto_bn_inverse_construct_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_construct_resultleftvaluemaskentryproductright. (((dc_right_inverse_construct_resultleftvaluemaskentry) = 2 * ge_signed_half_inverse_construct_resultleftvaluemaskentryproductright + 1 /\ (sto_bp_inverse_construct_resultleftvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_construct_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_construct_resultleftvaluemaskentryproductright))) /\ ((((((dc_value_inverse_construct_resultleftvaluemask) = 2 * (sto_cp_inverse_construct_resultleftvaluemaskentryproduct) /\ (sto_cn_inverse_construct_resultleftvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_construct_resultleftvaluemaskentryproductoutput. (((dc_value_inverse_construct_resultleftvaluemask) = 2 * ge_signed_half_inverse_construct_resultleftvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_construct_resultleftvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_construct_resultleftvaluemaskentryproduct) = S ge_signed_half_inverse_construct_resultleftvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_construct_resultleftvaluemaskentryproduct * sto_bp_inverse_construct_resultleftvaluemaskentryproduct + sto_an_inverse_construct_resultleftvaluemaskentryproduct * sto_bn_inverse_construct_resultleftvaluemaskentryproduct) + sto_cn_inverse_construct_resultleftvaluemaskentryproduct = (sto_ap_inverse_construct_resultleftvaluemaskentryproduct * sto_bn_inverse_construct_resultleftvaluemaskentryproduct + sto_an_inverse_construct_resultleftvaluemaskentryproduct * sto_bp_inverse_construct_resultleftvaluemaskentryproduct) + sto_cp_inverse_construct_resultleftvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_construct_resultleftvaluemask)=0 \/ ~(exists pvs_factor_inverse_construct_resultleftvaluemaskentrynondivisor. (dc_input_inverse_construct_resultleft) = (dc_index_inverse_construct_resultleftvaluemask) * pvs_factor_inverse_construct_resultleftvaluemaskentrynondivisor)) /\ ((dc_value_inverse_construct_resultleftvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_construct_resultleftvaluefold dst_positive_scale_inverse_construct_resultleftvaluefold dst_negative_code_inverse_construct_resultleftvaluefold dst_negative_scale_inverse_construct_resultleftvaluefold dst_positive_sum_inverse_construct_resultleftvaluefold dst_negative_sum_inverse_construct_resultleftvaluefold. (((dc_mask_inverse_construct_resultleftvalue) = (((((dst_positive_code_inverse_construct_resultleftvaluefold) + (dst_positive_scale_inverse_construct_resultleftvaluefold)) * S ((dst_positive_code_inverse_construct_resultleftvaluefold) + (dst_positive_scale_inverse_construct_resultleftvaluefold)) + ((dst_positive_scale_inverse_construct_resultleftvaluefold) + (dst_positive_scale_inverse_construct_resultleftvaluefold))) + (((dst_negative_code_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)) * S ((dst_negative_code_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)) + ((dst_negative_scale_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)))) * S ((((dst_positive_code_inverse_construct_resultleftvaluefold) + (dst_positive_scale_inverse_construct_resultleftvaluefold)) * S ((dst_positive_code_inverse_construct_resultleftvaluefold) + (dst_positive_scale_inverse_construct_resultleftvaluefold)) + ((dst_positive_scale_inverse_construct_resultleftvaluefold) + (dst_positive_scale_inverse_construct_resultleftvaluefold))) + (((dst_negative_code_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)) * S ((dst_negative_code_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)) + ((dst_negative_scale_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)))) + ((((dst_negative_code_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)) * S ((dst_negative_code_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)) + ((dst_negative_scale_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold))) + (((dst_negative_code_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)) * S ((dst_negative_code_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)) + ((dst_negative_scale_inverse_construct_resultleftvaluefold) + (dst_negative_scale_inverse_construct_resultleftvaluefold)))))) /\ (((exists fs_u_dst_inverse_construct_resultleftvaluefoldpositive fs_v_dst_inverse_construct_resultleftvaluefoldpositive. ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_start. fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_construct_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_start. fs_u_dst_inverse_construct_resultleftvaluefoldpositive = fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_construct_resultleftvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_terminal. fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_construct_resultleftvaluefold) = S ((S (S (dc_input_inverse_construct_resultleft))) * fs_v_dst_inverse_construct_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_terminal. fs_u_dst_inverse_construct_resultleftvaluefoldpositive = fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_construct_resultleft))) * fs_v_dst_inverse_construct_resultleftvaluefoldpositive) + (dst_positive_sum_inverse_construct_resultleftvaluefold))) /\ forall fs_i_dst_inverse_construct_resultleftvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_construct_resultleftvaluefoldpositive_body_steps = S (dc_input_inverse_construct_resultleft)) -> exists fs_a_dst_inverse_construct_resultleftvaluefoldpositive_body_steps fs_r_dst_inverse_construct_resultleftvaluefoldpositive_body_steps fs_s_dst_inverse_construct_resultleftvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_construct_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_construct_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_construct_resultleftvaluefold)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_construct_resultleftvaluefold = fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_construct_resultleftvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_construct_resultleftvaluefold) + (fs_a_dst_inverse_construct_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_construct_resultleftvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_construct_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_construct_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_construct_resultleftvaluefoldpositive = fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_construct_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_construct_resultleftvaluefoldpositive) + (fs_r_dst_inverse_construct_resultleftvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_construct_resultleftvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_construct_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_construct_resultleftvaluefoldpositive)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_construct_resultleftvaluefoldpositive = fs_q_dst_inverse_construct_resultleftvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_construct_resultleftvaluefoldpositive_body_steps)) * fs_v_dst_inverse_construct_resultleftvaluefoldpositive) + (fs_s_dst_inverse_construct_resultleftvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_construct_resultleftvaluefoldpositive_body_steps = fs_r_dst_inverse_construct_resultleftvaluefoldpositive_body_steps + fs_a_dst_inverse_construct_resultleftvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_construct_resultleftvaluefoldnegative fs_v_dst_inverse_construct_resultleftvaluefoldnegative. ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_start. fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_construct_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_start. fs_u_dst_inverse_construct_resultleftvaluefoldnegative = fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_construct_resultleftvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_terminal. fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_construct_resultleftvaluefold) = S ((S (S (dc_input_inverse_construct_resultleft))) * fs_v_dst_inverse_construct_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_terminal. fs_u_dst_inverse_construct_resultleftvaluefoldnegative = fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_construct_resultleft))) * fs_v_dst_inverse_construct_resultleftvaluefoldnegative) + (dst_negative_sum_inverse_construct_resultleftvaluefold))) /\ forall fs_i_dst_inverse_construct_resultleftvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_construct_resultleftvaluefoldnegative_body_steps = S (dc_input_inverse_construct_resultleft)) -> exists fs_a_dst_inverse_construct_resultleftvaluefoldnegative_body_steps fs_r_dst_inverse_construct_resultleftvaluefoldnegative_body_steps fs_s_dst_inverse_construct_resultleftvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_construct_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_construct_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_construct_resultleftvaluefold)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_construct_resultleftvaluefold = fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_construct_resultleftvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_construct_resultleftvaluefold) + (fs_a_dst_inverse_construct_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_construct_resultleftvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_construct_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_construct_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_construct_resultleftvaluefoldnegative = fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_construct_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_construct_resultleftvaluefoldnegative) + (fs_r_dst_inverse_construct_resultleftvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_construct_resultleftvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_construct_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_construct_resultleftvaluefoldnegative)) /\ exists fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_construct_resultleftvaluefoldnegative = fs_q_dst_inverse_construct_resultleftvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_construct_resultleftvaluefoldnegative_body_steps)) * fs_v_dst_inverse_construct_resultleftvaluefoldnegative) + (fs_s_dst_inverse_construct_resultleftvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_construct_resultleftvaluefoldnegative_body_steps = fs_r_dst_inverse_construct_resultleftvaluefoldnegative_body_steps + fs_a_dst_inverse_construct_resultleftvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_construct_resultleftvaluefoldresult ge_balance_negative_inverse_construct_resultleftvaluefoldresult. (((((dc_output_inverse_construct_resultleft) = 2 * (ge_balance_positive_inverse_construct_resultleftvaluefoldresult) /\ (ge_balance_negative_inverse_construct_resultleftvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_construct_resultleftvaluefoldresultdecode. (((dc_output_inverse_construct_resultleft) = 2 * ge_signed_half_inverse_construct_resultleftvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_construct_resultleftvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_construct_resultleftvaluefoldresult) = S ge_signed_half_inverse_construct_resultleftvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_construct_resultleftvaluefold) + ge_balance_negative_inverse_construct_resultleftvaluefoldresult = (dst_negative_sum_inverse_construct_resultleftvaluefold) + ge_balance_positive_inverse_construct_resultleftvaluefoldresult)))))))))))))))))))) /\ (((exists dst_positive_code_inverse_construct_resultrightleft dst_positive_scale_inverse_construct_resultrightleft dst_negative_code_inverse_construct_resultrightleft dst_negative_scale_inverse_construct_resultrightleft. (((G) = (((((dst_positive_code_inverse_construct_resultrightleft) + (dst_positive_scale_inverse_construct_resultrightleft)) * S ((dst_positive_code_inverse_construct_resultrightleft) + (dst_positive_scale_inverse_construct_resultrightleft)) + ((dst_positive_scale_inverse_construct_resultrightleft) + (dst_positive_scale_inverse_construct_resultrightleft))) + (((dst_negative_code_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)) * S ((dst_negative_code_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)) + ((dst_negative_scale_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)))) * S ((((dst_positive_code_inverse_construct_resultrightleft) + (dst_positive_scale_inverse_construct_resultrightleft)) * S ((dst_positive_code_inverse_construct_resultrightleft) + (dst_positive_scale_inverse_construct_resultrightleft)) + ((dst_positive_scale_inverse_construct_resultrightleft) + (dst_positive_scale_inverse_construct_resultrightleft))) + (((dst_negative_code_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)) * S ((dst_negative_code_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)) + ((dst_negative_scale_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)))) + ((((dst_negative_code_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)) * S ((dst_negative_code_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)) + ((dst_negative_scale_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft))) + (((dst_negative_code_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)) * S ((dst_negative_code_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)) + ((dst_negative_scale_inverse_construct_resultrightleft) + (dst_negative_scale_inverse_construct_resultrightleft)))))) /\ (forall dst_index_inverse_construct_resultrightleft. (exists pvs_le_gap_inverse_construct_resultrightleftdomain. pvs_le_gap_inverse_construct_resultrightleftdomain + (dst_index_inverse_construct_resultrightleft) = (N)) -> exists dst_positive_inverse_construct_resultrightleft dst_negative_inverse_construct_resultrightleft dst_value_inverse_construct_resultrightleft. ((((exists ff_h_pvs_inverse_construct_resultrightleftentrypositive. ff_h_pvs_inverse_construct_resultrightleftentrypositive + S (dst_positive_inverse_construct_resultrightleft) = S ((S (dst_index_inverse_construct_resultrightleft)) * dst_positive_scale_inverse_construct_resultrightleft)) /\ exists ff_q_pvs_inverse_construct_resultrightleftentrypositive. dst_positive_code_inverse_construct_resultrightleft = ff_q_pvs_inverse_construct_resultrightleftentrypositive * S ((S (dst_index_inverse_construct_resultrightleft)) * dst_positive_scale_inverse_construct_resultrightleft) + (dst_positive_inverse_construct_resultrightleft))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightleftentrynegative. ff_h_pvs_inverse_construct_resultrightleftentrynegative + S (dst_negative_inverse_construct_resultrightleft) = S ((S (dst_index_inverse_construct_resultrightleft)) * dst_negative_scale_inverse_construct_resultrightleft)) /\ exists ff_q_pvs_inverse_construct_resultrightleftentrynegative. dst_negative_code_inverse_construct_resultrightleft = ff_q_pvs_inverse_construct_resultrightleftentrynegative * S ((S (dst_index_inverse_construct_resultrightleft)) * dst_negative_scale_inverse_construct_resultrightleft) + (dst_negative_inverse_construct_resultrightleft))) /\ (exists ge_balance_positive_inverse_construct_resultrightleftentryvalue ge_balance_negative_inverse_construct_resultrightleftentryvalue. (((((dst_value_inverse_construct_resultrightleft) = 2 * (ge_balance_positive_inverse_construct_resultrightleftentryvalue) /\ (ge_balance_negative_inverse_construct_resultrightleftentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultrightleftentryvaluedecode. (((dst_value_inverse_construct_resultrightleft) = 2 * ge_signed_half_inverse_construct_resultrightleftentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultrightleftentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultrightleftentryvalue) = S ge_signed_half_inverse_construct_resultrightleftentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultrightleft) + ge_balance_negative_inverse_construct_resultrightleftentryvalue = (dst_negative_inverse_construct_resultrightleft) + ge_balance_positive_inverse_construct_resultrightleftentryvalue))))))))) /\ (((exists dst_positive_code_inverse_construct_resultrightright dst_positive_scale_inverse_construct_resultrightright dst_negative_code_inverse_construct_resultrightright dst_negative_scale_inverse_construct_resultrightright. (((F) = (((((dst_positive_code_inverse_construct_resultrightright) + (dst_positive_scale_inverse_construct_resultrightright)) * S ((dst_positive_code_inverse_construct_resultrightright) + (dst_positive_scale_inverse_construct_resultrightright)) + ((dst_positive_scale_inverse_construct_resultrightright) + (dst_positive_scale_inverse_construct_resultrightright))) + (((dst_negative_code_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)) * S ((dst_negative_code_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)) + ((dst_negative_scale_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)))) * S ((((dst_positive_code_inverse_construct_resultrightright) + (dst_positive_scale_inverse_construct_resultrightright)) * S ((dst_positive_code_inverse_construct_resultrightright) + (dst_positive_scale_inverse_construct_resultrightright)) + ((dst_positive_scale_inverse_construct_resultrightright) + (dst_positive_scale_inverse_construct_resultrightright))) + (((dst_negative_code_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)) * S ((dst_negative_code_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)) + ((dst_negative_scale_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)))) + ((((dst_negative_code_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)) * S ((dst_negative_code_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)) + ((dst_negative_scale_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright))) + (((dst_negative_code_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)) * S ((dst_negative_code_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)) + ((dst_negative_scale_inverse_construct_resultrightright) + (dst_negative_scale_inverse_construct_resultrightright)))))) /\ (forall dst_index_inverse_construct_resultrightright. (exists pvs_le_gap_inverse_construct_resultrightrightdomain. pvs_le_gap_inverse_construct_resultrightrightdomain + (dst_index_inverse_construct_resultrightright) = (N)) -> exists dst_positive_inverse_construct_resultrightright dst_negative_inverse_construct_resultrightright dst_value_inverse_construct_resultrightright. ((((exists ff_h_pvs_inverse_construct_resultrightrightentrypositive. ff_h_pvs_inverse_construct_resultrightrightentrypositive + S (dst_positive_inverse_construct_resultrightright) = S ((S (dst_index_inverse_construct_resultrightright)) * dst_positive_scale_inverse_construct_resultrightright)) /\ exists ff_q_pvs_inverse_construct_resultrightrightentrypositive. dst_positive_code_inverse_construct_resultrightright = ff_q_pvs_inverse_construct_resultrightrightentrypositive * S ((S (dst_index_inverse_construct_resultrightright)) * dst_positive_scale_inverse_construct_resultrightright) + (dst_positive_inverse_construct_resultrightright))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightrightentrynegative. ff_h_pvs_inverse_construct_resultrightrightentrynegative + S (dst_negative_inverse_construct_resultrightright) = S ((S (dst_index_inverse_construct_resultrightright)) * dst_negative_scale_inverse_construct_resultrightright)) /\ exists ff_q_pvs_inverse_construct_resultrightrightentrynegative. dst_negative_code_inverse_construct_resultrightright = ff_q_pvs_inverse_construct_resultrightrightentrynegative * S ((S (dst_index_inverse_construct_resultrightright)) * dst_negative_scale_inverse_construct_resultrightright) + (dst_negative_inverse_construct_resultrightright))) /\ (exists ge_balance_positive_inverse_construct_resultrightrightentryvalue ge_balance_negative_inverse_construct_resultrightrightentryvalue. (((((dst_value_inverse_construct_resultrightright) = 2 * (ge_balance_positive_inverse_construct_resultrightrightentryvalue) /\ (ge_balance_negative_inverse_construct_resultrightrightentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultrightrightentryvaluedecode. (((dst_value_inverse_construct_resultrightright) = 2 * ge_signed_half_inverse_construct_resultrightrightentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultrightrightentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultrightrightentryvalue) = S ge_signed_half_inverse_construct_resultrightrightentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultrightright) + ge_balance_negative_inverse_construct_resultrightrightentryvalue = (dst_negative_inverse_construct_resultrightright) + ge_balance_positive_inverse_construct_resultrightrightentryvalue))))))))) /\ (((exists dst_positive_code_inverse_construct_resultrighttable dst_positive_scale_inverse_construct_resultrighttable dst_negative_code_inverse_construct_resultrighttable dst_negative_scale_inverse_construct_resultrighttable. (((di_delta_inverse_construct_result) = (((((dst_positive_code_inverse_construct_resultrighttable) + (dst_positive_scale_inverse_construct_resultrighttable)) * S ((dst_positive_code_inverse_construct_resultrighttable) + (dst_positive_scale_inverse_construct_resultrighttable)) + ((dst_positive_scale_inverse_construct_resultrighttable) + (dst_positive_scale_inverse_construct_resultrighttable))) + (((dst_negative_code_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)) * S ((dst_negative_code_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)) + ((dst_negative_scale_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)))) * S ((((dst_positive_code_inverse_construct_resultrighttable) + (dst_positive_scale_inverse_construct_resultrighttable)) * S ((dst_positive_code_inverse_construct_resultrighttable) + (dst_positive_scale_inverse_construct_resultrighttable)) + ((dst_positive_scale_inverse_construct_resultrighttable) + (dst_positive_scale_inverse_construct_resultrighttable))) + (((dst_negative_code_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)) * S ((dst_negative_code_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)) + ((dst_negative_scale_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)))) + ((((dst_negative_code_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)) * S ((dst_negative_code_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)) + ((dst_negative_scale_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable))) + (((dst_negative_code_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)) * S ((dst_negative_code_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)) + ((dst_negative_scale_inverse_construct_resultrighttable) + (dst_negative_scale_inverse_construct_resultrighttable)))))) /\ (forall dst_index_inverse_construct_resultrighttable. (exists pvs_le_gap_inverse_construct_resultrighttabledomain. pvs_le_gap_inverse_construct_resultrighttabledomain + (dst_index_inverse_construct_resultrighttable) = (N)) -> exists dst_positive_inverse_construct_resultrighttable dst_negative_inverse_construct_resultrighttable dst_value_inverse_construct_resultrighttable. ((((exists ff_h_pvs_inverse_construct_resultrighttableentrypositive. ff_h_pvs_inverse_construct_resultrighttableentrypositive + S (dst_positive_inverse_construct_resultrighttable) = S ((S (dst_index_inverse_construct_resultrighttable)) * dst_positive_scale_inverse_construct_resultrighttable)) /\ exists ff_q_pvs_inverse_construct_resultrighttableentrypositive. dst_positive_code_inverse_construct_resultrighttable = ff_q_pvs_inverse_construct_resultrighttableentrypositive * S ((S (dst_index_inverse_construct_resultrighttable)) * dst_positive_scale_inverse_construct_resultrighttable) + (dst_positive_inverse_construct_resultrighttable))) /\ (((((exists ff_h_pvs_inverse_construct_resultrighttableentrynegative. ff_h_pvs_inverse_construct_resultrighttableentrynegative + S (dst_negative_inverse_construct_resultrighttable) = S ((S (dst_index_inverse_construct_resultrighttable)) * dst_negative_scale_inverse_construct_resultrighttable)) /\ exists ff_q_pvs_inverse_construct_resultrighttableentrynegative. dst_negative_code_inverse_construct_resultrighttable = ff_q_pvs_inverse_construct_resultrighttableentrynegative * S ((S (dst_index_inverse_construct_resultrighttable)) * dst_negative_scale_inverse_construct_resultrighttable) + (dst_negative_inverse_construct_resultrighttable))) /\ (exists ge_balance_positive_inverse_construct_resultrighttableentryvalue ge_balance_negative_inverse_construct_resultrighttableentryvalue. (((((dst_value_inverse_construct_resultrighttable) = 2 * (ge_balance_positive_inverse_construct_resultrighttableentryvalue) /\ (ge_balance_negative_inverse_construct_resultrighttableentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultrighttableentryvaluedecode. (((dst_value_inverse_construct_resultrighttable) = 2 * ge_signed_half_inverse_construct_resultrighttableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultrighttableentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultrighttableentryvalue) = S ge_signed_half_inverse_construct_resultrighttableentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultrighttable) + ge_balance_negative_inverse_construct_resultrighttableentryvalue = (dst_negative_inverse_construct_resultrighttable) + ge_balance_positive_inverse_construct_resultrighttableentryvalue))))))))) /\ (forall dc_input_inverse_construct_resultright dc_output_inverse_construct_resultright. ~(dc_input_inverse_construct_resultright=0) -> (exists pvs_le_gap_inverse_construct_resultrightdomain. pvs_le_gap_inverse_construct_resultrightdomain + (dc_input_inverse_construct_resultright) = (N)) -> (exists dst_positive_code_inverse_construct_resultrightlookup dst_positive_scale_inverse_construct_resultrightlookup dst_negative_code_inverse_construct_resultrightlookup dst_negative_scale_inverse_construct_resultrightlookup dst_positive_inverse_construct_resultrightlookup dst_negative_inverse_construct_resultrightlookup. (((di_delta_inverse_construct_result) = (((((dst_positive_code_inverse_construct_resultrightlookup) + (dst_positive_scale_inverse_construct_resultrightlookup)) * S ((dst_positive_code_inverse_construct_resultrightlookup) + (dst_positive_scale_inverse_construct_resultrightlookup)) + ((dst_positive_scale_inverse_construct_resultrightlookup) + (dst_positive_scale_inverse_construct_resultrightlookup))) + (((dst_negative_code_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)) * S ((dst_negative_code_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)) + ((dst_negative_scale_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)))) * S ((((dst_positive_code_inverse_construct_resultrightlookup) + (dst_positive_scale_inverse_construct_resultrightlookup)) * S ((dst_positive_code_inverse_construct_resultrightlookup) + (dst_positive_scale_inverse_construct_resultrightlookup)) + ((dst_positive_scale_inverse_construct_resultrightlookup) + (dst_positive_scale_inverse_construct_resultrightlookup))) + (((dst_negative_code_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)) * S ((dst_negative_code_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)) + ((dst_negative_scale_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)))) + ((((dst_negative_code_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)) * S ((dst_negative_code_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)) + ((dst_negative_scale_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup))) + (((dst_negative_code_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)) * S ((dst_negative_code_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)) + ((dst_negative_scale_inverse_construct_resultrightlookup) + (dst_negative_scale_inverse_construct_resultrightlookup)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightlookuppositive. ff_h_pvs_inverse_construct_resultrightlookuppositive + S (dst_positive_inverse_construct_resultrightlookup) = S ((S (dc_input_inverse_construct_resultright)) * dst_positive_scale_inverse_construct_resultrightlookup)) /\ exists ff_q_pvs_inverse_construct_resultrightlookuppositive. dst_positive_code_inverse_construct_resultrightlookup = ff_q_pvs_inverse_construct_resultrightlookuppositive * S ((S (dc_input_inverse_construct_resultright)) * dst_positive_scale_inverse_construct_resultrightlookup) + (dst_positive_inverse_construct_resultrightlookup))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightlookupnegative. ff_h_pvs_inverse_construct_resultrightlookupnegative + S (dst_negative_inverse_construct_resultrightlookup) = S ((S (dc_input_inverse_construct_resultright)) * dst_negative_scale_inverse_construct_resultrightlookup)) /\ exists ff_q_pvs_inverse_construct_resultrightlookupnegative. dst_negative_code_inverse_construct_resultrightlookup = ff_q_pvs_inverse_construct_resultrightlookupnegative * S ((S (dc_input_inverse_construct_resultright)) * dst_negative_scale_inverse_construct_resultrightlookup) + (dst_negative_inverse_construct_resultrightlookup))) /\ (exists ge_balance_positive_inverse_construct_resultrightlookupvalue ge_balance_negative_inverse_construct_resultrightlookupvalue. (((((dc_output_inverse_construct_resultright) = 2 * (ge_balance_positive_inverse_construct_resultrightlookupvalue) /\ (ge_balance_negative_inverse_construct_resultrightlookupvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultrightlookupvaluedecode. (((dc_output_inverse_construct_resultright) = 2 * ge_signed_half_inverse_construct_resultrightlookupvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultrightlookupvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultrightlookupvalue) = S ge_signed_half_inverse_construct_resultrightlookupvaluedecode))) /\ ((dst_positive_inverse_construct_resultrightlookup) + ge_balance_negative_inverse_construct_resultrightlookupvalue = (dst_negative_inverse_construct_resultrightlookup) + ge_balance_positive_inverse_construct_resultrightlookupvalue))))))))) -> (((~((dc_input_inverse_construct_resultright)=0)) /\ (exists dc_mask_inverse_construct_resultrightvalue. ((((exists dst_positive_code_inverse_construct_resultrightvaluemasktable dst_positive_scale_inverse_construct_resultrightvaluemasktable dst_negative_code_inverse_construct_resultrightvaluemasktable dst_negative_scale_inverse_construct_resultrightvaluemasktable. (((dc_mask_inverse_construct_resultrightvalue) = (((((dst_positive_code_inverse_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_construct_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_construct_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_construct_resultrightvaluemasktable))) + (((dst_negative_code_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)))) * S ((((dst_positive_code_inverse_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_construct_resultrightvaluemasktable)) * S ((dst_positive_code_inverse_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_construct_resultrightvaluemasktable)) + ((dst_positive_scale_inverse_construct_resultrightvaluemasktable) + (dst_positive_scale_inverse_construct_resultrightvaluemasktable))) + (((dst_negative_code_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)))) + ((((dst_negative_code_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable))) + (((dst_negative_code_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)) * S ((dst_negative_code_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)) + ((dst_negative_scale_inverse_construct_resultrightvaluemasktable) + (dst_negative_scale_inverse_construct_resultrightvaluemasktable)))))) /\ (forall dst_index_inverse_construct_resultrightvaluemasktable. (exists pvs_le_gap_inverse_construct_resultrightvaluemasktabledomain. pvs_le_gap_inverse_construct_resultrightvaluemasktabledomain + (dst_index_inverse_construct_resultrightvaluemasktable) = (dc_input_inverse_construct_resultright)) -> exists dst_positive_inverse_construct_resultrightvaluemasktable dst_negative_inverse_construct_resultrightvaluemasktable dst_value_inverse_construct_resultrightvaluemasktable. ((((exists ff_h_pvs_inverse_construct_resultrightvaluemasktableentrypositive. ff_h_pvs_inverse_construct_resultrightvaluemasktableentrypositive + S (dst_positive_inverse_construct_resultrightvaluemasktable) = S ((S (dst_index_inverse_construct_resultrightvaluemasktable)) * dst_positive_scale_inverse_construct_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_construct_resultrightvaluemasktableentrypositive. dst_positive_code_inverse_construct_resultrightvaluemasktable = ff_q_pvs_inverse_construct_resultrightvaluemasktableentrypositive * S ((S (dst_index_inverse_construct_resultrightvaluemasktable)) * dst_positive_scale_inverse_construct_resultrightvaluemasktable) + (dst_positive_inverse_construct_resultrightvaluemasktable))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightvaluemasktableentrynegative. ff_h_pvs_inverse_construct_resultrightvaluemasktableentrynegative + S (dst_negative_inverse_construct_resultrightvaluemasktable) = S ((S (dst_index_inverse_construct_resultrightvaluemasktable)) * dst_negative_scale_inverse_construct_resultrightvaluemasktable)) /\ exists ff_q_pvs_inverse_construct_resultrightvaluemasktableentrynegative. dst_negative_code_inverse_construct_resultrightvaluemasktable = ff_q_pvs_inverse_construct_resultrightvaluemasktableentrynegative * S ((S (dst_index_inverse_construct_resultrightvaluemasktable)) * dst_negative_scale_inverse_construct_resultrightvaluemasktable) + (dst_negative_inverse_construct_resultrightvaluemasktable))) /\ (exists ge_balance_positive_inverse_construct_resultrightvaluemasktableentryvalue ge_balance_negative_inverse_construct_resultrightvaluemasktableentryvalue. (((((dst_value_inverse_construct_resultrightvaluemasktable) = 2 * (ge_balance_positive_inverse_construct_resultrightvaluemasktableentryvalue) /\ (ge_balance_negative_inverse_construct_resultrightvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultrightvaluemasktableentryvaluedecode. (((dst_value_inverse_construct_resultrightvaluemasktable) = 2 * ge_signed_half_inverse_construct_resultrightvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultrightvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultrightvaluemasktableentryvalue) = S ge_signed_half_inverse_construct_resultrightvaluemasktableentryvaluedecode))) /\ ((dst_positive_inverse_construct_resultrightvaluemasktable) + ge_balance_negative_inverse_construct_resultrightvaluemasktableentryvalue = (dst_negative_inverse_construct_resultrightvaluemasktable) + ge_balance_positive_inverse_construct_resultrightvaluemasktableentryvalue))))))))) /\ (forall dc_index_inverse_construct_resultrightvaluemask dc_value_inverse_construct_resultrightvaluemask. (exists pvs_le_gap_inverse_construct_resultrightvaluemaskdomain. pvs_le_gap_inverse_construct_resultrightvaluemaskdomain + (dc_index_inverse_construct_resultrightvaluemask) = (dc_input_inverse_construct_resultright)) -> (exists dst_positive_code_inverse_construct_resultrightvaluemasklookup dst_positive_scale_inverse_construct_resultrightvaluemasklookup dst_negative_code_inverse_construct_resultrightvaluemasklookup dst_negative_scale_inverse_construct_resultrightvaluemasklookup dst_positive_inverse_construct_resultrightvaluemasklookup dst_negative_inverse_construct_resultrightvaluemasklookup. (((dc_mask_inverse_construct_resultrightvalue) = (((((dst_positive_code_inverse_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_construct_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_construct_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_construct_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)))) * S ((((dst_positive_code_inverse_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_construct_resultrightvaluemasklookup)) * S ((dst_positive_code_inverse_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_construct_resultrightvaluemasklookup)) + ((dst_positive_scale_inverse_construct_resultrightvaluemasklookup) + (dst_positive_scale_inverse_construct_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)))) + ((((dst_negative_code_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup))) + (((dst_negative_code_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) * S ((dst_negative_code_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) + ((dst_negative_scale_inverse_construct_resultrightvaluemasklookup) + (dst_negative_scale_inverse_construct_resultrightvaluemasklookup)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightvaluemasklookuppositive. ff_h_pvs_inverse_construct_resultrightvaluemasklookuppositive + S (dst_positive_inverse_construct_resultrightvaluemasklookup) = S ((S (dc_index_inverse_construct_resultrightvaluemask)) * dst_positive_scale_inverse_construct_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_construct_resultrightvaluemasklookuppositive. dst_positive_code_inverse_construct_resultrightvaluemasklookup = ff_q_pvs_inverse_construct_resultrightvaluemasklookuppositive * S ((S (dc_index_inverse_construct_resultrightvaluemask)) * dst_positive_scale_inverse_construct_resultrightvaluemasklookup) + (dst_positive_inverse_construct_resultrightvaluemasklookup))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightvaluemasklookupnegative. ff_h_pvs_inverse_construct_resultrightvaluemasklookupnegative + S (dst_negative_inverse_construct_resultrightvaluemasklookup) = S ((S (dc_index_inverse_construct_resultrightvaluemask)) * dst_negative_scale_inverse_construct_resultrightvaluemasklookup)) /\ exists ff_q_pvs_inverse_construct_resultrightvaluemasklookupnegative. dst_negative_code_inverse_construct_resultrightvaluemasklookup = ff_q_pvs_inverse_construct_resultrightvaluemasklookupnegative * S ((S (dc_index_inverse_construct_resultrightvaluemask)) * dst_negative_scale_inverse_construct_resultrightvaluemasklookup) + (dst_negative_inverse_construct_resultrightvaluemasklookup))) /\ (exists ge_balance_positive_inverse_construct_resultrightvaluemasklookupvalue ge_balance_negative_inverse_construct_resultrightvaluemasklookupvalue. (((((dc_value_inverse_construct_resultrightvaluemask) = 2 * (ge_balance_positive_inverse_construct_resultrightvaluemasklookupvalue) /\ (ge_balance_negative_inverse_construct_resultrightvaluemasklookupvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultrightvaluemasklookupvaluedecode. (((dc_value_inverse_construct_resultrightvaluemask) = 2 * ge_signed_half_inverse_construct_resultrightvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultrightvaluemasklookupvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultrightvaluemasklookupvalue) = S ge_signed_half_inverse_construct_resultrightvaluemasklookupvaluedecode))) /\ ((dst_positive_inverse_construct_resultrightvaluemasklookup) + ge_balance_negative_inverse_construct_resultrightvaluemasklookupvalue = (dst_negative_inverse_construct_resultrightvaluemasklookup) + ge_balance_positive_inverse_construct_resultrightvaluemasklookupvalue))))))))) -> ((((~((dc_index_inverse_construct_resultrightvaluemask)=0)) /\ (exists dc_quotient_inverse_construct_resultrightvaluemaskentry dc_left_inverse_construct_resultrightvaluemaskentry dc_right_inverse_construct_resultrightvaluemaskentry. (((dc_input_inverse_construct_resultright)=(dc_index_inverse_construct_resultrightvaluemask)*dc_quotient_inverse_construct_resultrightvaluemaskentry) /\ (((exists dst_positive_code_inverse_construct_resultrightvaluemaskentryleft dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft dst_negative_code_inverse_construct_resultrightvaluemaskentryleft dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft dst_positive_inverse_construct_resultrightvaluemaskentryleft dst_negative_inverse_construct_resultrightvaluemaskentryleft. (((G) = (((((dst_positive_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)))) * S ((((dst_positive_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft)) * S ((dst_positive_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft)) + ((dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)))) + ((((dst_negative_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft))) + (((dst_negative_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) * S ((dst_negative_code_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) + ((dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightvaluemaskentryleftpositive. ff_h_pvs_inverse_construct_resultrightvaluemaskentryleftpositive + S (dst_positive_inverse_construct_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_construct_resultrightvaluemask)) * dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_construct_resultrightvaluemaskentryleftpositive. dst_positive_code_inverse_construct_resultrightvaluemaskentryleft = ff_q_pvs_inverse_construct_resultrightvaluemaskentryleftpositive * S ((S (dc_index_inverse_construct_resultrightvaluemask)) * dst_positive_scale_inverse_construct_resultrightvaluemaskentryleft) + (dst_positive_inverse_construct_resultrightvaluemaskentryleft))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightvaluemaskentryleftnegative. ff_h_pvs_inverse_construct_resultrightvaluemaskentryleftnegative + S (dst_negative_inverse_construct_resultrightvaluemaskentryleft) = S ((S (dc_index_inverse_construct_resultrightvaluemask)) * dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft)) /\ exists ff_q_pvs_inverse_construct_resultrightvaluemaskentryleftnegative. dst_negative_code_inverse_construct_resultrightvaluemaskentryleft = ff_q_pvs_inverse_construct_resultrightvaluemaskentryleftnegative * S ((S (dc_index_inverse_construct_resultrightvaluemask)) * dst_negative_scale_inverse_construct_resultrightvaluemaskentryleft) + (dst_negative_inverse_construct_resultrightvaluemaskentryleft))) /\ (exists ge_balance_positive_inverse_construct_resultrightvaluemaskentryleftvalue ge_balance_negative_inverse_construct_resultrightvaluemaskentryleftvalue. (((((dc_left_inverse_construct_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_construct_resultrightvaluemaskentryleftvalue) /\ (ge_balance_negative_inverse_construct_resultrightvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultrightvaluemaskentryleftvaluedecode. (((dc_left_inverse_construct_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_construct_resultrightvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultrightvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultrightvaluemaskentryleftvalue) = S ge_signed_half_inverse_construct_resultrightvaluemaskentryleftvaluedecode))) /\ ((dst_positive_inverse_construct_resultrightvaluemaskentryleft) + ge_balance_negative_inverse_construct_resultrightvaluemaskentryleftvalue = (dst_negative_inverse_construct_resultrightvaluemaskentryleft) + ge_balance_positive_inverse_construct_resultrightvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_inverse_construct_resultrightvaluemaskentryright dst_positive_scale_inverse_construct_resultrightvaluemaskentryright dst_negative_code_inverse_construct_resultrightvaluemaskentryright dst_negative_scale_inverse_construct_resultrightvaluemaskentryright dst_positive_inverse_construct_resultrightvaluemaskentryright dst_negative_inverse_construct_resultrightvaluemaskentryright. (((F) = (((((dst_positive_code_inverse_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)))) * S ((((dst_positive_code_inverse_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryright)) * S ((dst_positive_code_inverse_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryright)) + ((dst_positive_scale_inverse_construct_resultrightvaluemaskentryright) + (dst_positive_scale_inverse_construct_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)))) + ((((dst_negative_code_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright))) + (((dst_negative_code_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) * S ((dst_negative_code_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) + ((dst_negative_scale_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightvaluemaskentryrightpositive. ff_h_pvs_inverse_construct_resultrightvaluemaskentryrightpositive + S (dst_positive_inverse_construct_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_construct_resultrightvaluemaskentry)) * dst_positive_scale_inverse_construct_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_construct_resultrightvaluemaskentryrightpositive. dst_positive_code_inverse_construct_resultrightvaluemaskentryright = ff_q_pvs_inverse_construct_resultrightvaluemaskentryrightpositive * S ((S (dc_quotient_inverse_construct_resultrightvaluemaskentry)) * dst_positive_scale_inverse_construct_resultrightvaluemaskentryright) + (dst_positive_inverse_construct_resultrightvaluemaskentryright))) /\ (((((exists ff_h_pvs_inverse_construct_resultrightvaluemaskentryrightnegative. ff_h_pvs_inverse_construct_resultrightvaluemaskentryrightnegative + S (dst_negative_inverse_construct_resultrightvaluemaskentryright) = S ((S (dc_quotient_inverse_construct_resultrightvaluemaskentry)) * dst_negative_scale_inverse_construct_resultrightvaluemaskentryright)) /\ exists ff_q_pvs_inverse_construct_resultrightvaluemaskentryrightnegative. dst_negative_code_inverse_construct_resultrightvaluemaskentryright = ff_q_pvs_inverse_construct_resultrightvaluemaskentryrightnegative * S ((S (dc_quotient_inverse_construct_resultrightvaluemaskentry)) * dst_negative_scale_inverse_construct_resultrightvaluemaskentryright) + (dst_negative_inverse_construct_resultrightvaluemaskentryright))) /\ (exists ge_balance_positive_inverse_construct_resultrightvaluemaskentryrightvalue ge_balance_negative_inverse_construct_resultrightvaluemaskentryrightvalue. (((((dc_right_inverse_construct_resultrightvaluemaskentry) = 2 * (ge_balance_positive_inverse_construct_resultrightvaluemaskentryrightvalue) /\ (ge_balance_negative_inverse_construct_resultrightvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_inverse_construct_resultrightvaluemaskentryrightvaluedecode. (((dc_right_inverse_construct_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_construct_resultrightvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_inverse_construct_resultrightvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_inverse_construct_resultrightvaluemaskentryrightvalue) = S ge_signed_half_inverse_construct_resultrightvaluemaskentryrightvaluedecode))) /\ ((dst_positive_inverse_construct_resultrightvaluemaskentryright) + ge_balance_negative_inverse_construct_resultrightvaluemaskentryrightvalue = (dst_negative_inverse_construct_resultrightvaluemaskentryright) + ge_balance_positive_inverse_construct_resultrightvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_inverse_construct_resultrightvaluemaskentryproduct sto_an_inverse_construct_resultrightvaluemaskentryproduct sto_bp_inverse_construct_resultrightvaluemaskentryproduct sto_bn_inverse_construct_resultrightvaluemaskentryproduct sto_cp_inverse_construct_resultrightvaluemaskentryproduct sto_cn_inverse_construct_resultrightvaluemaskentryproduct. (((((dc_left_inverse_construct_resultrightvaluemaskentry) = 2 * (sto_ap_inverse_construct_resultrightvaluemaskentryproduct) /\ (sto_an_inverse_construct_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_construct_resultrightvaluemaskentryproductleft. (((dc_left_inverse_construct_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_construct_resultrightvaluemaskentryproductleft + 1 /\ (sto_ap_inverse_construct_resultrightvaluemaskentryproduct) = 0) /\ (sto_an_inverse_construct_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_construct_resultrightvaluemaskentryproductleft))) /\ ((((((dc_right_inverse_construct_resultrightvaluemaskentry) = 2 * (sto_bp_inverse_construct_resultrightvaluemaskentryproduct) /\ (sto_bn_inverse_construct_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_construct_resultrightvaluemaskentryproductright. (((dc_right_inverse_construct_resultrightvaluemaskentry) = 2 * ge_signed_half_inverse_construct_resultrightvaluemaskentryproductright + 1 /\ (sto_bp_inverse_construct_resultrightvaluemaskentryproduct) = 0) /\ (sto_bn_inverse_construct_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_construct_resultrightvaluemaskentryproductright))) /\ ((((((dc_value_inverse_construct_resultrightvaluemask) = 2 * (sto_cp_inverse_construct_resultrightvaluemaskentryproduct) /\ (sto_cn_inverse_construct_resultrightvaluemaskentryproduct) = 0) \/ exists ge_signed_half_inverse_construct_resultrightvaluemaskentryproductoutput. (((dc_value_inverse_construct_resultrightvaluemask) = 2 * ge_signed_half_inverse_construct_resultrightvaluemaskentryproductoutput + 1 /\ (sto_cp_inverse_construct_resultrightvaluemaskentryproduct) = 0) /\ (sto_cn_inverse_construct_resultrightvaluemaskentryproduct) = S ge_signed_half_inverse_construct_resultrightvaluemaskentryproductoutput))) /\ ((sto_ap_inverse_construct_resultrightvaluemaskentryproduct * sto_bp_inverse_construct_resultrightvaluemaskentryproduct + sto_an_inverse_construct_resultrightvaluemaskentryproduct * sto_bn_inverse_construct_resultrightvaluemaskentryproduct) + sto_cn_inverse_construct_resultrightvaluemaskentryproduct = (sto_ap_inverse_construct_resultrightvaluemaskentryproduct * sto_bn_inverse_construct_resultrightvaluemaskentryproduct + sto_an_inverse_construct_resultrightvaluemaskentryproduct * sto_bp_inverse_construct_resultrightvaluemaskentryproduct) + sto_cp_inverse_construct_resultrightvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_inverse_construct_resultrightvaluemask)=0 \/ ~(exists pvs_factor_inverse_construct_resultrightvaluemaskentrynondivisor. (dc_input_inverse_construct_resultright) = (dc_index_inverse_construct_resultrightvaluemask) * pvs_factor_inverse_construct_resultrightvaluemaskentrynondivisor)) /\ ((dc_value_inverse_construct_resultrightvaluemask)=0))))))) /\ (exists dst_positive_code_inverse_construct_resultrightvaluefold dst_positive_scale_inverse_construct_resultrightvaluefold dst_negative_code_inverse_construct_resultrightvaluefold dst_negative_scale_inverse_construct_resultrightvaluefold dst_positive_sum_inverse_construct_resultrightvaluefold dst_negative_sum_inverse_construct_resultrightvaluefold. (((dc_mask_inverse_construct_resultrightvalue) = (((((dst_positive_code_inverse_construct_resultrightvaluefold) + (dst_positive_scale_inverse_construct_resultrightvaluefold)) * S ((dst_positive_code_inverse_construct_resultrightvaluefold) + (dst_positive_scale_inverse_construct_resultrightvaluefold)) + ((dst_positive_scale_inverse_construct_resultrightvaluefold) + (dst_positive_scale_inverse_construct_resultrightvaluefold))) + (((dst_negative_code_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)) * S ((dst_negative_code_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)) + ((dst_negative_scale_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)))) * S ((((dst_positive_code_inverse_construct_resultrightvaluefold) + (dst_positive_scale_inverse_construct_resultrightvaluefold)) * S ((dst_positive_code_inverse_construct_resultrightvaluefold) + (dst_positive_scale_inverse_construct_resultrightvaluefold)) + ((dst_positive_scale_inverse_construct_resultrightvaluefold) + (dst_positive_scale_inverse_construct_resultrightvaluefold))) + (((dst_negative_code_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)) * S ((dst_negative_code_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)) + ((dst_negative_scale_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)))) + ((((dst_negative_code_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)) * S ((dst_negative_code_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)) + ((dst_negative_scale_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold))) + (((dst_negative_code_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)) * S ((dst_negative_code_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)) + ((dst_negative_scale_inverse_construct_resultrightvaluefold) + (dst_negative_scale_inverse_construct_resultrightvaluefold)))))) /\ (((exists fs_u_dst_inverse_construct_resultrightvaluefoldpositive fs_v_dst_inverse_construct_resultrightvaluefoldpositive. ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_start. fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_construct_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_start. fs_u_dst_inverse_construct_resultrightvaluefoldpositive = fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_inverse_construct_resultrightvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_terminal. fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_terminal + S (dst_positive_sum_inverse_construct_resultrightvaluefold) = S ((S (S (dc_input_inverse_construct_resultright))) * fs_v_dst_inverse_construct_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_terminal. fs_u_dst_inverse_construct_resultrightvaluefoldpositive = fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_terminal * S ((S (S (dc_input_inverse_construct_resultright))) * fs_v_dst_inverse_construct_resultrightvaluefoldpositive) + (dst_positive_sum_inverse_construct_resultrightvaluefold))) /\ forall fs_i_dst_inverse_construct_resultrightvaluefoldpositive_body_steps. (exists fs_lt_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_bound. fs_lt_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_bound + S fs_i_dst_inverse_construct_resultrightvaluefoldpositive_body_steps = S (dc_input_inverse_construct_resultright)) -> exists fs_a_dst_inverse_construct_resultrightvaluefoldpositive_body_steps fs_r_dst_inverse_construct_resultrightvaluefoldpositive_body_steps fs_s_dst_inverse_construct_resultrightvaluefoldpositive_body_steps. ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_summand. fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_summand + S (fs_a_dst_inverse_construct_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_construct_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_construct_resultrightvaluefold)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_summand. dst_positive_code_inverse_construct_resultrightvaluefold = fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_inverse_construct_resultrightvaluefoldpositive_body_steps)) * dst_positive_scale_inverse_construct_resultrightvaluefold) + (fs_a_dst_inverse_construct_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_partial. fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_partial + S (fs_r_dst_inverse_construct_resultrightvaluefoldpositive_body_steps) = S ((S (fs_i_dst_inverse_construct_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_construct_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_partial. fs_u_dst_inverse_construct_resultrightvaluefoldpositive = fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_inverse_construct_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_construct_resultrightvaluefoldpositive) + (fs_r_dst_inverse_construct_resultrightvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_successor. fs_h_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_successor + S (fs_s_dst_inverse_construct_resultrightvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_inverse_construct_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_construct_resultrightvaluefoldpositive)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_successor. fs_u_dst_inverse_construct_resultrightvaluefoldpositive = fs_q_dst_inverse_construct_resultrightvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_inverse_construct_resultrightvaluefoldpositive_body_steps)) * fs_v_dst_inverse_construct_resultrightvaluefoldpositive) + (fs_s_dst_inverse_construct_resultrightvaluefoldpositive_body_steps))) /\ fs_s_dst_inverse_construct_resultrightvaluefoldpositive_body_steps = fs_r_dst_inverse_construct_resultrightvaluefoldpositive_body_steps + fs_a_dst_inverse_construct_resultrightvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_inverse_construct_resultrightvaluefoldnegative fs_v_dst_inverse_construct_resultrightvaluefoldnegative. ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_start. fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_inverse_construct_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_start. fs_u_dst_inverse_construct_resultrightvaluefoldnegative = fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_inverse_construct_resultrightvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_terminal. fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_terminal + S (dst_negative_sum_inverse_construct_resultrightvaluefold) = S ((S (S (dc_input_inverse_construct_resultright))) * fs_v_dst_inverse_construct_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_terminal. fs_u_dst_inverse_construct_resultrightvaluefoldnegative = fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_terminal * S ((S (S (dc_input_inverse_construct_resultright))) * fs_v_dst_inverse_construct_resultrightvaluefoldnegative) + (dst_negative_sum_inverse_construct_resultrightvaluefold))) /\ forall fs_i_dst_inverse_construct_resultrightvaluefoldnegative_body_steps. (exists fs_lt_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_bound. fs_lt_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_bound + S fs_i_dst_inverse_construct_resultrightvaluefoldnegative_body_steps = S (dc_input_inverse_construct_resultright)) -> exists fs_a_dst_inverse_construct_resultrightvaluefoldnegative_body_steps fs_r_dst_inverse_construct_resultrightvaluefoldnegative_body_steps fs_s_dst_inverse_construct_resultrightvaluefoldnegative_body_steps. ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_summand. fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_summand + S (fs_a_dst_inverse_construct_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_construct_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_construct_resultrightvaluefold)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_summand. dst_negative_code_inverse_construct_resultrightvaluefold = fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_inverse_construct_resultrightvaluefoldnegative_body_steps)) * dst_negative_scale_inverse_construct_resultrightvaluefold) + (fs_a_dst_inverse_construct_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_partial. fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_partial + S (fs_r_dst_inverse_construct_resultrightvaluefoldnegative_body_steps) = S ((S (fs_i_dst_inverse_construct_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_construct_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_partial. fs_u_dst_inverse_construct_resultrightvaluefoldnegative = fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_inverse_construct_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_construct_resultrightvaluefoldnegative) + (fs_r_dst_inverse_construct_resultrightvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_successor. fs_h_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_successor + S (fs_s_dst_inverse_construct_resultrightvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_inverse_construct_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_construct_resultrightvaluefoldnegative)) /\ exists fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_successor. fs_u_dst_inverse_construct_resultrightvaluefoldnegative = fs_q_dst_inverse_construct_resultrightvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_inverse_construct_resultrightvaluefoldnegative_body_steps)) * fs_v_dst_inverse_construct_resultrightvaluefoldnegative) + (fs_s_dst_inverse_construct_resultrightvaluefoldnegative_body_steps))) /\ fs_s_dst_inverse_construct_resultrightvaluefoldnegative_body_steps = fs_r_dst_inverse_construct_resultrightvaluefoldnegative_body_steps + fs_a_dst_inverse_construct_resultrightvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_inverse_construct_resultrightvaluefoldresult ge_balance_negative_inverse_construct_resultrightvaluefoldresult. (((((dc_output_inverse_construct_resultright) = 2 * (ge_balance_positive_inverse_construct_resultrightvaluefoldresult) /\ (ge_balance_negative_inverse_construct_resultrightvaluefoldresult) = 0) \/ exists ge_signed_half_inverse_construct_resultrightvaluefoldresultdecode. (((dc_output_inverse_construct_resultright) = 2 * ge_signed_half_inverse_construct_resultrightvaluefoldresultdecode + 1 /\ (ge_balance_positive_inverse_construct_resultrightvaluefoldresult) = 0) /\ (ge_balance_negative_inverse_construct_resultrightvaluefoldresult) = S ge_signed_half_inverse_construct_resultrightvaluefoldresultdecode))) /\ ((dst_positive_sum_inverse_construct_resultrightvaluefold) + ge_balance_negative_inverse_construct_resultrightvaluefoldresult = (dst_negative_sum_inverse_construct_resultrightvaluefold) + ge_balance_positive_inverse_construct_resultrightvaluefoldresult)))))))))))))))))))))))) /\ (exists dst_positive_code_inverse_construct_zero dst_positive_scale_inverse_construct_zero dst_negative_code_inverse_construct_zero dst_negative_scale_inverse_construct_zero dst_positive_inverse_construct_zero dst_negative_inverse_construct_zero. (((G) = (((((dst_positive_code_inverse_construct_zero) + (dst_positive_scale_inverse_construct_zero)) * S ((dst_positive_code_inverse_construct_zero) + (dst_positive_scale_inverse_construct_zero)) + ((dst_positive_scale_inverse_construct_zero) + (dst_positive_scale_inverse_construct_zero))) + (((dst_negative_code_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)) * S ((dst_negative_code_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)) + ((dst_negative_scale_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)))) * S ((((dst_positive_code_inverse_construct_zero) + (dst_positive_scale_inverse_construct_zero)) * S ((dst_positive_code_inverse_construct_zero) + (dst_positive_scale_inverse_construct_zero)) + ((dst_positive_scale_inverse_construct_zero) + (dst_positive_scale_inverse_construct_zero))) + (((dst_negative_code_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)) * S ((dst_negative_code_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)) + ((dst_negative_scale_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)))) + ((((dst_negative_code_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)) * S ((dst_negative_code_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)) + ((dst_negative_scale_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero))) + (((dst_negative_code_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)) * S ((dst_negative_code_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)) + ((dst_negative_scale_inverse_construct_zero) + (dst_negative_scale_inverse_construct_zero)))))) /\ (((((exists ff_h_pvs_inverse_construct_zeropositive. ff_h_pvs_inverse_construct_zeropositive + S (dst_positive_inverse_construct_zero) = S ((S (0)) * dst_positive_scale_inverse_construct_zero)) /\ exists ff_q_pvs_inverse_construct_zeropositive. dst_positive_code_inverse_construct_zero = ff_q_pvs_inverse_construct_zeropositive * S ((S (0)) * dst_positive_scale_inverse_construct_zero) + (dst_positive_inverse_construct_zero))) /\ (((((exists ff_h_pvs_inverse_construct_zeronegative. ff_h_pvs_inverse_construct_zeronegative + S (dst_negative_inverse_construct_zero) = S ((S (0)) * dst_negative_scale_inverse_construct_zero)) /\ exists ff_q_pvs_inverse_construct_zeronegative. dst_negative_code_inverse_construct_zero = ff_q_pvs_inverse_construct_zeronegative * S ((S (0)) * dst_negative_scale_inverse_construct_zero) + (dst_negative_inverse_construct_zero))) /\ (exists ge_balance_positive_inverse_construct_zerovalue ge_balance_negative_inverse_construct_zerovalue. (((((w) = 2 * (ge_balance_positive_inverse_construct_zerovalue) /\ (ge_balance_negative_inverse_construct_zerovalue) = 0) \/ exists ge_signed_half_inverse_construct_zerovaluedecode. (((w) = 2 * ge_signed_half_inverse_construct_zerovaluedecode + 1 /\ (ge_balance_positive_inverse_construct_zerovalue) = 0) /\ (ge_balance_negative_inverse_construct_zerovalue) = S ge_signed_half_inverse_construct_zerovaluedecode))) /\ ((dst_positive_inverse_construct_zero) + ge_balance_negative_inverse_construct_zerovalue = (dst_negative_inverse_construct_zero) + ge_balance_positive_inverse_construct_zerovalue))))))))))Constructive proof overview
Generated structural guide
The exact empty-window-or-unit-at-one condition constructs actual inverse witnesses, preserving an arbitrary requested value at zero.
The unchanged tactic script uses 2 declared prerequisites and contains 27 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.
Read the argument
Proof checkpoints
This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.
Named ingredients (2)
01Fix variables and assumptionsL1–5
02Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
cases hc
03Calculate and transport equalitiesL7–16
04Calculate and transport equalitiesL17–17
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L17
rewrite hc_left
05Use earlier factsL18–27
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L18
specialize dirichlet_inverse_zero_construct (F) - L19
specialize dirichlet_inverse_zero_construct (w) - L20
apply dirichlet_inverse_zero_construct - L21
exact hF - L22
specialize dirichlet_inverse_from_unit_at_one (N) - L23
specialize dirichlet_inverse_from_unit_at_one (F) - L24
specialize dirichlet_inverse_from_unit_at_one (w) - L25
apply dirichlet_inverse_from_unit_at_one - L26
exact hF - L27
exact hc_right
Original exact command ledger · 27 lines
- 0001
intro N - 0002
intro F - 0003
intro w - 0004
intro hF - 0005
intro hc - 0006
cases hc - 0007
rewrite hc_left at hF - 0008
rewrite hc_left - 0009
rewrite hc_left - 0010
rewrite hc_left - 0011
rewrite hc_left - 0012
rewrite hc_left - 0013
rewrite hc_left - 0014
rewrite hc_left - 0015
rewrite hc_left - 0016
rewrite hc_left - 0017
rewrite hc_left - 0018
specialize dirichlet_inverse_zero_construct (F) - 0019
specialize dirichlet_inverse_zero_construct (w) - 0020
apply dirichlet_inverse_zero_construct - 0021
exact hF - 0022
specialize dirichlet_inverse_from_unit_at_one (N) - 0023
specialize dirichlet_inverse_from_unit_at_one (F) - 0024
specialize dirichlet_inverse_from_unit_at_one (w) - 0025
apply dirichlet_inverse_from_unit_at_one - 0026
exact hF - 0027
exact hc_right