PA0073 · theorem

gauss_signed_half_prefix_extend

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

Append one pointwise signed choice simultaneously to the magnitude and zero/one sign beta 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. ∀ mb. ∀ mc. ∀ sb. ∀ sc. ∀ l. (∀ 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)))))))) → (∃ x. ∃ y. ∃ z. BetaAt(b,c,l,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)))))) → ∃ x. ∃ y. ∃ z. ∃ n. ∀ m. Lt(m,S 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

21 occurrences

In local proof propositions

PD0001 Le PD0002 Lt PD0008 ModEq PD0013 BetaAt

16 occurrences

Exact expanded native-PA statement
forall p h a b c mb mc sb sc l. (forall gsp_index_extend_before. (exists gsp_lt_gap_extend_before_index_bound. gsp_lt_gap_extend_before_index_bound + S gsp_index_extend_before = l) -> (exists gsp_value_extend_before_entry gsp_magnitude_extend_before_entry gsp_sign_extend_before_entry. (((exists ff_h_gsp_extend_before_entry_source. ff_h_gsp_extend_before_entry_source + S (gsp_value_extend_before_entry) = S ((S (gsp_index_extend_before)) * c)) /\ exists ff_q_gsp_extend_before_entry_source. b = ff_q_gsp_extend_before_entry_source * S ((S (gsp_index_extend_before)) * c) + (gsp_value_extend_before_entry))) /\ ((((exists ff_h_gsp_extend_before_entry_magnitude. ff_h_gsp_extend_before_entry_magnitude + S (gsp_magnitude_extend_before_entry) = S ((S (gsp_index_extend_before)) * mc)) /\ exists ff_q_gsp_extend_before_entry_magnitude. mb = ff_q_gsp_extend_before_entry_magnitude * S ((S (gsp_index_extend_before)) * mc) + (gsp_magnitude_extend_before_entry))) /\ ((((exists ff_h_gsp_extend_before_entry_sign. ff_h_gsp_extend_before_entry_sign + S (gsp_sign_extend_before_entry) = S ((S (gsp_index_extend_before)) * sc)) /\ exists ff_q_gsp_extend_before_entry_sign. sb = ff_q_gsp_extend_before_entry_sign * S ((S (gsp_index_extend_before)) * sc) + (gsp_sign_extend_before_entry))) /\ ((exists gsp_lt_gap_extend_before_entry_positive. gsp_lt_gap_extend_before_entry_positive + S 0 = gsp_magnitude_extend_before_entry) /\ ((exists gsp_le_gap_extend_before_entry_bounded. gsp_le_gap_extend_before_entry_bounded + gsp_magnitude_extend_before_entry = h) /\ ((gsp_sign_extend_before_entry = 0 \/ gsp_sign_extend_before_entry = 1) /\ (((gsp_sign_extend_before_entry = 0 /\ (exists gsp_mod_left_extend_before_entry_lower gsp_mod_right_extend_before_entry_lower. (a * gsp_value_extend_before_entry) + p * gsp_mod_left_extend_before_entry_lower = (gsp_magnitude_extend_before_entry) + p * gsp_mod_right_extend_before_entry_lower)) \/ (gsp_sign_extend_before_entry = 1 /\ (exists gsp_mod_left_extend_before_entry_reflected gsp_mod_right_extend_before_entry_reflected. (a * gsp_value_extend_before_entry) + p * gsp_mod_left_extend_before_entry_reflected = ((2 * h) * gsp_magnitude_extend_before_entry) + p * gsp_mod_right_extend_before_entry_reflected))))))))))) -> (exists gsp_value_extend_choice gsp_magnitude_extend_choice gsp_sign_extend_choice. (((exists ff_h_gsp_extend_choice_source. ff_h_gsp_extend_choice_source + S (gsp_value_extend_choice) = S ((S (l)) * c)) /\ exists ff_q_gsp_extend_choice_source. b = ff_q_gsp_extend_choice_source * S ((S (l)) * c) + (gsp_value_extend_choice))) /\ ((exists gsp_lt_gap_extend_choice_positive. gsp_lt_gap_extend_choice_positive + S 0 = gsp_magnitude_extend_choice) /\ ((exists gsp_le_gap_extend_choice_bounded. gsp_le_gap_extend_choice_bounded + gsp_magnitude_extend_choice = h) /\ ((gsp_sign_extend_choice = 0 \/ gsp_sign_extend_choice = 1) /\ (((gsp_sign_extend_choice = 0 /\ (exists gsp_mod_left_extend_choice_lower gsp_mod_right_extend_choice_lower. (a * gsp_value_extend_choice) + p * gsp_mod_left_extend_choice_lower = (gsp_magnitude_extend_choice) + p * gsp_mod_right_extend_choice_lower)) \/ (gsp_sign_extend_choice = 1 /\ (exists gsp_mod_left_extend_choice_reflected gsp_mod_right_extend_choice_reflected. (a * gsp_value_extend_choice) + p * gsp_mod_left_extend_choice_reflected = ((2 * h) * gsp_magnitude_extend_choice) + p * gsp_mod_right_extend_choice_reflected)))))))) -> exists z d u v. (forall gsp_index_extend_after. (exists gsp_lt_gap_extend_after_index_bound. gsp_lt_gap_extend_after_index_bound + S gsp_index_extend_after = S l) -> (exists gsp_value_extend_after_entry gsp_magnitude_extend_after_entry gsp_sign_extend_after_entry. (((exists ff_h_gsp_extend_after_entry_source. ff_h_gsp_extend_after_entry_source + S (gsp_value_extend_after_entry) = S ((S (gsp_index_extend_after)) * c)) /\ exists ff_q_gsp_extend_after_entry_source. b = ff_q_gsp_extend_after_entry_source * S ((S (gsp_index_extend_after)) * c) + (gsp_value_extend_after_entry))) /\ ((((exists ff_h_gsp_extend_after_entry_magnitude. ff_h_gsp_extend_after_entry_magnitude + S (gsp_magnitude_extend_after_entry) = S ((S (gsp_index_extend_after)) * d)) /\ exists ff_q_gsp_extend_after_entry_magnitude. z = ff_q_gsp_extend_after_entry_magnitude * S ((S (gsp_index_extend_after)) * d) + (gsp_magnitude_extend_after_entry))) /\ ((((exists ff_h_gsp_extend_after_entry_sign. ff_h_gsp_extend_after_entry_sign + S (gsp_sign_extend_after_entry) = S ((S (gsp_index_extend_after)) * v)) /\ exists ff_q_gsp_extend_after_entry_sign. u = ff_q_gsp_extend_after_entry_sign * S ((S (gsp_index_extend_after)) * v) + (gsp_sign_extend_after_entry))) /\ ((exists gsp_lt_gap_extend_after_entry_positive. gsp_lt_gap_extend_after_entry_positive + S 0 = gsp_magnitude_extend_after_entry) /\ ((exists gsp_le_gap_extend_after_entry_bounded. gsp_le_gap_extend_after_entry_bounded + gsp_magnitude_extend_after_entry = h) /\ ((gsp_sign_extend_after_entry = 0 \/ gsp_sign_extend_after_entry = 1) /\ (((gsp_sign_extend_after_entry = 0 /\ (exists gsp_mod_left_extend_after_entry_lower gsp_mod_right_extend_after_entry_lower. (a * gsp_value_extend_after_entry) + p * gsp_mod_left_extend_after_entry_lower = (gsp_magnitude_extend_after_entry) + p * gsp_mod_right_extend_after_entry_lower)) \/ (gsp_sign_extend_after_entry = 1 /\ (exists gsp_mod_left_extend_after_entry_reflected gsp_mod_right_extend_after_entry_reflected. (a * gsp_value_extend_after_entry) + p * gsp_mod_left_extend_after_entry_reflected = ((2 * h) * gsp_magnitude_extend_after_entry) + p * gsp_mod_right_extend_after_entry_reflected)))))))))))

Proof neighborhood

Direct theorem prerequisites

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct theorem dependents

PA0074 gauss_signed_half_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

108 script commands · 42 reading checkpoints · 4 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 (2)
beta prefix extendfinite lt succ eq or lt
01Fix variables and assumptionsL1–10

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
  6. L6
    intro mb
  7. L7
    intro mc
  8. L8
    intro sb
  9. L9
    intro sc
  10. L10
    intro l
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hprefix
  2. L12
    intro hchoice
03Separate the logical casesL13–19

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

  1. L13
    cases hchoice
  2. L14
    cases hchoice_witness
  3. L15
    cases hchoice_witness_witness
  4. L16
    cases hchoice_witness_witness_witness
  5. L17
    cases hchoice_witness_witness_witness_right
  6. L18
    cases hchoice_witness_witness_witness_right_right
  7. L19
    cases hchoice_witness_witness_witness_right_right_right
04Establish hmag_extendL20–25

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

  1. L20
    have hmag_extend : ∃ gsp_new_code_magnitude_extension. ∃ gsp_new_scale_magnitude_extension. BetaAt(gsp_new_code_magnitude_extension,gsp_new_scale_magnitude_extension,l,x1) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(mb,mc,x,y) → BetaAt(gsp_new_code_magnitude_extension,gsp_new_scale_magnitude_extension,x,y))Definitions: BetaAt(gsp_new_code_magnitude_extension,gsp_new_scale_magnitude_extension,l,x1)Lt(x,l)BetaAt(mb,mc,x,y)BetaAt(gsp_new_code_magnitude_extension,gsp_new_scale_magnitude_extension,x,y)Original native command in the exact edition
  2. L21
    specialize beta_prefix_extend l
  3. L22
    specialize beta_prefix_extend mb
  4. L23
    specialize beta_prefix_extend mc
  5. L24
    specialize beta_prefix_extend x1
  6. L25
    exact beta_prefix_extend
