DV000A

mobius_table_exists

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Ordinary induction constructs a genuine packed Möbius table for every finite bound, using independently proved positive-input μ totality at each step.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved.

Exact expanded first-order arithmetic statement

forall N. exists M. (((exists dst_positive_code_exists_resulttable dst_positive_scale_exists_resulttable dst_negative_code_exists_resulttable dst_negative_scale_exists_resulttable. (((M) = (((((dst_positive_code_exists_resulttable) + (dst_positive_scale_exists_resulttable)) * S ((dst_positive_code_exists_resulttable) + (dst_positive_scale_exists_resulttable)) + ((dst_positive_scale_exists_resulttable) + (dst_positive_scale_exists_resulttable))) + (((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) * S ((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) + ((dst_negative_scale_exists_resulttable) + (dst_negative_scale_exists_resulttable)))) * S ((((dst_positive_code_exists_resulttable) + (dst_positive_scale_exists_resulttable)) * S ((dst_positive_code_exists_resulttable) + (dst_positive_scale_exists_resulttable)) + ((dst_positive_scale_exists_resulttable) + (dst_positive_scale_exists_resulttable))) + (((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) * S ((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) + ((dst_negative_scale_exists_resulttable) + (dst_negative_scale_exists_resulttable)))) + ((((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) * S ((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) + ((dst_negative_scale_exists_resulttable) + (dst_negative_scale_exists_resulttable))) + (((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) * S ((dst_negative_code_exists_resulttable) + (dst_negative_scale_exists_resulttable)) + ((dst_negative_scale_exists_resulttable) + (dst_negative_scale_exists_resulttable)))))) /\ (forall dst_index_exists_resulttable. (exists pvs_le_gap_exists_resulttabledomain. pvs_le_gap_exists_resulttabledomain + (dst_index_exists_resulttable) = (N)) -> exists dst_positive_exists_resulttable dst_negative_exists_resulttable dst_value_exists_resulttable. ((((exists ff_h_pvs_exists_resulttableentrypositive. ff_h_pvs_exists_resulttableentrypositive + S (dst_positive_exists_resulttable) = S ((S (dst_index_exists_resulttable)) * dst_positive_scale_exists_resulttable)) /\ exists ff_q_pvs_exists_resulttableentrypositive. dst_positive_code_exists_resulttable = ff_q_pvs_exists_resulttableentrypositive * S ((S (dst_index_exists_resulttable)) * dst_positive_scale_exists_resulttable) + (dst_positive_exists_resulttable))) /\ (((((exists ff_h_pvs_exists_resulttableentrynegative. ff_h_pvs_exists_resulttableentrynegative + S (dst_negative_exists_resulttable) = S ((S (dst_index_exists_resulttable)) * dst_negative_scale_exists_resulttable)) /\ exists ff_q_pvs_exists_resulttableentrynegative. dst_negative_code_exists_resulttable = ff_q_pvs_exists_resulttableentrynegative * S ((S (dst_index_exists_resulttable)) * dst_negative_scale_exists_resulttable) + (dst_negative_exists_resulttable))) /\ (exists ge_balance_positive_exists_resulttableentryvalue ge_balance_negative_exists_resulttableentryvalue. (((((dst_value_exists_resulttable) = 2 * (ge_balance_positive_exists_resulttableentryvalue) /\ (ge_balance_negative_exists_resulttableentryvalue) = 0) \/ exists ge_signed_half_exists_resulttableentryvaluedecode. (((dst_value_exists_resulttable) = 2 * ge_signed_half_exists_resulttableentryvaluedecode + 1 /\ (ge_balance_positive_exists_resulttableentryvalue) = 0) /\ (ge_balance_negative_exists_resulttableentryvalue) = S ge_signed_half_exists_resulttableentryvaluedecode))) /\ ((dst_positive_exists_resulttable) + ge_balance_negative_exists_resulttableentryvalue = (dst_negative_exists_resulttable) + ge_balance_positive_exists_resulttableentryvalue))))))))) /\ (((exists dst_positive_code_exists_resultzero dst_positive_scale_exists_resultzero dst_negative_code_exists_resultzero dst_negative_scale_exists_resultzero dst_positive_exists_resultzero dst_negative_exists_resultzero. (((M) = (((((dst_positive_code_exists_resultzero) + (dst_positive_scale_exists_resultzero)) * S ((dst_positive_code_exists_resultzero) + (dst_positive_scale_exists_resultzero)) + ((dst_positive_scale_exists_resultzero) + (dst_positive_scale_exists_resultzero))) + (((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) * S ((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) + ((dst_negative_scale_exists_resultzero) + (dst_negative_scale_exists_resultzero)))) * S ((((dst_positive_code_exists_resultzero) + (dst_positive_scale_exists_resultzero)) * S ((dst_positive_code_exists_resultzero) + (dst_positive_scale_exists_resultzero)) + ((dst_positive_scale_exists_resultzero) + (dst_positive_scale_exists_resultzero))) + (((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) * S ((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) + ((dst_negative_scale_exists_resultzero) + (dst_negative_scale_exists_resultzero)))) + ((((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) * S ((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) + ((dst_negative_scale_exists_resultzero) + (dst_negative_scale_exists_resultzero))) + (((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) * S ((dst_negative_code_exists_resultzero) + (dst_negative_scale_exists_resultzero)) + ((dst_negative_scale_exists_resultzero) + (dst_negative_scale_exists_resultzero)))))) /\ (((((exists ff_h_pvs_exists_resultzeropositive. ff_h_pvs_exists_resultzeropositive + S (dst_positive_exists_resultzero) = S ((S (0)) * dst_positive_scale_exists_resultzero)) /\ exists ff_q_pvs_exists_resultzeropositive. dst_positive_code_exists_resultzero = ff_q_pvs_exists_resultzeropositive * S ((S (0)) * dst_positive_scale_exists_resultzero) + (dst_positive_exists_resultzero))) /\ (((((exists ff_h_pvs_exists_resultzeronegative. ff_h_pvs_exists_resultzeronegative + S (dst_negative_exists_resultzero) = S ((S (0)) * dst_negative_scale_exists_resultzero)) /\ exists ff_q_pvs_exists_resultzeronegative. dst_negative_code_exists_resultzero = ff_q_pvs_exists_resultzeronegative * S ((S (0)) * dst_negative_scale_exists_resultzero) + (dst_negative_exists_resultzero))) /\ (exists ge_balance_positive_exists_resultzerovalue ge_balance_negative_exists_resultzerovalue. (((((0) = 2 * (ge_balance_positive_exists_resultzerovalue) /\ (ge_balance_negative_exists_resultzerovalue) = 0) \/ exists ge_signed_half_exists_resultzerovaluedecode. (((0) = 2 * ge_signed_half_exists_resultzerovaluedecode + 1 /\ (ge_balance_positive_exists_resultzerovalue) = 0) /\ (ge_balance_negative_exists_resultzerovalue) = S ge_signed_half_exists_resultzerovaluedecode))) /\ ((dst_positive_exists_resultzero) + ge_balance_negative_exists_resultzerovalue = (dst_negative_exists_resultzero) + ge_balance_positive_exists_resultzerovalue))))))))) /\ (forall mt_index_exists_result mt_value_exists_result. ~(mt_index_exists_result=0) -> (exists pvs_le_gap_exists_resultdomain. pvs_le_gap_exists_resultdomain + (mt_index_exists_result) = (N)) -> (exists dst_positive_code_exists_resultentry dst_positive_scale_exists_resultentry dst_negative_code_exists_resultentry dst_negative_scale_exists_resultentry dst_positive_exists_resultentry dst_negative_exists_resultentry. (((M) = (((((dst_positive_code_exists_resultentry) + (dst_positive_scale_exists_resultentry)) * S ((dst_positive_code_exists_resultentry) + (dst_positive_scale_exists_resultentry)) + ((dst_positive_scale_exists_resultentry) + (dst_positive_scale_exists_resultentry))) + (((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) * S ((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) + ((dst_negative_scale_exists_resultentry) + (dst_negative_scale_exists_resultentry)))) * S ((((dst_positive_code_exists_resultentry) + (dst_positive_scale_exists_resultentry)) * S ((dst_positive_code_exists_resultentry) + (dst_positive_scale_exists_resultentry)) + ((dst_positive_scale_exists_resultentry) + (dst_positive_scale_exists_resultentry))) + (((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) * S ((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) + ((dst_negative_scale_exists_resultentry) + (dst_negative_scale_exists_resultentry)))) + ((((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) * S ((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) + ((dst_negative_scale_exists_resultentry) + (dst_negative_scale_exists_resultentry))) + (((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) * S ((dst_negative_code_exists_resultentry) + (dst_negative_scale_exists_resultentry)) + ((dst_negative_scale_exists_resultentry) + (dst_negative_scale_exists_resultentry)))))) /\ (((((exists ff_h_pvs_exists_resultentrypositive. ff_h_pvs_exists_resultentrypositive + S (dst_positive_exists_resultentry) = S ((S (mt_index_exists_result)) * dst_positive_scale_exists_resultentry)) /\ exists ff_q_pvs_exists_resultentrypositive. dst_positive_code_exists_resultentry = ff_q_pvs_exists_resultentrypositive * S ((S (mt_index_exists_result)) * dst_positive_scale_exists_resultentry) + (dst_positive_exists_resultentry))) /\ (((((exists ff_h_pvs_exists_resultentrynegative. ff_h_pvs_exists_resultentrynegative + S (dst_negative_exists_resultentry) = S ((S (mt_index_exists_result)) * dst_negative_scale_exists_resultentry)) /\ exists ff_q_pvs_exists_resultentrynegative. dst_negative_code_exists_resultentry = ff_q_pvs_exists_resultentrynegative * S ((S (mt_index_exists_result)) * dst_negative_scale_exists_resultentry) + (dst_negative_exists_resultentry))) /\ (exists ge_balance_positive_exists_resultentryvalue ge_balance_negative_exists_resultentryvalue. (((((mt_value_exists_result) = 2 * (ge_balance_positive_exists_resultentryvalue) /\ (ge_balance_negative_exists_resultentryvalue) = 0) \/ exists ge_signed_half_exists_resultentryvaluedecode. (((mt_value_exists_result) = 2 * ge_signed_half_exists_resultentryvaluedecode + 1 /\ (ge_balance_positive_exists_resultentryvalue) = 0) /\ (ge_balance_negative_exists_resultentryvalue) = S ge_signed_half_exists_resultentryvaluedecode))) /\ ((dst_positive_exists_resultentry) + ge_balance_negative_exists_resultentryvalue = (dst_negative_exists_resultentry) + ge_balance_positive_exists_resultentryvalue))))))))) -> (((~((mt_index_exists_result) = 0)) /\ ((((exists mv_square_prime_exists_resultvaluesquare. ((~((mv_square_prime_exists_resultvaluesquare) = 1) /\ forall pvs_left_exists_resultvaluesquareprime pvs_right_exists_resultvaluesquareprime. (mv_square_prime_exists_resultvaluesquare) = pvs_left_exists_resultvaluesquareprime * pvs_right_exists_resultvaluesquareprime -> pvs_left_exists_resultvaluesquareprime = 1 \/ pvs_right_exists_resultvaluesquareprime = 1) /\ (exists pvs_factor_exists_resultvaluesquaredivisor. (mt_index_exists_result) = (mv_square_prime_exists_resultvaluesquare * mv_square_prime_exists_resultvaluesquare) * pvs_factor_exists_resultvaluesquaredivisor))) /\ ((mt_value_exists_result) = 0))) \/ (((((~((mt_index_exists_result) = 0)) /\ (forall sfd_prime_exists_resultvaluesquarefree. (~((sfd_prime_exists_resultvaluesquarefree) = 1) /\ forall pvs_left_exists_resultvaluesquarefreedomain pvs_right_exists_resultvaluesquarefreedomain. (sfd_prime_exists_resultvaluesquarefree) = pvs_left_exists_resultvaluesquarefreedomain * pvs_right_exists_resultvaluesquarefreedomain -> pvs_left_exists_resultvaluesquarefreedomain = 1 \/ pvs_right_exists_resultvaluesquarefreedomain = 1) -> (exists pvs_le_gap_exists_resultvaluesquarefreebound. pvs_le_gap_exists_resultvaluesquarefreebound + (sfd_prime_exists_resultvaluesquarefree) = (mt_index_exists_result)) -> ~(exists pvs_factor_exists_resultvaluesquarefreesquare. (mt_index_exists_result) = (sfd_prime_exists_resultvaluesquarefree * sfd_prime_exists_resultvaluesquarefree) * pvs_factor_exists_resultvaluesquarefreesquare)))) /\ (exists mv_factor_code_exists_resultvaluefactors mv_factor_scale_exists_resultvaluefactors mv_factor_count_exists_resultvaluefactors. (((~(mt_index_exists_result = 0) /\ ((exists ff_u_fsat_exists_resultvaluefactorsfactorization_product ff_v_fsat_exists_resultvaluefactorsfactorization_product. ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_start. ff_h_fsat_exists_resultvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_start. ff_u_fsat_exists_resultvaluefactorsfactorization_product = ff_q_fsat_exists_resultvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_terminal. ff_h_fsat_exists_resultvaluefactorsfactorization_product_terminal + S (mt_index_exists_result) = S ((S (mv_factor_count_exists_resultvaluefactors)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_terminal. ff_u_fsat_exists_resultvaluefactorsfactorization_product = ff_q_fsat_exists_resultvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_exists_resultvaluefactors)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product) + (mt_index_exists_result))) /\ forall ff_i_fsat_exists_resultvaluefactorsfactorization_product. (exists ff_lt_fsat_exists_resultvaluefactorsfactorization_product_bound. ff_lt_fsat_exists_resultvaluefactorsfactorization_product_bound + S ff_i_fsat_exists_resultvaluefactorsfactorization_product = mv_factor_count_exists_resultvaluefactors) -> exists ff_p_fsat_exists_resultvaluefactorsfactorization_product ff_r_fsat_exists_resultvaluefactorsfactorization_product ff_s_fsat_exists_resultvaluefactorsfactorization_product. ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_factor. ff_h_fsat_exists_resultvaluefactorsfactorization_product_factor + S (ff_p_fsat_exists_resultvaluefactorsfactorization_product) = S ((S (ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * mv_factor_scale_exists_resultvaluefactors)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_factor. mv_factor_code_exists_resultvaluefactors = ff_q_fsat_exists_resultvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * mv_factor_scale_exists_resultvaluefactors) + (ff_p_fsat_exists_resultvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_partial. ff_h_fsat_exists_resultvaluefactorsfactorization_product_partial + S (ff_r_fsat_exists_resultvaluefactorsfactorization_product) = S ((S (ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_partial. ff_u_fsat_exists_resultvaluefactorsfactorization_product = ff_q_fsat_exists_resultvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product) + (ff_r_fsat_exists_resultvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_resultvaluefactorsfactorization_product_successor. ff_h_fsat_exists_resultvaluefactorsfactorization_product_successor + S (ff_s_fsat_exists_resultvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_resultvaluefactorsfactorization_product_successor. ff_u_fsat_exists_resultvaluefactorsfactorization_product = ff_q_fsat_exists_resultvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_exists_resultvaluefactorsfactorization_product)) * ff_v_fsat_exists_resultvaluefactorsfactorization_product) + (ff_s_fsat_exists_resultvaluefactorsfactorization_product))) /\ ff_s_fsat_exists_resultvaluefactorsfactorization_product = ff_r_fsat_exists_resultvaluefactorsfactorization_product * ff_p_fsat_exists_resultvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_exists_resultvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_exists_resultvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_exists_resultvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_exists_resultvaluefactorsfactorization_primes = (mv_factor_count_exists_resultvaluefactors)) -> exists ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_exists_resultvaluefactorsfactorization_primes)) * mv_factor_scale_exists_resultvaluefactors)) /\ exists ff_q_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_entry. mv_factor_code_exists_resultvaluefactors = ff_q_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_exists_resultvaluefactorsfactorization_primes)) * mv_factor_scale_exists_resultvaluefactors) + (ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_exists_resultvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_exists_resultvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_exists_resultvaluefactorsparityeven. (mv_factor_count_exists_resultvaluefactors) = 2 * mv_even_half_exists_resultvaluefactorsparityeven) /\ ((mt_value_exists_result) = 2))) \/ (((exists mv_odd_half_exists_resultvaluefactorsparityodd. (mv_factor_count_exists_resultvaluefactors) = 2 * mv_odd_half_exists_resultvaluefactorsparityodd + 1) /\ ((mt_value_exists_result) = 1))))))))))))))))

Constructive proof overview

Generated structural guide

Ordinary induction constructs a genuine packed Möbius table for every finite bound, using independently proved positive-input μ totality at each step.

The unchanged tactic script uses 4 declared prerequisites and contains 31 exact native proof lines.

Alpha v34 checked-use · first admitted v31 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

DV0005 arithmetic_signed_table_singleton DV0008 mobius_table_zero_constructor mobius_value_exists Alpha theorem; checked-use authorized DV0009 mobius_table_append

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

31 script commands · 13 reading checkpoints · 3 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.

Named ingredients (3)
arithmetic signed table singletonmobius table zero constructormobius table append

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–1

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro N
02Induction on NL2–2

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L2
    induction N
03Establish hbaseL3–5

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply arithmetic signed table singleton.

  1. L3
    have hbase : ∃ F. ArithTable(0,F) ∧ ArithAt(F,0,0)Definitions: ArithTableArithAt
  2. L4
    specialize arithmetic_signed_table_singleton (0)
  3. L5
    apply arithmetic_signed_table_singleton
04Separate the logical casesL6–7

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L6
    cases hbase
  2. L7
    cases hbase_witness
05Construct an explicit witnessL8–8

Supply the displayed value, then prove that it has the required property.

  1. L8
    exists x
06Use earlier factsL9–12

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L9
    specialize mobius_table_zero_constructor (x)
  2. L10
    apply mobius_table_zero_constructor
  3. L11
    exact hbase_witness_left
  4. L12
    exact hbase_witness_right
07Separate the logical casesL13–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L13
    cases IH
08Establish hzL14–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mobius value exists.

  1. L14
    have hz : ∃ z. Mobius(S N,z)Definitions: Mobius
  2. L15
    specialize mobius_value_exists (S N)
  3. L16
    apply mobius_value_exists
  4. L17
    intro hzero
  5. L18
    apply PA1
  6. L19
    exact hzero
09Separate the logical casesL20–20

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L20
    cases hz
10Establish hnextL21–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mobius table append.

  1. L21
    have hnext : ∃ G. MobiusTable(S N,G) ∧ ArithTableEqual(x,G,S N)Definitions: ArithTableEqualMobiusTable
  2. L22
    specialize mobius_table_append (N)
  3. L23
    specialize mobius_table_append (x)
  4. L24
    specialize mobius_table_append (x1)
  5. L25
    apply mobius_table_append
  6. L26
    exact IH_witness
  7. L27
    exact hz_witness
11Separate the logical casesL28–29

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L28
    cases hnext
  2. L29
    cases hnext_witness
12Construct an explicit witnessL30–30

Supply the displayed value, then prove that it has the required property.

  1. L30
    exists x2
13Use earlier factsL31–31

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L31
    exact hnext_witness_left

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro N
  2. 0002induction N
  3. 0003have hbase : exists F. (exists dst_positive_code_exists_base_table dst_positive_scale_exists_base_table dst_negative_code_exists_base_table dst_negative_scale_exists_base_table. (((F) = (((((dst_positive_code_exists_base_table) + (dst_positive_scale_exists_base_table)) * S ((dst_positive_code_exists_base_table) + (dst_positive_scale_exists_base_table)) + ((dst_positive_scale_exists_base_table) + (dst_positive_scale_exists_base_table))) + (((dst_negative_code_exists_base_table) + (dst_negative_scale_exists_base_table)) * S ((dst_negative_code_exists_base_table) + (dst_negative_scale_exists_base_table)) + ((dst_negative_scale_exists_base_table) + (dst_negative_scale_exists_base_table)))) * S ((((dst_positive_code_exists_base_table) + (dst_positive_scale_exists_base_table)) * S ((dst_positive_code_exists_base_table) + (dst_positive_scale_exists_base_table)) + ((dst_positive_scale_exists_base_table) + (dst_positive_scale_exists_base_table))) + (((dst_negative_code_exists_base_table) + (dst_negative_scale_exists_base_table)) * S ((dst_negative_code_exists_base_table) + (dst_negative_scale_exists_base_table)) + ((dst_negative_scale_exists_base_table) + (dst_negative_scale_exists_base_table)))) + ((((dst_negative_code_exists_base_table) + (dst_negative_scale_exists_base_table)) * S ((dst_negative_code_exists_base_table) + (dst_negative_scale_exists_base_table)) + ((dst_negative_scale_exists_base_table) + (dst_negative_scale_exists_base_table))) + (((dst_negative_code_exists_base_table) + (dst_negative_scale_exists_base_table)) * S ((dst_negative_code_exists_base_table) + (dst_negative_scale_exists_base_table)) + ((dst_negative_scale_exists_base_table) + (dst_negative_scale_exists_base_table)))))) /\ (forall dst_index_exists_base_table. (exists pvs_le_gap_exists_base_tabledomain. pvs_le_gap_exists_base_tabledomain + (dst_index_exists_base_table) = (0)) -> exists dst_positive_exists_base_table dst_negative_exists_base_table dst_value_exists_base_table. ((((exists ff_h_pvs_exists_base_tableentrypositive. ff_h_pvs_exists_base_tableentrypositive + S (dst_positive_exists_base_table) = S ((S (dst_index_exists_base_table)) * dst_positive_scale_exists_base_table)) /\ exists ff_q_pvs_exists_base_tableentrypositive. dst_positive_code_exists_base_table = ff_q_pvs_exists_base_tableentrypositive * S ((S (dst_index_exists_base_table)) * dst_positive_scale_exists_base_table) + (dst_positive_exists_base_table))) /\ (((((exists ff_h_pvs_exists_base_tableentrynegative. ff_h_pvs_exists_base_tableentrynegative + S (dst_negative_exists_base_table) = S ((S (dst_index_exists_base_table)) * dst_negative_scale_exists_base_table)) /\ exists ff_q_pvs_exists_base_tableentrynegative. dst_negative_code_exists_base_table = ff_q_pvs_exists_base_tableentrynegative * S ((S (dst_index_exists_base_table)) * dst_negative_scale_exists_base_table) + (dst_negative_exists_base_table))) /\ (exists ge_balance_positive_exists_base_tableentryvalue ge_balance_negative_exists_base_tableentryvalue. (((((dst_value_exists_base_table) = 2 * (ge_balance_positive_exists_base_tableentryvalue) /\ (ge_balance_negative_exists_base_tableentryvalue) = 0) \/ exists ge_signed_half_exists_base_tableentryvaluedecode. (((dst_value_exists_base_table) = 2 * ge_signed_half_exists_base_tableentryvaluedecode + 1 /\ (ge_balance_positive_exists_base_tableentryvalue) = 0) /\ (ge_balance_negative_exists_base_tableentryvalue) = S ge_signed_half_exists_base_tableentryvaluedecode))) /\ ((dst_positive_exists_base_table) + ge_balance_negative_exists_base_tableentryvalue = (dst_negative_exists_base_table) + ge_balance_positive_exists_base_tableentryvalue))))))))) /\ (exists dst_positive_code_exists_base_zero dst_positive_scale_exists_base_zero dst_negative_code_exists_base_zero dst_negative_scale_exists_base_zero dst_positive_exists_base_zero dst_negative_exists_base_zero. (((F) = (((((dst_positive_code_exists_base_zero) + (dst_positive_scale_exists_base_zero)) * S ((dst_positive_code_exists_base_zero) + (dst_positive_scale_exists_base_zero)) + ((dst_positive_scale_exists_base_zero) + (dst_positive_scale_exists_base_zero))) + (((dst_negative_code_exists_base_zero) + (dst_negative_scale_exists_base_zero)) * S ((dst_negative_code_exists_base_zero) + (dst_negative_scale_exists_base_zero)) + ((dst_negative_scale_exists_base_zero) + (dst_negative_scale_exists_base_zero)))) * S ((((dst_positive_code_exists_base_zero) + (dst_positive_scale_exists_base_zero)) * S ((dst_positive_code_exists_base_zero) + (dst_positive_scale_exists_base_zero)) + ((dst_positive_scale_exists_base_zero) + (dst_positive_scale_exists_base_zero))) + (((dst_negative_code_exists_base_zero) + (dst_negative_scale_exists_base_zero)) * S ((dst_negative_code_exists_base_zero) + (dst_negative_scale_exists_base_zero)) + ((dst_negative_scale_exists_base_zero) + (dst_negative_scale_exists_base_zero)))) + ((((dst_negative_code_exists_base_zero) + (dst_negative_scale_exists_base_zero)) * S ((dst_negative_code_exists_base_zero) + (dst_negative_scale_exists_base_zero)) + ((dst_negative_scale_exists_base_zero) + (dst_negative_scale_exists_base_zero))) + (((dst_negative_code_exists_base_zero) + (dst_negative_scale_exists_base_zero)) * S ((dst_negative_code_exists_base_zero) + (dst_negative_scale_exists_base_zero)) + ((dst_negative_scale_exists_base_zero) + (dst_negative_scale_exists_base_zero)))))) /\ (((((exists ff_h_pvs_exists_base_zeropositive. ff_h_pvs_exists_base_zeropositive + S (dst_positive_exists_base_zero) = S ((S (0)) * dst_positive_scale_exists_base_zero)) /\ exists ff_q_pvs_exists_base_zeropositive. dst_positive_code_exists_base_zero = ff_q_pvs_exists_base_zeropositive * S ((S (0)) * dst_positive_scale_exists_base_zero) + (dst_positive_exists_base_zero))) /\ (((((exists ff_h_pvs_exists_base_zeronegative. ff_h_pvs_exists_base_zeronegative + S (dst_negative_exists_base_zero) = S ((S (0)) * dst_negative_scale_exists_base_zero)) /\ exists ff_q_pvs_exists_base_zeronegative. dst_negative_code_exists_base_zero = ff_q_pvs_exists_base_zeronegative * S ((S (0)) * dst_negative_scale_exists_base_zero) + (dst_negative_exists_base_zero))) /\ (exists ge_balance_positive_exists_base_zerovalue ge_balance_negative_exists_base_zerovalue. (((((0) = 2 * (ge_balance_positive_exists_base_zerovalue) /\ (ge_balance_negative_exists_base_zerovalue) = 0) \/ exists ge_signed_half_exists_base_zerovaluedecode. (((0) = 2 * ge_signed_half_exists_base_zerovaluedecode + 1 /\ (ge_balance_positive_exists_base_zerovalue) = 0) /\ (ge_balance_negative_exists_base_zerovalue) = S ge_signed_half_exists_base_zerovaluedecode))) /\ ((dst_positive_exists_base_zero) + ge_balance_negative_exists_base_zerovalue = (dst_negative_exists_base_zero) + ge_balance_positive_exists_base_zerovalue)))))))))
  4. 0004specialize arithmetic_signed_table_singleton (0)
  5. 0005apply arithmetic_signed_table_singleton
  6. 0006cases hbase
  7. 0007cases hbase_witness
  8. 0008exists x
  9. 0009specialize mobius_table_zero_constructor (x)
  10. 0010apply mobius_table_zero_constructor
  11. 0011exact hbase_witness_left
  12. 0012exact hbase_witness_right
  13. 0013cases IH
  14. 0014have hz : exists z. (((~((S N) = 0)) /\ ((((exists mv_square_prime_exists_step_valuesquare. ((~((mv_square_prime_exists_step_valuesquare) = 1) /\ forall pvs_left_exists_step_valuesquareprime pvs_right_exists_step_valuesquareprime. (mv_square_prime_exists_step_valuesquare) = pvs_left_exists_step_valuesquareprime * pvs_right_exists_step_valuesquareprime -> pvs_left_exists_step_valuesquareprime = 1 \/ pvs_right_exists_step_valuesquareprime = 1) /\ (exists pvs_factor_exists_step_valuesquaredivisor. (S N) = (mv_square_prime_exists_step_valuesquare * mv_square_prime_exists_step_valuesquare) * pvs_factor_exists_step_valuesquaredivisor))) /\ ((z) = 0))) \/ (((((~((S N) = 0)) /\ (forall sfd_prime_exists_step_valuesquarefree. (~((sfd_prime_exists_step_valuesquarefree) = 1) /\ forall pvs_left_exists_step_valuesquarefreedomain pvs_right_exists_step_valuesquarefreedomain. (sfd_prime_exists_step_valuesquarefree) = pvs_left_exists_step_valuesquarefreedomain * pvs_right_exists_step_valuesquarefreedomain -> pvs_left_exists_step_valuesquarefreedomain = 1 \/ pvs_right_exists_step_valuesquarefreedomain = 1) -> (exists pvs_le_gap_exists_step_valuesquarefreebound. pvs_le_gap_exists_step_valuesquarefreebound + (sfd_prime_exists_step_valuesquarefree) = (S N)) -> ~(exists pvs_factor_exists_step_valuesquarefreesquare. (S N) = (sfd_prime_exists_step_valuesquarefree * sfd_prime_exists_step_valuesquarefree) * pvs_factor_exists_step_valuesquarefreesquare)))) /\ (exists mv_factor_code_exists_step_valuefactors mv_factor_scale_exists_step_valuefactors mv_factor_count_exists_step_valuefactors. (((~(S N = 0) /\ ((exists ff_u_fsat_exists_step_valuefactorsfactorization_product ff_v_fsat_exists_step_valuefactorsfactorization_product. ((((exists ff_h_fsat_exists_step_valuefactorsfactorization_product_start. ff_h_fsat_exists_step_valuefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_exists_step_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_step_valuefactorsfactorization_product_start. ff_u_fsat_exists_step_valuefactorsfactorization_product = ff_q_fsat_exists_step_valuefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_exists_step_valuefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_exists_step_valuefactorsfactorization_product_terminal. ff_h_fsat_exists_step_valuefactorsfactorization_product_terminal + S (S N) = S ((S (mv_factor_count_exists_step_valuefactors)) * ff_v_fsat_exists_step_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_step_valuefactorsfactorization_product_terminal. ff_u_fsat_exists_step_valuefactorsfactorization_product = ff_q_fsat_exists_step_valuefactorsfactorization_product_terminal * S ((S (mv_factor_count_exists_step_valuefactors)) * ff_v_fsat_exists_step_valuefactorsfactorization_product) + (S N))) /\ forall ff_i_fsat_exists_step_valuefactorsfactorization_product. (exists ff_lt_fsat_exists_step_valuefactorsfactorization_product_bound. ff_lt_fsat_exists_step_valuefactorsfactorization_product_bound + S ff_i_fsat_exists_step_valuefactorsfactorization_product = mv_factor_count_exists_step_valuefactors) -> exists ff_p_fsat_exists_step_valuefactorsfactorization_product ff_r_fsat_exists_step_valuefactorsfactorization_product ff_s_fsat_exists_step_valuefactorsfactorization_product. ((((exists ff_h_fsat_exists_step_valuefactorsfactorization_product_factor. ff_h_fsat_exists_step_valuefactorsfactorization_product_factor + S (ff_p_fsat_exists_step_valuefactorsfactorization_product) = S ((S (ff_i_fsat_exists_step_valuefactorsfactorization_product)) * mv_factor_scale_exists_step_valuefactors)) /\ exists ff_q_fsat_exists_step_valuefactorsfactorization_product_factor. mv_factor_code_exists_step_valuefactors = ff_q_fsat_exists_step_valuefactorsfactorization_product_factor * S ((S (ff_i_fsat_exists_step_valuefactorsfactorization_product)) * mv_factor_scale_exists_step_valuefactors) + (ff_p_fsat_exists_step_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_step_valuefactorsfactorization_product_partial. ff_h_fsat_exists_step_valuefactorsfactorization_product_partial + S (ff_r_fsat_exists_step_valuefactorsfactorization_product) = S ((S (ff_i_fsat_exists_step_valuefactorsfactorization_product)) * ff_v_fsat_exists_step_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_step_valuefactorsfactorization_product_partial. ff_u_fsat_exists_step_valuefactorsfactorization_product = ff_q_fsat_exists_step_valuefactorsfactorization_product_partial * S ((S (ff_i_fsat_exists_step_valuefactorsfactorization_product)) * ff_v_fsat_exists_step_valuefactorsfactorization_product) + (ff_r_fsat_exists_step_valuefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_step_valuefactorsfactorization_product_successor. ff_h_fsat_exists_step_valuefactorsfactorization_product_successor + S (ff_s_fsat_exists_step_valuefactorsfactorization_product) = S ((S (S ff_i_fsat_exists_step_valuefactorsfactorization_product)) * ff_v_fsat_exists_step_valuefactorsfactorization_product)) /\ exists ff_q_fsat_exists_step_valuefactorsfactorization_product_successor. ff_u_fsat_exists_step_valuefactorsfactorization_product = ff_q_fsat_exists_step_valuefactorsfactorization_product_successor * S ((S (S ff_i_fsat_exists_step_valuefactorsfactorization_product)) * ff_v_fsat_exists_step_valuefactorsfactorization_product) + (ff_s_fsat_exists_step_valuefactorsfactorization_product))) /\ ff_s_fsat_exists_step_valuefactorsfactorization_product = ff_r_fsat_exists_step_valuefactorsfactorization_product * ff_p_fsat_exists_step_valuefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_exists_step_valuefactorsfactorization_primes. (exists ftsf_gap_fsat_exists_step_valuefactorsfactorization_primes_bound. ftsf_gap_fsat_exists_step_valuefactorsfactorization_primes_bound + S ftsf_index_fsat_exists_step_valuefactorsfactorization_primes = (mv_factor_count_exists_step_valuefactors)) -> exists ftsf_factor_fsat_exists_step_valuefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_exists_step_valuefactorsfactorization_primes_entry. ff_h_ftsf_fsat_exists_step_valuefactorsfactorization_primes_entry + S (ftsf_factor_fsat_exists_step_valuefactorsfactorization_primes) = S ((S (ftsf_index_fsat_exists_step_valuefactorsfactorization_primes)) * mv_factor_scale_exists_step_valuefactors)) /\ exists ff_q_ftsf_fsat_exists_step_valuefactorsfactorization_primes_entry. mv_factor_code_exists_step_valuefactors = ff_q_ftsf_fsat_exists_step_valuefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_exists_step_valuefactorsfactorization_primes)) * mv_factor_scale_exists_step_valuefactors) + (ftsf_factor_fsat_exists_step_valuefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_exists_step_valuefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_exists_step_valuefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_exists_step_valuefactorsfactorization_primes_prime. ftsf_factor_fsat_exists_step_valuefactorsfactorization_primes = frm_prime_left_ftsf_fsat_exists_step_valuefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_exists_step_valuefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_exists_step_valuefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_exists_step_valuefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_exists_step_valuefactorsparityeven. (mv_factor_count_exists_step_valuefactors) = 2 * mv_even_half_exists_step_valuefactorsparityeven) /\ ((z) = 2))) \/ (((exists mv_odd_half_exists_step_valuefactorsparityodd. (mv_factor_count_exists_step_valuefactors) = 2 * mv_odd_half_exists_step_valuefactorsparityodd + 1) /\ ((z) = 1)))))))))))
  15. 0015specialize mobius_value_exists (S N)
  16. 0016apply mobius_value_exists
  17. 0017intro hzero
  18. 0018apply PA1
  19. 0019exact hzero
  20. 0020cases hz
  21. 0021have hnext : exists G. (((exists dst_positive_code_exists_nexttable dst_positive_scale_exists_nexttable dst_negative_code_exists_nexttable dst_negative_scale_exists_nexttable. (((G) = (((((dst_positive_code_exists_nexttable) + (dst_positive_scale_exists_nexttable)) * S ((dst_positive_code_exists_nexttable) + (dst_positive_scale_exists_nexttable)) + ((dst_positive_scale_exists_nexttable) + (dst_positive_scale_exists_nexttable))) + (((dst_negative_code_exists_nexttable) + (dst_negative_scale_exists_nexttable)) * S ((dst_negative_code_exists_nexttable) + (dst_negative_scale_exists_nexttable)) + ((dst_negative_scale_exists_nexttable) + (dst_negative_scale_exists_nexttable)))) * S ((((dst_positive_code_exists_nexttable) + (dst_positive_scale_exists_nexttable)) * S ((dst_positive_code_exists_nexttable) + (dst_positive_scale_exists_nexttable)) + ((dst_positive_scale_exists_nexttable) + (dst_positive_scale_exists_nexttable))) + (((dst_negative_code_exists_nexttable) + (dst_negative_scale_exists_nexttable)) * S ((dst_negative_code_exists_nexttable) + (dst_negative_scale_exists_nexttable)) + ((dst_negative_scale_exists_nexttable) + (dst_negative_scale_exists_nexttable)))) + ((((dst_negative_code_exists_nexttable) + (dst_negative_scale_exists_nexttable)) * S ((dst_negative_code_exists_nexttable) + (dst_negative_scale_exists_nexttable)) + ((dst_negative_scale_exists_nexttable) + (dst_negative_scale_exists_nexttable))) + (((dst_negative_code_exists_nexttable) + (dst_negative_scale_exists_nexttable)) * S ((dst_negative_code_exists_nexttable) + (dst_negative_scale_exists_nexttable)) + ((dst_negative_scale_exists_nexttable) + (dst_negative_scale_exists_nexttable)))))) /\ (forall dst_index_exists_nexttable. (exists pvs_le_gap_exists_nexttabledomain. pvs_le_gap_exists_nexttabledomain + (dst_index_exists_nexttable) = (S N)) -> exists dst_positive_exists_nexttable dst_negative_exists_nexttable dst_value_exists_nexttable. ((((exists ff_h_pvs_exists_nexttableentrypositive. ff_h_pvs_exists_nexttableentrypositive + S (dst_positive_exists_nexttable) = S ((S (dst_index_exists_nexttable)) * dst_positive_scale_exists_nexttable)) /\ exists ff_q_pvs_exists_nexttableentrypositive. dst_positive_code_exists_nexttable = ff_q_pvs_exists_nexttableentrypositive * S ((S (dst_index_exists_nexttable)) * dst_positive_scale_exists_nexttable) + (dst_positive_exists_nexttable))) /\ (((((exists ff_h_pvs_exists_nexttableentrynegative. ff_h_pvs_exists_nexttableentrynegative + S (dst_negative_exists_nexttable) = S ((S (dst_index_exists_nexttable)) * dst_negative_scale_exists_nexttable)) /\ exists ff_q_pvs_exists_nexttableentrynegative. dst_negative_code_exists_nexttable = ff_q_pvs_exists_nexttableentrynegative * S ((S (dst_index_exists_nexttable)) * dst_negative_scale_exists_nexttable) + (dst_negative_exists_nexttable))) /\ (exists ge_balance_positive_exists_nexttableentryvalue ge_balance_negative_exists_nexttableentryvalue. (((((dst_value_exists_nexttable) = 2 * (ge_balance_positive_exists_nexttableentryvalue) /\ (ge_balance_negative_exists_nexttableentryvalue) = 0) \/ exists ge_signed_half_exists_nexttableentryvaluedecode. (((dst_value_exists_nexttable) = 2 * ge_signed_half_exists_nexttableentryvaluedecode + 1 /\ (ge_balance_positive_exists_nexttableentryvalue) = 0) /\ (ge_balance_negative_exists_nexttableentryvalue) = S ge_signed_half_exists_nexttableentryvaluedecode))) /\ ((dst_positive_exists_nexttable) + ge_balance_negative_exists_nexttableentryvalue = (dst_negative_exists_nexttable) + ge_balance_positive_exists_nexttableentryvalue))))))))) /\ (((exists dst_positive_code_exists_nextzero dst_positive_scale_exists_nextzero dst_negative_code_exists_nextzero dst_negative_scale_exists_nextzero dst_positive_exists_nextzero dst_negative_exists_nextzero. (((G) = (((((dst_positive_code_exists_nextzero) + (dst_positive_scale_exists_nextzero)) * S ((dst_positive_code_exists_nextzero) + (dst_positive_scale_exists_nextzero)) + ((dst_positive_scale_exists_nextzero) + (dst_positive_scale_exists_nextzero))) + (((dst_negative_code_exists_nextzero) + (dst_negative_scale_exists_nextzero)) * S ((dst_negative_code_exists_nextzero) + (dst_negative_scale_exists_nextzero)) + ((dst_negative_scale_exists_nextzero) + (dst_negative_scale_exists_nextzero)))) * S ((((dst_positive_code_exists_nextzero) + (dst_positive_scale_exists_nextzero)) * S ((dst_positive_code_exists_nextzero) + (dst_positive_scale_exists_nextzero)) + ((dst_positive_scale_exists_nextzero) + (dst_positive_scale_exists_nextzero))) + (((dst_negative_code_exists_nextzero) + (dst_negative_scale_exists_nextzero)) * S ((dst_negative_code_exists_nextzero) + (dst_negative_scale_exists_nextzero)) + ((dst_negative_scale_exists_nextzero) + (dst_negative_scale_exists_nextzero)))) + ((((dst_negative_code_exists_nextzero) + (dst_negative_scale_exists_nextzero)) * S ((dst_negative_code_exists_nextzero) + (dst_negative_scale_exists_nextzero)) + ((dst_negative_scale_exists_nextzero) + (dst_negative_scale_exists_nextzero))) + (((dst_negative_code_exists_nextzero) + (dst_negative_scale_exists_nextzero)) * S ((dst_negative_code_exists_nextzero) + (dst_negative_scale_exists_nextzero)) + ((dst_negative_scale_exists_nextzero) + (dst_negative_scale_exists_nextzero)))))) /\ (((((exists ff_h_pvs_exists_nextzeropositive. ff_h_pvs_exists_nextzeropositive + S (dst_positive_exists_nextzero) = S ((S (0)) * dst_positive_scale_exists_nextzero)) /\ exists ff_q_pvs_exists_nextzeropositive. dst_positive_code_exists_nextzero = ff_q_pvs_exists_nextzeropositive * S ((S (0)) * dst_positive_scale_exists_nextzero) + (dst_positive_exists_nextzero))) /\ (((((exists ff_h_pvs_exists_nextzeronegative. ff_h_pvs_exists_nextzeronegative + S (dst_negative_exists_nextzero) = S ((S (0)) * dst_negative_scale_exists_nextzero)) /\ exists ff_q_pvs_exists_nextzeronegative. dst_negative_code_exists_nextzero = ff_q_pvs_exists_nextzeronegative * S ((S (0)) * dst_negative_scale_exists_nextzero) + (dst_negative_exists_nextzero))) /\ (exists ge_balance_positive_exists_nextzerovalue ge_balance_negative_exists_nextzerovalue. (((((0) = 2 * (ge_balance_positive_exists_nextzerovalue) /\ (ge_balance_negative_exists_nextzerovalue) = 0) \/ exists ge_signed_half_exists_nextzerovaluedecode. (((0) = 2 * ge_signed_half_exists_nextzerovaluedecode + 1 /\ (ge_balance_positive_exists_nextzerovalue) = 0) /\ (ge_balance_negative_exists_nextzerovalue) = S ge_signed_half_exists_nextzerovaluedecode))) /\ ((dst_positive_exists_nextzero) + ge_balance_negative_exists_nextzerovalue = (dst_negative_exists_nextzero) + ge_balance_positive_exists_nextzerovalue))))))))) /\ (forall mt_index_exists_next mt_value_exists_next. ~(mt_index_exists_next=0) -> (exists pvs_le_gap_exists_nextdomain. pvs_le_gap_exists_nextdomain + (mt_index_exists_next) = (S N)) -> (exists dst_positive_code_exists_nextentry dst_positive_scale_exists_nextentry dst_negative_code_exists_nextentry dst_negative_scale_exists_nextentry dst_positive_exists_nextentry dst_negative_exists_nextentry. (((G) = (((((dst_positive_code_exists_nextentry) + (dst_positive_scale_exists_nextentry)) * S ((dst_positive_code_exists_nextentry) + (dst_positive_scale_exists_nextentry)) + ((dst_positive_scale_exists_nextentry) + (dst_positive_scale_exists_nextentry))) + (((dst_negative_code_exists_nextentry) + (dst_negative_scale_exists_nextentry)) * S ((dst_negative_code_exists_nextentry) + (dst_negative_scale_exists_nextentry)) + ((dst_negative_scale_exists_nextentry) + (dst_negative_scale_exists_nextentry)))) * S ((((dst_positive_code_exists_nextentry) + (dst_positive_scale_exists_nextentry)) * S ((dst_positive_code_exists_nextentry) + (dst_positive_scale_exists_nextentry)) + ((dst_positive_scale_exists_nextentry) + (dst_positive_scale_exists_nextentry))) + (((dst_negative_code_exists_nextentry) + (dst_negative_scale_exists_nextentry)) * S ((dst_negative_code_exists_nextentry) + (dst_negative_scale_exists_nextentry)) + ((dst_negative_scale_exists_nextentry) + (dst_negative_scale_exists_nextentry)))) + ((((dst_negative_code_exists_nextentry) + (dst_negative_scale_exists_nextentry)) * S ((dst_negative_code_exists_nextentry) + (dst_negative_scale_exists_nextentry)) + ((dst_negative_scale_exists_nextentry) + (dst_negative_scale_exists_nextentry))) + (((dst_negative_code_exists_nextentry) + (dst_negative_scale_exists_nextentry)) * S ((dst_negative_code_exists_nextentry) + (dst_negative_scale_exists_nextentry)) + ((dst_negative_scale_exists_nextentry) + (dst_negative_scale_exists_nextentry)))))) /\ (((((exists ff_h_pvs_exists_nextentrypositive. ff_h_pvs_exists_nextentrypositive + S (dst_positive_exists_nextentry) = S ((S (mt_index_exists_next)) * dst_positive_scale_exists_nextentry)) /\ exists ff_q_pvs_exists_nextentrypositive. dst_positive_code_exists_nextentry = ff_q_pvs_exists_nextentrypositive * S ((S (mt_index_exists_next)) * dst_positive_scale_exists_nextentry) + (dst_positive_exists_nextentry))) /\ (((((exists ff_h_pvs_exists_nextentrynegative. ff_h_pvs_exists_nextentrynegative + S (dst_negative_exists_nextentry) = S ((S (mt_index_exists_next)) * dst_negative_scale_exists_nextentry)) /\ exists ff_q_pvs_exists_nextentrynegative. dst_negative_code_exists_nextentry = ff_q_pvs_exists_nextentrynegative * S ((S (mt_index_exists_next)) * dst_negative_scale_exists_nextentry) + (dst_negative_exists_nextentry))) /\ (exists ge_balance_positive_exists_nextentryvalue ge_balance_negative_exists_nextentryvalue. (((((mt_value_exists_next) = 2 * (ge_balance_positive_exists_nextentryvalue) /\ (ge_balance_negative_exists_nextentryvalue) = 0) \/ exists ge_signed_half_exists_nextentryvaluedecode. (((mt_value_exists_next) = 2 * ge_signed_half_exists_nextentryvaluedecode + 1 /\ (ge_balance_positive_exists_nextentryvalue) = 0) /\ (ge_balance_negative_exists_nextentryvalue) = S ge_signed_half_exists_nextentryvaluedecode))) /\ ((dst_positive_exists_nextentry) + ge_balance_negative_exists_nextentryvalue = (dst_negative_exists_nextentry) + ge_balance_positive_exists_nextentryvalue))))))))) -> (((~((mt_index_exists_next) = 0)) /\ ((((exists mv_square_prime_exists_nextvaluesquare. ((~((mv_square_prime_exists_nextvaluesquare) = 1) /\ forall pvs_left_exists_nextvaluesquareprime pvs_right_exists_nextvaluesquareprime. (mv_square_prime_exists_nextvaluesquare) = pvs_left_exists_nextvaluesquareprime * pvs_right_exists_nextvaluesquareprime -> pvs_left_exists_nextvaluesquareprime = 1 \/ pvs_right_exists_nextvaluesquareprime = 1) /\ (exists pvs_factor_exists_nextvaluesquaredivisor. (mt_index_exists_next) = (mv_square_prime_exists_nextvaluesquare * mv_square_prime_exists_nextvaluesquare) * pvs_factor_exists_nextvaluesquaredivisor))) /\ ((mt_value_exists_next) = 0))) \/ (((((~((mt_index_exists_next) = 0)) /\ (forall sfd_prime_exists_nextvaluesquarefree. (~((sfd_prime_exists_nextvaluesquarefree) = 1) /\ forall pvs_left_exists_nextvaluesquarefreedomain pvs_right_exists_nextvaluesquarefreedomain. (sfd_prime_exists_nextvaluesquarefree) = pvs_left_exists_nextvaluesquarefreedomain * pvs_right_exists_nextvaluesquarefreedomain -> pvs_left_exists_nextvaluesquarefreedomain = 1 \/ pvs_right_exists_nextvaluesquarefreedomain = 1) -> (exists pvs_le_gap_exists_nextvaluesquarefreebound. pvs_le_gap_exists_nextvaluesquarefreebound + (sfd_prime_exists_nextvaluesquarefree) = (mt_index_exists_next)) -> ~(exists pvs_factor_exists_nextvaluesquarefreesquare. (mt_index_exists_next) = (sfd_prime_exists_nextvaluesquarefree * sfd_prime_exists_nextvaluesquarefree) * pvs_factor_exists_nextvaluesquarefreesquare)))) /\ (exists mv_factor_code_exists_nextvaluefactors mv_factor_scale_exists_nextvaluefactors mv_factor_count_exists_nextvaluefactors. (((~(mt_index_exists_next = 0) /\ ((exists ff_u_fsat_exists_nextvaluefactorsfactorization_product ff_v_fsat_exists_nextvaluefactorsfactorization_product. ((((exists ff_h_fsat_exists_nextvaluefactorsfactorization_product_start. ff_h_fsat_exists_nextvaluefactorsfactorization_product_start + S (1) = S ((S (0)) * ff_v_fsat_exists_nextvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_nextvaluefactorsfactorization_product_start. ff_u_fsat_exists_nextvaluefactorsfactorization_product = ff_q_fsat_exists_nextvaluefactorsfactorization_product_start * S ((S (0)) * ff_v_fsat_exists_nextvaluefactorsfactorization_product) + (1))) /\ ((((exists ff_h_fsat_exists_nextvaluefactorsfactorization_product_terminal. ff_h_fsat_exists_nextvaluefactorsfactorization_product_terminal + S (mt_index_exists_next) = S ((S (mv_factor_count_exists_nextvaluefactors)) * ff_v_fsat_exists_nextvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_nextvaluefactorsfactorization_product_terminal. ff_u_fsat_exists_nextvaluefactorsfactorization_product = ff_q_fsat_exists_nextvaluefactorsfactorization_product_terminal * S ((S (mv_factor_count_exists_nextvaluefactors)) * ff_v_fsat_exists_nextvaluefactorsfactorization_product) + (mt_index_exists_next))) /\ forall ff_i_fsat_exists_nextvaluefactorsfactorization_product. (exists ff_lt_fsat_exists_nextvaluefactorsfactorization_product_bound. ff_lt_fsat_exists_nextvaluefactorsfactorization_product_bound + S ff_i_fsat_exists_nextvaluefactorsfactorization_product = mv_factor_count_exists_nextvaluefactors) -> exists ff_p_fsat_exists_nextvaluefactorsfactorization_product ff_r_fsat_exists_nextvaluefactorsfactorization_product ff_s_fsat_exists_nextvaluefactorsfactorization_product. ((((exists ff_h_fsat_exists_nextvaluefactorsfactorization_product_factor. ff_h_fsat_exists_nextvaluefactorsfactorization_product_factor + S (ff_p_fsat_exists_nextvaluefactorsfactorization_product) = S ((S (ff_i_fsat_exists_nextvaluefactorsfactorization_product)) * mv_factor_scale_exists_nextvaluefactors)) /\ exists ff_q_fsat_exists_nextvaluefactorsfactorization_product_factor. mv_factor_code_exists_nextvaluefactors = ff_q_fsat_exists_nextvaluefactorsfactorization_product_factor * S ((S (ff_i_fsat_exists_nextvaluefactorsfactorization_product)) * mv_factor_scale_exists_nextvaluefactors) + (ff_p_fsat_exists_nextvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_nextvaluefactorsfactorization_product_partial. ff_h_fsat_exists_nextvaluefactorsfactorization_product_partial + S (ff_r_fsat_exists_nextvaluefactorsfactorization_product) = S ((S (ff_i_fsat_exists_nextvaluefactorsfactorization_product)) * ff_v_fsat_exists_nextvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_nextvaluefactorsfactorization_product_partial. ff_u_fsat_exists_nextvaluefactorsfactorization_product = ff_q_fsat_exists_nextvaluefactorsfactorization_product_partial * S ((S (ff_i_fsat_exists_nextvaluefactorsfactorization_product)) * ff_v_fsat_exists_nextvaluefactorsfactorization_product) + (ff_r_fsat_exists_nextvaluefactorsfactorization_product))) /\ ((((exists ff_h_fsat_exists_nextvaluefactorsfactorization_product_successor. ff_h_fsat_exists_nextvaluefactorsfactorization_product_successor + S (ff_s_fsat_exists_nextvaluefactorsfactorization_product) = S ((S (S ff_i_fsat_exists_nextvaluefactorsfactorization_product)) * ff_v_fsat_exists_nextvaluefactorsfactorization_product)) /\ exists ff_q_fsat_exists_nextvaluefactorsfactorization_product_successor. ff_u_fsat_exists_nextvaluefactorsfactorization_product = ff_q_fsat_exists_nextvaluefactorsfactorization_product_successor * S ((S (S ff_i_fsat_exists_nextvaluefactorsfactorization_product)) * ff_v_fsat_exists_nextvaluefactorsfactorization_product) + (ff_s_fsat_exists_nextvaluefactorsfactorization_product))) /\ ff_s_fsat_exists_nextvaluefactorsfactorization_product = ff_r_fsat_exists_nextvaluefactorsfactorization_product * ff_p_fsat_exists_nextvaluefactorsfactorization_product)))))) /\ (forall ftsf_index_fsat_exists_nextvaluefactorsfactorization_primes. (exists ftsf_gap_fsat_exists_nextvaluefactorsfactorization_primes_bound. ftsf_gap_fsat_exists_nextvaluefactorsfactorization_primes_bound + S ftsf_index_fsat_exists_nextvaluefactorsfactorization_primes = (mv_factor_count_exists_nextvaluefactors)) -> exists ftsf_factor_fsat_exists_nextvaluefactorsfactorization_primes. ((((exists ff_h_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_entry. ff_h_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_entry + S (ftsf_factor_fsat_exists_nextvaluefactorsfactorization_primes) = S ((S (ftsf_index_fsat_exists_nextvaluefactorsfactorization_primes)) * mv_factor_scale_exists_nextvaluefactors)) /\ exists ff_q_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_entry. mv_factor_code_exists_nextvaluefactors = ff_q_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_entry * S ((S (ftsf_index_fsat_exists_nextvaluefactorsfactorization_primes)) * mv_factor_scale_exists_nextvaluefactors) + (ftsf_factor_fsat_exists_nextvaluefactorsfactorization_primes))) /\ ((~(ftsf_factor_fsat_exists_nextvaluefactorsfactorization_primes = 1) /\ forall frm_prime_left_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_prime frm_prime_right_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_prime. ftsf_factor_fsat_exists_nextvaluefactorsfactorization_primes = frm_prime_left_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_prime * frm_prime_right_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_prime -> frm_prime_left_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_exists_nextvaluefactorsfactorization_primes_prime = 1))))))) /\ ((((exists mv_even_half_exists_nextvaluefactorsparityeven. (mv_factor_count_exists_nextvaluefactors) = 2 * mv_even_half_exists_nextvaluefactorsparityeven) /\ ((mt_value_exists_next) = 2))) \/ (((exists mv_odd_half_exists_nextvaluefactorsparityodd. (mv_factor_count_exists_nextvaluefactors) = 2 * mv_odd_half_exists_nextvaluefactorsparityodd + 1) /\ ((mt_value_exists_next) = 1)))))))))))))))) /\ (forall dst_index_exists_preserve dst_first_exists_preserve dst_second_exists_preserve. (exists pvs_gap_exists_preservebound. pvs_gap_exists_preservebound + S (dst_index_exists_preserve) = (S N)) -> (exists dst_positive_code_exists_preservefirst dst_positive_scale_exists_preservefirst dst_negative_code_exists_preservefirst dst_negative_scale_exists_preservefirst dst_positive_exists_preservefirst dst_negative_exists_preservefirst. (((x) = (((((dst_positive_code_exists_preservefirst) + (dst_positive_scale_exists_preservefirst)) * S ((dst_positive_code_exists_preservefirst) + (dst_positive_scale_exists_preservefirst)) + ((dst_positive_scale_exists_preservefirst) + (dst_positive_scale_exists_preservefirst))) + (((dst_negative_code_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)) * S ((dst_negative_code_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)) + ((dst_negative_scale_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)))) * S ((((dst_positive_code_exists_preservefirst) + (dst_positive_scale_exists_preservefirst)) * S ((dst_positive_code_exists_preservefirst) + (dst_positive_scale_exists_preservefirst)) + ((dst_positive_scale_exists_preservefirst) + (dst_positive_scale_exists_preservefirst))) + (((dst_negative_code_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)) * S ((dst_negative_code_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)) + ((dst_negative_scale_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)))) + ((((dst_negative_code_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)) * S ((dst_negative_code_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)) + ((dst_negative_scale_exists_preservefirst) + (dst_negative_scale_exists_preservefirst))) + (((dst_negative_code_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)) * S ((dst_negative_code_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)) + ((dst_negative_scale_exists_preservefirst) + (dst_negative_scale_exists_preservefirst)))))) /\ (((((exists ff_h_pvs_exists_preservefirstpositive. ff_h_pvs_exists_preservefirstpositive + S (dst_positive_exists_preservefirst) = S ((S (dst_index_exists_preserve)) * dst_positive_scale_exists_preservefirst)) /\ exists ff_q_pvs_exists_preservefirstpositive. dst_positive_code_exists_preservefirst = ff_q_pvs_exists_preservefirstpositive * S ((S (dst_index_exists_preserve)) * dst_positive_scale_exists_preservefirst) + (dst_positive_exists_preservefirst))) /\ (((((exists ff_h_pvs_exists_preservefirstnegative. ff_h_pvs_exists_preservefirstnegative + S (dst_negative_exists_preservefirst) = S ((S (dst_index_exists_preserve)) * dst_negative_scale_exists_preservefirst)) /\ exists ff_q_pvs_exists_preservefirstnegative. dst_negative_code_exists_preservefirst = ff_q_pvs_exists_preservefirstnegative * S ((S (dst_index_exists_preserve)) * dst_negative_scale_exists_preservefirst) + (dst_negative_exists_preservefirst))) /\ (exists ge_balance_positive_exists_preservefirstvalue ge_balance_negative_exists_preservefirstvalue. (((((dst_first_exists_preserve) = 2 * (ge_balance_positive_exists_preservefirstvalue) /\ (ge_balance_negative_exists_preservefirstvalue) = 0) \/ exists ge_signed_half_exists_preservefirstvaluedecode. (((dst_first_exists_preserve) = 2 * ge_signed_half_exists_preservefirstvaluedecode + 1 /\ (ge_balance_positive_exists_preservefirstvalue) = 0) /\ (ge_balance_negative_exists_preservefirstvalue) = S ge_signed_half_exists_preservefirstvaluedecode))) /\ ((dst_positive_exists_preservefirst) + ge_balance_negative_exists_preservefirstvalue = (dst_negative_exists_preservefirst) + ge_balance_positive_exists_preservefirstvalue))))))))) -> (exists dst_positive_code_exists_preservesecond dst_positive_scale_exists_preservesecond dst_negative_code_exists_preservesecond dst_negative_scale_exists_preservesecond dst_positive_exists_preservesecond dst_negative_exists_preservesecond. (((G) = (((((dst_positive_code_exists_preservesecond) + (dst_positive_scale_exists_preservesecond)) * S ((dst_positive_code_exists_preservesecond) + (dst_positive_scale_exists_preservesecond)) + ((dst_positive_scale_exists_preservesecond) + (dst_positive_scale_exists_preservesecond))) + (((dst_negative_code_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)) * S ((dst_negative_code_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)) + ((dst_negative_scale_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)))) * S ((((dst_positive_code_exists_preservesecond) + (dst_positive_scale_exists_preservesecond)) * S ((dst_positive_code_exists_preservesecond) + (dst_positive_scale_exists_preservesecond)) + ((dst_positive_scale_exists_preservesecond) + (dst_positive_scale_exists_preservesecond))) + (((dst_negative_code_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)) * S ((dst_negative_code_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)) + ((dst_negative_scale_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)))) + ((((dst_negative_code_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)) * S ((dst_negative_code_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)) + ((dst_negative_scale_exists_preservesecond) + (dst_negative_scale_exists_preservesecond))) + (((dst_negative_code_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)) * S ((dst_negative_code_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)) + ((dst_negative_scale_exists_preservesecond) + (dst_negative_scale_exists_preservesecond)))))) /\ (((((exists ff_h_pvs_exists_preservesecondpositive. ff_h_pvs_exists_preservesecondpositive + S (dst_positive_exists_preservesecond) = S ((S (dst_index_exists_preserve)) * dst_positive_scale_exists_preservesecond)) /\ exists ff_q_pvs_exists_preservesecondpositive. dst_positive_code_exists_preservesecond = ff_q_pvs_exists_preservesecondpositive * S ((S (dst_index_exists_preserve)) * dst_positive_scale_exists_preservesecond) + (dst_positive_exists_preservesecond))) /\ (((((exists ff_h_pvs_exists_preservesecondnegative. ff_h_pvs_exists_preservesecondnegative + S (dst_negative_exists_preservesecond) = S ((S (dst_index_exists_preserve)) * dst_negative_scale_exists_preservesecond)) /\ exists ff_q_pvs_exists_preservesecondnegative. dst_negative_code_exists_preservesecond = ff_q_pvs_exists_preservesecondnegative * S ((S (dst_index_exists_preserve)) * dst_negative_scale_exists_preservesecond) + (dst_negative_exists_preservesecond))) /\ (exists ge_balance_positive_exists_preservesecondvalue ge_balance_negative_exists_preservesecondvalue. (((((dst_second_exists_preserve) = 2 * (ge_balance_positive_exists_preservesecondvalue) /\ (ge_balance_negative_exists_preservesecondvalue) = 0) \/ exists ge_signed_half_exists_preservesecondvaluedecode. (((dst_second_exists_preserve) = 2 * ge_signed_half_exists_preservesecondvaluedecode + 1 /\ (ge_balance_positive_exists_preservesecondvalue) = 0) /\ (ge_balance_negative_exists_preservesecondvalue) = S ge_signed_half_exists_preservesecondvaluedecode))) /\ ((dst_positive_exists_preservesecond) + ge_balance_negative_exists_preservesecondvalue = (dst_negative_exists_preservesecond) + ge_balance_positive_exists_preservesecondvalue))))))))) -> dst_first_exists_preserve = dst_second_exists_preserve)
  22. 0022specialize mobius_table_append (N)
  23. 0023specialize mobius_table_append (x)
  24. 0024specialize mobius_table_append (x1)
  25. 0025apply mobius_table_append
  26. 0026exact IH_witness
  27. 0027exact hz_witness
  28. 0028cases hnext
  29. 0029cases hnext_witness
  30. 0030exists x2
  31. 0031exact hnext_witness_left