PA0074

gauss_signed_half_prefix_exists

Alpha v34 checked-use theorem · independently closed; not Stable

Every bounded family of pointwise signed choices admits aligned beta-coded magnitude and sign prefixes.

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 original first-admission records.

Exact expanded PA statement

forall p h a b c l. (forall gsp_choice_index_exists_all. (exists gsp_lt_gap_exists_all_choice_bound. gsp_lt_gap_exists_all_choice_bound + S gsp_choice_index_exists_all = l) -> (exists gsp_value_exists_all_choice gsp_magnitude_exists_all_choice gsp_sign_exists_all_choice. (((exists ff_h_gsp_exists_all_choice_source. ff_h_gsp_exists_all_choice_source + S (gsp_value_exists_all_choice) = S ((S (gsp_choice_index_exists_all)) * c)) /\ exists ff_q_gsp_exists_all_choice_source. b = ff_q_gsp_exists_all_choice_source * S ((S (gsp_choice_index_exists_all)) * c) + (gsp_value_exists_all_choice))) /\ ((exists gsp_lt_gap_exists_all_choice_positive. gsp_lt_gap_exists_all_choice_positive + S 0 = gsp_magnitude_exists_all_choice) /\ ((exists gsp_le_gap_exists_all_choice_bounded. gsp_le_gap_exists_all_choice_bounded + gsp_magnitude_exists_all_choice = h) /\ ((gsp_sign_exists_all_choice = 0 \/ gsp_sign_exists_all_choice = 1) /\ (((gsp_sign_exists_all_choice = 0 /\ (exists gsp_mod_left_exists_all_choice_lower gsp_mod_right_exists_all_choice_lower. (a * gsp_value_exists_all_choice) + p * gsp_mod_left_exists_all_choice_lower = (gsp_magnitude_exists_all_choice) + p * gsp_mod_right_exists_all_choice_lower)) \/ (gsp_sign_exists_all_choice = 1 /\ (exists gsp_mod_left_exists_all_choice_reflected gsp_mod_right_exists_all_choice_reflected. (a * gsp_value_exists_all_choice) + p * gsp_mod_left_exists_all_choice_reflected = ((2 * h) * gsp_magnitude_exists_all_choice) + p * gsp_mod_right_exists_all_choice_reflected))))))))) -> (exists mb mc sb sc. (forall gsp_index_exists_result. (exists gsp_lt_gap_exists_result_index_bound. gsp_lt_gap_exists_result_index_bound + S gsp_index_exists_result = l) -> (exists gsp_value_exists_result_entry gsp_magnitude_exists_result_entry gsp_sign_exists_result_entry. (((exists ff_h_gsp_exists_result_entry_source. ff_h_gsp_exists_result_entry_source + S (gsp_value_exists_result_entry) = S ((S (gsp_index_exists_result)) * c)) /\ exists ff_q_gsp_exists_result_entry_source. b = ff_q_gsp_exists_result_entry_source * S ((S (gsp_index_exists_result)) * c) + (gsp_value_exists_result_entry))) /\ ((((exists ff_h_gsp_exists_result_entry_magnitude. ff_h_gsp_exists_result_entry_magnitude + S (gsp_magnitude_exists_result_entry) = S ((S (gsp_index_exists_result)) * mc)) /\ exists ff_q_gsp_exists_result_entry_magnitude. mb = ff_q_gsp_exists_result_entry_magnitude * S ((S (gsp_index_exists_result)) * mc) + (gsp_magnitude_exists_result_entry))) /\ ((((exists ff_h_gsp_exists_result_entry_sign. ff_h_gsp_exists_result_entry_sign + S (gsp_sign_exists_result_entry) = S ((S (gsp_index_exists_result)) * sc)) /\ exists ff_q_gsp_exists_result_entry_sign. sb = ff_q_gsp_exists_result_entry_sign * S ((S (gsp_index_exists_result)) * sc) + (gsp_sign_exists_result_entry))) /\ ((exists gsp_lt_gap_exists_result_entry_positive. gsp_lt_gap_exists_result_entry_positive + S 0 = gsp_magnitude_exists_result_entry) /\ ((exists gsp_le_gap_exists_result_entry_bounded. gsp_le_gap_exists_result_entry_bounded + gsp_magnitude_exists_result_entry = h) /\ ((gsp_sign_exists_result_entry = 0 \/ gsp_sign_exists_result_entry = 1) /\ (((gsp_sign_exists_result_entry = 0 /\ (exists gsp_mod_left_exists_result_entry_lower gsp_mod_right_exists_result_entry_lower. (a * gsp_value_exists_result_entry) + p * gsp_mod_left_exists_result_entry_lower = (gsp_magnitude_exists_result_entry) + p * gsp_mod_right_exists_result_entry_lower)) \/ (gsp_sign_exists_result_entry = 1 /\ (exists gsp_mod_left_exists_result_entry_reflected gsp_mod_right_exists_result_entry_reflected. (a * gsp_value_exists_result_entry) + p * gsp_mod_left_exists_result_entry_reflected = ((2 * h) * gsp_magnitude_exists_result_entry) + p * gsp_mod_right_exists_result_entry_reflected))))))))))))