05Separate the logical casesL26–28

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

  1. L26
    cases hmag_extend
  2. L27
    cases hmag_extend_witness
  3. L28
    cases hmag_extend_witness_witness
06Establish hsign_extendL29–34

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

  1. L29
    have hsign_extend : ∃ gsp_new_code_sign_extension. ∃ gsp_new_scale_sign_extension. BetaAt(gsp_new_code_sign_extension,gsp_new_scale_sign_extension,l,x2) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(sb,sc,x,y) → BetaAt(gsp_new_code_sign_extension,gsp_new_scale_sign_extension,x,y))Definitions: BetaAt(gsp_new_code_sign_extension,gsp_new_scale_sign_extension,l,x2)Lt(x,l)BetaAt(sb,sc,x,y)BetaAt(gsp_new_code_sign_extension,gsp_new_scale_sign_extension,x,y)Original native command in the exact edition
  2. L30
    specialize beta_prefix_extend l
  3. L31
    specialize beta_prefix_extend sb
  4. L32
    specialize beta_prefix_extend sc
  5. L33
    specialize beta_prefix_extend x2
  6. L34
    exact beta_prefix_extend
07Separate the logical casesL35–37

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

  1. L35
    cases hsign_extend
  2. L36
    cases hsign_extend_witness
  3. L37
    cases hsign_extend_witness_witness
