PA00BX · theorem

beta_division_prefix_extend

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

Append one quotient/remainder pair while preserving the decoded prefix.

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. ∀ b. ∀ c. ∀ qb. ∀ qc. ∀ rb. ∀ rc. ∀ l. DivisionPrefix(p,b,c,qb,qc,rb,rc,l) → (∃ x. ∃ y. ∃ z. BetaAt(b,c,l,x) ∧ DivRem(x,p,y,z)) → ∃ x. ∃ y. ∃ z. ∃ n. DivisionPrefix(p,b,c,x,y,z,n,S l)

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

PD0007 DivRem PD0013 BetaAt PD0040 DivisionPrefix

4 occurrences

In local proof propositions

PD0002 Lt PD0007 DivRem PD0013 BetaAt

13 occurrences

Exact expanded native-PA statement
forall p b c qb qc rb rc l. (forall fdp_index_before. (exists gsp_lt_gap_before_index_bound. gsp_lt_gap_before_index_bound + S fdp_index_before = l) -> exists fdp_value_before fdp_quotient_before fdp_remainder_before. (((exists ff_h_fdp_before_source. ff_h_fdp_before_source + S (fdp_value_before) = S ((S (fdp_index_before)) * c)) /\ exists ff_q_fdp_before_source. b = ff_q_fdp_before_source * S ((S (fdp_index_before)) * c) + (fdp_value_before))) /\ ((((exists ff_h_fdp_before_quotient_entry. ff_h_fdp_before_quotient_entry + S (fdp_quotient_before) = S ((S (fdp_index_before)) * qc)) /\ exists ff_q_fdp_before_quotient_entry. qb = ff_q_fdp_before_quotient_entry * S ((S (fdp_index_before)) * qc) + (fdp_quotient_before))) /\ ((((exists ff_h_fdp_before_remainder_entry. ff_h_fdp_before_remainder_entry + S (fdp_remainder_before) = S ((S (fdp_index_before)) * rc)) /\ exists ff_q_fdp_before_remainder_entry. rb = ff_q_fdp_before_remainder_entry * S ((S (fdp_index_before)) * rc) + (fdp_remainder_before))) /\ (fdp_value_before = p * fdp_quotient_before + fdp_remainder_before /\ (exists gsp_lt_gap_before_remainder_bound. gsp_lt_gap_before_remainder_bound + S fdp_remainder_before = p))))) -> (exists x q r. (((exists ff_h_fdp_choice_source. ff_h_fdp_choice_source + S (x) = S ((S (l)) * c)) /\ exists ff_q_fdp_choice_source. b = ff_q_fdp_choice_source * S ((S (l)) * c) + (x))) /\ (x = p * q + r /\ (exists gsp_lt_gap_fdp_choice_remainder_bound. gsp_lt_gap_fdp_choice_remainder_bound + S r = p))) -> exists z d u v. (forall fdp_index_after. (exists gsp_lt_gap_after_index_bound. gsp_lt_gap_after_index_bound + S fdp_index_after = S l) -> exists fdp_value_after fdp_quotient_after fdp_remainder_after. (((exists ff_h_fdp_after_source. ff_h_fdp_after_source + S (fdp_value_after) = S ((S (fdp_index_after)) * c)) /\ exists ff_q_fdp_after_source. b = ff_q_fdp_after_source * S ((S (fdp_index_after)) * c) + (fdp_value_after))) /\ ((((exists ff_h_fdp_after_quotient_entry. ff_h_fdp_after_quotient_entry + S (fdp_quotient_after) = S ((S (fdp_index_after)) * d)) /\ exists ff_q_fdp_after_quotient_entry. z = ff_q_fdp_after_quotient_entry * S ((S (fdp_index_after)) * d) + (fdp_quotient_after))) /\ ((((exists ff_h_fdp_after_remainder_entry. ff_h_fdp_after_remainder_entry + S (fdp_remainder_after) = S ((S (fdp_index_after)) * v)) /\ exists ff_q_fdp_after_remainder_entry. u = ff_q_fdp_after_remainder_entry * S ((S (fdp_index_after)) * v) + (fdp_remainder_after))) /\ (fdp_value_after = p * fdp_quotient_after + fdp_remainder_after /\ (exists gsp_lt_gap_after_remainder_bound. gsp_lt_gap_after_remainder_bound + S fdp_remainder_after = p)))))

Proof neighborhood

Direct theorem prerequisites

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct theorem dependents

PA00BY beta_division_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

94 script commands · 33 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 b
  3. L3
    intro c
  4. L4
    intro qb
  5. L5
    intro qc
  6. L6
    intro rb
  7. L7
    intro rc
  8. L8
    intro l
  9. L9
    intro hprefix
  10. L10
    intro hchoice
