PA0093 · theorem

finite_inverse_choice_prefix_extend

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

Append one chosen source preimage to a beta-coded inverse-choice 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

∀ b. ∀ c. ∀ l. ∀ z. ∀ d. ∀ k. ContainsPrefix(b,c,l,k) → (∀ x. Lt(x,k) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))) → ∃ x. ∃ y. ∀ n. Lt(n,S k) → ∃ m. BetaAt(x,y,n,m) ∧ (Lt(m,l) ∧ BetaAt(b,c,m,n))

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

PD0002 Lt PD0013 BetaAt PD0027 ContainsPrefix

9 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt

9 occurrences

Exact expanded native-PA statement
forall b c l z d k. (exists fp_i_extend_contains. ((exists fp_gap_extend_contains_index. fp_gap_extend_contains_index + S fp_i_extend_contains = l) /\ (((exists ff_h_extend_contains_entry. ff_h_extend_contains_entry + S (k) = S ((S (fp_i_extend_contains)) * c)) /\ exists ff_q_extend_contains_entry. b = ff_q_extend_contains_entry * S ((S (fp_i_extend_contains)) * c) + (k))))) -> (forall fom_value_extend_before. (exists fom_gap_extend_before_value_bound. fom_gap_extend_before_value_bound + S (fom_value_extend_before) = k) -> exists fom_index_extend_before. ((((exists fom_beta_height_extend_before_choice_entry. fom_beta_height_extend_before_choice_entry + S (fom_index_extend_before) = S ((S (fom_value_extend_before)) * d)) /\ exists fom_beta_quotient_extend_before_choice_entry. z = fom_beta_quotient_extend_before_choice_entry * S ((S (fom_value_extend_before)) * d) + (fom_index_extend_before))) /\ ((exists fom_gap_extend_before_index_bound. fom_gap_extend_before_index_bound + S (fom_index_extend_before) = l) /\ (((exists fom_beta_height_extend_before_source_entry. fom_beta_height_extend_before_source_entry + S (fom_value_extend_before) = S ((S (fom_index_extend_before)) * c)) /\ exists fom_beta_quotient_extend_before_source_entry. b = fom_beta_quotient_extend_before_source_entry * S ((S (fom_index_extend_before)) * c) + (fom_value_extend_before)))))) -> exists r s. (forall fom_value_extend_after. (exists fom_gap_extend_after_value_bound. fom_gap_extend_after_value_bound + S (fom_value_extend_after) = S k) -> exists fom_index_extend_after. ((((exists fom_beta_height_extend_after_choice_entry. fom_beta_height_extend_after_choice_entry + S (fom_index_extend_after) = S ((S (fom_value_extend_after)) * s)) /\ exists fom_beta_quotient_extend_after_choice_entry. r = fom_beta_quotient_extend_after_choice_entry * S ((S (fom_value_extend_after)) * s) + (fom_index_extend_after))) /\ ((exists fom_gap_extend_after_index_bound. fom_gap_extend_after_index_bound + S (fom_index_extend_after) = l) /\ (((exists fom_beta_height_extend_after_source_entry. fom_beta_height_extend_after_source_entry + S (fom_value_extend_after) = S ((S (fom_index_extend_after)) * c)) /\ exists fom_beta_quotient_extend_after_source_entry. b = fom_beta_quotient_extend_after_source_entry * S ((S (fom_index_extend_after)) * c) + (fom_value_extend_after))))))

Proof neighborhood

Direct theorem prerequisites

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct theorem dependents

PA0094 finite_inverse_choice_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

55 script commands · 22 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–8

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro z
  5. L5
    intro d
  6. L6
    intro k
  7. L7
    intro hcontains
  8. L8
    intro hchoice
02Separate the logical casesL9–10

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

  1. L9
    cases hcontains
  2. L10
    cases hcontains_witness
03Use earlier factsL11–14

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

  1. L11
    specialize beta_prefix_extend k
  2. L12
    specialize beta_prefix_extend z
  3. L13
    specialize beta_prefix_extend d
  4. L14
    specialize beta_prefix_extend x