Structural proof guide

Generated structural guide

Every bounded family of pointwise signed choices admits aligned beta-coded magnitude and sign prefixes.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, le_succ, le_refl, gauss_signed_half_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (5), intermediate claims (5).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA0073 gauss_signed_half_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA0073 gauss_signed_half_prefix_extend

Direct dependents

PA0075 gauss_half_range_signed_prefix_exists

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

60 script commands · 12 reading checkpoints · 5 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 (5)
add eq zero rightsucc ne zerole succle reflgauss signed half prefix extend

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–5

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
02Induction on lL6–7

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

  1. L6
    induction l
  2. L7
    intro hchoices
03Construct an explicit witnessL8–11

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

  1. L8
    exists 0
  2. L9
    exists 0
  3. L10
    exists 0
  4. L11
    exists 0
04Fix variables and assumptionsL12–13

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

  1. L12
    intro i
  2. L13
    intro hi
05Separate the logical casesL14–15

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

  1. L14
    exfalso
  2. L15
    cases hi
06Establish hsiL16–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply add eq zero right.

  1. L16
    have hsi : S i = 0
  2. L17
    specialize add_eq_zero_right x
  3. L18
    specialize add_eq_zero_right (S i)
  4. L19
    apply add_eq_zero_right
  5. L20
    exact hi_witness
  6. L21
    specialize succ_ne_zero i
  7. L22
    apply succ_ne_zero
  8. L23
    exact hsi
  9. L24
    intro hchoices
07Establish hprevious_choicesL25–33

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

  1. L25
    have hprevious_choices : ∀ gsp_choice_index_exists_previous. Lt(gsp_choice_index_exists_previous,l) → ∃ x. ∃ y. ∃ z. BetaAt(b,c,gsp_choice_index_exists_previous,x) ∧ (Lt(0,y) ∧ (Le(y,h) ∧ ((z = 0 ∨ z = 1) ∧ (z = 0 ∧ ModEq(p,a · x,y) ∨ z = 1 ∧ ModEq(p,a · x,2 · h · y)))))Definitions: LeLtModEqBetaAt
  2. L26
    intro i
  3. L27
    intro hi
  4. L28
    specialize hchoices i
  5. L29
    apply hchoices
  6. L30
    specialize le_succ (S i)
  7. L31
    specialize le_succ l
  8. L32
    apply le_succ
  9. L33
    exact hi
08Establish hpreviousL34–36

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

  1. L34
    have hprevious : ∃ mb. ∃ mc. ∃ sb. ∃ sc. ∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(mb,mc,x,z) ∧ (BetaAt(sb,sc,x,n) ∧ (Lt(0,z) ∧ (Le(z,h) ∧ ((n = 0 ∨ n = 1) ∧ (n = 0 ∧ ModEq(p,a · y,z) ∨ n = 1 ∧ ModEq(p,a · y,2 · h · z)))))))Definitions: LeLtModEqBetaAt
  2. L35
    apply IH
  3. L36
    exact hprevious_choices