08Construct an explicit witnessL38–41

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

  1. L38
    exists x3
  2. L39
    exists x4
  3. L40
    exists x5
  4. L41
    exists x6
09Fix variables and assumptionsL42–43

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

  1. L42
    intro i
  2. L43
    intro hi
10Establish hsplitL44–48

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L44
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L45
    specialize finite_lt_succ_eq_or_lt l
  3. L46
    specialize finite_lt_succ_eq_or_lt i
  4. L47
    apply finite_lt_succ_eq_or_lt
  5. L48
    exact hi
11Separate the logical casesL49–49

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

  1. L49
    cases hsplit
12Construct an explicit witnessL50–52

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

  1. L50
    exists x
  2. L51
    exists x1
  3. L52
    exists x2
13Separate the logical casesL53–53

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

  1. L53
    split
14Calculate and transport equalitiesL54–55

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L54
    rewrite hsplit_left
  2. L55
    rewrite hsplit_left
15Use earlier factsL56–56

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

  1. L56
    exact hchoice_witness_witness_witness_left
16Separate the logical casesL57–57

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

  1. L57
    split
17Calculate and transport equalitiesL58–59

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L58
    rewrite hsplit_left
  2. L59
    rewrite hsplit_left
18Use earlier factsL60–60

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

  1. L60
    exact hmag_extend_witness_witness_left
19Separate the logical casesL61–61

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

  1. L61
    split
20Calculate and transport equalitiesL62–63

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L62
    rewrite hsplit_left
  2. L63
    rewrite hsplit_left
21Use earlier factsL64–64

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

  1. L64
    exact hsign_extend_witness_witness_left
22Separate the logical casesL65–65

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

  1. L65
    split