04Separate the logical casesL15–17

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

  1. L15
    cases beta_prefix_extend
  2. L16
    cases beta_prefix_extend_witness
  3. L17
    cases beta_prefix_extend_witness_witness
05Construct an explicit witnessL18–19

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

  1. L18
    exists x1
  2. L19
    exists x2
06Fix variables and assumptionsL20–21

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

  1. L20
    intro y
  2. L21
    intro hy
07Establish hsplitL22–26

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. L22
    have hsplit : y = k ∨ Lt(y,k)Definitions: Lt(y,k)Original native command in the exact edition
  2. L23
    specialize finite_lt_succ_eq_or_lt k
  3. L24
    specialize finite_lt_succ_eq_or_lt y
  4. L25
    apply finite_lt_succ_eq_or_lt
  5. L26
    exact hy
08Separate the logical casesL27–27

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

  1. L27
    cases hsplit
09Construct an explicit witnessL28–28

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

  1. L28
    exists x
10Separate the logical casesL29–29

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

  1. L29
    split
11Calculate and transport equalitiesL30–31

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

  1. L30
    rewrite hsplit_left
  2. L31
    rewrite hsplit_left
12Establish hnew_entryL32–34

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

  1. L32
    have hnew_entry : BetaAt(x1,x2,k,x)Definitions: BetaAt(x1,x2,k,x)Original native command in the exact edition
  2. L33
    exact beta_prefix_extend_witness_witness_left
  3. L34
    exact hnew_entry
13Separate the logical casesL35–35

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

  1. L35
    split
14Use earlier factsL36–36

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

  1. L36
    exact hcontains_witness_left
15Calculate and transport equalitiesL37–38

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

  1. L37
    rewrite hsplit_left
  2. L38
    rewrite hsplit_left
16Use earlier factsL39–39

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

  1. L39
    exact hcontains_witness_right
17Establish holdL40–42

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

  1. L40
    have hold : ∀ fom_value_extend_old_result. Lt(fom_value_extend_old_result,k) → ∃ x. BetaAt(z,d,fom_value_extend_old_result,x) ∧ (Lt(x,l) ∧ BetaAt(b,c,x,fom_value_extend_old_result))Definitions: Lt(fom_value_extend_old_result,k)BetaAt(z,d,fom_value_extend_old_result,x)Lt(x,l)BetaAt(b,c,x,fom_value_extend_old_result)Original native command in the exact edition
  2. L41
    exact hchoice
  3. L42
    specialize hold y
18Establish hold_yL43–45

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

  1. L43
    have hold_y : ∃ i. BetaAt(z,d,y,i) ∧ (Lt(i,l) ∧ BetaAt(b,c,i,y))Definitions: BetaAt(z,d,y,i)Lt(i,l)BetaAt(b,c,i,y)Original native command in the exact edition
  2. L44
    apply hold
  3. L45
    exact hsplit_right
19Separate the logical casesL46–47

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

  1. L46
    cases hold_y
  2. L47
    cases hold_y_witness
20Construct an explicit witnessL48–48

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

  1. L48
    exists x3
21Separate the logical casesL49–49

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

  1. L49
    split