09Separate the logical casesL37–40

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

  1. L37
    cases hprevious
  2. L38
    cases hprevious_witness
  3. L39
    cases hprevious_witness_witness
  4. L40
    cases hprevious_witness_witness_witness
10Establish hlastL41–45

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

  1. L41
    have hlast : ∃ gsp_value_exists_last_choice. ∃ gsp_magnitude_exists_last_choice. ∃ gsp_sign_exists_last_choice. BetaAt(b,c,l,gsp_value_exists_last_choice) ∧ (Lt(0,gsp_magnitude_exists_last_choice) ∧ (Le(gsp_magnitude_exists_last_choice,h) ∧ ((gsp_sign_exists_last_choice = 0 ∨ gsp_sign_exists_last_choice = 1) ∧ (gsp_sign_exists_last_choice = 0 ∧ ModEq(p,a · gsp_value_exists_last_choice,gsp_magnitude_exists_last_choice) ∨ gsp_sign_exists_last_choice = 1 ∧ ModEq(p,a · gsp_value_exists_last_choice,2 · h · gsp_magnitude_exists_last_choice)))))Definitions: LeLtModEqBetaAt
  2. L42
    specialize hchoices l
  3. L43
    apply hchoices
  4. L44
    specialize le_refl (S l)
  5. L45
    exact le_refl
11Establish hnextL46–55