23Use earlier factsL66–66

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

  1. L66
    exact hchoice_witness_witness_witness_right_left
24Separate the logical casesL67–67

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

  1. L67
    split
25Use earlier factsL68–68

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

  1. L68
    exact hchoice_witness_witness_witness_right_right_left
26Separate the logical casesL69–69

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

  1. L69
    split
27Use earlier factsL70–71

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

  1. L70
    exact hchoice_witness_witness_witness_right_right_right_left
  2. L71
    exact hchoice_witness_witness_witness_right_right_right_right
28Establish holdL72–75

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

  1. L72
    have hold · expand full local formula (692 characters)have hold : ∃ gsp_value_extend_previous_entry. ∃ gsp_magnitude_extend_previous_entry. ∃ gsp_sign_extend_previous_entry. BetaAt(b,c,i,gsp_value_extend_previous_entry) ∧ (BetaAt(mb,mc,i,gsp_magnitude_extend_previous_entry) ∧ (BetaAt(sb,sc,i,gsp_sign_extend_previous_entry) ∧ (Lt(0,gsp_magnitude_extend_previous_entry) ∧ (Le(gsp_magnitude_extend_previous_entry,h) ∧ ((gsp_sign_extend_previous_entry = 0 ∨ gsp_sign_extend_previous_entry = 1) ∧ (gsp_sign_extend_previous_entry = 0 ∧ ModEq(p,a · gsp_value_extend_previous_entry,gsp_magnitude_extend_previous_entry) ∨ gsp_sign_extend_previous_entry = 1 ∧ ModEq(p,a · gsp_value_extend_previous_entry,2 · h · gsp_magnitude_extend_previous_entry)))))))
    Definitions: BetaAt(b,c,i,gsp_value_extend_previous_entry)BetaAt(mb,mc,i,gsp_magnitude_extend_previous_entry)BetaAt(sb,sc,i,gsp_sign_extend_previous_entry)Lt(0,gsp_magnitude_extend_previous_entry)Le(gsp_magnitude_extend_previous_entry,h)ModEq(p,a · gsp_value_extend_previous_entry,gsp_magnitude_extend_previous_entry)ModEq(p,a · gsp_value_extend_previous_entry,2 · h · gsp_magnitude_extend_previous_entry)Original native command in the exact edition
  2. L73
    specialize hprefix i
  3. L74
    apply hprefix
  4. L75
    exact hsplit_right
29Separate the logical casesL76–84

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

  1. L76
    cases hold
  2. L77
    cases hold_witness
  3. L78
    cases hold_witness_witness
  4. L79
    cases hold_witness_witness_witness
  5. L80
    cases hold_witness_witness_witness_right
  6. L81
    cases hold_witness_witness_witness_right_right
  7. L82
    cases hold_witness_witness_witness_right_right_right
  8. L83
    cases hold_witness_witness_witness_right_right_right_right
  9. L84
    cases hold_witness_witness_witness_right_right_right_right_right
30Construct an explicit witnessL85–87

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

  1. L85
    exists x7
  2. L86
    exists x8
  3. L87
    exists x9
31Separate the logical casesL88–88

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

  1. L88
    split
32Use earlier factsL89–89

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

  1. L89
    exact hold_witness_witness_witness_left
33Separate the logical casesL90–90

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

  1. L90
    split
34Use earlier factsL91–95

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

  1. L91
    specialize hmag_extend_witness_witness_right i
  2. L92
    specialize hmag_extend_witness_witness_right x8
  3. L93
    apply hmag_extend_witness_witness_right
  4. L94
    exact hsplit_right
  5. L95
    exact hold_witness_witness_witness_right_left
35Separate the logical casesL96–96

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

  1. L96
    split
36Use earlier factsL97–101

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

  1. L97
    specialize hsign_extend_witness_witness_right i
  2. L98
    specialize hsign_extend_witness_witness_right x9
  3. L99
    apply hsign_extend_witness_witness_right
  4. L100
    exact hsplit_right
  5. L101
    exact hold_witness_witness_witness_right_right_left
37Separate the logical casesL102–102

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

  1. L102
    split
38Use earlier factsL103–103

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

  1. L103
    exact hold_witness_witness_witness_right_right_right_left
39Separate the logical casesL104–104

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

  1. L104
    split
40Use earlier factsL105–105

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

  1. L105
    exact hold_witness_witness_witness_right_right_right_right_left