22Use earlier factsL50–55

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

  1. L50
    specialize beta_prefix_extend_witness_witness_right y
  2. L51
    specialize beta_prefix_extend_witness_witness_right x3
  3. L52
    apply beta_prefix_extend_witness_witness_right
  4. L53
    exact hsplit_right
  5. L54
    exact hold_y_witness_left
  6. L55
    exact hold_y_witness_right

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro z
  5. 0005intro d
  6. 0006intro k
  7. 0007intro hcontains
  8. 0008intro hchoice
  9. 0009cases hcontains
  10. 0010cases hcontains_witness
  11. 0011specialize beta_prefix_extend k
  12. 0012specialize beta_prefix_extend z
  13. 0013specialize beta_prefix_extend d
  14. 0014specialize beta_prefix_extend x
  15. 0015cases beta_prefix_extend
  16. 0016cases beta_prefix_extend_witness
  17. 0017cases beta_prefix_extend_witness_witness
  18. 0018exists x1
  19. 0019exists x2
  20. 0020intro y
  21. 0021intro hy
  22. 0022have hsplit : y = k ∨ Lt(y,k)
    Exact native replay linehave hsplit : y = k \/ exists h. h + S y = k
  23. 0023specialize finite_lt_succ_eq_or_lt k
  24. 0024specialize finite_lt_succ_eq_or_lt y
  25. 0025apply finite_lt_succ_eq_or_lt
  26. 0026exact hy
  27. 0027cases hsplit
  28. 0028exists x
  29. 0029split
  30. 0030rewrite hsplit_left
  31. 0031rewrite hsplit_left
  32. 0032have hnew_entry : BetaAt(x1,x2,k,x)
    Exact native replay linehave hnew_entry : ((exists fom_beta_height_extend_new_entry. fom_beta_height_extend_new_entry + S (x) = S ((S (k)) * x2)) /\ exists fom_beta_quotient_extend_new_entry. x1 = fom_beta_quotient_extend_new_entry * S ((S (k)) * x2) + (x))
  33. 0033exact beta_prefix_extend_witness_witness_left
  34. 0034exact hnew_entry
  35. 0035split
  36. 0036exact hcontains_witness_left
  37. 0037rewrite hsplit_left
  38. 0038rewrite hsplit_left
  39. 0039exact hcontains_witness_right
  40. 0040have hold : ∀ fom_value_extend_old_result. Lt(fom_value_extend_old_result,k) → ∃ x. BetaAt(z,d,fom_value_extend_old_result,x) ∧ (Lt(x,l) ∧ BetaAt(b,c,x,fom_value_extend_old_result))
    Exact native replay linehave hold : forall fom_value_extend_old_result. (exists fom_gap_extend_old_result_value_bound. fom_gap_extend_old_result_value_bound + S (fom_value_extend_old_result) = k) -> exists fom_index_extend_old_result. ((((exists fom_beta_height_extend_old_result_choice_entry. fom_beta_height_extend_old_result_choice_entry + S (fom_index_extend_old_result) = S ((S (fom_value_extend_old_result)) * d)) /\ exists fom_beta_quotient_extend_old_result_choice_entry. z = fom_beta_quotient_extend_old_result_choice_entry * S ((S (fom_value_extend_old_result)) * d) + (fom_index_extend_old_result))) /\ ((exists fom_gap_extend_old_result_index_bound. fom_gap_extend_old_result_index_bound + S (fom_index_extend_old_result) = l) /\ (((exists fom_beta_height_extend_old_result_source_entry. fom_beta_height_extend_old_result_source_entry + S (fom_value_extend_old_result) = S ((S (fom_index_extend_old_result)) * c)) /\ exists fom_beta_quotient_extend_old_result_source_entry. b = fom_beta_quotient_extend_old_result_source_entry * S ((S (fom_index_extend_old_result)) * c) + (fom_value_extend_old_result)))))
  41. 0041exact hchoice
  42. 0042specialize hold y
  43. 0043have hold_y : ∃ i. BetaAt(z,d,y,i) ∧ (Lt(i,l) ∧ BetaAt(b,c,i,y))
    Exact native replay linehave hold_y : exists i. (((exists h. h + S i = S ((S y) * d)) /\ exists q. z = q * S ((S y) * d) + i) /\ ((exists h. h + S i = l) /\ ((exists h. h + S y = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + y)))
  44. 0044apply hold
  45. 0045exact hsplit_right
  46. 0046cases hold_y
  47. 0047cases hold_y_witness
  48. 0048exists x3
  49. 0049split
  50. 0050specialize beta_prefix_extend_witness_witness_right y
  51. 0051specialize beta_prefix_extend_witness_witness_right x3
  52. 0052apply beta_prefix_extend_witness_witness_right
  53. 0053exact hsplit_right
  54. 0054exact hold_y_witness_left
  55. 0055exact hold_y_witness_right