Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.
The full finite signed G007 theorem includes the reverse equivalence and actual witnesses at N=0. The divisor-transform premise covers every required positive quotient. F(0), G(0) and H(0) are unrestricted; only the historical Möbius witness retains its separate zero convention. Full G009 multiplicative closure is admitted in Alpha v32; G091 prime-power fields remain open.
Exact theorem in conservative defined notation
∀ N. ∀ F. ∀ G. ArithTable(N,F) → ArithTable(N,G) → DivisorTransform(N,F,G) → ∃ x. ∃ y. MobiusTable(N,x) ∧ (DirichletTable(N,x,G,y) ∧ ArithPositiveEqual(y,F,N))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
Original expanded first-order 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))))Complete tactic proof in conservative notation
All 38 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
38 script commands · 10 reading checkpoints · 1 local claims
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.
Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.
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(N,M)Original native command in the exact edition - 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 defined 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 : ∃ M. MobiusTable(N,M) - 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