Establish this local claim before using it. It is not an additional assumption.

  1. L46
    have hnext : ∃ mb. ∃ mc. ∃ sb. ∃ sc. ∀ x. Lt(x,S l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (BetaAt(mb,mc,x,z) ∧ (BetaAt(sb,sc,x,n) ∧ (Lt(0,z) ∧ (Le(z,h) ∧ ((n = 0 ∨ n = 1) ∧ (n = 0 ∧ ModEq(p,a · y,z) ∨ n = 1 ∧ ModEq(p,a · y,2 · h · z)))))))Definitions: LeLtModEqBetaAt
  2. L47
    specialize gauss_signed_half_prefix_extend p
  3. L48
    specialize gauss_signed_half_prefix_extend h
  4. L49
    specialize gauss_signed_half_prefix_extend a
  5. L50
    specialize gauss_signed_half_prefix_extend b
  6. L51
    specialize gauss_signed_half_prefix_extend c
  7. L52
    specialize gauss_signed_half_prefix_extend x
  8. L53
    specialize gauss_signed_half_prefix_extend x1
  9. L54
    specialize gauss_signed_half_prefix_extend x2
  10. L55
    specialize gauss_signed_half_prefix_extend x3
12Use earlier factsL56–60

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

  1. L56
    specialize gauss_signed_half_prefix_extend l
  2. L57
    apply gauss_signed_half_prefix_extend
  3. L58
    exact hprevious_witness_witness_witness_witness
  4. L59
    exact hlast
  5. L60
    exact hnext

Library-wide reading audit

Original exact command ledger · 60 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006induction l
  7. 0007intro hchoices
  8. 0008exists 0
  9. 0009exists 0
  10. 0010exists 0
  11. 0011exists 0
  12. 0012intro i
  13. 0013intro hi
  14. 0014exfalso
  15. 0015cases hi
  16. 0016have hsi : S i = 0
  17. 0017specialize add_eq_zero_right x
  18. 0018specialize add_eq_zero_right (S i)
  19. 0019apply add_eq_zero_right
  20. 0020exact hi_witness
  21. 0021specialize succ_ne_zero i
  22. 0022apply succ_ne_zero
  23. 0023exact hsi
  24. 0024intro hchoices
  25. 0025have hprevious_choices : forall gsp_choice_index_exists_previous. (exists gsp_lt_gap_exists_previous_choice_bound. gsp_lt_gap_exists_previous_choice_bound + S gsp_choice_index_exists_previous = l) -> (exists gsp_value_exists_previous_choice gsp_magnitude_exists_previous_choice gsp_sign_exists_previous_choice. (((exists ff_h_gsp_exists_previous_choice_source. ff_h_gsp_exists_previous_choice_source + S (gsp_value_exists_previous_choice) = S ((S (gsp_choice_index_exists_previous)) * c)) /\ exists ff_q_gsp_exists_previous_choice_source. b = ff_q_gsp_exists_previous_choice_source * S ((S (gsp_choice_index_exists_previous)) * c) + (gsp_value_exists_previous_choice))) /\ ((exists gsp_lt_gap_exists_previous_choice_positive. gsp_lt_gap_exists_previous_choice_positive + S 0 = gsp_magnitude_exists_previous_choice) /\ ((exists gsp_le_gap_exists_previous_choice_bounded. gsp_le_gap_exists_previous_choice_bounded + gsp_magnitude_exists_previous_choice = h) /\ ((gsp_sign_exists_previous_choice = 0 \/ gsp_sign_exists_previous_choice = 1) /\ (((gsp_sign_exists_previous_choice = 0 /\ (exists gsp_mod_left_exists_previous_choice_lower gsp_mod_right_exists_previous_choice_lower. (a * gsp_value_exists_previous_choice) + p * gsp_mod_left_exists_previous_choice_lower = (gsp_magnitude_exists_previous_choice) + p * gsp_mod_right_exists_previous_choice_lower)) \/ (gsp_sign_exists_previous_choice = 1 /\ (exists gsp_mod_left_exists_previous_choice_reflected gsp_mod_right_exists_previous_choice_reflected. (a * gsp_value_exists_previous_choice) + p * gsp_mod_left_exists_previous_choice_reflected = ((2 * h) * gsp_magnitude_exists_previous_choice) + p * gsp_mod_right_exists_previous_choice_reflected))))))))
  26. 0026intro i
  27. 0027intro hi
  28. 0028specialize hchoices i
  29. 0029apply hchoices
  30. 0030specialize le_succ (S i)
  31. 0031specialize le_succ l
  32. 0032apply le_succ
  33. 0033exact hi
  34. 0034have hprevious : exists mb mc sb sc. (forall gsp_index_exists_previous_result. (exists gsp_lt_gap_exists_previous_result_index_bound. gsp_lt_gap_exists_previous_result_index_bound + S gsp_index_exists_previous_result = l) -> (exists gsp_value_exists_previous_result_entry gsp_magnitude_exists_previous_result_entry gsp_sign_exists_previous_result_entry. (((exists ff_h_gsp_exists_previous_result_entry_source. ff_h_gsp_exists_previous_result_entry_source + S (gsp_value_exists_previous_result_entry) = S ((S (gsp_index_exists_previous_result)) * c)) /\ exists ff_q_gsp_exists_previous_result_entry_source. b = ff_q_gsp_exists_previous_result_entry_source * S ((S (gsp_index_exists_previous_result)) * c) + (gsp_value_exists_previous_result_entry))) /\ ((((exists ff_h_gsp_exists_previous_result_entry_magnitude. ff_h_gsp_exists_previous_result_entry_magnitude + S (gsp_magnitude_exists_previous_result_entry) = S ((S (gsp_index_exists_previous_result)) * mc)) /\ exists ff_q_gsp_exists_previous_result_entry_magnitude. mb = ff_q_gsp_exists_previous_result_entry_magnitude * S ((S (gsp_index_exists_previous_result)) * mc) + (gsp_magnitude_exists_previous_result_entry))) /\ ((((exists ff_h_gsp_exists_previous_result_entry_sign. ff_h_gsp_exists_previous_result_entry_sign + S (gsp_sign_exists_previous_result_entry) = S ((S (gsp_index_exists_previous_result)) * sc)) /\ exists ff_q_gsp_exists_previous_result_entry_sign. sb = ff_q_gsp_exists_previous_result_entry_sign * S ((S (gsp_index_exists_previous_result)) * sc) + (gsp_sign_exists_previous_result_entry))) /\ ((exists gsp_lt_gap_exists_previous_result_entry_positive. gsp_lt_gap_exists_previous_result_entry_positive + S 0 = gsp_magnitude_exists_previous_result_entry) /\ ((exists gsp_le_gap_exists_previous_result_entry_bounded. gsp_le_gap_exists_previous_result_entry_bounded + gsp_magnitude_exists_previous_result_entry = h) /\ ((gsp_sign_exists_previous_result_entry = 0 \/ gsp_sign_exists_previous_result_entry = 1) /\ (((gsp_sign_exists_previous_result_entry = 0 /\ (exists gsp_mod_left_exists_previous_result_entry_lower gsp_mod_right_exists_previous_result_entry_lower. (a * gsp_value_exists_previous_result_entry) + p * gsp_mod_left_exists_previous_result_entry_lower = (gsp_magnitude_exists_previous_result_entry) + p * gsp_mod_right_exists_previous_result_entry_lower)) \/ (gsp_sign_exists_previous_result_entry = 1 /\ (exists gsp_mod_left_exists_previous_result_entry_reflected gsp_mod_right_exists_previous_result_entry_reflected. (a * gsp_value_exists_previous_result_entry) + p * gsp_mod_left_exists_previous_result_entry_reflected = ((2 * h) * gsp_magnitude_exists_previous_result_entry) + p * gsp_mod_right_exists_previous_result_entry_reflected)))))))))))
  35. 0035apply IH
  36. 0036exact hprevious_choices
  37. 0037cases hprevious
  38. 0038cases hprevious_witness
  39. 0039cases hprevious_witness_witness
  40. 0040cases hprevious_witness_witness_witness
  41. 0041have hlast : exists gsp_value_exists_last_choice gsp_magnitude_exists_last_choice gsp_sign_exists_last_choice. (((exists ff_h_gsp_exists_last_choice_source. ff_h_gsp_exists_last_choice_source + S (gsp_value_exists_last_choice) = S ((S (l)) * c)) /\ exists ff_q_gsp_exists_last_choice_source. b = ff_q_gsp_exists_last_choice_source * S ((S (l)) * c) + (gsp_value_exists_last_choice))) /\ ((exists gsp_lt_gap_exists_last_choice_positive. gsp_lt_gap_exists_last_choice_positive + S 0 = gsp_magnitude_exists_last_choice) /\ ((exists gsp_le_gap_exists_last_choice_bounded. gsp_le_gap_exists_last_choice_bounded + gsp_magnitude_exists_last_choice = h) /\ ((gsp_sign_exists_last_choice = 0 \/ gsp_sign_exists_last_choice = 1) /\ (((gsp_sign_exists_last_choice = 0 /\ (exists gsp_mod_left_exists_last_choice_lower gsp_mod_right_exists_last_choice_lower. (a * gsp_value_exists_last_choice) + p * gsp_mod_left_exists_last_choice_lower = (gsp_magnitude_exists_last_choice) + p * gsp_mod_right_exists_last_choice_lower)) \/ (gsp_sign_exists_last_choice = 1 /\ (exists gsp_mod_left_exists_last_choice_reflected gsp_mod_right_exists_last_choice_reflected. (a * gsp_value_exists_last_choice) + p * gsp_mod_left_exists_last_choice_reflected = ((2 * h) * gsp_magnitude_exists_last_choice) + p * gsp_mod_right_exists_last_choice_reflected)))))))
  42. 0042specialize hchoices l
  43. 0043apply hchoices
  44. 0044specialize le_refl (S l)
  45. 0045exact le_refl
  46. 0046have hnext : exists mb mc sb sc. (forall gsp_index_exists_next_result. (exists gsp_lt_gap_exists_next_result_index_bound. gsp_lt_gap_exists_next_result_index_bound + S gsp_index_exists_next_result = S l) -> (exists gsp_value_exists_next_result_entry gsp_magnitude_exists_next_result_entry gsp_sign_exists_next_result_entry. (((exists ff_h_gsp_exists_next_result_entry_source. ff_h_gsp_exists_next_result_entry_source + S (gsp_value_exists_next_result_entry) = S ((S (gsp_index_exists_next_result)) * c)) /\ exists ff_q_gsp_exists_next_result_entry_source. b = ff_q_gsp_exists_next_result_entry_source * S ((S (gsp_index_exists_next_result)) * c) + (gsp_value_exists_next_result_entry))) /\ ((((exists ff_h_gsp_exists_next_result_entry_magnitude. ff_h_gsp_exists_next_result_entry_magnitude + S (gsp_magnitude_exists_next_result_entry) = S ((S (gsp_index_exists_next_result)) * mc)) /\ exists ff_q_gsp_exists_next_result_entry_magnitude. mb = ff_q_gsp_exists_next_result_entry_magnitude * S ((S (gsp_index_exists_next_result)) * mc) + (gsp_magnitude_exists_next_result_entry))) /\ ((((exists ff_h_gsp_exists_next_result_entry_sign. ff_h_gsp_exists_next_result_entry_sign + S (gsp_sign_exists_next_result_entry) = S ((S (gsp_index_exists_next_result)) * sc)) /\ exists ff_q_gsp_exists_next_result_entry_sign. sb = ff_q_gsp_exists_next_result_entry_sign * S ((S (gsp_index_exists_next_result)) * sc) + (gsp_sign_exists_next_result_entry))) /\ ((exists gsp_lt_gap_exists_next_result_entry_positive. gsp_lt_gap_exists_next_result_entry_positive + S 0 = gsp_magnitude_exists_next_result_entry) /\ ((exists gsp_le_gap_exists_next_result_entry_bounded. gsp_le_gap_exists_next_result_entry_bounded + gsp_magnitude_exists_next_result_entry = h) /\ ((gsp_sign_exists_next_result_entry = 0 \/ gsp_sign_exists_next_result_entry = 1) /\ (((gsp_sign_exists_next_result_entry = 0 /\ (exists gsp_mod_left_exists_next_result_entry_lower gsp_mod_right_exists_next_result_entry_lower. (a * gsp_value_exists_next_result_entry) + p * gsp_mod_left_exists_next_result_entry_lower = (gsp_magnitude_exists_next_result_entry) + p * gsp_mod_right_exists_next_result_entry_lower)) \/ (gsp_sign_exists_next_result_entry = 1 /\ (exists gsp_mod_left_exists_next_result_entry_reflected gsp_mod_right_exists_next_result_entry_reflected. (a * gsp_value_exists_next_result_entry) + p * gsp_mod_left_exists_next_result_entry_reflected = ((2 * h) * gsp_magnitude_exists_next_result_entry) + p * gsp_mod_right_exists_next_result_entry_reflected)))))))))))
  47. 0047specialize gauss_signed_half_prefix_extend p
  48. 0048specialize gauss_signed_half_prefix_extend h
  49. 0049specialize gauss_signed_half_prefix_extend a
  50. 0050specialize gauss_signed_half_prefix_extend b
  51. 0051specialize gauss_signed_half_prefix_extend c
  52. 0052specialize gauss_signed_half_prefix_extend x
  53. 0053specialize gauss_signed_half_prefix_extend x1
  54. 0054specialize gauss_signed_half_prefix_extend x2
  55. 0055specialize gauss_signed_half_prefix_extend x3
  56. 0056specialize gauss_signed_half_prefix_extend l
  57. 0057apply gauss_signed_half_prefix_extend
  58. 0058exact hprevious_witness_witness_witness_witness
  59. 0059exact hlast
  60. 0060exact hnext