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 G. (exists dst_positive_code_full_source dst_positive_scale_full_source dst_negative_code_full_source dst_negative_scale_full_source. (((F) = (((((dst_positive_code_full_source) + (dst_positive_scale_full_source)) * S ((dst_positive_code_full_source) + (dst_positive_scale_full_source)) + ((dst_positive_scale_full_source) + (dst_positive_scale_full_source))) + (((dst_negative_code_full_source) + (dst_negative_scale_full_source)) * S ((dst_negative_code_full_source) + (dst_negative_scale_full_source)) + ((dst_negative_scale_full_source) + (dst_negative_scale_full_source)))) * S ((((dst_positive_code_full_source) + (dst_positive_scale_full_source)) * S ((dst_positive_code_full_source) + (dst_positive_scale_full_source)) + ((dst_positive_scale_full_source) + (dst_positive_scale_full_source))) + (((dst_negative_code_full_source) + (dst_negative_scale_full_source)) * S ((dst_negative_code_full_source) + (dst_negative_scale_full_source)) + ((dst_negative_scale_full_source) + (dst_negative_scale_full_source)))) + ((((dst_negative_code_full_source) + (dst_negative_scale_full_source)) * S ((dst_negative_code_full_source) + (dst_negative_scale_full_source)) + ((dst_negative_scale_full_source) + (dst_negative_scale_full_source))) + (((dst_negative_code_full_source) + (dst_negative_scale_full_source)) * S ((dst_negative_code_full_source) + (dst_negative_scale_full_source)) + ((dst_negative_scale_full_source) + (dst_negative_scale_full_source)))))) /\ (forall dst_index_full_source. (exists pvs_le_gap_full_sourcedomain. pvs_le_gap_full_sourcedomain + (dst_index_full_source) = (N)) -> exists dst_positive_full_source dst_negative_full_source dst_value_full_source. ((((exists ff_h_pvs_full_sourceentrypositive. ff_h_pvs_full_sourceentrypositive + S (dst_positive_full_source) = S ((S (dst_index_full_source)) * dst_positive_scale_full_source)) /\ exists ff_q_pvs_full_sourceentrypositive. dst_positive_code_full_source = ff_q_pvs_full_sourceentrypositive * S ((S (dst_index_full_source)) * dst_positive_scale_full_source) + (dst_positive_full_source))) /\ (((((exists ff_h_pvs_full_sourceentrynegative. ff_h_pvs_full_sourceentrynegative + S (dst_negative_full_source) = S ((S (dst_index_full_source)) * dst_negative_scale_full_source)) /\ exists ff_q_pvs_full_sourceentrynegative. dst_negative_code_full_source = ff_q_pvs_full_sourceentrynegative * S ((S (dst_index_full_source)) * dst_negative_scale_full_source) + (dst_negative_full_source))) /\ (exists ge_balance_positive_full_sourceentryvalue ge_balance_negative_full_sourceentryvalue. (((((dst_value_full_source) = 2 * (ge_balance_positive_full_sourceentryvalue) /\ (ge_balance_negative_full_sourceentryvalue) = 0) \/ exists ge_signed_half_full_sourceentryvaluedecode. (((dst_value_full_source) = 2 * ge_signed_half_full_sourceentryvaluedecode + 1 /\ (ge_balance_positive_full_sourceentryvalue) = 0) /\ (ge_balance_negative_full_sourceentryvalue) = S ge_signed_half_full_sourceentryvaluedecode))) /\ ((dst_positive_full_source) + ge_balance_negative_full_sourceentryvalue = (dst_negative_full_source) + ge_balance_positive_full_sourceentryvalue))))))))) -> (exists dst_positive_code_full_transform_table dst_positive_scale_full_transform_table dst_negative_code_full_transform_table dst_negative_scale_full_transform_table. (((G) = (((((dst_positive_code_full_transform_table) + (dst_positive_scale_full_transform_table)) * S ((dst_positive_code_full_transform_table) + (dst_positive_scale_full_transform_table)) + ((dst_positive_scale_full_transform_table) + (dst_positive_scale_full_transform_table))) + (((dst_negative_code_full_transform_table) + (dst_negative_scale_full_transform_table)) * S ((dst_negative_code_full_transform_table) + (dst_negative_scale_full_transform_table)) + ((dst_negative_scale_full_transform_table) + (dst_negative_scale_full_transform_table)))) * S ((((dst_positive_code_full_transform_table) + (dst_positive_scale_full_transform_table)) * S ((dst_positive_code_full_transform_table) + (dst_positive_scale_full_transform_table)) + ((dst_positive_scale_full_transform_table) + (dst_positive_scale_full_transform_table))) + (((dst_negative_code_full_transform_table) + (dst_negative_scale_full_transform_table)) * S ((dst_negative_code_full_transform_table) + (dst_negative_scale_full_transform_table)) + ((dst_negative_scale_full_transform_table) + (dst_negative_scale_full_transform_table)))) + ((((dst_negative_code_full_transform_table) + (dst_negative_scale_full_transform_table)) * S ((dst_negative_code_full_transform_table) + (dst_negative_scale_full_transform_table)) + ((dst_negative_scale_full_transform_table) + (dst_negative_scale_full_transform_table))) + (((dst_negative_code_full_transform_table) + (dst_negative_scale_full_transform_table)) * S ((dst_negative_code_full_transform_table) + (dst_negative_scale_full_transform_table)) + ((dst_negative_scale_full_transform_table) + (dst_negative_scale_full_transform_table)))))) /\ (forall dst_index_full_transform_table. (exists pvs_le_gap_full_transform_tabledomain. pvs_le_gap_full_transform_tabledomain + (dst_index_full_transform_table) = (N)) -> exists dst_positive_full_transform_table dst_negative_full_transform_table dst_value_full_transform_table. ((((exists ff_h_pvs_full_transform_tableentrypositive. ff_h_pvs_full_transform_tableentrypositive + S (dst_positive_full_transform_table) = S ((S (dst_index_full_transform_table)) * dst_positive_scale_full_transform_table)) /\ exists ff_q_pvs_full_transform_tableentrypositive. dst_positive_code_full_transform_table = ff_q_pvs_full_transform_tableentrypositive * S ((S (dst_index_full_transform_table)) * dst_positive_scale_full_transform_table) + (dst_positive_full_transform_table))) /\ (((((exists ff_h_pvs_full_transform_tableentrynegative. ff_h_pvs_full_transform_tableentrynegative + S (dst_negative_full_transform_table) = S ((S (dst_index_full_transform_table)) * dst_negative_scale_full_transform_table)) /\ exists ff_q_pvs_full_transform_tableentrynegative. dst_negative_code_full_transform_table = ff_q_pvs_full_transform_tableentrynegative * S ((S (dst_index_full_transform_table)) * dst_negative_scale_full_transform_table) + (dst_negative_full_transform_table))) /\ (exists ge_balance_positive_full_transform_tableentryvalue ge_balance_negative_full_transform_tableentryvalue. (((((dst_value_full_transform_table) = 2 * (ge_balance_positive_full_transform_tableentryvalue) /\ (ge_balance_negative_full_transform_tableentryvalue) = 0) \/ exists ge_signed_half_full_transform_tableentryvaluedecode. (((dst_value_full_transform_table) = 2 * ge_signed_half_full_transform_tableentryvaluedecode + 1 /\ (ge_balance_positive_full_transform_tableentryvalue) = 0) /\ (ge_balance_negative_full_transform_tableentryvalue) = S ge_signed_half_full_transform_tableentryvaluedecode))) /\ ((dst_positive_full_transform_table) + ge_balance_negative_full_transform_tableentryvalue = (dst_negative_full_transform_table) + ge_balance_positive_full_transform_tableentryvalue))))))))) -> (forall mi_index_full_all_inputs mi_value_full_all_inputs. ~(mi_index_full_all_inputs=0) -> (exists pvs_le_gap_full_all_inputsbound. pvs_le_gap_full_all_inputsbound + (mi_index_full_all_inputs) = (N)) -> (exists dst_positive_code_full_all_inputsentry dst_positive_scale_full_all_inputsentry dst_negative_code_full_all_inputsentry dst_negative_scale_full_all_inputsentry dst_positive_full_all_inputsentry dst_negative_full_all_inputsentry. (((G) = (((((dst_positive_code_full_all_inputsentry) + (dst_positive_scale_full_all_inputsentry)) * S ((dst_positive_code_full_all_inputsentry) + (dst_positive_scale_full_all_inputsentry)) + ((dst_positive_scale_full_all_inputsentry) + (dst_positive_scale_full_all_inputsentry))) + (((dst_negative_code_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)) * S ((dst_negative_code_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)) + ((dst_negative_scale_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)))) * S ((((dst_positive_code_full_all_inputsentry) + (dst_positive_scale_full_all_inputsentry)) * S ((dst_positive_code_full_all_inputsentry) + (dst_positive_scale_full_all_inputsentry)) + ((dst_positive_scale_full_all_inputsentry) + (dst_positive_scale_full_all_inputsentry))) + (((dst_negative_code_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)) * S ((dst_negative_code_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)) + ((dst_negative_scale_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)))) + ((((dst_negative_code_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)) * S ((dst_negative_code_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)) + ((dst_negative_scale_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry))) + (((dst_negative_code_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)) * S ((dst_negative_code_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)) + ((dst_negative_scale_full_all_inputsentry) + (dst_negative_scale_full_all_inputsentry)))))) /\ (((((exists ff_h_pvs_full_all_inputsentrypositive. ff_h_pvs_full_all_inputsentrypositive + S (dst_positive_full_all_inputsentry) = S ((S (mi_index_full_all_inputs)) * dst_positive_scale_full_all_inputsentry)) /\ exists ff_q_pvs_full_all_inputsentrypositive. dst_positive_code_full_all_inputsentry = ff_q_pvs_full_all_inputsentrypositive * S ((S (mi_index_full_all_inputs)) * dst_positive_scale_full_all_inputsentry) + (dst_positive_full_all_inputsentry))) /\ (((((exists ff_h_pvs_full_all_inputsentrynegative. ff_h_pvs_full_all_inputsentrynegative + S (dst_negative_full_all_inputsentry) = S ((S (mi_index_full_all_inputs)) * dst_negative_scale_full_all_inputsentry)) /\ exists ff_q_pvs_full_all_inputsentrynegative. dst_negative_code_full_all_inputsentry = ff_q_pvs_full_all_inputsentrynegative * S ((S (mi_index_full_all_inputs)) * dst_negative_scale_full_all_inputsentry) + (dst_negative_full_all_inputsentry))) /\ (exists ge_balance_positive_full_all_inputsentryvalue ge_balance_negative_full_all_inputsentryvalue. (((((mi_value_full_all_inputs) = 2 * (ge_balance_positive_full_all_inputsentryvalue) /\ (ge_balance_negative_full_all_inputsentryvalue) = 0) \/ exists ge_signed_half_full_all_inputsentryvaluedecode. (((mi_value_full_all_inputs) = 2 * ge_signed_half_full_all_inputsentryvaluedecode + 1 /\ (ge_balance_positive_full_all_inputsentryvalue) = 0) /\ (ge_balance_negative_full_all_inputsentryvalue) = S ge_signed_half_full_all_inputsentryvaluedecode))) /\ ((dst_positive_full_all_inputsentry) + ge_balance_negative_full_all_inputsentryvalue = (dst_negative_full_all_inputsentry) + ge_balance_positive_full_all_inputsentryvalue))))))))) -> (((~((mi_index_full_all_inputs)=0)) /\ (exists dm_mask_table_full_all_inputssum. ((((exists dst_positive_code_full_all_inputssummasktable dst_positive_scale_full_all_inputssummasktable dst_negative_code_full_all_inputssummasktable dst_negative_scale_full_all_inputssummasktable. (((dm_mask_table_full_all_inputssum) = (((((dst_positive_code_full_all_inputssummasktable) + (dst_positive_scale_full_all_inputssummasktable)) * S ((dst_positive_code_full_all_inputssummasktable) + (dst_positive_scale_full_all_inputssummasktable)) + ((dst_positive_scale_full_all_inputssummasktable) + (dst_positive_scale_full_all_inputssummasktable))) + (((dst_negative_code_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)) * S ((dst_negative_code_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)) + ((dst_negative_scale_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)))) * S ((((dst_positive_code_full_all_inputssummasktable) + (dst_positive_scale_full_all_inputssummasktable)) * S ((dst_positive_code_full_all_inputssummasktable) + (dst_positive_scale_full_all_inputssummasktable)) + ((dst_positive_scale_full_all_inputssummasktable) + (dst_positive_scale_full_all_inputssummasktable))) + (((dst_negative_code_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)) * S ((dst_negative_code_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)) + ((dst_negative_scale_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)))) + ((((dst_negative_code_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)) * S ((dst_negative_code_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)) + ((dst_negative_scale_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable))) + (((dst_negative_code_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)) * S ((dst_negative_code_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)) + ((dst_negative_scale_full_all_inputssummasktable) + (dst_negative_scale_full_all_inputssummasktable)))))) /\ (forall dst_index_full_all_inputssummasktable. (exists pvs_le_gap_full_all_inputssummasktabledomain. pvs_le_gap_full_all_inputssummasktabledomain + (dst_index_full_all_inputssummasktable) = (mi_index_full_all_inputs)) -> exists dst_positive_full_all_inputssummasktable dst_negative_full_all_inputssummasktable dst_value_full_all_inputssummasktable. ((((exists ff_h_pvs_full_all_inputssummasktableentrypositive. ff_h_pvs_full_all_inputssummasktableentrypositive + S (dst_positive_full_all_inputssummasktable) = S ((S (dst_index_full_all_inputssummasktable)) * dst_positive_scale_full_all_inputssummasktable)) /\ exists ff_q_pvs_full_all_inputssummasktableentrypositive. dst_positive_code_full_all_inputssummasktable = ff_q_pvs_full_all_inputssummasktableentrypositive * S ((S (dst_index_full_all_inputssummasktable)) * dst_positive_scale_full_all_inputssummasktable) + (dst_positive_full_all_inputssummasktable))) /\ (((((exists ff_h_pvs_full_all_inputssummasktableentrynegative. ff_h_pvs_full_all_inputssummasktableentrynegative + S (dst_negative_full_all_inputssummasktable) = S ((S (dst_index_full_all_inputssummasktable)) * dst_negative_scale_full_all_inputssummasktable)) /\ exists ff_q_pvs_full_all_inputssummasktableentrynegative. dst_negative_code_full_all_inputssummasktable = ff_q_pvs_full_all_inputssummasktableentrynegative * S ((S (dst_index_full_all_inputssummasktable)) * dst_negative_scale_full_all_inputssummasktable) + (dst_negative_full_all_inputssummasktable))) /\ (exists ge_balance_positive_full_all_inputssummasktableentryvalue ge_balance_negative_full_all_inputssummasktableentryvalue. (((((dst_value_full_all_inputssummasktable) = 2 * (ge_balance_positive_full_all_inputssummasktableentryvalue) /\ (ge_balance_negative_full_all_inputssummasktableentryvalue) = 0) \/ exists ge_signed_half_full_all_inputssummasktableentryvaluedecode. (((dst_value_full_all_inputssummasktable) = 2 * ge_signed_half_full_all_inputssummasktableentryvaluedecode + 1 /\ (ge_balance_positive_full_all_inputssummasktableentryvalue) = 0) /\ (ge_balance_negative_full_all_inputssummasktableentryvalue) = S ge_signed_half_full_all_inputssummasktableentryvaluedecode))) /\ ((dst_positive_full_all_inputssummasktable) + ge_balance_negative_full_all_inputssummasktableentryvalue = (dst_negative_full_all_inputssummasktable) + ge_balance_positive_full_all_inputssummasktableentryvalue))))))))) /\ (forall dm_index_full_all_inputssummask dm_value_full_all_inputssummask. (exists pvs_le_gap_full_all_inputssummaskdomain. pvs_le_gap_full_all_inputssummaskdomain + (dm_index_full_all_inputssummask) = (mi_index_full_all_inputs)) -> (exists dst_positive_code_full_all_inputssummasklookup dst_positive_scale_full_all_inputssummasklookup dst_negative_code_full_all_inputssummasklookup dst_negative_scale_full_all_inputssummasklookup dst_positive_full_all_inputssummasklookup dst_negative_full_all_inputssummasklookup. (((dm_mask_table_full_all_inputssum) = (((((dst_positive_code_full_all_inputssummasklookup) + (dst_positive_scale_full_all_inputssummasklookup)) * S ((dst_positive_code_full_all_inputssummasklookup) + (dst_positive_scale_full_all_inputssummasklookup)) + ((dst_positive_scale_full_all_inputssummasklookup) + (dst_positive_scale_full_all_inputssummasklookup))) + (((dst_negative_code_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)) * S ((dst_negative_code_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)) + ((dst_negative_scale_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)))) * S ((((dst_positive_code_full_all_inputssummasklookup) + (dst_positive_scale_full_all_inputssummasklookup)) * S ((dst_positive_code_full_all_inputssummasklookup) + (dst_positive_scale_full_all_inputssummasklookup)) + ((dst_positive_scale_full_all_inputssummasklookup) + (dst_positive_scale_full_all_inputssummasklookup))) + (((dst_negative_code_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)) * S ((dst_negative_code_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)) + ((dst_negative_scale_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)))) + ((((dst_negative_code_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)) * S ((dst_negative_code_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)) + ((dst_negative_scale_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup))) + (((dst_negative_code_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)) * S ((dst_negative_code_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)) + ((dst_negative_scale_full_all_inputssummasklookup) + (dst_negative_scale_full_all_inputssummasklookup)))))) /\ (((((exists ff_h_pvs_full_all_inputssummasklookuppositive. ff_h_pvs_full_all_inputssummasklookuppositive + S (dst_positive_full_all_inputssummasklookup) = S ((S (dm_index_full_all_inputssummask)) * dst_positive_scale_full_all_inputssummasklookup)) /\ exists ff_q_pvs_full_all_inputssummasklookuppositive. dst_positive_code_full_all_inputssummasklookup = ff_q_pvs_full_all_inputssummasklookuppositive * S ((S (dm_index_full_all_inputssummask)) * dst_positive_scale_full_all_inputssummasklookup) + (dst_positive_full_all_inputssummasklookup))) /\ (((((exists ff_h_pvs_full_all_inputssummasklookupnegative. ff_h_pvs_full_all_inputssummasklookupnegative + S (dst_negative_full_all_inputssummasklookup) = S ((S (dm_index_full_all_inputssummask)) * dst_negative_scale_full_all_inputssummasklookup)) /\ exists ff_q_pvs_full_all_inputssummasklookupnegative. dst_negative_code_full_all_inputssummasklookup = ff_q_pvs_full_all_inputssummasklookupnegative * S ((S (dm_index_full_all_inputssummask)) * dst_negative_scale_full_all_inputssummasklookup) + (dst_negative_full_all_inputssummasklookup))) /\ (exists ge_balance_positive_full_all_inputssummasklookupvalue ge_balance_negative_full_all_inputssummasklookupvalue. (((((dm_value_full_all_inputssummask) = 2 * (ge_balance_positive_full_all_inputssummasklookupvalue) /\ (ge_balance_negative_full_all_inputssummasklookupvalue) = 0) \/ exists ge_signed_half_full_all_inputssummasklookupvaluedecode. (((dm_value_full_all_inputssummask) = 2 * ge_signed_half_full_all_inputssummasklookupvaluedecode + 1 /\ (ge_balance_positive_full_all_inputssummasklookupvalue) = 0) /\ (ge_balance_negative_full_all_inputssummasklookupvalue) = S ge_signed_half_full_all_inputssummasklookupvaluedecode))) /\ ((dst_positive_full_all_inputssummasklookup) + ge_balance_negative_full_all_inputssummasklookupvalue = (dst_negative_full_all_inputssummasklookup) + ge_balance_positive_full_all_inputssummasklookupvalue))))))))) -> ((((~((dm_index_full_all_inputssummask)=0)) /\ (exists dm_quotient_full_all_inputssummaskentry. (((mi_index_full_all_inputs)=(dm_index_full_all_inputssummask)*dm_quotient_full_all_inputssummaskentry) /\ (exists dst_positive_code_full_all_inputssummaskentryinput dst_positive_scale_full_all_inputssummaskentryinput dst_negative_code_full_all_inputssummaskentryinput dst_negative_scale_full_all_inputssummaskentryinput dst_positive_full_all_inputssummaskentryinput dst_negative_full_all_inputssummaskentryinput. (((F) = (((((dst_positive_code_full_all_inputssummaskentryinput) + (dst_positive_scale_full_all_inputssummaskentryinput)) * S ((dst_positive_code_full_all_inputssummaskentryinput) + (dst_positive_scale_full_all_inputssummaskentryinput)) + ((dst_positive_scale_full_all_inputssummaskentryinput) + (dst_positive_scale_full_all_inputssummaskentryinput))) + (((dst_negative_code_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)) * S ((dst_negative_code_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)) + ((dst_negative_scale_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)))) * S ((((dst_positive_code_full_all_inputssummaskentryinput) + (dst_positive_scale_full_all_inputssummaskentryinput)) * S ((dst_positive_code_full_all_inputssummaskentryinput) + (dst_positive_scale_full_all_inputssummaskentryinput)) + ((dst_positive_scale_full_all_inputssummaskentryinput) + (dst_positive_scale_full_all_inputssummaskentryinput))) + (((dst_negative_code_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)) * S ((dst_negative_code_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)) + ((dst_negative_scale_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)))) + ((((dst_negative_code_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)) * S ((dst_negative_code_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)) + ((dst_negative_scale_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput))) + (((dst_negative_code_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)) * S ((dst_negative_code_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)) + ((dst_negative_scale_full_all_inputssummaskentryinput) + (dst_negative_scale_full_all_inputssummaskentryinput)))))) /\ (((((exists ff_h_pvs_full_all_inputssummaskentryinputpositive. ff_h_pvs_full_all_inputssummaskentryinputpositive + S (dst_positive_full_all_inputssummaskentryinput) = S ((S (dm_index_full_all_inputssummask)) * dst_positive_scale_full_all_inputssummaskentryinput)) /\ exists ff_q_pvs_full_all_inputssummaskentryinputpositive. dst_positive_code_full_all_inputssummaskentryinput = ff_q_pvs_full_all_inputssummaskentryinputpositive * S ((S (dm_index_full_all_inputssummask)) * dst_positive_scale_full_all_inputssummaskentryinput) + (dst_positive_full_all_inputssummaskentryinput))) /\ (((((exists ff_h_pvs_full_all_inputssummaskentryinputnegative. ff_h_pvs_full_all_inputssummaskentryinputnegative + S (dst_negative_full_all_inputssummaskentryinput) = S ((S (dm_index_full_all_inputssummask)) * dst_negative_scale_full_all_inputssummaskentryinput)) /\ exists ff_q_pvs_full_all_inputssummaskentryinputnegative. dst_negative_code_full_all_inputssummaskentryinput = ff_q_pvs_full_all_inputssummaskentryinputnegative * S ((S (dm_index_full_all_inputssummask)) * dst_negative_scale_full_all_inputssummaskentryinput) + (dst_negative_full_all_inputssummaskentryinput))) /\ (exists ge_balance_positive_full_all_inputssummaskentryinputvalue ge_balance_negative_full_all_inputssummaskentryinputvalue. (((((dm_value_full_all_inputssummask) = 2 * (ge_balance_positive_full_all_inputssummaskentryinputvalue) /\ (ge_balance_negative_full_all_inputssummaskentryinputvalue) = 0) \/ exists ge_signed_half_full_all_inputssummaskentryinputvaluedecode. (((dm_value_full_all_inputssummask) = 2 * ge_signed_half_full_all_inputssummaskentryinputvaluedecode + 1 /\ (ge_balance_positive_full_all_inputssummaskentryinputvalue) = 0) /\ (ge_balance_negative_full_all_inputssummaskentryinputvalue) = S ge_signed_half_full_all_inputssummaskentryinputvaluedecode))) /\ ((dst_positive_full_all_inputssummaskentryinput) + ge_balance_negative_full_all_inputssummaskentryinputvalue = (dst_negative_full_all_inputssummaskentryinput) + ge_balance_positive_full_all_inputssummaskentryinputvalue))))))))))))) \/ ((((dm_index_full_all_inputssummask)=0 \/ ~(exists pvs_factor_full_all_inputssummaskentrynondivisor. (mi_index_full_all_inputs) = (dm_index_full_all_inputssummask) * pvs_factor_full_all_inputssummaskentrynondivisor)) /\ ((dm_value_full_all_inputssummask)=0))))))) /\ (exists dst_positive_code_full_all_inputssumfold dst_positive_scale_full_all_inputssumfold dst_negative_code_full_all_inputssumfold dst_negative_scale_full_all_inputssumfold dst_positive_sum_full_all_inputssumfold dst_negative_sum_full_all_inputssumfold. (((dm_mask_table_full_all_inputssum) = (((((dst_positive_code_full_all_inputssumfold) + (dst_positive_scale_full_all_inputssumfold)) * S ((dst_positive_code_full_all_inputssumfold) + (dst_positive_scale_full_all_inputssumfold)) + ((dst_positive_scale_full_all_inputssumfold) + (dst_positive_scale_full_all_inputssumfold))) + (((dst_negative_code_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)) * S ((dst_negative_code_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)) + ((dst_negative_scale_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)))) * S ((((dst_positive_code_full_all_inputssumfold) + (dst_positive_scale_full_all_inputssumfold)) * S ((dst_positive_code_full_all_inputssumfold) + (dst_positive_scale_full_all_inputssumfold)) + ((dst_positive_scale_full_all_inputssumfold) + (dst_positive_scale_full_all_inputssumfold))) + (((dst_negative_code_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)) * S ((dst_negative_code_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)) + ((dst_negative_scale_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)))) + ((((dst_negative_code_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)) * S ((dst_negative_code_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)) + ((dst_negative_scale_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold))) + (((dst_negative_code_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)) * S ((dst_negative_code_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)) + ((dst_negative_scale_full_all_inputssumfold) + (dst_negative_scale_full_all_inputssumfold)))))) /\ (((exists fs_u_dst_full_all_inputssumfoldpositive fs_v_dst_full_all_inputssumfoldpositive. ((((exists fs_h_dst_full_all_inputssumfoldpositive_body_start. fs_h_dst_full_all_inputssumfoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_full_all_inputssumfoldpositive)) /\ exists fs_q_dst_full_all_inputssumfoldpositive_body_start. fs_u_dst_full_all_inputssumfoldpositive = fs_q_dst_full_all_inputssumfoldpositive_body_start * S ((S (0)) * fs_v_dst_full_all_inputssumfoldpositive) + (0))) /\ ((((exists fs_h_dst_full_all_inputssumfoldpositive_body_terminal. fs_h_dst_full_all_inputssumfoldpositive_body_terminal + S (dst_positive_sum_full_all_inputssumfold) = S ((S (S (mi_index_full_all_inputs))) * fs_v_dst_full_all_inputssumfoldpositive)) /\ exists fs_q_dst_full_all_inputssumfoldpositive_body_terminal. fs_u_dst_full_all_inputssumfoldpositive = fs_q_dst_full_all_inputssumfoldpositive_body_terminal * S ((S (S (mi_index_full_all_inputs))) * fs_v_dst_full_all_inputssumfoldpositive) + (dst_positive_sum_full_all_inputssumfold))) /\ forall fs_i_dst_full_all_inputssumfoldpositive_body_steps. (exists fs_lt_dst_full_all_inputssumfoldpositive_body_steps_bound. fs_lt_dst_full_all_inputssumfoldpositive_body_steps_bound + S fs_i_dst_full_all_inputssumfoldpositive_body_steps = S (mi_index_full_all_inputs)) -> exists fs_a_dst_full_all_inputssumfoldpositive_body_steps fs_r_dst_full_all_inputssumfoldpositive_body_steps fs_s_dst_full_all_inputssumfoldpositive_body_steps. ((((exists fs_h_dst_full_all_inputssumfoldpositive_body_steps_summand. fs_h_dst_full_all_inputssumfoldpositive_body_steps_summand + S (fs_a_dst_full_all_inputssumfoldpositive_body_steps) = S ((S (fs_i_dst_full_all_inputssumfoldpositive_body_steps)) * dst_positive_scale_full_all_inputssumfold)) /\ exists fs_q_dst_full_all_inputssumfoldpositive_body_steps_summand. dst_positive_code_full_all_inputssumfold = fs_q_dst_full_all_inputssumfoldpositive_body_steps_summand * S ((S (fs_i_dst_full_all_inputssumfoldpositive_body_steps)) * dst_positive_scale_full_all_inputssumfold) + (fs_a_dst_full_all_inputssumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_full_all_inputssumfoldpositive_body_steps_partial. fs_h_dst_full_all_inputssumfoldpositive_body_steps_partial + S (fs_r_dst_full_all_inputssumfoldpositive_body_steps) = S ((S (fs_i_dst_full_all_inputssumfoldpositive_body_steps)) * fs_v_dst_full_all_inputssumfoldpositive)) /\ exists fs_q_dst_full_all_inputssumfoldpositive_body_steps_partial. fs_u_dst_full_all_inputssumfoldpositive = fs_q_dst_full_all_inputssumfoldpositive_body_steps_partial * S ((S (fs_i_dst_full_all_inputssumfoldpositive_body_steps)) * fs_v_dst_full_all_inputssumfoldpositive) + (fs_r_dst_full_all_inputssumfoldpositive_body_steps))) /\ ((((exists fs_h_dst_full_all_inputssumfoldpositive_body_steps_successor. fs_h_dst_full_all_inputssumfoldpositive_body_steps_successor + S (fs_s_dst_full_all_inputssumfoldpositive_body_steps) = S ((S (S fs_i_dst_full_all_inputssumfoldpositive_body_steps)) * fs_v_dst_full_all_inputssumfoldpositive)) /\ exists fs_q_dst_full_all_inputssumfoldpositive_body_steps_successor. fs_u_dst_full_all_inputssumfoldpositive = fs_q_dst_full_all_inputssumfoldpositive_body_steps_successor * S ((S (S fs_i_dst_full_all_inputssumfoldpositive_body_steps)) * fs_v_dst_full_all_inputssumfoldpositive) + (fs_s_dst_full_all_inputssumfoldpositive_body_steps))) /\ fs_s_dst_full_all_inputssumfoldpositive_body_steps = fs_r_dst_full_all_inputssumfoldpositive_body_steps + fs_a_dst_full_all_inputssumfoldpositive_body_steps)))))) /\ (((exists fs_u_dst_full_all_inputssumfoldnegative fs_v_dst_full_all_inputssumfoldnegative. ((((exists fs_h_dst_full_all_inputssumfoldnegative_body_start. fs_h_dst_full_all_inputssumfoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_full_all_inputssumfoldnegative)) /\ exists fs_q_dst_full_all_inputssumfoldnegative_body_start. fs_u_dst_full_all_inputssumfoldnegative = fs_q_dst_full_all_inputssumfoldnegative_body_start * S ((S (0)) * fs_v_dst_full_all_inputssumfoldnegative) + (0))) /\ ((((exists fs_h_dst_full_all_inputssumfoldnegative_body_terminal. fs_h_dst_full_all_inputssumfoldnegative_body_terminal + S (dst_negative_sum_full_all_inputssumfold) = S ((S (S (mi_index_full_all_inputs))) * fs_v_dst_full_all_inputssumfoldnegative)) /\ exists fs_q_dst_full_all_inputssumfoldnegative_body_terminal. fs_u_dst_full_all_inputssumfoldnegative = fs_q_dst_full_all_inputssumfoldnegative_body_terminal * S ((S (S (mi_index_full_all_inputs))) * fs_v_dst_full_all_inputssumfoldnegative) + (dst_negative_sum_full_all_inputssumfold))) /\ forall fs_i_dst_full_all_inputssumfoldnegative_body_steps. (exists fs_lt_dst_full_all_inputssumfoldnegative_body_steps_bound. fs_lt_dst_full_all_inputssumfoldnegative_body_steps_bound + S fs_i_dst_full_all_inputssumfoldnegative_body_steps = S (mi_index_full_all_inputs)) -> exists fs_a_dst_full_all_inputssumfoldnegative_body_steps fs_r_dst_full_all_inputssumfoldnegative_body_steps fs_s_dst_full_all_inputssumfoldnegative_body_steps. ((((exists fs_h_dst_full_all_inputssumfoldnegative_body_steps_summand. fs_h_dst_full_all_inputssumfoldnegative_body_steps_summand + S (fs_a_dst_full_all_inputssumfoldnegative_body_steps) = S ((S (fs_i_dst_full_all_inputssumfoldnegative_body_steps)) * dst_negative_scale_full_all_inputssumfold)) /\ exists fs_q_dst_full_all_inputssumfoldnegative_body_steps_summand. dst_negative_code_full_all_inputssumfold = fs_q_dst_full_all_inputssumfoldnegative_body_steps_summand * S ((S (fs_i_dst_full_all_inputssumfoldnegative_body_steps)) * dst_negative_scale_full_all_inputssumfold) + (fs_a_dst_full_all_inputssumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_full_all_inputssumfoldnegative_body_steps_partial. fs_h_dst_full_all_inputssumfoldnegative_body_steps_partial + S (fs_r_dst_full_all_inputssumfoldnegative_body_steps) = S ((S (fs_i_dst_full_all_inputssumfoldnegative_body_steps)) * fs_v_dst_full_all_inputssumfoldnegative)) /\ exists fs_q_dst_full_all_inputssumfoldnegative_body_steps_partial. fs_u_dst_full_all_inputssumfoldnegative = fs_q_dst_full_all_inputssumfoldnegative_body_steps_partial * S ((S (fs_i_dst_full_all_inputssumfoldnegative_body_steps)) * fs_v_dst_full_all_inputssumfoldnegative) + (fs_r_dst_full_all_inputssumfoldnegative_body_steps))) /\ ((((exists fs_h_dst_full_all_inputssumfoldnegative_body_steps_successor. fs_h_dst_full_all_inputssumfoldnegative_body_steps_successor + S (fs_s_dst_full_all_inputssumfoldnegative_body_steps) = S ((S (S fs_i_dst_full_all_inputssumfoldnegative_body_steps)) * fs_v_dst_full_all_inputssumfoldnegative)) /\ exists fs_q_dst_full_all_inputssumfoldnegative_body_steps_successor. fs_u_dst_full_all_inputssumfoldnegative = fs_q_dst_full_all_inputssumfoldnegative_body_steps_successor * S ((S (S fs_i_dst_full_all_inputssumfoldnegative_body_steps)) * fs_v_dst_full_all_inputssumfoldnegative) + (fs_s_dst_full_all_inputssumfoldnegative_body_steps))) /\ fs_s_dst_full_all_inputssumfoldnegative_body_steps = fs_r_dst_full_all_inputssumfoldnegative_body_steps + fs_a_dst_full_all_inputssumfoldnegative_body_steps)))))) /\ (exists ge_balance_positive_full_all_inputssumfoldresult ge_balance_negative_full_all_inputssumfoldresult. (((((mi_value_full_all_inputs) = 2 * (ge_balance_positive_full_all_inputssumfoldresult) /\ (ge_balance_negative_full_all_inputssumfoldresult) = 0) \/ exists ge_signed_half_full_all_inputssumfoldresultdecode. (((mi_value_full_all_inputs) = 2 * ge_signed_half_full_all_inputssumfoldresultdecode + 1 /\ (ge_balance_positive_full_all_inputssumfoldresult) = 0) /\ (ge_balance_negative_full_all_inputssumfoldresult) = S ge_signed_half_full_all_inputssumfoldresultdecode))) /\ ((dst_positive_sum_full_all_inputssumfold) + ge_balance_negative_full_all_inputssumfoldresult = (dst_negative_sum_full_all_inputssumfold) + ge_balance_positive_full_all_inputssumfoldresult)))))))))))))) -> exists M H. ((((exists dst_positive_code_full_mobius_witnesstable dst_positive_scale_full_mobius_witnesstable dst_negative_code_full_mobius_witnesstable dst_negative_scale_full_mobius_witnesstable. (((M) = (((((dst_positive_code_full_mobius_witnesstable) + (dst_positive_scale_full_mobius_witnesstable)) * S ((dst_positive_code_full_mobius_witnesstable) + (dst_positive_scale_full_mobius_witnesstable)) + ((dst_positive_scale_full_mobius_witnesstable) + (dst_positive_scale_full_mobius_witnesstable))) + (((dst_negative_code_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)) * S ((dst_negative_code_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)) + ((dst_negative_scale_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)))) * S ((((dst_positive_code_full_mobius_witnesstable) + (dst_positive_scale_full_mobius_witnesstable)) * S ((dst_positive_code_full_mobius_witnesstable) + (dst_positive_scale_full_mobius_witnesstable)) + ((dst_positive_scale_full_mobius_witnesstable) + (dst_positive_scale_full_mobius_witnesstable))) + (((dst_negative_code_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)) * S ((dst_negative_code_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)) + ((dst_negative_scale_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)))) + ((((dst_negative_code_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)) * S ((dst_negative_code_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)) + ((dst_negative_scale_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable))) + (((dst_negative_code_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)) * S ((dst_negative_code_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)) + ((dst_negative_scale_full_mobius_witnesstable) + (dst_negative_scale_full_mobius_witnesstable)))))) /\ (forall dst_index_full_mobius_witnesstable. (exists pvs_le_gap_full_mobius_witnesstabledomain. pvs_le_gap_full_mobius_witnesstabledomain + (dst_index_full_mobius_witnesstable) = (N)) -> exists dst_positive_full_mobius_witnesstable dst_negative_full_mobius_witnesstable dst_value_full_mobius_witnesstable. ((((exists ff_h_pvs_full_mobius_witnesstableentrypositive. ff_h_pvs_full_mobius_witnesstableentrypositive + S (dst_positive_full_mobius_witnesstable) = S ((S (dst_index_full_mobius_witnesstable)) * dst_positive_scale_full_mobius_witnesstable)) /\ exists ff_q_pvs_full_mobius_witnesstableentrypositive. dst_positive_code_full_mobius_witnesstable = ff_q_pvs_full_mobius_witnesstableentrypositive * S ((S (dst_index_full_mobius_witnesstable)) * dst_positive_scale_full_mobius_witnesstable) + (dst_positive_full_mobius_witnesstable))) /\ (((((exists ff_h_pvs_full_mobius_witnesstableentrynegative. ff_h_pvs_full_mobius_witnesstableentrynegative + S (dst_negative_full_mobius_witnesstable) = S ((S (dst_index_full_mobius_witnesstable)) * dst_negative_scale_full_mobius_witnesstable)) /\ exists ff_q_pvs_full_mobius_witnesstableentrynegative. dst_negative_code_full_mobius_witnesstable = ff_q_pvs_full_mobius_witnesstableentrynegative * S ((S (dst_index_full_mobius_witnesstable)) * dst_negative_scale_full_mobius_witnesstable) + (dst_negative_full_mobius_witnesstable))) /\ (exists ge_balance_positive_full_mobius_witnesstableentryvalue ge_balance_negative_full_mobius_witnesstableentryvalue. (((((dst_value_full_mobius_witnesstable) = 2 * (ge_balance_positive_full_mobius_witnesstableentryvalue) /\ (ge_balance_negative_full_mobius_witnesstableentryvalue) = 0) \/ exists ge_signed_half_full_mobius_witnesstableentryvaluedecode. (((dst_value_full_mobius_witnesstable) = 2 * ge_signed_half_full_mobius_witnesstableentryvaluedecode + 1 /\ (ge_balance_positive_full_mobius_witnesstableentryvalue) = 0) /\ (ge_balance_negative_full_mobius_witnesstableentryvalue) = S ge_signed_half_full_mobius_witnesstableentryvaluedecode))) /\ ((dst_positive_full_mobius_witnesstable) + ge_balance_negative_full_mobius_witnesstableentryvalue = (dst_negative_full_mobius_witnesstable) + ge_balance_positive_full_mobius_witnesstableentryvalue))))))))) /\ (((exists dst_positive_code_full_mobius_witnesszero dst_positive_scale_full_mobius_witnesszero dst_negative_code_full_mobius_witnesszero dst_negative_scale_full_mobius_witnesszero dst_positive_full_mobius_witnesszero dst_negative_full_mobius_witnesszero. (((M) = (((((dst_positive_code_full_mobius_witnesszero) + (dst_positive_scale_full_mobius_witnesszero)) * S ((dst_positive_code_full_mobius_witnesszero) + (dst_positive_scale_full_mobius_witnesszero)) + ((dst_positive_scale_full_mobius_witnesszero) + (dst_positive_scale_full_mobius_witnesszero))) + (((dst_negative_code_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)) * S ((dst_negative_code_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)) + ((dst_negative_scale_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)))) * S ((((dst_positive_code_full_mobius_witnesszero) + (dst_positive_scale_full_mobius_witnesszero)) * S ((dst_positive_code_full_mobius_witnesszero) + (dst_positive_scale_full_mobius_witnesszero)) + ((dst_positive_scale_full_mobius_witnesszero) + (dst_positive_scale_full_mobius_witnesszero))) + (((dst_negative_code_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)) * S ((dst_negative_code_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)) + ((dst_negative_scale_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)))) + ((((dst_negative_code_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)) * S ((dst_negative_code_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)) + ((dst_negative_scale_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero))) + (((dst_negative_code_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)) * S ((dst_negative_code_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)) + ((dst_negative_scale_full_mobius_witnesszero) + (dst_negative_scale_full_mobius_witnesszero)))))) /\ (((((exists ff_h_pvs_full_mobius_witnesszeropositive. ff_h_pvs_full_mobius_witnesszeropositive + S (dst_positive_full_mobius_witnesszero) = S ((S (0)) * dst_positive_scale_full_mobius_witnesszero)) /\ exists ff_q_pvs_full_mobius_witnesszeropositive. dst_positive_code_full_mobius_witnesszero = ff_q_pvs_full_mobius_witnesszeropositive * S ((S (0)) * dst_positive_scale_full_mobius_witnesszero) + (dst_positive_full_mobius_witnesszero))) /\ (((((exists ff_h_pvs_full_mobius_witnesszeronegative. ff_h_pvs_full_mobius_witnesszeronegative + S (dst_negative_full_mobius_witnesszero) = S ((S (0)) * dst_negative_scale_full_mobius_witnesszero)) /\ exists ff_q_pvs_full_mobius_witnesszeronegative. dst_negative_code_full_mobius_witnesszero = ff_q_pvs_full_mobius_witnesszeronegative * S ((S (0)) * dst_negative_scale_full_mobius_witnesszero) + (dst_negative_full_mobius_witnesszero))) /\ (exists ge_balance_positive_full_mobius_witnesszerovalue ge_balance_negative_full_mobius_witnesszerovalue. (((((0) = 2 * (ge_balance_positive_full_mobius_witnesszerovalue) /\ (ge_balance_negative_full_mobius_witnesszerovalue) = 0) \/ exists ge_signed_half_full_mobius_witnesszerovaluedecode. (((0) = 2 * ge_signed_half_full_mobius_witnesszerovaluedecode + 1 /\ (ge_balance_positive_full_mobius_witnesszerovalue) = 0) /\ (ge_balance_negative_full_mobius_witnesszerovalue) = S ge_signed_half_full_mobius_witnesszerovaluedecode))) /\ ((dst_positive_full_mobius_witnesszero) + ge_balance_negative_full_mobius_witnesszerovalue = (dst_negative_full_mobius_witnesszero) + ge_balance_positive_full_mobius_witnesszerovalue))))))))) /\ (forall mt_index_full_mobius_witness mt_value_full_mobius_witness. ~(mt_index_full_mobius_witness=0) -> (exists pvs_le_gap_full_mobius_witnessdomain. pvs_le_gap_full_mobius_witnessdomain + (mt_index_full_mobius_witness) = (N)) -> (exists dst_positive_code_full_mobius_witnessentry dst_positive_scale_full_mobius_witnessentry dst_negative_code_full_mobius_witnessentry dst_negative_scale_full_mobius_witnessentry dst_positive_full_mobius_witnessentry dst_negative_full_mobius_witnessentry. (((M) = (((((dst_positive_code_full_mobius_witnessentry) + (dst_positive_scale_full_mobius_witnessentry)) * S ((dst_positive_code_full_mobius_witnessentry) + (dst_positive_scale_full_mobius_witnessentry)) + ((dst_positive_scale_full_mobius_witnessentry) + (dst_positive_scale_full_mobius_witnessentry))) + (((dst_negative_code_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)) * S ((dst_negative_code_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)) + ((dst_negative_scale_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)))) * S ((((dst_positive_code_full_mobius_witnessentry) + (dst_positive_scale_full_mobius_witnessentry)) * S ((dst_positive_code_full_mobius_witnessentry) + (dst_positive_scale_full_mobius_witnessentry)) + ((dst_positive_scale_full_mobius_witnessentry) + (dst_positive_scale_full_mobius_witnessentry))) + (((dst_negative_code_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)) * S ((dst_negative_code_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)) + ((dst_negative_scale_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)))) + ((((dst_negative_code_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)) * S ((dst_negative_code_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)) + ((dst_negative_scale_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry))) + (((dst_negative_code_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)) * S ((dst_negative_code_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)) + ((dst_negative_scale_full_mobius_witnessentry) + (dst_negative_scale_full_mobius_witnessentry)))))) /\ (((((exists ff_h_pvs_full_mobius_witnessentrypositive. ff_h_pvs_full_mobius_witnessentrypositive + S (dst_positive_full_mobius_witnessentry) = S ((S (mt_index_full_mobius_witness)) * dst_positive_scale_full_mobius_witnessentry)) /\ exists ff_q_pvs_full_mobius_witnessentrypositive. dst_positive_code_full_mobius_witnessentry = ff_q_pvs_full_mobius_witnessentrypositive * S ((S (mt_index_full_mobius_witness)) * dst_positive_scale_full_mobius_witnessentry) + (dst_positive_full_mobius_witnessentry))) /\ (((((exists ff_h_pvs_full_mobius_witnessentrynegative. ff_h_pvs_full_mobius_witnessentrynegative + S (dst_negative_full_mobius_witnessentry) = S ((S (mt_index_full_mobius_witness)) * dst_negative_scale_full_mobius_witnessentry)) /\ exists ff_q_pvs_full_mobius_witnessentrynegative. dst_negative_code_full_mobius_witnessentry = ff_q_pvs_full_mobius_witnessentrynegative * S ((S (mt_index_full_mobius_witness)) * dst_negative_scale_full_mobius_witnessentry) + (dst_negative_full_mobius_witnessentry))) /\ (exists ge_balance_positive_full_mobius_witnessentryvalue ge_balance_negative_full_mobius_witnessentryvalue. (((((mt_value_full_mobius_witness) = 2 * (ge_balance_positive_full_mobius_witnessentryvalue) /\ (ge_balance_negative_full_mobius_witnessentryvalue) = 0) \/ exists ge_signed_half_full_mobius_witnessentryvaluedecode. (((mt_value_full_mobius_witness) = 2 * ge_signed_half_full_mobius_witnessentryvaluedecode + 1 /\ (ge_balance_positive_full_mobius_witnessentryvalue) = 0) /\ (ge_balance_negative_full_mobius_witnessentryvalue) = S ge_signed_half_full_mobius_witnessentryvaluedecode))) /\ ((dst_positive_full_mobius_witnessentry) + ge_balance_negative_full_mobius_witnessentryvalue = (dst_negative_full_mobius_witnessentry) + ge_balance_positive_full_mobius_witnessentryvalue))))))))) -> (((~((mt_index_full_mobius_witness) = 0)) /\ ((((exists mv_square_prime_full_mobius_witnessvaluesquare. ((~((mv_square_prime_full_mobius_witnessvaluesquare) = 1) /\ forall pvs_left_full_mobius_witnessvaluesquareprime pvs_right_full_mobius_witnessvaluesquareprime. (mv_square_prime_full_mobius_witnessvaluesquare) = pvs_left_full_mobius_witnessvaluesquareprime * pvs_right_full_mobius_witnessvaluesquareprime -> pvs_left_full_mobius_witnessvaluesquareprime = 1 \/ pvs_right_full_mobius_witnessvaluesquareprime = 1) /\ (exists pvs_factor_full_mobius_witnessvaluesquaredivisor. (mt_index_full_mobius_witness) = (mv_square_prime_full_mobius_witnessvaluesquare * mv_square_prime_full_mobius_witnessvaluesquare) * pvs_factor_full_mobius_witnessvaluesquaredivisor))) /\ ((mt_value_full_mobius_witness) = 0))) \/ (((((~((mt_index_full_mobius_witness) = 0)) /\ (forall sfd_prime_full_mobius_witnessvaluesquarefree. (~((sfd_prime_full_mobius_witnessvaluesquarefree) = 1) /\ forall pvs_left_full_mobius_witnessvaluesquarefreedomain pvs_right_full_mobius_witnessvaluesquarefreedomain. (sfd_prime_full_mobius_witnessvaluesquarefree) = pvs_left_full_mobius_witnessvaluesquarefreedomain * pvs_right_full_mobius_witnessvaluesquarefreedomain -> pvs_left_full_mobius_witnessvaluesquarefreedomain = 1 \/ pvs_right_full_mobius_witnessvaluesquarefreedomain = 1) -> (exists pvs_le_gap_full_mobius_witnessvaluesquarefreebound. pvs_le_gap_full_mobius_witnessvaluesquarefreebound + (sfd_prime_full_mobius_witnessvaluesquarefree) = (mt_index_full_mobius_witness)) -> ~(exists pvs_factor_full_mobius_witnessvaluesquarefreesquare. (mt_index_full_mobius_witness) = (sfd_prime_full_mobius_witnessvaluesquarefree * sfd_prime_full_mobius_witnessvaluesquarefree) * pvs_factor_full_mobius_witnessvaluesquarefreesquare)))) /\ (exists mv_factor_code_full_mobius_witnessvaluefactors mv_factor_scale_full_mobius_witnessvaluefactors mv_factor_count_full_mobius_witnessvaluefactors. (((~(mt_index_full_mobius_witness = 0) /\ ((exists ff_u_fsat_full_mobius_witnessvaluefactorsfactorization_product ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product. ((((exists ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_start. ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product)) /\ exists ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_start. ff_u_fsat_full_mobius_witnessvaluefactorsfactorization_product = ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_terminal. ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_terminal + S (mt_index_full_mobius_witness) = S ((S (mv_factor_count_full_mobius_witnessvaluefactors)) * ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product)) /\ exists ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_terminal. ff_u_fsat_full_mobius_witnessvaluefactorsfactorization_product = ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_full_mobius_witnessvaluefactors)) * ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product) + (mt_index_full_mobius_witness))) /\ forall ff_i_fsat_full_mobius_witnessvaluefactorsfactorization_product. (exists ff_lt_fsat_full_mobius_witnessvaluefactorsfactorization_product_bound. ff_lt_fsat_full_mobius_witnessvaluefactorsfactorization_product_bound + S ff_i_fsat_full_mobius_witnessvaluefactorsfactorization_product = mv_factor_count_full_mobius_witnessvaluefactors) -> exists ff_p_fsat_full_mobius_witnessvaluefactorsfactorization_product ff_r_fsat_full_mobius_witnessvaluefactorsfactorization_product ff_s_fsat_full_mobius_witnessvaluefactorsfactorization_product. ((((exists ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_factor. ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_factor + S (ff_p_fsat_full_mobius_witnessvaluefactorsfactorization_product) = S ((S (ff_i_fsat_full_mobius_witnessvaluefactorsfactorization_product)) * mv_factor_scale_full_mobius_witnessvaluefactors)) /\ exists ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_factor. mv_factor_code_full_mobius_witnessvaluefactors = ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_full_mobius_witnessvaluefactorsfactorization_product)) * mv_factor_scale_full_mobius_witnessvaluefactors) + (ff_p_fsat_full_mobius_witnessvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_partial. ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_partial + S (ff_r_fsat_full_mobius_witnessvaluefactorsfactorization_product) = S ((S (ff_i_fsat_full_mobius_witnessvaluefactorsfactorization_product)) * ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product)) /\ exists ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_partial. ff_u_fsat_full_mobius_witnessvaluefactorsfactorization_product = ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_full_mobius_witnessvaluefactorsfactorization_product)) * ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product) + (ff_r_fsat_full_mobius_witnessvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_successor. ff_h_fsat_full_mobius_witnessvaluefactorsfactorization_product_successor + S (ff_s_fsat_full_mobius_witnessvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_full_mobius_witnessvaluefactorsfactorization_product)) * ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product)) /\ exists ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_successor. ff_u_fsat_full_mobius_witnessvaluefactorsfactorization_product = ff_q_fsat_full_mobius_witnessvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_full_mobius_witnessvaluefactorsfactorization_product)) * ff_v_fsat_full_mobius_witnessvaluefactorsfactorization_product) + (ff_s_fsat_full_mobius_witnessvaluefactorsfactorization_product))) /\ ff_s_fsat_full_mobius_witnessvaluefactorsfactorization_product = ff_r_fsat_full_mobius_witnessvaluefactorsfactorization_product * ff_p_fsat_full_mobius_witnessvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_full_mobius_witnessvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_full_mobius_witnessvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_full_mobius_witnessvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_full_mobius_witnessvaluefactorsfactorization_primes = (mv_factor_count_full_mobius_witnessvaluefactors)) -> exists ftsf_factor_fsat_full_mobius_witnessvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_full_mobius_witnessvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_full_mobius_witnessvaluefactorsfactorization_primes)) * mv_factor_scale_full_mobius_witnessvaluefactors)) /\ exists ff_q_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_entry. mv_factor_code_full_mobius_witnessvaluefactors = ff_q_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_full_mobius_witnessvaluefactorsfactorization_primes)) * mv_factor_scale_full_mobius_witnessvaluefactors) + (ftsf_factor_fsat_full_mobius_witnessvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_full_mobius_witnessvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_full_mobius_witnessvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_full_mobius_witnessvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_full_mobius_witnessvaluefactorsparityeven. (mv_factor_count_full_mobius_witnessvaluefactors) = 2 * mv_even_half_full_mobius_witnessvaluefactorsparityeven) /\ ((mt_value_full_mobius_witness) = 2))) \/ (((exists mv_odd_half_full_mobius_witnessvaluefactorsparityodd. (mv_factor_count_full_mobius_witnessvaluefactors) = 2 * mv_odd_half_full_mobius_witnessvaluefactorsparityodd + 1) /\ ((mt_value_full_mobius_witness) = 1)))))))))))))))) /\ (((((exists dst_positive_code_full_weighted_outputleft dst_positive_scale_full_weighted_outputleft dst_negative_code_full_weighted_outputleft dst_negative_scale_full_weighted_outputleft. (((M) = (((((dst_positive_code_full_weighted_outputleft) + (dst_positive_scale_full_weighted_outputleft)) * S ((dst_positive_code_full_weighted_outputleft) + (dst_positive_scale_full_weighted_outputleft)) + ((dst_positive_scale_full_weighted_outputleft) + (dst_positive_scale_full_weighted_outputleft))) + (((dst_negative_code_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)) * S ((dst_negative_code_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)) + ((dst_negative_scale_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)))) * S ((((dst_positive_code_full_weighted_outputleft) + (dst_positive_scale_full_weighted_outputleft)) * S ((dst_positive_code_full_weighted_outputleft) + (dst_positive_scale_full_weighted_outputleft)) + ((dst_positive_scale_full_weighted_outputleft) + (dst_positive_scale_full_weighted_outputleft))) + (((dst_negative_code_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)) * S ((dst_negative_code_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)) + ((dst_negative_scale_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)))) + ((((dst_negative_code_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)) * S ((dst_negative_code_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)) + ((dst_negative_scale_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft))) + (((dst_negative_code_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)) * S ((dst_negative_code_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)) + ((dst_negative_scale_full_weighted_outputleft) + (dst_negative_scale_full_weighted_outputleft)))))) /\ (forall dst_index_full_weighted_outputleft. (exists pvs_le_gap_full_weighted_outputleftdomain. pvs_le_gap_full_weighted_outputleftdomain + (dst_index_full_weighted_outputleft) = (N)) -> exists dst_positive_full_weighted_outputleft dst_negative_full_weighted_outputleft dst_value_full_weighted_outputleft. ((((exists ff_h_pvs_full_weighted_outputleftentrypositive. ff_h_pvs_full_weighted_outputleftentrypositive + S (dst_positive_full_weighted_outputleft) = S ((S (dst_index_full_weighted_outputleft)) * dst_positive_scale_full_weighted_outputleft)) /\ exists ff_q_pvs_full_weighted_outputleftentrypositive. dst_positive_code_full_weighted_outputleft = ff_q_pvs_full_weighted_outputleftentrypositive * S ((S (dst_index_full_weighted_outputleft)) * dst_positive_scale_full_weighted_outputleft) + (dst_positive_full_weighted_outputleft))) /\ (((((exists ff_h_pvs_full_weighted_outputleftentrynegative. ff_h_pvs_full_weighted_outputleftentrynegative + S (dst_negative_full_weighted_outputleft) = S ((S (dst_index_full_weighted_outputleft)) * dst_negative_scale_full_weighted_outputleft)) /\ exists ff_q_pvs_full_weighted_outputleftentrynegative. dst_negative_code_full_weighted_outputleft = ff_q_pvs_full_weighted_outputleftentrynegative * S ((S (dst_index_full_weighted_outputleft)) * dst_negative_scale_full_weighted_outputleft) + (dst_negative_full_weighted_outputleft))) /\ (exists ge_balance_positive_full_weighted_outputleftentryvalue ge_balance_negative_full_weighted_outputleftentryvalue. (((((dst_value_full_weighted_outputleft) = 2 * (ge_balance_positive_full_weighted_outputleftentryvalue) /\ (ge_balance_negative_full_weighted_outputleftentryvalue) = 0) \/ exists ge_signed_half_full_weighted_outputleftentryvaluedecode. (((dst_value_full_weighted_outputleft) = 2 * ge_signed_half_full_weighted_outputleftentryvaluedecode + 1 /\ (ge_balance_positive_full_weighted_outputleftentryvalue) = 0) /\ (ge_balance_negative_full_weighted_outputleftentryvalue) = S ge_signed_half_full_weighted_outputleftentryvaluedecode))) /\ ((dst_positive_full_weighted_outputleft) + ge_balance_negative_full_weighted_outputleftentryvalue = (dst_negative_full_weighted_outputleft) + ge_balance_positive_full_weighted_outputleftentryvalue))))))))) /\ (((exists dst_positive_code_full_weighted_outputright dst_positive_scale_full_weighted_outputright dst_negative_code_full_weighted_outputright dst_negative_scale_full_weighted_outputright. (((G) = (((((dst_positive_code_full_weighted_outputright) + (dst_positive_scale_full_weighted_outputright)) * S ((dst_positive_code_full_weighted_outputright) + (dst_positive_scale_full_weighted_outputright)) + ((dst_positive_scale_full_weighted_outputright) + (dst_positive_scale_full_weighted_outputright))) + (((dst_negative_code_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)) * S ((dst_negative_code_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)) + ((dst_negative_scale_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)))) * S ((((dst_positive_code_full_weighted_outputright) + (dst_positive_scale_full_weighted_outputright)) * S ((dst_positive_code_full_weighted_outputright) + (dst_positive_scale_full_weighted_outputright)) + ((dst_positive_scale_full_weighted_outputright) + (dst_positive_scale_full_weighted_outputright))) + (((dst_negative_code_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)) * S ((dst_negative_code_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)) + ((dst_negative_scale_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)))) + ((((dst_negative_code_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)) * S ((dst_negative_code_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)) + ((dst_negative_scale_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright))) + (((dst_negative_code_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)) * S ((dst_negative_code_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)) + ((dst_negative_scale_full_weighted_outputright) + (dst_negative_scale_full_weighted_outputright)))))) /\ (forall dst_index_full_weighted_outputright. (exists pvs_le_gap_full_weighted_outputrightdomain. pvs_le_gap_full_weighted_outputrightdomain + (dst_index_full_weighted_outputright) = (N)) -> exists dst_positive_full_weighted_outputright dst_negative_full_weighted_outputright dst_value_full_weighted_outputright. ((((exists ff_h_pvs_full_weighted_outputrightentrypositive. ff_h_pvs_full_weighted_outputrightentrypositive + S (dst_positive_full_weighted_outputright) = S ((S (dst_index_full_weighted_outputright)) * dst_positive_scale_full_weighted_outputright)) /\ exists ff_q_pvs_full_weighted_outputrightentrypositive. dst_positive_code_full_weighted_outputright = ff_q_pvs_full_weighted_outputrightentrypositive * S ((S (dst_index_full_weighted_outputright)) * dst_positive_scale_full_weighted_outputright) + (dst_positive_full_weighted_outputright))) /\ (((((exists ff_h_pvs_full_weighted_outputrightentrynegative. ff_h_pvs_full_weighted_outputrightentrynegative + S (dst_negative_full_weighted_outputright) = S ((S (dst_index_full_weighted_outputright)) * dst_negative_scale_full_weighted_outputright)) /\ exists ff_q_pvs_full_weighted_outputrightentrynegative. dst_negative_code_full_weighted_outputright = ff_q_pvs_full_weighted_outputrightentrynegative * S ((S (dst_index_full_weighted_outputright)) * dst_negative_scale_full_weighted_outputright) + (dst_negative_full_weighted_outputright))) /\ (exists ge_balance_positive_full_weighted_outputrightentryvalue ge_balance_negative_full_weighted_outputrightentryvalue. (((((dst_value_full_weighted_outputright) = 2 * (ge_balance_positive_full_weighted_outputrightentryvalue) /\ (ge_balance_negative_full_weighted_outputrightentryvalue) = 0) \/ exists ge_signed_half_full_weighted_outputrightentryvaluedecode. (((dst_value_full_weighted_outputright) = 2 * ge_signed_half_full_weighted_outputrightentryvaluedecode + 1 /\ (ge_balance_positive_full_weighted_outputrightentryvalue) = 0) /\ (ge_balance_negative_full_weighted_outputrightentryvalue) = S ge_signed_half_full_weighted_outputrightentryvaluedecode))) /\ ((dst_positive_full_weighted_outputright) + ge_balance_negative_full_weighted_outputrightentryvalue = (dst_negative_full_weighted_outputright) + ge_balance_positive_full_weighted_outputrightentryvalue))))))))) /\ (((exists dst_positive_code_full_weighted_outputtable dst_positive_scale_full_weighted_outputtable dst_negative_code_full_weighted_outputtable dst_negative_scale_full_weighted_outputtable. (((H) = (((((dst_positive_code_full_weighted_outputtable) + (dst_positive_scale_full_weighted_outputtable)) * S ((dst_positive_code_full_weighted_outputtable) + (dst_positive_scale_full_weighted_outputtable)) + ((dst_positive_scale_full_weighted_outputtable) + (dst_positive_scale_full_weighted_outputtable))) + (((dst_negative_code_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)) * S ((dst_negative_code_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)) + ((dst_negative_scale_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)))) * S ((((dst_positive_code_full_weighted_outputtable) + (dst_positive_scale_full_weighted_outputtable)) * S ((dst_positive_code_full_weighted_outputtable) + (dst_positive_scale_full_weighted_outputtable)) + ((dst_positive_scale_full_weighted_outputtable) + (dst_positive_scale_full_weighted_outputtable))) + (((dst_negative_code_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)) * S ((dst_negative_code_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)) + ((dst_negative_scale_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)))) + ((((dst_negative_code_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)) * S ((dst_negative_code_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)) + ((dst_negative_scale_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable))) + (((dst_negative_code_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)) * S ((dst_negative_code_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)) + ((dst_negative_scale_full_weighted_outputtable) + (dst_negative_scale_full_weighted_outputtable)))))) /\ (forall dst_index_full_weighted_outputtable. (exists pvs_le_gap_full_weighted_outputtabledomain. pvs_le_gap_full_weighted_outputtabledomain + (dst_index_full_weighted_outputtable) = (N)) -> exists dst_positive_full_weighted_outputtable dst_negative_full_weighted_outputtable dst_value_full_weighted_outputtable. ((((exists ff_h_pvs_full_weighted_outputtableentrypositive. ff_h_pvs_full_weighted_outputtableentrypositive + S (dst_positive_full_weighted_outputtable) = S ((S (dst_index_full_weighted_outputtable)) * dst_positive_scale_full_weighted_outputtable)) /\ exists ff_q_pvs_full_weighted_outputtableentrypositive. dst_positive_code_full_weighted_outputtable = ff_q_pvs_full_weighted_outputtableentrypositive * S ((S (dst_index_full_weighted_outputtable)) * dst_positive_scale_full_weighted_outputtable) + (dst_positive_full_weighted_outputtable))) /\ (((((exists ff_h_pvs_full_weighted_outputtableentrynegative. ff_h_pvs_full_weighted_outputtableentrynegative + S (dst_negative_full_weighted_outputtable) = S ((S (dst_index_full_weighted_outputtable)) * dst_negative_scale_full_weighted_outputtable)) /\ exists ff_q_pvs_full_weighted_outputtableentrynegative. dst_negative_code_full_weighted_outputtable = ff_q_pvs_full_weighted_outputtableentrynegative * S ((S (dst_index_full_weighted_outputtable)) * dst_negative_scale_full_weighted_outputtable) + (dst_negative_full_weighted_outputtable))) /\ (exists ge_balance_positive_full_weighted_outputtableentryvalue ge_balance_negative_full_weighted_outputtableentryvalue. (((((dst_value_full_weighted_outputtable) = 2 * (ge_balance_positive_full_weighted_outputtableentryvalue) /\ (ge_balance_negative_full_weighted_outputtableentryvalue) = 0) \/ exists ge_signed_half_full_weighted_outputtableentryvaluedecode. (((dst_value_full_weighted_outputtable) = 2 * ge_signed_half_full_weighted_outputtableentryvaluedecode + 1 /\ (ge_balance_positive_full_weighted_outputtableentryvalue) = 0) /\ (ge_balance_negative_full_weighted_outputtableentryvalue) = S ge_signed_half_full_weighted_outputtableentryvaluedecode))) /\ ((dst_positive_full_weighted_outputtable) + ge_balance_negative_full_weighted_outputtableentryvalue = (dst_negative_full_weighted_outputtable) + ge_balance_positive_full_weighted_outputtableentryvalue))))))))) /\ (forall dc_input_full_weighted_output dc_output_full_weighted_output. ~(dc_input_full_weighted_output=0) -> (exists pvs_le_gap_full_weighted_outputdomain. pvs_le_gap_full_weighted_outputdomain + (dc_input_full_weighted_output) = (N)) -> (exists dst_positive_code_full_weighted_outputlookup dst_positive_scale_full_weighted_outputlookup dst_negative_code_full_weighted_outputlookup dst_negative_scale_full_weighted_outputlookup dst_positive_full_weighted_outputlookup dst_negative_full_weighted_outputlookup. (((H) = (((((dst_positive_code_full_weighted_outputlookup) + (dst_positive_scale_full_weighted_outputlookup)) * S ((dst_positive_code_full_weighted_outputlookup) + (dst_positive_scale_full_weighted_outputlookup)) + ((dst_positive_scale_full_weighted_outputlookup) + (dst_positive_scale_full_weighted_outputlookup))) + (((dst_negative_code_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)) * S ((dst_negative_code_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)) + ((dst_negative_scale_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)))) * S ((((dst_positive_code_full_weighted_outputlookup) + (dst_positive_scale_full_weighted_outputlookup)) * S ((dst_positive_code_full_weighted_outputlookup) + (dst_positive_scale_full_weighted_outputlookup)) + ((dst_positive_scale_full_weighted_outputlookup) + (dst_positive_scale_full_weighted_outputlookup))) + (((dst_negative_code_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)) * S ((dst_negative_code_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)) + ((dst_negative_scale_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)))) + ((((dst_negative_code_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)) * S ((dst_negative_code_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)) + ((dst_negative_scale_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup))) + (((dst_negative_code_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)) * S ((dst_negative_code_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)) + ((dst_negative_scale_full_weighted_outputlookup) + (dst_negative_scale_full_weighted_outputlookup)))))) /\ (((((exists ff_h_pvs_full_weighted_outputlookuppositive. ff_h_pvs_full_weighted_outputlookuppositive + S (dst_positive_full_weighted_outputlookup) = S ((S (dc_input_full_weighted_output)) * dst_positive_scale_full_weighted_outputlookup)) /\ exists ff_q_pvs_full_weighted_outputlookuppositive. dst_positive_code_full_weighted_outputlookup = ff_q_pvs_full_weighted_outputlookuppositive * S ((S (dc_input_full_weighted_output)) * dst_positive_scale_full_weighted_outputlookup) + (dst_positive_full_weighted_outputlookup))) /\ (((((exists ff_h_pvs_full_weighted_outputlookupnegative. ff_h_pvs_full_weighted_outputlookupnegative + S (dst_negative_full_weighted_outputlookup) = S ((S (dc_input_full_weighted_output)) * dst_negative_scale_full_weighted_outputlookup)) /\ exists ff_q_pvs_full_weighted_outputlookupnegative. dst_negative_code_full_weighted_outputlookup = ff_q_pvs_full_weighted_outputlookupnegative * S ((S (dc_input_full_weighted_output)) * dst_negative_scale_full_weighted_outputlookup) + (dst_negative_full_weighted_outputlookup))) /\ (exists ge_balance_positive_full_weighted_outputlookupvalue ge_balance_negative_full_weighted_outputlookupvalue. (((((dc_output_full_weighted_output) = 2 * (ge_balance_positive_full_weighted_outputlookupvalue) /\ (ge_balance_negative_full_weighted_outputlookupvalue) = 0) \/ exists ge_signed_half_full_weighted_outputlookupvaluedecode. (((dc_output_full_weighted_output) = 2 * ge_signed_half_full_weighted_outputlookupvaluedecode + 1 /\ (ge_balance_positive_full_weighted_outputlookupvalue) = 0) /\ (ge_balance_negative_full_weighted_outputlookupvalue) = S ge_signed_half_full_weighted_outputlookupvaluedecode))) /\ ((dst_positive_full_weighted_outputlookup) + ge_balance_negative_full_weighted_outputlookupvalue = (dst_negative_full_weighted_outputlookup) + ge_balance_positive_full_weighted_outputlookupvalue))))))))) -> (((~((dc_input_full_weighted_output)=0)) /\ (exists dc_mask_full_weighted_outputvalue. ((((exists dst_positive_code_full_weighted_outputvaluemasktable dst_positive_scale_full_weighted_outputvaluemasktable dst_negative_code_full_weighted_outputvaluemasktable dst_negative_scale_full_weighted_outputvaluemasktable. (((dc_mask_full_weighted_outputvalue) = (((((dst_positive_code_full_weighted_outputvaluemasktable) + (dst_positive_scale_full_weighted_outputvaluemasktable)) * S ((dst_positive_code_full_weighted_outputvaluemasktable) + (dst_positive_scale_full_weighted_outputvaluemasktable)) + ((dst_positive_scale_full_weighted_outputvaluemasktable) + (dst_positive_scale_full_weighted_outputvaluemasktable))) + (((dst_negative_code_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)) * S ((dst_negative_code_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)) + ((dst_negative_scale_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)))) * S ((((dst_positive_code_full_weighted_outputvaluemasktable) + (dst_positive_scale_full_weighted_outputvaluemasktable)) * S ((dst_positive_code_full_weighted_outputvaluemasktable) + (dst_positive_scale_full_weighted_outputvaluemasktable)) + ((dst_positive_scale_full_weighted_outputvaluemasktable) + (dst_positive_scale_full_weighted_outputvaluemasktable))) + (((dst_negative_code_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)) * S ((dst_negative_code_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)) + ((dst_negative_scale_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)))) + ((((dst_negative_code_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)) * S ((dst_negative_code_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)) + ((dst_negative_scale_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable))) + (((dst_negative_code_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)) * S ((dst_negative_code_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)) + ((dst_negative_scale_full_weighted_outputvaluemasktable) + (dst_negative_scale_full_weighted_outputvaluemasktable)))))) /\ (forall dst_index_full_weighted_outputvaluemasktable. (exists pvs_le_gap_full_weighted_outputvaluemasktabledomain. pvs_le_gap_full_weighted_outputvaluemasktabledomain + (dst_index_full_weighted_outputvaluemasktable) = (dc_input_full_weighted_output)) -> exists dst_positive_full_weighted_outputvaluemasktable dst_negative_full_weighted_outputvaluemasktable dst_value_full_weighted_outputvaluemasktable. ((((exists ff_h_pvs_full_weighted_outputvaluemasktableentrypositive. ff_h_pvs_full_weighted_outputvaluemasktableentrypositive + S (dst_positive_full_weighted_outputvaluemasktable) = S ((S (dst_index_full_weighted_outputvaluemasktable)) * dst_positive_scale_full_weighted_outputvaluemasktable)) /\ exists ff_q_pvs_full_weighted_outputvaluemasktableentrypositive. dst_positive_code_full_weighted_outputvaluemasktable = ff_q_pvs_full_weighted_outputvaluemasktableentrypositive * S ((S (dst_index_full_weighted_outputvaluemasktable)) * dst_positive_scale_full_weighted_outputvaluemasktable) + (dst_positive_full_weighted_outputvaluemasktable))) /\ (((((exists ff_h_pvs_full_weighted_outputvaluemasktableentrynegative. ff_h_pvs_full_weighted_outputvaluemasktableentrynegative + S (dst_negative_full_weighted_outputvaluemasktable) = S ((S (dst_index_full_weighted_outputvaluemasktable)) * dst_negative_scale_full_weighted_outputvaluemasktable)) /\ exists ff_q_pvs_full_weighted_outputvaluemasktableentrynegative. dst_negative_code_full_weighted_outputvaluemasktable = ff_q_pvs_full_weighted_outputvaluemasktableentrynegative * S ((S (dst_index_full_weighted_outputvaluemasktable)) * dst_negative_scale_full_weighted_outputvaluemasktable) + (dst_negative_full_weighted_outputvaluemasktable))) /\ (exists ge_balance_positive_full_weighted_outputvaluemasktableentryvalue ge_balance_negative_full_weighted_outputvaluemasktableentryvalue. (((((dst_value_full_weighted_outputvaluemasktable) = 2 * (ge_balance_positive_full_weighted_outputvaluemasktableentryvalue) /\ (ge_balance_negative_full_weighted_outputvaluemasktableentryvalue) = 0) \/ exists ge_signed_half_full_weighted_outputvaluemasktableentryvaluedecode. (((dst_value_full_weighted_outputvaluemasktable) = 2 * ge_signed_half_full_weighted_outputvaluemasktableentryvaluedecode + 1 /\ (ge_balance_positive_full_weighted_outputvaluemasktableentryvalue) = 0) /\ (ge_balance_negative_full_weighted_outputvaluemasktableentryvalue) = S ge_signed_half_full_weighted_outputvaluemasktableentryvaluedecode))) /\ ((dst_positive_full_weighted_outputvaluemasktable) + ge_balance_negative_full_weighted_outputvaluemasktableentryvalue = (dst_negative_full_weighted_outputvaluemasktable) + ge_balance_positive_full_weighted_outputvaluemasktableentryvalue))))))))) /\ (forall dc_index_full_weighted_outputvaluemask dc_value_full_weighted_outputvaluemask. (exists pvs_le_gap_full_weighted_outputvaluemaskdomain. pvs_le_gap_full_weighted_outputvaluemaskdomain + (dc_index_full_weighted_outputvaluemask) = (dc_input_full_weighted_output)) -> (exists dst_positive_code_full_weighted_outputvaluemasklookup dst_positive_scale_full_weighted_outputvaluemasklookup dst_negative_code_full_weighted_outputvaluemasklookup dst_negative_scale_full_weighted_outputvaluemasklookup dst_positive_full_weighted_outputvaluemasklookup dst_negative_full_weighted_outputvaluemasklookup. (((dc_mask_full_weighted_outputvalue) = (((((dst_positive_code_full_weighted_outputvaluemasklookup) + (dst_positive_scale_full_weighted_outputvaluemasklookup)) * S ((dst_positive_code_full_weighted_outputvaluemasklookup) + (dst_positive_scale_full_weighted_outputvaluemasklookup)) + ((dst_positive_scale_full_weighted_outputvaluemasklookup) + (dst_positive_scale_full_weighted_outputvaluemasklookup))) + (((dst_negative_code_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)) * S ((dst_negative_code_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)) + ((dst_negative_scale_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)))) * S ((((dst_positive_code_full_weighted_outputvaluemasklookup) + (dst_positive_scale_full_weighted_outputvaluemasklookup)) * S ((dst_positive_code_full_weighted_outputvaluemasklookup) + (dst_positive_scale_full_weighted_outputvaluemasklookup)) + ((dst_positive_scale_full_weighted_outputvaluemasklookup) + (dst_positive_scale_full_weighted_outputvaluemasklookup))) + (((dst_negative_code_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)) * S ((dst_negative_code_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)) + ((dst_negative_scale_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)))) + ((((dst_negative_code_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)) * S ((dst_negative_code_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)) + ((dst_negative_scale_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup))) + (((dst_negative_code_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)) * S ((dst_negative_code_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)) + ((dst_negative_scale_full_weighted_outputvaluemasklookup) + (dst_negative_scale_full_weighted_outputvaluemasklookup)))))) /\ (((((exists ff_h_pvs_full_weighted_outputvaluemasklookuppositive. ff_h_pvs_full_weighted_outputvaluemasklookuppositive + S (dst_positive_full_weighted_outputvaluemasklookup) = S ((S (dc_index_full_weighted_outputvaluemask)) * dst_positive_scale_full_weighted_outputvaluemasklookup)) /\ exists ff_q_pvs_full_weighted_outputvaluemasklookuppositive. dst_positive_code_full_weighted_outputvaluemasklookup = ff_q_pvs_full_weighted_outputvaluemasklookuppositive * S ((S (dc_index_full_weighted_outputvaluemask)) * dst_positive_scale_full_weighted_outputvaluemasklookup) + (dst_positive_full_weighted_outputvaluemasklookup))) /\ (((((exists ff_h_pvs_full_weighted_outputvaluemasklookupnegative. ff_h_pvs_full_weighted_outputvaluemasklookupnegative + S (dst_negative_full_weighted_outputvaluemasklookup) = S ((S (dc_index_full_weighted_outputvaluemask)) * dst_negative_scale_full_weighted_outputvaluemasklookup)) /\ exists ff_q_pvs_full_weighted_outputvaluemasklookupnegative. dst_negative_code_full_weighted_outputvaluemasklookup = ff_q_pvs_full_weighted_outputvaluemasklookupnegative * S ((S (dc_index_full_weighted_outputvaluemask)) * dst_negative_scale_full_weighted_outputvaluemasklookup) + (dst_negative_full_weighted_outputvaluemasklookup))) /\ (exists ge_balance_positive_full_weighted_outputvaluemasklookupvalue ge_balance_negative_full_weighted_outputvaluemasklookupvalue. (((((dc_value_full_weighted_outputvaluemask) = 2 * (ge_balance_positive_full_weighted_outputvaluemasklookupvalue) /\ (ge_balance_negative_full_weighted_outputvaluemasklookupvalue) = 0) \/ exists ge_signed_half_full_weighted_outputvaluemasklookupvaluedecode. (((dc_value_full_weighted_outputvaluemask) = 2 * ge_signed_half_full_weighted_outputvaluemasklookupvaluedecode + 1 /\ (ge_balance_positive_full_weighted_outputvaluemasklookupvalue) = 0) /\ (ge_balance_negative_full_weighted_outputvaluemasklookupvalue) = S ge_signed_half_full_weighted_outputvaluemasklookupvaluedecode))) /\ ((dst_positive_full_weighted_outputvaluemasklookup) + ge_balance_negative_full_weighted_outputvaluemasklookupvalue = (dst_negative_full_weighted_outputvaluemasklookup) + ge_balance_positive_full_weighted_outputvaluemasklookupvalue))))))))) -> ((((~((dc_index_full_weighted_outputvaluemask)=0)) /\ (exists dc_quotient_full_weighted_outputvaluemaskentry dc_left_full_weighted_outputvaluemaskentry dc_right_full_weighted_outputvaluemaskentry. (((dc_input_full_weighted_output)=(dc_index_full_weighted_outputvaluemask)*dc_quotient_full_weighted_outputvaluemaskentry) /\ (((exists dst_positive_code_full_weighted_outputvaluemaskentryleft dst_positive_scale_full_weighted_outputvaluemaskentryleft dst_negative_code_full_weighted_outputvaluemaskentryleft dst_negative_scale_full_weighted_outputvaluemaskentryleft dst_positive_full_weighted_outputvaluemaskentryleft dst_negative_full_weighted_outputvaluemaskentryleft. (((M) = (((((dst_positive_code_full_weighted_outputvaluemaskentryleft) + (dst_positive_scale_full_weighted_outputvaluemaskentryleft)) * S ((dst_positive_code_full_weighted_outputvaluemaskentryleft) + (dst_positive_scale_full_weighted_outputvaluemaskentryleft)) + ((dst_positive_scale_full_weighted_outputvaluemaskentryleft) + (dst_positive_scale_full_weighted_outputvaluemaskentryleft))) + (((dst_negative_code_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)) * S ((dst_negative_code_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)) + ((dst_negative_scale_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)))) * S ((((dst_positive_code_full_weighted_outputvaluemaskentryleft) + (dst_positive_scale_full_weighted_outputvaluemaskentryleft)) * S ((dst_positive_code_full_weighted_outputvaluemaskentryleft) + (dst_positive_scale_full_weighted_outputvaluemaskentryleft)) + ((dst_positive_scale_full_weighted_outputvaluemaskentryleft) + (dst_positive_scale_full_weighted_outputvaluemaskentryleft))) + (((dst_negative_code_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)) * S ((dst_negative_code_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)) + ((dst_negative_scale_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)))) + ((((dst_negative_code_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)) * S ((dst_negative_code_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)) + ((dst_negative_scale_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft))) + (((dst_negative_code_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)) * S ((dst_negative_code_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)) + ((dst_negative_scale_full_weighted_outputvaluemaskentryleft) + (dst_negative_scale_full_weighted_outputvaluemaskentryleft)))))) /\ (((((exists ff_h_pvs_full_weighted_outputvaluemaskentryleftpositive. ff_h_pvs_full_weighted_outputvaluemaskentryleftpositive + S (dst_positive_full_weighted_outputvaluemaskentryleft) = S ((S (dc_index_full_weighted_outputvaluemask)) * dst_positive_scale_full_weighted_outputvaluemaskentryleft)) /\ exists ff_q_pvs_full_weighted_outputvaluemaskentryleftpositive. dst_positive_code_full_weighted_outputvaluemaskentryleft = ff_q_pvs_full_weighted_outputvaluemaskentryleftpositive * S ((S (dc_index_full_weighted_outputvaluemask)) * dst_positive_scale_full_weighted_outputvaluemaskentryleft) + (dst_positive_full_weighted_outputvaluemaskentryleft))) /\ (((((exists ff_h_pvs_full_weighted_outputvaluemaskentryleftnegative. ff_h_pvs_full_weighted_outputvaluemaskentryleftnegative + S (dst_negative_full_weighted_outputvaluemaskentryleft) = S ((S (dc_index_full_weighted_outputvaluemask)) * dst_negative_scale_full_weighted_outputvaluemaskentryleft)) /\ exists ff_q_pvs_full_weighted_outputvaluemaskentryleftnegative. dst_negative_code_full_weighted_outputvaluemaskentryleft = ff_q_pvs_full_weighted_outputvaluemaskentryleftnegative * S ((S (dc_index_full_weighted_outputvaluemask)) * dst_negative_scale_full_weighted_outputvaluemaskentryleft) + (dst_negative_full_weighted_outputvaluemaskentryleft))) /\ (exists ge_balance_positive_full_weighted_outputvaluemaskentryleftvalue ge_balance_negative_full_weighted_outputvaluemaskentryleftvalue. (((((dc_left_full_weighted_outputvaluemaskentry) = 2 * (ge_balance_positive_full_weighted_outputvaluemaskentryleftvalue) /\ (ge_balance_negative_full_weighted_outputvaluemaskentryleftvalue) = 0) \/ exists ge_signed_half_full_weighted_outputvaluemaskentryleftvaluedecode. (((dc_left_full_weighted_outputvaluemaskentry) = 2 * ge_signed_half_full_weighted_outputvaluemaskentryleftvaluedecode + 1 /\ (ge_balance_positive_full_weighted_outputvaluemaskentryleftvalue) = 0) /\ (ge_balance_negative_full_weighted_outputvaluemaskentryleftvalue) = S ge_signed_half_full_weighted_outputvaluemaskentryleftvaluedecode))) /\ ((dst_positive_full_weighted_outputvaluemaskentryleft) + ge_balance_negative_full_weighted_outputvaluemaskentryleftvalue = (dst_negative_full_weighted_outputvaluemaskentryleft) + ge_balance_positive_full_weighted_outputvaluemaskentryleftvalue))))))))) /\ (((exists dst_positive_code_full_weighted_outputvaluemaskentryright dst_positive_scale_full_weighted_outputvaluemaskentryright dst_negative_code_full_weighted_outputvaluemaskentryright dst_negative_scale_full_weighted_outputvaluemaskentryright dst_positive_full_weighted_outputvaluemaskentryright dst_negative_full_weighted_outputvaluemaskentryright. (((G) = (((((dst_positive_code_full_weighted_outputvaluemaskentryright) + (dst_positive_scale_full_weighted_outputvaluemaskentryright)) * S ((dst_positive_code_full_weighted_outputvaluemaskentryright) + (dst_positive_scale_full_weighted_outputvaluemaskentryright)) + ((dst_positive_scale_full_weighted_outputvaluemaskentryright) + (dst_positive_scale_full_weighted_outputvaluemaskentryright))) + (((dst_negative_code_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)) * S ((dst_negative_code_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)) + ((dst_negative_scale_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)))) * S ((((dst_positive_code_full_weighted_outputvaluemaskentryright) + (dst_positive_scale_full_weighted_outputvaluemaskentryright)) * S ((dst_positive_code_full_weighted_outputvaluemaskentryright) + (dst_positive_scale_full_weighted_outputvaluemaskentryright)) + ((dst_positive_scale_full_weighted_outputvaluemaskentryright) + (dst_positive_scale_full_weighted_outputvaluemaskentryright))) + (((dst_negative_code_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)) * S ((dst_negative_code_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)) + ((dst_negative_scale_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)))) + ((((dst_negative_code_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)) * S ((dst_negative_code_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)) + ((dst_negative_scale_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright))) + (((dst_negative_code_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)) * S ((dst_negative_code_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)) + ((dst_negative_scale_full_weighted_outputvaluemaskentryright) + (dst_negative_scale_full_weighted_outputvaluemaskentryright)))))) /\ (((((exists ff_h_pvs_full_weighted_outputvaluemaskentryrightpositive. ff_h_pvs_full_weighted_outputvaluemaskentryrightpositive + S (dst_positive_full_weighted_outputvaluemaskentryright) = S ((S (dc_quotient_full_weighted_outputvaluemaskentry)) * dst_positive_scale_full_weighted_outputvaluemaskentryright)) /\ exists ff_q_pvs_full_weighted_outputvaluemaskentryrightpositive. dst_positive_code_full_weighted_outputvaluemaskentryright = ff_q_pvs_full_weighted_outputvaluemaskentryrightpositive * S ((S (dc_quotient_full_weighted_outputvaluemaskentry)) * dst_positive_scale_full_weighted_outputvaluemaskentryright) + (dst_positive_full_weighted_outputvaluemaskentryright))) /\ (((((exists ff_h_pvs_full_weighted_outputvaluemaskentryrightnegative. ff_h_pvs_full_weighted_outputvaluemaskentryrightnegative + S (dst_negative_full_weighted_outputvaluemaskentryright) = S ((S (dc_quotient_full_weighted_outputvaluemaskentry)) * dst_negative_scale_full_weighted_outputvaluemaskentryright)) /\ exists ff_q_pvs_full_weighted_outputvaluemaskentryrightnegative. dst_negative_code_full_weighted_outputvaluemaskentryright = ff_q_pvs_full_weighted_outputvaluemaskentryrightnegative * S ((S (dc_quotient_full_weighted_outputvaluemaskentry)) * dst_negative_scale_full_weighted_outputvaluemaskentryright) + (dst_negative_full_weighted_outputvaluemaskentryright))) /\ (exists ge_balance_positive_full_weighted_outputvaluemaskentryrightvalue ge_balance_negative_full_weighted_outputvaluemaskentryrightvalue. (((((dc_right_full_weighted_outputvaluemaskentry) = 2 * (ge_balance_positive_full_weighted_outputvaluemaskentryrightvalue) /\ (ge_balance_negative_full_weighted_outputvaluemaskentryrightvalue) = 0) \/ exists ge_signed_half_full_weighted_outputvaluemaskentryrightvaluedecode. (((dc_right_full_weighted_outputvaluemaskentry) = 2 * ge_signed_half_full_weighted_outputvaluemaskentryrightvaluedecode + 1 /\ (ge_balance_positive_full_weighted_outputvaluemaskentryrightvalue) = 0) /\ (ge_balance_negative_full_weighted_outputvaluemaskentryrightvalue) = S ge_signed_half_full_weighted_outputvaluemaskentryrightvaluedecode))) /\ ((dst_positive_full_weighted_outputvaluemaskentryright) + ge_balance_negative_full_weighted_outputvaluemaskentryrightvalue = (dst_negative_full_weighted_outputvaluemaskentryright) + ge_balance_positive_full_weighted_outputvaluemaskentryrightvalue))))))))) /\ (exists sto_ap_full_weighted_outputvaluemaskentryproduct sto_an_full_weighted_outputvaluemaskentryproduct sto_bp_full_weighted_outputvaluemaskentryproduct sto_bn_full_weighted_outputvaluemaskentryproduct sto_cp_full_weighted_outputvaluemaskentryproduct sto_cn_full_weighted_outputvaluemaskentryproduct. (((((dc_left_full_weighted_outputvaluemaskentry) = 2 * (sto_ap_full_weighted_outputvaluemaskentryproduct) /\ (sto_an_full_weighted_outputvaluemaskentryproduct) = 0) \/ exists ge_signed_half_full_weighted_outputvaluemaskentryproductleft. (((dc_left_full_weighted_outputvaluemaskentry) = 2 * ge_signed_half_full_weighted_outputvaluemaskentryproductleft + 1 /\ (sto_ap_full_weighted_outputvaluemaskentryproduct) = 0) /\ (sto_an_full_weighted_outputvaluemaskentryproduct) = S ge_signed_half_full_weighted_outputvaluemaskentryproductleft))) /\ ((((((dc_right_full_weighted_outputvaluemaskentry) = 2 * (sto_bp_full_weighted_outputvaluemaskentryproduct) /\ (sto_bn_full_weighted_outputvaluemaskentryproduct) = 0) \/ exists ge_signed_half_full_weighted_outputvaluemaskentryproductright. (((dc_right_full_weighted_outputvaluemaskentry) = 2 * ge_signed_half_full_weighted_outputvaluemaskentryproductright + 1 /\ (sto_bp_full_weighted_outputvaluemaskentryproduct) = 0) /\ (sto_bn_full_weighted_outputvaluemaskentryproduct) = S ge_signed_half_full_weighted_outputvaluemaskentryproductright))) /\ ((((((dc_value_full_weighted_outputvaluemask) = 2 * (sto_cp_full_weighted_outputvaluemaskentryproduct) /\ (sto_cn_full_weighted_outputvaluemaskentryproduct) = 0) \/ exists ge_signed_half_full_weighted_outputvaluemaskentryproductoutput. (((dc_value_full_weighted_outputvaluemask) = 2 * ge_signed_half_full_weighted_outputvaluemaskentryproductoutput + 1 /\ (sto_cp_full_weighted_outputvaluemaskentryproduct) = 0) /\ (sto_cn_full_weighted_outputvaluemaskentryproduct) = S ge_signed_half_full_weighted_outputvaluemaskentryproductoutput))) /\ ((sto_ap_full_weighted_outputvaluemaskentryproduct * sto_bp_full_weighted_outputvaluemaskentryproduct + sto_an_full_weighted_outputvaluemaskentryproduct * sto_bn_full_weighted_outputvaluemaskentryproduct) + sto_cn_full_weighted_outputvaluemaskentryproduct = (sto_ap_full_weighted_outputvaluemaskentryproduct * sto_bn_full_weighted_outputvaluemaskentryproduct + sto_an_full_weighted_outputvaluemaskentryproduct * sto_bp_full_weighted_outputvaluemaskentryproduct) + sto_cp_full_weighted_outputvaluemaskentryproduct))))))))))))))) \/ ((((dc_index_full_weighted_outputvaluemask)=0 \/ ~(exists pvs_factor_full_weighted_outputvaluemaskentrynondivisor. (dc_input_full_weighted_output) = (dc_index_full_weighted_outputvaluemask) * pvs_factor_full_weighted_outputvaluemaskentrynondivisor)) /\ ((dc_value_full_weighted_outputvaluemask)=0))))))) /\ (exists dst_positive_code_full_weighted_outputvaluefold dst_positive_scale_full_weighted_outputvaluefold dst_negative_code_full_weighted_outputvaluefold dst_negative_scale_full_weighted_outputvaluefold dst_positive_sum_full_weighted_outputvaluefold dst_negative_sum_full_weighted_outputvaluefold. (((dc_mask_full_weighted_outputvalue) = (((((dst_positive_code_full_weighted_outputvaluefold) + (dst_positive_scale_full_weighted_outputvaluefold)) * S ((dst_positive_code_full_weighted_outputvaluefold) + (dst_positive_scale_full_weighted_outputvaluefold)) + ((dst_positive_scale_full_weighted_outputvaluefold) + (dst_positive_scale_full_weighted_outputvaluefold))) + (((dst_negative_code_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)) * S ((dst_negative_code_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)) + ((dst_negative_scale_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)))) * S ((((dst_positive_code_full_weighted_outputvaluefold) + (dst_positive_scale_full_weighted_outputvaluefold)) * S ((dst_positive_code_full_weighted_outputvaluefold) + (dst_positive_scale_full_weighted_outputvaluefold)) + ((dst_positive_scale_full_weighted_outputvaluefold) + (dst_positive_scale_full_weighted_outputvaluefold))) + (((dst_negative_code_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)) * S ((dst_negative_code_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)) + ((dst_negative_scale_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)))) + ((((dst_negative_code_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)) * S ((dst_negative_code_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)) + ((dst_negative_scale_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold))) + (((dst_negative_code_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)) * S ((dst_negative_code_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)) + ((dst_negative_scale_full_weighted_outputvaluefold) + (dst_negative_scale_full_weighted_outputvaluefold)))))) /\ (((exists fs_u_dst_full_weighted_outputvaluefoldpositive fs_v_dst_full_weighted_outputvaluefoldpositive. ((((exists fs_h_dst_full_weighted_outputvaluefoldpositive_body_start. fs_h_dst_full_weighted_outputvaluefoldpositive_body_start + S (0) = S ((S (0)) * fs_v_dst_full_weighted_outputvaluefoldpositive)) /\ exists fs_q_dst_full_weighted_outputvaluefoldpositive_body_start. fs_u_dst_full_weighted_outputvaluefoldpositive = fs_q_dst_full_weighted_outputvaluefoldpositive_body_start * S ((S (0)) * fs_v_dst_full_weighted_outputvaluefoldpositive) + (0))) /\ ((((exists fs_h_dst_full_weighted_outputvaluefoldpositive_body_terminal. fs_h_dst_full_weighted_outputvaluefoldpositive_body_terminal + S (dst_positive_sum_full_weighted_outputvaluefold) = S ((S (S (dc_input_full_weighted_output))) * fs_v_dst_full_weighted_outputvaluefoldpositive)) /\ exists fs_q_dst_full_weighted_outputvaluefoldpositive_body_terminal. fs_u_dst_full_weighted_outputvaluefoldpositive = fs_q_dst_full_weighted_outputvaluefoldpositive_body_terminal * S ((S (S (dc_input_full_weighted_output))) * fs_v_dst_full_weighted_outputvaluefoldpositive) + (dst_positive_sum_full_weighted_outputvaluefold))) /\ forall fs_i_dst_full_weighted_outputvaluefoldpositive_body_steps. (exists fs_lt_dst_full_weighted_outputvaluefoldpositive_body_steps_bound. fs_lt_dst_full_weighted_outputvaluefoldpositive_body_steps_bound + S fs_i_dst_full_weighted_outputvaluefoldpositive_body_steps = S (dc_input_full_weighted_output)) -> exists fs_a_dst_full_weighted_outputvaluefoldpositive_body_steps fs_r_dst_full_weighted_outputvaluefoldpositive_body_steps fs_s_dst_full_weighted_outputvaluefoldpositive_body_steps. ((((exists fs_h_dst_full_weighted_outputvaluefoldpositive_body_steps_summand. fs_h_dst_full_weighted_outputvaluefoldpositive_body_steps_summand + S (fs_a_dst_full_weighted_outputvaluefoldpositive_body_steps) = S ((S (fs_i_dst_full_weighted_outputvaluefoldpositive_body_steps)) * dst_positive_scale_full_weighted_outputvaluefold)) /\ exists fs_q_dst_full_weighted_outputvaluefoldpositive_body_steps_summand. dst_positive_code_full_weighted_outputvaluefold = fs_q_dst_full_weighted_outputvaluefoldpositive_body_steps_summand * S ((S (fs_i_dst_full_weighted_outputvaluefoldpositive_body_steps)) * dst_positive_scale_full_weighted_outputvaluefold) + (fs_a_dst_full_weighted_outputvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_full_weighted_outputvaluefoldpositive_body_steps_partial. fs_h_dst_full_weighted_outputvaluefoldpositive_body_steps_partial + S (fs_r_dst_full_weighted_outputvaluefoldpositive_body_steps) = S ((S (fs_i_dst_full_weighted_outputvaluefoldpositive_body_steps)) * fs_v_dst_full_weighted_outputvaluefoldpositive)) /\ exists fs_q_dst_full_weighted_outputvaluefoldpositive_body_steps_partial. fs_u_dst_full_weighted_outputvaluefoldpositive = fs_q_dst_full_weighted_outputvaluefoldpositive_body_steps_partial * S ((S (fs_i_dst_full_weighted_outputvaluefoldpositive_body_steps)) * fs_v_dst_full_weighted_outputvaluefoldpositive) + (fs_r_dst_full_weighted_outputvaluefoldpositive_body_steps))) /\ ((((exists fs_h_dst_full_weighted_outputvaluefoldpositive_body_steps_successor. fs_h_dst_full_weighted_outputvaluefoldpositive_body_steps_successor + S (fs_s_dst_full_weighted_outputvaluefoldpositive_body_steps) = S ((S (S fs_i_dst_full_weighted_outputvaluefoldpositive_body_steps)) * fs_v_dst_full_weighted_outputvaluefoldpositive)) /\ exists fs_q_dst_full_weighted_outputvaluefoldpositive_body_steps_successor. fs_u_dst_full_weighted_outputvaluefoldpositive = fs_q_dst_full_weighted_outputvaluefoldpositive_body_steps_successor * S ((S (S fs_i_dst_full_weighted_outputvaluefoldpositive_body_steps)) * fs_v_dst_full_weighted_outputvaluefoldpositive) + (fs_s_dst_full_weighted_outputvaluefoldpositive_body_steps))) /\ fs_s_dst_full_weighted_outputvaluefoldpositive_body_steps = fs_r_dst_full_weighted_outputvaluefoldpositive_body_steps + fs_a_dst_full_weighted_outputvaluefoldpositive_body_steps)))))) /\ (((exists fs_u_dst_full_weighted_outputvaluefoldnegative fs_v_dst_full_weighted_outputvaluefoldnegative. ((((exists fs_h_dst_full_weighted_outputvaluefoldnegative_body_start. fs_h_dst_full_weighted_outputvaluefoldnegative_body_start + S (0) = S ((S (0)) * fs_v_dst_full_weighted_outputvaluefoldnegative)) /\ exists fs_q_dst_full_weighted_outputvaluefoldnegative_body_start. fs_u_dst_full_weighted_outputvaluefoldnegative = fs_q_dst_full_weighted_outputvaluefoldnegative_body_start * S ((S (0)) * fs_v_dst_full_weighted_outputvaluefoldnegative) + (0))) /\ ((((exists fs_h_dst_full_weighted_outputvaluefoldnegative_body_terminal. fs_h_dst_full_weighted_outputvaluefoldnegative_body_terminal + S (dst_negative_sum_full_weighted_outputvaluefold) = S ((S (S (dc_input_full_weighted_output))) * fs_v_dst_full_weighted_outputvaluefoldnegative)) /\ exists fs_q_dst_full_weighted_outputvaluefoldnegative_body_terminal. fs_u_dst_full_weighted_outputvaluefoldnegative = fs_q_dst_full_weighted_outputvaluefoldnegative_body_terminal * S ((S (S (dc_input_full_weighted_output))) * fs_v_dst_full_weighted_outputvaluefoldnegative) + (dst_negative_sum_full_weighted_outputvaluefold))) /\ forall fs_i_dst_full_weighted_outputvaluefoldnegative_body_steps. (exists fs_lt_dst_full_weighted_outputvaluefoldnegative_body_steps_bound. fs_lt_dst_full_weighted_outputvaluefoldnegative_body_steps_bound + S fs_i_dst_full_weighted_outputvaluefoldnegative_body_steps = S (dc_input_full_weighted_output)) -> exists fs_a_dst_full_weighted_outputvaluefoldnegative_body_steps fs_r_dst_full_weighted_outputvaluefoldnegative_body_steps fs_s_dst_full_weighted_outputvaluefoldnegative_body_steps. ((((exists fs_h_dst_full_weighted_outputvaluefoldnegative_body_steps_summand. fs_h_dst_full_weighted_outputvaluefoldnegative_body_steps_summand + S (fs_a_dst_full_weighted_outputvaluefoldnegative_body_steps) = S ((S (fs_i_dst_full_weighted_outputvaluefoldnegative_body_steps)) * dst_negative_scale_full_weighted_outputvaluefold)) /\ exists fs_q_dst_full_weighted_outputvaluefoldnegative_body_steps_summand. dst_negative_code_full_weighted_outputvaluefold = fs_q_dst_full_weighted_outputvaluefoldnegative_body_steps_summand * S ((S (fs_i_dst_full_weighted_outputvaluefoldnegative_body_steps)) * dst_negative_scale_full_weighted_outputvaluefold) + (fs_a_dst_full_weighted_outputvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_full_weighted_outputvaluefoldnegative_body_steps_partial. fs_h_dst_full_weighted_outputvaluefoldnegative_body_steps_partial + S (fs_r_dst_full_weighted_outputvaluefoldnegative_body_steps) = S ((S (fs_i_dst_full_weighted_outputvaluefoldnegative_body_steps)) * fs_v_dst_full_weighted_outputvaluefoldnegative)) /\ exists fs_q_dst_full_weighted_outputvaluefoldnegative_body_steps_partial. fs_u_dst_full_weighted_outputvaluefoldnegative = fs_q_dst_full_weighted_outputvaluefoldnegative_body_steps_partial * S ((S (fs_i_dst_full_weighted_outputvaluefoldnegative_body_steps)) * fs_v_dst_full_weighted_outputvaluefoldnegative) + (fs_r_dst_full_weighted_outputvaluefoldnegative_body_steps))) /\ ((((exists fs_h_dst_full_weighted_outputvaluefoldnegative_body_steps_successor. fs_h_dst_full_weighted_outputvaluefoldnegative_body_steps_successor + S (fs_s_dst_full_weighted_outputvaluefoldnegative_body_steps) = S ((S (S fs_i_dst_full_weighted_outputvaluefoldnegative_body_steps)) * fs_v_dst_full_weighted_outputvaluefoldnegative)) /\ exists fs_q_dst_full_weighted_outputvaluefoldnegative_body_steps_successor. fs_u_dst_full_weighted_outputvaluefoldnegative = fs_q_dst_full_weighted_outputvaluefoldnegative_body_steps_successor * S ((S (S fs_i_dst_full_weighted_outputvaluefoldnegative_body_steps)) * fs_v_dst_full_weighted_outputvaluefoldnegative) + (fs_s_dst_full_weighted_outputvaluefoldnegative_body_steps))) /\ fs_s_dst_full_weighted_outputvaluefoldnegative_body_steps = fs_r_dst_full_weighted_outputvaluefoldnegative_body_steps + fs_a_dst_full_weighted_outputvaluefoldnegative_body_steps)))))) /\ (exists ge_balance_positive_full_weighted_outputvaluefoldresult ge_balance_negative_full_weighted_outputvaluefoldresult. (((((dc_output_full_weighted_output) = 2 * (ge_balance_positive_full_weighted_outputvaluefoldresult) /\ (ge_balance_negative_full_weighted_outputvaluefoldresult) = 0) \/ exists ge_signed_half_full_weighted_outputvaluefoldresultdecode. (((dc_output_full_weighted_output) = 2 * ge_signed_half_full_weighted_outputvaluefoldresultdecode + 1 /\ (ge_balance_positive_full_weighted_outputvaluefoldresult) = 0) /\ (ge_balance_negative_full_weighted_outputvaluefoldresult) = S ge_signed_half_full_weighted_outputvaluefoldresultdecode))) /\ ((dst_positive_sum_full_weighted_outputvaluefold) + ge_balance_negative_full_weighted_outputvaluefoldresult = (dst_negative_sum_full_weighted_outputvaluefold) + ge_balance_positive_full_weighted_outputvaluefoldresult)))))))))))))))))))) /\ (forall dm_index_full_original_values dm_first_value_full_original_values dm_second_value_full_original_values. ~(dm_index_full_original_values=0) -> (exists pvs_le_gap_full_original_valuesdomain. pvs_le_gap_full_original_valuesdomain + (dm_index_full_original_values) = (N)) -> (exists dst_positive_code_full_original_valuesfirst dst_positive_scale_full_original_valuesfirst dst_negative_code_full_original_valuesfirst dst_negative_scale_full_original_valuesfirst dst_positive_full_original_valuesfirst dst_negative_full_original_valuesfirst. (((H) = (((((dst_positive_code_full_original_valuesfirst) + (dst_positive_scale_full_original_valuesfirst)) * S ((dst_positive_code_full_original_valuesfirst) + (dst_positive_scale_full_original_valuesfirst)) + ((dst_positive_scale_full_original_valuesfirst) + (dst_positive_scale_full_original_valuesfirst))) + (((dst_negative_code_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)) * S ((dst_negative_code_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)) + ((dst_negative_scale_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)))) * S ((((dst_positive_code_full_original_valuesfirst) + (dst_positive_scale_full_original_valuesfirst)) * S ((dst_positive_code_full_original_valuesfirst) + (dst_positive_scale_full_original_valuesfirst)) + ((dst_positive_scale_full_original_valuesfirst) + (dst_positive_scale_full_original_valuesfirst))) + (((dst_negative_code_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)) * S ((dst_negative_code_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)) + ((dst_negative_scale_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)))) + ((((dst_negative_code_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)) * S ((dst_negative_code_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)) + ((dst_negative_scale_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst))) + (((dst_negative_code_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)) * S ((dst_negative_code_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)) + ((dst_negative_scale_full_original_valuesfirst) + (dst_negative_scale_full_original_valuesfirst)))))) /\ (((((exists ff_h_pvs_full_original_valuesfirstpositive. ff_h_pvs_full_original_valuesfirstpositive + S (dst_positive_full_original_valuesfirst) = S ((S (dm_index_full_original_values)) * dst_positive_scale_full_original_valuesfirst)) /\ exists ff_q_pvs_full_original_valuesfirstpositive. dst_positive_code_full_original_valuesfirst = ff_q_pvs_full_original_valuesfirstpositive * S ((S (dm_index_full_original_values)) * dst_positive_scale_full_original_valuesfirst) + (dst_positive_full_original_valuesfirst))) /\ (((((exists ff_h_pvs_full_original_valuesfirstnegative. ff_h_pvs_full_original_valuesfirstnegative + S (dst_negative_full_original_valuesfirst) = S ((S (dm_index_full_original_values)) * dst_negative_scale_full_original_valuesfirst)) /\ exists ff_q_pvs_full_original_valuesfirstnegative. dst_negative_code_full_original_valuesfirst = ff_q_pvs_full_original_valuesfirstnegative * S ((S (dm_index_full_original_values)) * dst_negative_scale_full_original_valuesfirst) + (dst_negative_full_original_valuesfirst))) /\ (exists ge_balance_positive_full_original_valuesfirstvalue ge_balance_negative_full_original_valuesfirstvalue. (((((dm_first_value_full_original_values) = 2 * (ge_balance_positive_full_original_valuesfirstvalue) /\ (ge_balance_negative_full_original_valuesfirstvalue) = 0) \/ exists ge_signed_half_full_original_valuesfirstvaluedecode. (((dm_first_value_full_original_values) = 2 * ge_signed_half_full_original_valuesfirstvaluedecode + 1 /\ (ge_balance_positive_full_original_valuesfirstvalue) = 0) /\ (ge_balance_negative_full_original_valuesfirstvalue) = S ge_signed_half_full_original_valuesfirstvaluedecode))) /\ ((dst_positive_full_original_valuesfirst) + ge_balance_negative_full_original_valuesfirstvalue = (dst_negative_full_original_valuesfirst) + ge_balance_positive_full_original_valuesfirstvalue))))))))) -> (exists dst_positive_code_full_original_valuessecond dst_positive_scale_full_original_valuessecond dst_negative_code_full_original_valuessecond dst_negative_scale_full_original_valuessecond dst_positive_full_original_valuessecond dst_negative_full_original_valuessecond. (((F) = (((((dst_positive_code_full_original_valuessecond) + (dst_positive_scale_full_original_valuessecond)) * S ((dst_positive_code_full_original_valuessecond) + (dst_positive_scale_full_original_valuessecond)) + ((dst_positive_scale_full_original_valuessecond) + (dst_positive_scale_full_original_valuessecond))) + (((dst_negative_code_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)) * S ((dst_negative_code_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)) + ((dst_negative_scale_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)))) * S ((((dst_positive_code_full_original_valuessecond) + (dst_positive_scale_full_original_valuessecond)) * S ((dst_positive_code_full_original_valuessecond) + (dst_positive_scale_full_original_valuessecond)) + ((dst_positive_scale_full_original_valuessecond) + (dst_positive_scale_full_original_valuessecond))) + (((dst_negative_code_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)) * S ((dst_negative_code_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)) + ((dst_negative_scale_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)))) + ((((dst_negative_code_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)) * S ((dst_negative_code_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)) + ((dst_negative_scale_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond))) + (((dst_negative_code_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)) * S ((dst_negative_code_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)) + ((dst_negative_scale_full_original_valuessecond) + (dst_negative_scale_full_original_valuessecond)))))) /\ (((((exists ff_h_pvs_full_original_valuessecondpositive. ff_h_pvs_full_original_valuessecondpositive + S (dst_positive_full_original_valuessecond) = S ((S (dm_index_full_original_values)) * dst_positive_scale_full_original_valuessecond)) /\ exists ff_q_pvs_full_original_valuessecondpositive. dst_positive_code_full_original_valuessecond = ff_q_pvs_full_original_valuessecondpositive * S ((S (dm_index_full_original_values)) * dst_positive_scale_full_original_valuessecond) + (dst_positive_full_original_valuessecond))) /\ (((((exists ff_h_pvs_full_original_valuessecondnegative. ff_h_pvs_full_original_valuessecondnegative + S (dst_negative_full_original_valuessecond) = S ((S (dm_index_full_original_values)) * dst_negative_scale_full_original_valuessecond)) /\ exists ff_q_pvs_full_original_valuessecondnegative. dst_negative_code_full_original_valuessecond = ff_q_pvs_full_original_valuessecondnegative * S ((S (dm_index_full_original_values)) * dst_negative_scale_full_original_valuessecond) + (dst_negative_full_original_valuessecond))) /\ (exists ge_balance_positive_full_original_valuessecondvalue ge_balance_negative_full_original_valuessecondvalue. (((((dm_second_value_full_original_values) = 2 * (ge_balance_positive_full_original_valuessecondvalue) /\ (ge_balance_negative_full_original_valuessecondvalue) = 0) \/ exists ge_signed_half_full_original_valuessecondvaluedecode. (((dm_second_value_full_original_values) = 2 * ge_signed_half_full_original_valuessecondvaluedecode + 1 /\ (ge_balance_positive_full_original_valuessecondvalue) = 0) /\ (ge_balance_negative_full_original_valuessecondvalue) = S ge_signed_half_full_original_valuessecondvaluedecode))) /\ ((dst_positive_full_original_valuessecond) + ge_balance_negative_full_original_valuessecondvalue = (dst_negative_full_original_valuessecond) + ge_balance_positive_full_original_valuessecondvalue))))))))) -> dm_first_value_full_original_values=dm_second_value_full_original_values))))Constructive proof overview
Generated structural guide
Full finite signed Möbius inversion constructs the independent Möbius table and a real output table whose actual weighted divisor sums recover every positive original value, including the genuine empty-window case N=0.
The unchanged tactic script uses 3 declared prerequisites and contains 38 exact native proof lines.
Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable
Proof neighborhood
Direct dependencies
mobius_table_exists Alpha theorem; checked-use authorized MI0005 mobius_inversion_for_actual_mobius_table divisor_signed_table_at_functional Alpha theorem; checked-use authorizedDirect dependents
none
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 (1)
01Fix variables and assumptionsL1–6
02Establish hML7–9
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mobius table exists.
- L7
have hM : ∃ M. MobiusTable(N,M)Definitions: MobiusTable - L8
specialize mobius_table_exists (N) - L9
apply mobius_table_exists
03Separate the logical casesL10–10
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L10
cases hM
04Construct an explicit witnessL11–12
05Separate the logical casesL13–13
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L13
split
06Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact hM_witness
07Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
split
08Use earlier factsL16–24
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
specialize mobius_inversion_for_actual_mobius_table (N) - L17
specialize mobius_inversion_for_actual_mobius_table (F) - L18
specialize mobius_inversion_for_actual_mobius_table (G) - L19
specialize mobius_inversion_for_actual_mobius_table (x) - L20
apply mobius_inversion_for_actual_mobius_table - L21
exact hF - L22
exact hG - L23
exact hM_witness - L24
exact ht
09Fix variables and assumptionsL25–31
10Use earlier factsL32–38
Instantiate or apply named facts and discharge the corresponding proof obligations.
Original exact command ledger · 38 lines
- 0001
intro N - 0002
intro F - 0003
intro G - 0004
intro hF - 0005
intro hG - 0006
intro ht - 0007
have hM : exists M. (((exists dst_positive_code_inversion_actual_mobiustable dst_positive_scale_inversion_actual_mobiustable dst_negative_code_inversion_actual_mobiustable dst_negative_scale_inversion_actual_mobiustable. (((M) = (((((dst_positive_code_inversion_actual_mobiustable) + (dst_positive_scale_inversion_actual_mobiustable)) * S ((dst_positive_code_inversion_actual_mobiustable) + (dst_positive_scale_inversion_actual_mobiustable)) + ((dst_positive_scale_inversion_actual_mobiustable) + (dst_positive_scale_inversion_actual_mobiustable))) + (((dst_negative_code_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)) * S ((dst_negative_code_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)) + ((dst_negative_scale_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)))) * S ((((dst_positive_code_inversion_actual_mobiustable) + (dst_positive_scale_inversion_actual_mobiustable)) * S ((dst_positive_code_inversion_actual_mobiustable) + (dst_positive_scale_inversion_actual_mobiustable)) + ((dst_positive_scale_inversion_actual_mobiustable) + (dst_positive_scale_inversion_actual_mobiustable))) + (((dst_negative_code_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)) * S ((dst_negative_code_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)) + ((dst_negative_scale_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)))) + ((((dst_negative_code_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)) * S ((dst_negative_code_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)) + ((dst_negative_scale_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable))) + (((dst_negative_code_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)) * S ((dst_negative_code_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)) + ((dst_negative_scale_inversion_actual_mobiustable) + (dst_negative_scale_inversion_actual_mobiustable)))))) /\ (forall dst_index_inversion_actual_mobiustable. (exists pvs_le_gap_inversion_actual_mobiustabledomain. pvs_le_gap_inversion_actual_mobiustabledomain + (dst_index_inversion_actual_mobiustable) = (N)) -> exists dst_positive_inversion_actual_mobiustable dst_negative_inversion_actual_mobiustable dst_value_inversion_actual_mobiustable. ((((exists ff_h_pvs_inversion_actual_mobiustableentrypositive. ff_h_pvs_inversion_actual_mobiustableentrypositive + S (dst_positive_inversion_actual_mobiustable) = S ((S (dst_index_inversion_actual_mobiustable)) * dst_positive_scale_inversion_actual_mobiustable)) /\ exists ff_q_pvs_inversion_actual_mobiustableentrypositive. dst_positive_code_inversion_actual_mobiustable = ff_q_pvs_inversion_actual_mobiustableentrypositive * S ((S (dst_index_inversion_actual_mobiustable)) * dst_positive_scale_inversion_actual_mobiustable) + (dst_positive_inversion_actual_mobiustable))) /\ (((((exists ff_h_pvs_inversion_actual_mobiustableentrynegative. ff_h_pvs_inversion_actual_mobiustableentrynegative + S (dst_negative_inversion_actual_mobiustable) = S ((S (dst_index_inversion_actual_mobiustable)) * dst_negative_scale_inversion_actual_mobiustable)) /\ exists ff_q_pvs_inversion_actual_mobiustableentrynegative. dst_negative_code_inversion_actual_mobiustable = ff_q_pvs_inversion_actual_mobiustableentrynegative * S ((S (dst_index_inversion_actual_mobiustable)) * dst_negative_scale_inversion_actual_mobiustable) + (dst_negative_inversion_actual_mobiustable))) /\ (exists ge_balance_positive_inversion_actual_mobiustableentryvalue ge_balance_negative_inversion_actual_mobiustableentryvalue. (((((dst_value_inversion_actual_mobiustable) = 2 * (ge_balance_positive_inversion_actual_mobiustableentryvalue) /\ (ge_balance_negative_inversion_actual_mobiustableentryvalue) = 0) \/ exists ge_signed_half_inversion_actual_mobiustableentryvaluedecode. (((dst_value_inversion_actual_mobiustable) = 2 * ge_signed_half_inversion_actual_mobiustableentryvaluedecode + 1 /\ (ge_balance_positive_inversion_actual_mobiustableentryvalue) = 0) /\ (ge_balance_negative_inversion_actual_mobiustableentryvalue) = S ge_signed_half_inversion_actual_mobiustableentryvaluedecode))) /\ ((dst_positive_inversion_actual_mobiustable) + ge_balance_negative_inversion_actual_mobiustableentryvalue = (dst_negative_inversion_actual_mobiustable) + ge_balance_positive_inversion_actual_mobiustableentryvalue))))))))) /\ (((exists dst_positive_code_inversion_actual_mobiuszero dst_positive_scale_inversion_actual_mobiuszero dst_negative_code_inversion_actual_mobiuszero dst_negative_scale_inversion_actual_mobiuszero dst_positive_inversion_actual_mobiuszero dst_negative_inversion_actual_mobiuszero. (((M) = (((((dst_positive_code_inversion_actual_mobiuszero) + (dst_positive_scale_inversion_actual_mobiuszero)) * S ((dst_positive_code_inversion_actual_mobiuszero) + (dst_positive_scale_inversion_actual_mobiuszero)) + ((dst_positive_scale_inversion_actual_mobiuszero) + (dst_positive_scale_inversion_actual_mobiuszero))) + (((dst_negative_code_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)) * S ((dst_negative_code_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)) + ((dst_negative_scale_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)))) * S ((((dst_positive_code_inversion_actual_mobiuszero) + (dst_positive_scale_inversion_actual_mobiuszero)) * S ((dst_positive_code_inversion_actual_mobiuszero) + (dst_positive_scale_inversion_actual_mobiuszero)) + ((dst_positive_scale_inversion_actual_mobiuszero) + (dst_positive_scale_inversion_actual_mobiuszero))) + (((dst_negative_code_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)) * S ((dst_negative_code_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)) + ((dst_negative_scale_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)))) + ((((dst_negative_code_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)) * S ((dst_negative_code_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)) + ((dst_negative_scale_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero))) + (((dst_negative_code_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)) * S ((dst_negative_code_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)) + ((dst_negative_scale_inversion_actual_mobiuszero) + (dst_negative_scale_inversion_actual_mobiuszero)))))) /\ (((((exists ff_h_pvs_inversion_actual_mobiuszeropositive. ff_h_pvs_inversion_actual_mobiuszeropositive + S (dst_positive_inversion_actual_mobiuszero) = S ((S (0)) * dst_positive_scale_inversion_actual_mobiuszero)) /\ exists ff_q_pvs_inversion_actual_mobiuszeropositive. dst_positive_code_inversion_actual_mobiuszero = ff_q_pvs_inversion_actual_mobiuszeropositive * S ((S (0)) * dst_positive_scale_inversion_actual_mobiuszero) + (dst_positive_inversion_actual_mobiuszero))) /\ (((((exists ff_h_pvs_inversion_actual_mobiuszeronegative. ff_h_pvs_inversion_actual_mobiuszeronegative + S (dst_negative_inversion_actual_mobiuszero) = S ((S (0)) * dst_negative_scale_inversion_actual_mobiuszero)) /\ exists ff_q_pvs_inversion_actual_mobiuszeronegative. dst_negative_code_inversion_actual_mobiuszero = ff_q_pvs_inversion_actual_mobiuszeronegative * S ((S (0)) * dst_negative_scale_inversion_actual_mobiuszero) + (dst_negative_inversion_actual_mobiuszero))) /\ (exists ge_balance_positive_inversion_actual_mobiuszerovalue ge_balance_negative_inversion_actual_mobiuszerovalue. (((((0) = 2 * (ge_balance_positive_inversion_actual_mobiuszerovalue) /\ (ge_balance_negative_inversion_actual_mobiuszerovalue) = 0) \/ exists ge_signed_half_inversion_actual_mobiuszerovaluedecode. (((0) = 2 * ge_signed_half_inversion_actual_mobiuszerovaluedecode + 1 /\ (ge_balance_positive_inversion_actual_mobiuszerovalue) = 0) /\ (ge_balance_negative_inversion_actual_mobiuszerovalue) = S ge_signed_half_inversion_actual_mobiuszerovaluedecode))) /\ ((dst_positive_inversion_actual_mobiuszero) + ge_balance_negative_inversion_actual_mobiuszerovalue = (dst_negative_inversion_actual_mobiuszero) + ge_balance_positive_inversion_actual_mobiuszerovalue))))))))) /\ (forall mt_index_inversion_actual_mobius mt_value_inversion_actual_mobius. ~(mt_index_inversion_actual_mobius=0) -> (exists pvs_le_gap_inversion_actual_mobiusdomain. pvs_le_gap_inversion_actual_mobiusdomain + (mt_index_inversion_actual_mobius) = (N)) -> (exists dst_positive_code_inversion_actual_mobiusentry dst_positive_scale_inversion_actual_mobiusentry dst_negative_code_inversion_actual_mobiusentry dst_negative_scale_inversion_actual_mobiusentry dst_positive_inversion_actual_mobiusentry dst_negative_inversion_actual_mobiusentry. (((M) = (((((dst_positive_code_inversion_actual_mobiusentry) + (dst_positive_scale_inversion_actual_mobiusentry)) * S ((dst_positive_code_inversion_actual_mobiusentry) + (dst_positive_scale_inversion_actual_mobiusentry)) + ((dst_positive_scale_inversion_actual_mobiusentry) + (dst_positive_scale_inversion_actual_mobiusentry))) + (((dst_negative_code_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)) * S ((dst_negative_code_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)) + ((dst_negative_scale_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)))) * S ((((dst_positive_code_inversion_actual_mobiusentry) + (dst_positive_scale_inversion_actual_mobiusentry)) * S ((dst_positive_code_inversion_actual_mobiusentry) + (dst_positive_scale_inversion_actual_mobiusentry)) + ((dst_positive_scale_inversion_actual_mobiusentry) + (dst_positive_scale_inversion_actual_mobiusentry))) + (((dst_negative_code_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)) * S ((dst_negative_code_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)) + ((dst_negative_scale_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)))) + ((((dst_negative_code_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)) * S ((dst_negative_code_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)) + ((dst_negative_scale_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry))) + (((dst_negative_code_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)) * S ((dst_negative_code_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)) + ((dst_negative_scale_inversion_actual_mobiusentry) + (dst_negative_scale_inversion_actual_mobiusentry)))))) /\ (((((exists ff_h_pvs_inversion_actual_mobiusentrypositive. ff_h_pvs_inversion_actual_mobiusentrypositive + S (dst_positive_inversion_actual_mobiusentry) = S ((S (mt_index_inversion_actual_mobius)) * dst_positive_scale_inversion_actual_mobiusentry)) /\ exists ff_q_pvs_inversion_actual_mobiusentrypositive. dst_positive_code_inversion_actual_mobiusentry = ff_q_pvs_inversion_actual_mobiusentrypositive * S ((S (mt_index_inversion_actual_mobius)) * dst_positive_scale_inversion_actual_mobiusentry) + (dst_positive_inversion_actual_mobiusentry))) /\ (((((exists ff_h_pvs_inversion_actual_mobiusentrynegative. ff_h_pvs_inversion_actual_mobiusentrynegative + S (dst_negative_inversion_actual_mobiusentry) = S ((S (mt_index_inversion_actual_mobius)) * dst_negative_scale_inversion_actual_mobiusentry)) /\ exists ff_q_pvs_inversion_actual_mobiusentrynegative. dst_negative_code_inversion_actual_mobiusentry = ff_q_pvs_inversion_actual_mobiusentrynegative * S ((S (mt_index_inversion_actual_mobius)) * dst_negative_scale_inversion_actual_mobiusentry) + (dst_negative_inversion_actual_mobiusentry))) /\ (exists ge_balance_positive_inversion_actual_mobiusentryvalue ge_balance_negative_inversion_actual_mobiusentryvalue. (((((mt_value_inversion_actual_mobius) = 2 * (ge_balance_positive_inversion_actual_mobiusentryvalue) /\ (ge_balance_negative_inversion_actual_mobiusentryvalue) = 0) \/ exists ge_signed_half_inversion_actual_mobiusentryvaluedecode. (((mt_value_inversion_actual_mobius) = 2 * ge_signed_half_inversion_actual_mobiusentryvaluedecode + 1 /\ (ge_balance_positive_inversion_actual_mobiusentryvalue) = 0) /\ (ge_balance_negative_inversion_actual_mobiusentryvalue) = S ge_signed_half_inversion_actual_mobiusentryvaluedecode))) /\ ((dst_positive_inversion_actual_mobiusentry) + ge_balance_negative_inversion_actual_mobiusentryvalue = (dst_negative_inversion_actual_mobiusentry) + ge_balance_positive_inversion_actual_mobiusentryvalue))))))))) -> (((~((mt_index_inversion_actual_mobius) = 0)) /\ ((((exists mv_square_prime_inversion_actual_mobiusvaluesquare. ((~((mv_square_prime_inversion_actual_mobiusvaluesquare) = 1) /\ forall pvs_left_inversion_actual_mobiusvaluesquareprime pvs_right_inversion_actual_mobiusvaluesquareprime. (mv_square_prime_inversion_actual_mobiusvaluesquare) = pvs_left_inversion_actual_mobiusvaluesquareprime * pvs_right_inversion_actual_mobiusvaluesquareprime -> pvs_left_inversion_actual_mobiusvaluesquareprime = 1 \/ pvs_right_inversion_actual_mobiusvaluesquareprime = 1) /\ (exists pvs_factor_inversion_actual_mobiusvaluesquaredivisor. (mt_index_inversion_actual_mobius) = (mv_square_prime_inversion_actual_mobiusvaluesquare * mv_square_prime_inversion_actual_mobiusvaluesquare) * pvs_factor_inversion_actual_mobiusvaluesquaredivisor))) /\ ((mt_value_inversion_actual_mobius) = 0))) \/ (((((~((mt_index_inversion_actual_mobius) = 0)) /\ (forall sfd_prime_inversion_actual_mobiusvaluesquarefree. (~((sfd_prime_inversion_actual_mobiusvaluesquarefree) = 1) /\ forall pvs_left_inversion_actual_mobiusvaluesquarefreedomain pvs_right_inversion_actual_mobiusvaluesquarefreedomain. (sfd_prime_inversion_actual_mobiusvaluesquarefree) = pvs_left_inversion_actual_mobiusvaluesquarefreedomain * pvs_right_inversion_actual_mobiusvaluesquarefreedomain -> pvs_left_inversion_actual_mobiusvaluesquarefreedomain = 1 \/ pvs_right_inversion_actual_mobiusvaluesquarefreedomain = 1) -> (exists pvs_le_gap_inversion_actual_mobiusvaluesquarefreebound. pvs_le_gap_inversion_actual_mobiusvaluesquarefreebound + (sfd_prime_inversion_actual_mobiusvaluesquarefree) = (mt_index_inversion_actual_mobius)) -> ~(exists pvs_factor_inversion_actual_mobiusvaluesquarefreesquare. (mt_index_inversion_actual_mobius) = (sfd_prime_inversion_actual_mobiusvaluesquarefree * sfd_prime_inversion_actual_mobiusvaluesquarefree) * pvs_factor_inversion_actual_mobiusvaluesquarefreesquare)))) /\ (exists mv_factor_code_inversion_actual_mobiusvaluefactors mv_factor_scale_inversion_actual_mobiusvaluefactors mv_factor_count_inversion_actual_mobiusvaluefactors. (((~(mt_index_inversion_actual_mobius = 0) /\ ((exists ff_u_fsat_inversion_actual_mobiusvaluefactorsfactorization_product ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_start. ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_start. ff_u_fsat_inversion_actual_mobiusvaluefactorsfactorization_product = ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_terminal. ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_terminal + S (mt_index_inversion_actual_mobius) = S ((S (mv_factor_count_inversion_actual_mobiusvaluefactors)) * ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_terminal. ff_u_fsat_inversion_actual_mobiusvaluefactorsfactorization_product = ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_inversion_actual_mobiusvaluefactors)) * ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product) + (mt_index_inversion_actual_mobius))) /\ forall ff_i_fsat_inversion_actual_mobiusvaluefactorsfactorization_product. (exists ff_lt_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_bound. ff_lt_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_bound + S ff_i_fsat_inversion_actual_mobiusvaluefactorsfactorization_product = mv_factor_count_inversion_actual_mobiusvaluefactors) -> exists ff_p_fsat_inversion_actual_mobiusvaluefactorsfactorization_product ff_r_fsat_inversion_actual_mobiusvaluefactorsfactorization_product ff_s_fsat_inversion_actual_mobiusvaluefactorsfactorization_product. ((((exists ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_factor. ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_factor + S (ff_p_fsat_inversion_actual_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_inversion_actual_mobiusvaluefactors)) /\ exists ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_factor. mv_factor_code_inversion_actual_mobiusvaluefactors = ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) * mv_factor_scale_inversion_actual_mobiusvaluefactors) + (ff_p_fsat_inversion_actual_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_partial. ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_partial + S (ff_r_fsat_inversion_actual_mobiusvaluefactorsfactorization_product) = S ((S (ff_i_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_partial. ff_u_fsat_inversion_actual_mobiusvaluefactorsfactorization_product = ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product) + (ff_r_fsat_inversion_actual_mobiusvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_successor. ff_h_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_successor + S (ff_s_fsat_inversion_actual_mobiusvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) /\ exists ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_successor. ff_u_fsat_inversion_actual_mobiusvaluefactorsfactorization_product = ff_q_fsat_inversion_actual_mobiusvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)) * ff_v_fsat_inversion_actual_mobiusvaluefactorsfactorization_product) + (ff_s_fsat_inversion_actual_mobiusvaluefactorsfactorization_product))) /\ ff_s_fsat_inversion_actual_mobiusvaluefactorsfactorization_product = ff_r_fsat_inversion_actual_mobiusvaluefactorsfactorization_product * ff_p_fsat_inversion_actual_mobiusvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes = (mv_factor_count_inversion_actual_mobiusvaluefactors)) -> exists ftsf_factor_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_inversion_actual_mobiusvaluefactors)) /\ exists ff_q_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_entry. mv_factor_code_inversion_actual_mobiusvaluefactors = ff_q_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes)) * mv_factor_scale_inversion_actual_mobiusvaluefactors) + (ftsf_factor_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_inversion_actual_mobiusvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_inversion_actual_mobiusvaluefactorsparityeven. (mv_factor_count_inversion_actual_mobiusvaluefactors) = 2 * mv_even_half_inversion_actual_mobiusvaluefactorsparityeven) /\ ((mt_value_inversion_actual_mobius) = 2))) \/ (((exists mv_odd_half_inversion_actual_mobiusvaluefactorsparityodd. (mv_factor_count_inversion_actual_mobiusvaluefactors) = 2 * mv_odd_half_inversion_actual_mobiusvaluefactorsparityodd + 1) /\ ((mt_value_inversion_actual_mobius) = 1)))))))))))))))) - 0008
specialize mobius_table_exists (N) - 0009
apply mobius_table_exists - 0010
cases hM - 0011
exists x - 0012
exists F - 0013
split - 0014
exact hM_witness - 0015
split - 0016
specialize mobius_inversion_for_actual_mobius_table (N) - 0017
specialize mobius_inversion_for_actual_mobius_table (F) - 0018
specialize mobius_inversion_for_actual_mobius_table (G) - 0019
specialize mobius_inversion_for_actual_mobius_table (x) - 0020
apply mobius_inversion_for_actual_mobius_table - 0021
exact hF - 0022
exact hG - 0023
exact hM_witness - 0024
exact ht - 0025
intro n - 0026
intro a - 0027
intro b - 0028
intro hn - 0029
intro hbound - 0030
intro ha - 0031
intro hb - 0032
specialize divisor_signed_table_at_functional (F) - 0033
specialize divisor_signed_table_at_functional (n) - 0034
specialize divisor_signed_table_at_functional (a) - 0035
specialize divisor_signed_table_at_functional (b) - 0036
apply divisor_signed_table_at_functional - 0037
exact ha - 0038
exact hb