41Separate the logical casesL106–106

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

  1. L106
    split
42Use earlier factsL107–108

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

  1. L107
    exact hold_witness_witness_witness_right_right_right_right_right_left
  2. L108
    exact hold_witness_witness_witness_right_right_right_right_right_right

Library-wide reading audit

Original defined command ledger · 108 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro mb
  7. 0007intro mc
  8. 0008intro sb
  9. 0009intro sc
  10. 0010intro l
  11. 0011intro hprefix
  12. 0012intro hchoice
  13. 0013cases hchoice
  14. 0014cases hchoice_witness
  15. 0015cases hchoice_witness_witness
  16. 0016cases hchoice_witness_witness_witness
  17. 0017cases hchoice_witness_witness_witness_right
  18. 0018cases hchoice_witness_witness_witness_right_right
  19. 0019cases hchoice_witness_witness_witness_right_right_right
  20. 0020have hmag_extend : ∃ gsp_new_code_magnitude_extension. ∃ gsp_new_scale_magnitude_extension. BetaAt(gsp_new_code_magnitude_extension,gsp_new_scale_magnitude_extension,l,x1) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(mb,mc,x,y) → BetaAt(gsp_new_code_magnitude_extension,gsp_new_scale_magnitude_extension,x,y))
    Exact native replay linehave hmag_extend : exists gsp_new_code_magnitude_extension gsp_new_scale_magnitude_extension. (((exists ff_h_gsp_magnitude_extension_new_last. ff_h_gsp_magnitude_extension_new_last + S (x1) = S ((S (l)) * gsp_new_scale_magnitude_extension)) /\ exists ff_q_gsp_magnitude_extension_new_last. gsp_new_code_magnitude_extension = ff_q_gsp_magnitude_extension_new_last * S ((S (l)) * gsp_new_scale_magnitude_extension) + (x1))) /\ forall gsp_old_index_magnitude_extension gsp_old_value_magnitude_extension. (exists gsp_lt_gap_magnitude_extension_old_bound. gsp_lt_gap_magnitude_extension_old_bound + S gsp_old_index_magnitude_extension = l) -> (((exists ff_h_gsp_magnitude_extension_old_entry. ff_h_gsp_magnitude_extension_old_entry + S (gsp_old_value_magnitude_extension) = S ((S (gsp_old_index_magnitude_extension)) * mc)) /\ exists ff_q_gsp_magnitude_extension_old_entry. mb = ff_q_gsp_magnitude_extension_old_entry * S ((S (gsp_old_index_magnitude_extension)) * mc) + (gsp_old_value_magnitude_extension))) -> (((exists ff_h_gsp_magnitude_extension_new_entry. ff_h_gsp_magnitude_extension_new_entry + S (gsp_old_value_magnitude_extension) = S ((S (gsp_old_index_magnitude_extension)) * gsp_new_scale_magnitude_extension)) /\ exists ff_q_gsp_magnitude_extension_new_entry. gsp_new_code_magnitude_extension = ff_q_gsp_magnitude_extension_new_entry * S ((S (gsp_old_index_magnitude_extension)) * gsp_new_scale_magnitude_extension) + (gsp_old_value_magnitude_extension)))
  21. 0021specialize beta_prefix_extend l
  22. 0022specialize beta_prefix_extend mb
  23. 0023specialize beta_prefix_extend mc
  24. 0024specialize beta_prefix_extend x1
  25. 0025exact beta_prefix_extend
  26. 0026cases hmag_extend
  27. 0027cases hmag_extend_witness
  28. 0028cases hmag_extend_witness_witness
  29. 0029have hsign_extend : ∃ gsp_new_code_sign_extension. ∃ gsp_new_scale_sign_extension. BetaAt(gsp_new_code_sign_extension,gsp_new_scale_sign_extension,l,x2) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(sb,sc,x,y) → BetaAt(gsp_new_code_sign_extension,gsp_new_scale_sign_extension,x,y))
    Exact native replay linehave hsign_extend : exists gsp_new_code_sign_extension gsp_new_scale_sign_extension. (((exists ff_h_gsp_sign_extension_new_last. ff_h_gsp_sign_extension_new_last + S (x2) = S ((S (l)) * gsp_new_scale_sign_extension)) /\ exists ff_q_gsp_sign_extension_new_last. gsp_new_code_sign_extension = ff_q_gsp_sign_extension_new_last * S ((S (l)) * gsp_new_scale_sign_extension) + (x2))) /\ forall gsp_old_index_sign_extension gsp_old_value_sign_extension. (exists gsp_lt_gap_sign_extension_old_bound. gsp_lt_gap_sign_extension_old_bound + S gsp_old_index_sign_extension = l) -> (((exists ff_h_gsp_sign_extension_old_entry. ff_h_gsp_sign_extension_old_entry + S (gsp_old_value_sign_extension) = S ((S (gsp_old_index_sign_extension)) * sc)) /\ exists ff_q_gsp_sign_extension_old_entry. sb = ff_q_gsp_sign_extension_old_entry * S ((S (gsp_old_index_sign_extension)) * sc) + (gsp_old_value_sign_extension))) -> (((exists ff_h_gsp_sign_extension_new_entry. ff_h_gsp_sign_extension_new_entry + S (gsp_old_value_sign_extension) = S ((S (gsp_old_index_sign_extension)) * gsp_new_scale_sign_extension)) /\ exists ff_q_gsp_sign_extension_new_entry. gsp_new_code_sign_extension = ff_q_gsp_sign_extension_new_entry * S ((S (gsp_old_index_sign_extension)) * gsp_new_scale_sign_extension) + (gsp_old_value_sign_extension)))
  30. 0030specialize beta_prefix_extend l
  31. 0031specialize beta_prefix_extend sb
  32. 0032specialize beta_prefix_extend sc
  33. 0033specialize beta_prefix_extend x2
  34. 0034exact beta_prefix_extend
  35. 0035cases hsign_extend
  36. 0036cases hsign_extend_witness
  37. 0037cases hsign_extend_witness_witness
  38. 0038exists x3
  39. 0039exists x4
  40. 0040exists x5
  41. 0041exists x6
  42. 0042intro i
  43. 0043intro hi
  44. 0044have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists gap. gap + S i = l
  45. 0045specialize finite_lt_succ_eq_or_lt l
  46. 0046specialize finite_lt_succ_eq_or_lt i
  47. 0047apply finite_lt_succ_eq_or_lt
  48. 0048exact hi
  49. 0049cases hsplit
  50. 0050exists x
  51. 0051exists x1
  52. 0052exists x2
  53. 0053split
  54. 0054rewrite hsplit_left
  55. 0055rewrite hsplit_left
  56. 0056exact hchoice_witness_witness_witness_left
  57. 0057split
  58. 0058rewrite hsplit_left
  59. 0059rewrite hsplit_left
  60. 0060exact hmag_extend_witness_witness_left
  61. 0061split
  62. 0062rewrite hsplit_left
  63. 0063rewrite hsplit_left
  64. 0064exact hsign_extend_witness_witness_left
  65. 0065split
  66. 0066exact hchoice_witness_witness_witness_right_left
  67. 0067split
  68. 0068exact hchoice_witness_witness_witness_right_right_left
  69. 0069split
  70. 0070exact hchoice_witness_witness_witness_right_right_right_left
  71. 0071exact hchoice_witness_witness_witness_right_right_right_right
  72. 0072have hold : ∃ gsp_value_extend_previous_entry. ∃ gsp_magnitude_extend_previous_entry. ∃ gsp_sign_extend_previous_entry. BetaAt(b,c,i,gsp_value_extend_previous_entry) ∧ (BetaAt(mb,mc,i,gsp_magnitude_extend_previous_entry) ∧ (BetaAt(sb,sc,i,gsp_sign_extend_previous_entry) ∧ (Lt(0,gsp_magnitude_extend_previous_entry) ∧ (Le(gsp_magnitude_extend_previous_entry,h) ∧ ((gsp_sign_extend_previous_entry = 0 ∨ gsp_sign_extend_previous_entry = 1) ∧ (gsp_sign_extend_previous_entry = 0 ∧ ModEq(p,a · gsp_value_extend_previous_entry,gsp_magnitude_extend_previous_entry) ∨ gsp_sign_extend_previous_entry = 1 ∧ ModEq(p,a · gsp_value_extend_previous_entry,2 · h · gsp_magnitude_extend_previous_entry)))))))
    Exact native replay linehave hold : exists gsp_value_extend_previous_entry gsp_magnitude_extend_previous_entry gsp_sign_extend_previous_entry. (((exists ff_h_gsp_extend_previous_entry_source. ff_h_gsp_extend_previous_entry_source + S (gsp_value_extend_previous_entry) = S ((S (i)) * c)) /\ exists ff_q_gsp_extend_previous_entry_source. b = ff_q_gsp_extend_previous_entry_source * S ((S (i)) * c) + (gsp_value_extend_previous_entry))) /\ ((((exists ff_h_gsp_extend_previous_entry_magnitude. ff_h_gsp_extend_previous_entry_magnitude + S (gsp_magnitude_extend_previous_entry) = S ((S (i)) * mc)) /\ exists ff_q_gsp_extend_previous_entry_magnitude. mb = ff_q_gsp_extend_previous_entry_magnitude * S ((S (i)) * mc) + (gsp_magnitude_extend_previous_entry))) /\ ((((exists ff_h_gsp_extend_previous_entry_sign. ff_h_gsp_extend_previous_entry_sign + S (gsp_sign_extend_previous_entry) = S ((S (i)) * sc)) /\ exists ff_q_gsp_extend_previous_entry_sign. sb = ff_q_gsp_extend_previous_entry_sign * S ((S (i)) * sc) + (gsp_sign_extend_previous_entry))) /\ ((exists gsp_lt_gap_extend_previous_entry_positive. gsp_lt_gap_extend_previous_entry_positive + S 0 = gsp_magnitude_extend_previous_entry) /\ ((exists gsp_le_gap_extend_previous_entry_bounded. gsp_le_gap_extend_previous_entry_bounded + gsp_magnitude_extend_previous_entry = h) /\ ((gsp_sign_extend_previous_entry = 0 \/ gsp_sign_extend_previous_entry = 1) /\ (((gsp_sign_extend_previous_entry = 0 /\ (exists gsp_mod_left_extend_previous_entry_lower gsp_mod_right_extend_previous_entry_lower. (a * gsp_value_extend_previous_entry) + p * gsp_mod_left_extend_previous_entry_lower = (gsp_magnitude_extend_previous_entry) + p * gsp_mod_right_extend_previous_entry_lower)) \/ (gsp_sign_extend_previous_entry = 1 /\ (exists gsp_mod_left_extend_previous_entry_reflected gsp_mod_right_extend_previous_entry_reflected. (a * gsp_value_extend_previous_entry) + p * gsp_mod_left_extend_previous_entry_reflected = ((2 * h) * gsp_magnitude_extend_previous_entry) + p * gsp_mod_right_extend_previous_entry_reflected)))))))))
  73. 0073specialize hprefix i
  74. 0074apply hprefix
  75. 0075exact hsplit_right
  76. 0076cases hold
  77. 0077cases hold_witness
  78. 0078cases hold_witness_witness
  79. 0079cases hold_witness_witness_witness
  80. 0080cases hold_witness_witness_witness_right
  81. 0081cases hold_witness_witness_witness_right_right
  82. 0082cases hold_witness_witness_witness_right_right_right
  83. 0083cases hold_witness_witness_witness_right_right_right_right
  84. 0084cases hold_witness_witness_witness_right_right_right_right_right
  85. 0085exists x7
  86. 0086exists x8
  87. 0087exists x9
  88. 0088split
  89. 0089exact hold_witness_witness_witness_left
  90. 0090split
  91. 0091specialize hmag_extend_witness_witness_right i
  92. 0092specialize hmag_extend_witness_witness_right x8
  93. 0093apply hmag_extend_witness_witness_right
  94. 0094exact hsplit_right
  95. 0095exact hold_witness_witness_witness_right_left
  96. 0096split
  97. 0097specialize hsign_extend_witness_witness_right i
  98. 0098specialize hsign_extend_witness_witness_right x9
  99. 0099apply hsign_extend_witness_witness_right
  100. 0100exact hsplit_right
  101. 0101exact hold_witness_witness_witness_right_right_left
  102. 0102split
  103. 0103exact hold_witness_witness_witness_right_right_right_left
  104. 0104split
  105. 0105exact hold_witness_witness_witness_right_right_right_right_left
  106. 0106split
  107. 0107exact hold_witness_witness_witness_right_right_right_right_right_left
  108. 0108exact hold_witness_witness_witness_right_right_right_right_right_right