02Separate the logical casesL11–15

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

  1. L11
    cases hchoice
  2. L12
    cases hchoice_witness
  3. L13
    cases hchoice_witness_witness
  4. L14
    cases hchoice_witness_witness_witness
  5. L15
    cases hchoice_witness_witness_witness_right
03Establish hqextendL16–21

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

  1. L16
    have hqextend : ∃ z. ∃ d. BetaAt(z,d,l,x1) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(qb,qc,x,y) → BetaAt(z,d,x,y))Definitions: BetaAt(z,d,l,x1)Lt(x,l)BetaAt(qb,qc,x,y)BetaAt(z,d,x,y)Original native command in the exact edition
  2. L17
    specialize beta_prefix_extend l
  3. L18
    specialize beta_prefix_extend qb
  4. L19
    specialize beta_prefix_extend qc
  5. L20
    specialize beta_prefix_extend x1
  6. L21
    exact beta_prefix_extend
04Separate the logical casesL22–24

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

  1. L22
    cases hqextend
  2. L23
    cases hqextend_witness
  3. L24
    cases hqextend_witness_witness
05Establish hrextendL25–30

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

  1. L25
    have hrextend : ∃ u. ∃ v. BetaAt(u,v,l,x2) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(rb,rc,x,y) → BetaAt(u,v,x,y))Definitions: BetaAt(u,v,l,x2)Lt(x,l)BetaAt(rb,rc,x,y)BetaAt(u,v,x,y)Original native command in the exact edition
  2. L26
    specialize beta_prefix_extend l
  3. L27
    specialize beta_prefix_extend rb
  4. L28
    specialize beta_prefix_extend rc
  5. L29
    specialize beta_prefix_extend x2
  6. L30
    exact beta_prefix_extend
06Separate the logical casesL31–33

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

  1. L31
    cases hrextend
  2. L32
    cases hrextend_witness
  3. L33
    cases hrextend_witness_witness
07Construct an explicit witnessL34–37

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

  1. L34
    exists x3
  2. L35
    exists x4
  3. L36
    exists x5
  4. L37
    exists x6
08Fix variables and assumptionsL38–39

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

  1. L38
    intro i
  2. L39
    intro hi
09Establish hsplitL40–44

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. L40
    have hsplit : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L41
    specialize finite_lt_succ_eq_or_lt l
  3. L42
    specialize finite_lt_succ_eq_or_lt i
  4. L43
    apply finite_lt_succ_eq_or_lt
  5. L44
    exact hi
10Separate the logical casesL45–45

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

  1. L45
    cases hsplit
11Construct an explicit witnessL46–48

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

  1. L46
    exists x
  2. L47
    exists x1
  3. L48
    exists x2
12Separate the logical casesL49–49

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

  1. L49
    split
13Calculate and transport equalitiesL50–51

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

  1. L50
    rewrite hsplit_left
  2. L51
    rewrite hsplit_left
14Use earlier factsL52–52

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

  1. L52
    exact hchoice_witness_witness_witness_left
15Separate the logical casesL53–53

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

  1. L53
    split
16Calculate 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
17Use earlier factsL56–56

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

  1. L56
    exact hqextend_witness_witness_left
18Separate the logical casesL57–57

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

  1. L57
    split
19Calculate 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
20Use earlier factsL60–60

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

  1. L60
    exact hrextend_witness_witness_left
21Separate the logical casesL61–61

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

  1. L61
    split
22Use earlier factsL62–63

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

  1. L62
    exact hchoice_witness_witness_witness_right_left
  2. L63
    exact hchoice_witness_witness_witness_right_right
23Establish holdL64–67

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

  1. L64
    have hold : ∃ x. ∃ q. ∃ r. BetaAt(b,c,i,x) ∧ (BetaAt(qb,qc,i,q) ∧ (BetaAt(rb,rc,i,r) ∧ DivRem(x,p,q,r)))Definitions: BetaAt(b,c,i,x)BetaAt(qb,qc,i,q)BetaAt(rb,rc,i,r)DivRem(x,p,q,r)Original native command in the exact edition
  2. L65
    specialize hprefix i
  3. L66
    apply hprefix
  4. L67
    exact hsplit_right
24Separate the logical casesL68–74

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

  1. L68
    cases hold
  2. L69
    cases hold_witness
  3. L70
    cases hold_witness_witness
  4. L71
    cases hold_witness_witness_witness
  5. L72
    cases hold_witness_witness_witness_right
  6. L73
    cases hold_witness_witness_witness_right_right
  7. L74
    cases hold_witness_witness_witness_right_right_right
