PA0074 · theorem

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.

Statement with defined notation

∀ p. ∀ h. ∀ a. ∀ b. ∀ c. ∀ l. (∀ x. Lt(x,l) → ∃ y. ∃ z. ∃ n. BetaAt(b,c,x,y) ∧ (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)))))) → ∃ x. ∃ y. ∃ z. ∃ n. ∀ m. Lt(m,l) → ∃ k. ∃ i. ∃ j. BetaAt(b,c,m,k) ∧ (BetaAt(x,y,m,i) ∧ (BetaAt(z,n,m,j) ∧ (Lt(0,i) ∧ (Le(i,h) ∧ ((j = 0 ∨ j = 1) ∧ (j = 0 ∧ ModEq(p,a · k,i) ∨ j = 1 ∧ ModEq(p,a · k,2 · h · i)))))))

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt

14 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt

27 occurrences

Exact expanded native-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))))))))))))

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA0073 gauss_signed_half_prefix_extend

Direct theorem dependents

PA0075 gauss_half_range_signed_prefix_exists

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

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 (5)
add eq zero rightsucc ne zerole succle reflgauss signed half prefix extend
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: Lt(gsp_choice_index_exists_previous,l)BetaAt(b,c,gsp_choice_index_exists_previous,x)Lt(0,y)Le(y,h)ModEq(p,a · x,y)ModEq(p,a · x,2 · h · y)Original native command in the exact edition
  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: Lt(x,l)BetaAt(b,c,x,y)BetaAt(mb,mc,x,z)BetaAt(sb,sc,x,n)Lt(0,z)Le(z,h)ModEq(p,a · y,z)ModEq(p,a · y,2 · h · z)Original native command in the exact edition
  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: BetaAt(b,c,l,gsp_value_exists_last_choice)Lt(0,gsp_magnitude_exists_last_choice)Le(gsp_magnitude_exists_last_choice,h)ModEq(p,a · gsp_value_exists_last_choice,gsp_magnitude_exists_last_choice)ModEq(p,a · gsp_value_exists_last_choice,2 · h · gsp_magnitude_exists_last_choice)Original native command in the exact edition
  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: Lt(x,S l)BetaAt(b,c,x,y)BetaAt(mb,mc,x,z)BetaAt(sb,sc,x,n)Lt(0,z)Le(z,h)ModEq(p,a · y,z)ModEq(p,a · y,2 · h · z)Original native command in the exact edition
  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 defined 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 : ∀ 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)))))
    Exact native replay linehave 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 : ∃ 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)))))))
    Exact native replay linehave 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 : ∃ 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)))))
    Exact native replay linehave 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 : ∃ 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)))))))
    Exact native replay linehave 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