25Construct an explicit witnessL75–77

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

  1. L75
    exists x7
  2. L76
    exists x8
  3. L77
    exists x9
26Separate the logical casesL78–78

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

  1. L78
    split
27Use earlier factsL79–79

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

  1. L79
    exact hold_witness_witness_witness_left
28Separate the logical casesL80–80

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

  1. L80
    split
29Use earlier factsL81–85

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

  1. L81
    specialize hqextend_witness_witness_right i
  2. L82
    specialize hqextend_witness_witness_right x8
  3. L83
    apply hqextend_witness_witness_right
  4. L84
    exact hsplit_right
  5. L85
    exact hold_witness_witness_witness_right_left
30Separate the logical casesL86–86

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

  1. L86
    split
31Use earlier factsL87–91

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

  1. L87
    specialize hrextend_witness_witness_right i
  2. L88
    specialize hrextend_witness_witness_right x9
  3. L89
    apply hrextend_witness_witness_right
  4. L90
    exact hsplit_right
  5. L91
    exact hold_witness_witness_witness_right_right_left
32Separate the logical casesL92–92

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

  1. L92
    split
33Use earlier factsL93–94

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

  1. L93
    exact hold_witness_witness_witness_right_right_right_left
  2. L94
    exact hold_witness_witness_witness_right_right_right_right

Library-wide reading audit

Original defined command ledger · 94 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro qb
  5. 0005intro qc
  6. 0006intro rb
  7. 0007intro rc
  8. 0008intro l
  9. 0009intro hprefix
  10. 0010intro hchoice
  11. 0011cases hchoice
  12. 0012cases hchoice_witness
  13. 0013cases hchoice_witness_witness
  14. 0014cases hchoice_witness_witness_witness
  15. 0015cases hchoice_witness_witness_witness_right
  16. 0016have hqextend : ∃ z. ∃ d. BetaAt(z,d,l,x1) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(qb,qc,x,y) → BetaAt(z,d,x,y))
    Exact native replay linehave hqextend : exists z d. (((exists ff_h_fdp_quotient_extension_last. ff_h_fdp_quotient_extension_last + S (x1) = S ((S (l)) * d)) /\ exists ff_q_fdp_quotient_extension_last. z = ff_q_fdp_quotient_extension_last * S ((S (l)) * d) + (x1))) /\ forall i q0. (exists gsp_lt_gap_fdp_quotient_extension_old_bound. gsp_lt_gap_fdp_quotient_extension_old_bound + S i = l) -> (((exists ff_h_fdp_quotient_extension_old_source. ff_h_fdp_quotient_extension_old_source + S (q0) = S ((S (i)) * qc)) /\ exists ff_q_fdp_quotient_extension_old_source. qb = ff_q_fdp_quotient_extension_old_source * S ((S (i)) * qc) + (q0))) -> (((exists ff_h_fdp_quotient_extension_old_target_symbolic. ff_h_fdp_quotient_extension_old_target_symbolic + S (q0) = S ((S (i)) * d)) /\ exists ff_q_fdp_quotient_extension_old_target_symbolic. z = ff_q_fdp_quotient_extension_old_target_symbolic * S ((S (i)) * d) + (q0)))
  17. 0017specialize beta_prefix_extend l
  18. 0018specialize beta_prefix_extend qb
  19. 0019specialize beta_prefix_extend qc
  20. 0020specialize beta_prefix_extend x1
  21. 0021exact beta_prefix_extend
  22. 0022cases hqextend
  23. 0023cases hqextend_witness
  24. 0024cases hqextend_witness_witness
  25. 0025have hrextend : ∃ u. ∃ v. BetaAt(u,v,l,x2) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(rb,rc,x,y) → BetaAt(u,v,x,y))
    Exact native replay linehave hrextend : exists u v. (((exists ff_h_fdp_remainder_extension_last. ff_h_fdp_remainder_extension_last + S (x2) = S ((S (l)) * v)) /\ exists ff_q_fdp_remainder_extension_last. u = ff_q_fdp_remainder_extension_last * S ((S (l)) * v) + (x2))) /\ forall i r0. (exists gsp_lt_gap_fdp_remainder_extension_old_bound. gsp_lt_gap_fdp_remainder_extension_old_bound + S i = l) -> (((exists ff_h_fdp_remainder_extension_old_source. ff_h_fdp_remainder_extension_old_source + S (r0) = S ((S (i)) * rc)) /\ exists ff_q_fdp_remainder_extension_old_source. rb = ff_q_fdp_remainder_extension_old_source * S ((S (i)) * rc) + (r0))) -> (((exists ff_h_fdp_remainder_extension_old_target. ff_h_fdp_remainder_extension_old_target + S (r0) = S ((S (i)) * v)) /\ exists ff_q_fdp_remainder_extension_old_target. u = ff_q_fdp_remainder_extension_old_target * S ((S (i)) * v) + (r0)))
  26. 0026specialize beta_prefix_extend l
  27. 0027specialize beta_prefix_extend rb
  28. 0028specialize beta_prefix_extend rc
  29. 0029specialize beta_prefix_extend x2
  30. 0030exact beta_prefix_extend
  31. 0031cases hrextend
  32. 0032cases hrextend_witness
  33. 0033cases hrextend_witness_witness
  34. 0034exists x3
  35. 0035exists x4
  36. 0036exists x5
  37. 0037exists x6
  38. 0038intro i
  39. 0039intro hi
  40. 0040have hsplit : i = l ∨ Lt(i,l)
    Exact native replay linehave hsplit : i = l \/ exists gap. gap + S i = l
  41. 0041specialize finite_lt_succ_eq_or_lt l
  42. 0042specialize finite_lt_succ_eq_or_lt i
  43. 0043apply finite_lt_succ_eq_or_lt
  44. 0044exact hi
  45. 0045cases hsplit
  46. 0046exists x
  47. 0047exists x1
  48. 0048exists x2
  49. 0049split
  50. 0050rewrite hsplit_left
  51. 0051rewrite hsplit_left
  52. 0052exact hchoice_witness_witness_witness_left
  53. 0053split
  54. 0054rewrite hsplit_left
  55. 0055rewrite hsplit_left
  56. 0056exact hqextend_witness_witness_left
  57. 0057split
  58. 0058rewrite hsplit_left
  59. 0059rewrite hsplit_left
  60. 0060exact hrextend_witness_witness_left
  61. 0061split
  62. 0062exact hchoice_witness_witness_witness_right_left
  63. 0063exact hchoice_witness_witness_witness_right_right
  64. 0064have hold : ∃ x. ∃ q. ∃ r. BetaAt(b,c,i,x) ∧ (BetaAt(qb,qc,i,q) ∧ (BetaAt(rb,rc,i,r) ∧ DivRem(x,p,q,r)))
    Exact native replay linehave hold : exists x q r. (((exists ff_h_fdp_previous_source. ff_h_fdp_previous_source + S (x) = S ((S (i)) * c)) /\ exists ff_q_fdp_previous_source. b = ff_q_fdp_previous_source * S ((S (i)) * c) + (x))) /\ ((((exists ff_h_fdp_previous_quotient. ff_h_fdp_previous_quotient + S (q) = S ((S (i)) * qc)) /\ exists ff_q_fdp_previous_quotient. qb = ff_q_fdp_previous_quotient * S ((S (i)) * qc) + (q))) /\ ((((exists ff_h_fdp_previous_remainder. ff_h_fdp_previous_remainder + S (r) = S ((S (i)) * rc)) /\ exists ff_q_fdp_previous_remainder. rb = ff_q_fdp_previous_remainder * S ((S (i)) * rc) + (r))) /\ (x = p * q + r /\ (exists gsp_lt_gap_fdp_previous_remainder_bound. gsp_lt_gap_fdp_previous_remainder_bound + S r = p))))
  65. 0065specialize hprefix i
  66. 0066apply hprefix
  67. 0067exact hsplit_right
  68. 0068cases hold
  69. 0069cases hold_witness
  70. 0070cases hold_witness_witness
  71. 0071cases hold_witness_witness_witness
  72. 0072cases hold_witness_witness_witness_right
  73. 0073cases hold_witness_witness_witness_right_right
  74. 0074cases hold_witness_witness_witness_right_right_right
  75. 0075exists x7
  76. 0076exists x8
  77. 0077exists x9
  78. 0078split
  79. 0079exact hold_witness_witness_witness_left
  80. 0080split
  81. 0081specialize hqextend_witness_witness_right i
  82. 0082specialize hqextend_witness_witness_right x8
  83. 0083apply hqextend_witness_witness_right
  84. 0084exact hsplit_right
  85. 0085exact hold_witness_witness_witness_right_left
  86. 0086split
  87. 0087specialize hrextend_witness_witness_right i
  88. 0088specialize hrextend_witness_witness_right x9
  89. 0089apply hrextend_witness_witness_right
  90. 0090exact hsplit_right
  91. 0091exact hold_witness_witness_witness_right_right_left
  92. 0092split
  93. 0093exact hold_witness_witness_witness_right_right_right_left
  94. 0094exact hold_witness_witness_witness_right_right_right_right