PA0094 · theorem

finite_inverse_choice_prefix_exists

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

Full finite coverage admits a beta-coded choice of one preimage for each target value.

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. ∀ n. (∀ x. Lt(x,n) → ContainsPrefix(b,c,l,x)) → ∃ x. ∃ y. ∀ z. Lt(z,n) → ∃ m. BetaAt(x,y,z,m) ∧ (Lt(m,l) ∧ BetaAt(b,c,m,z))

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

6 occurrences

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0027 ContainsPrefix

13 occurrences

Exact expanded native-PA statement
forall b c l n. (forall fom_value_exists_cover. (exists fom_gap_exists_cover_value_bound. fom_gap_exists_cover_value_bound + S (fom_value_exists_cover) = n) -> exists fom_index_exists_cover. ((exists fom_gap_exists_cover_index_bound. fom_gap_exists_cover_index_bound + S (fom_index_exists_cover) = l) /\ (((exists fom_beta_height_exists_cover_entry. fom_beta_height_exists_cover_entry + S (fom_value_exists_cover) = S ((S (fom_index_exists_cover)) * c)) /\ exists fom_beta_quotient_exists_cover_entry. b = fom_beta_quotient_exists_cover_entry * S ((S (fom_index_exists_cover)) * c) + (fom_value_exists_cover))))) -> exists z d. (forall fom_value_exists_result. (exists fom_gap_exists_result_value_bound. fom_gap_exists_result_value_bound + S (fom_value_exists_result) = n) -> exists fom_index_exists_result. ((((exists fom_beta_height_exists_result_choice_entry. fom_beta_height_exists_result_choice_entry + S (fom_index_exists_result) = S ((S (fom_value_exists_result)) * d)) /\ exists fom_beta_quotient_exists_result_choice_entry. z = fom_beta_quotient_exists_result_choice_entry * S ((S (fom_value_exists_result)) * d) + (fom_index_exists_result))) /\ ((exists fom_gap_exists_result_index_bound. fom_gap_exists_result_index_bound + S (fom_index_exists_result) = l) /\ (((exists fom_beta_height_exists_result_source_entry. fom_beta_height_exists_result_source_entry + S (fom_value_exists_result) = S ((S (fom_index_exists_result)) * c)) /\ exists fom_beta_quotient_exists_result_source_entry. b = fom_beta_quotient_exists_result_source_entry * S ((S (fom_index_exists_result)) * c) + (fom_value_exists_result))))))

Proof neighborhood

Direct theorem prerequisites

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA002O le_succ PA001A le_refl PA0093 finite_inverse_choice_prefix_extend

Direct theorem dependents

PA0097 finite_short_cover_impossible

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

52 script commands · 13 reading checkpoints · 6 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 reflfinite inverse choice prefix extend
01Fix variables and assumptionsL1–3

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
02Induction on nL4–5

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

  1. L4
    induction n
  2. L5
    intro hcover
03Construct an explicit witnessL6–7

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

  1. L6
    exists 0
  2. L7
    exists 0
04Fix variables and assumptionsL8–9

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

  1. L8
    intro y
  2. L9
    intro hy
05Separate the logical casesL10–11

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

  1. L10
    exfalso
  2. L11
    cases hy
06Establish hsyL12–20

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

  1. L12
    have hsy : S y = 0
  2. L13
    specialize add_eq_zero_right x
  3. L14
    specialize add_eq_zero_right (S y)
  4. L15
    apply add_eq_zero_right
  5. L16
    exact hy_witness
  6. L17
    specialize succ_ne_zero y
  7. L18
    apply succ_ne_zero
  8. L19
    exact hsy
  9. L20
    intro hcover
07Establish hcover_allL21–22

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

  1. L21
    have hcover_all : ∀ fom_value_exists_successor_cover. Lt(fom_value_exists_successor_cover,S n) → ContainsPrefix(b,c,l,fom_value_exists_successor_cover)Definitions: Lt(fom_value_exists_successor_cover,S n)ContainsPrefix(b,c,l,fom_value_exists_successor_cover)Original native command in the exact edition
  2. L22
    exact hcover
08Establish hpastL23–31

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

  1. L23
    have hpast : ∀ fom_value_exists_previous_cover. Lt(fom_value_exists_previous_cover,n) → ContainsPrefix(b,c,l,fom_value_exists_previous_cover)Definitions: Lt(fom_value_exists_previous_cover,n)ContainsPrefix(b,c,l,fom_value_exists_previous_cover)Original native command in the exact edition
  2. L24
    intro y
  3. L25
    intro hy
  4. L26
    specialize hcover_all y
  5. L27
    apply hcover_all
  6. L28
    specialize le_succ (S y)
  7. L29
    specialize le_succ n
  8. L30
    apply le_succ
  9. L31
    exact hy
09Establish hpreviousL32–34

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

  1. L32
    have hprevious : ∃ z. ∃ d. ∀ x. Lt(x,n) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))Definitions: Lt(x,n)BetaAt(z,d,x,y)Lt(y,l)BetaAt(b,c,y,x)Original native command in the exact edition
  2. L33
    apply IH
  3. L34
    exact hpast
10Separate the logical casesL35–36

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

  1. L35
    cases hprevious
  2. L36
    cases hprevious_witness
11Establish htopL37–41

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

  1. L37
    have htop : ContainsPrefix(b,c,l,n)Definitions: ContainsPrefix(b,c,l,n)Original native command in the exact edition
  2. L38
    specialize hcover n
  3. L39
    apply hcover
  4. L40
    specialize le_refl (S n)
  5. L41
    exact le_refl
12Establish hnextL42–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite inverse choice prefix extend.

  1. L42
    have hnext : ∃ z. ∃ d. ∀ x. Lt(x,S n) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))Definitions: Lt(x,S n)BetaAt(z,d,x,y)Lt(y,l)BetaAt(b,c,y,x)Original native command in the exact edition
  2. L43
    specialize finite_inverse_choice_prefix_extend b
  3. L44
    specialize finite_inverse_choice_prefix_extend c
  4. L45
    specialize finite_inverse_choice_prefix_extend l
  5. L46
    specialize finite_inverse_choice_prefix_extend x
  6. L47
    specialize finite_inverse_choice_prefix_extend x1
  7. L48
    specialize finite_inverse_choice_prefix_extend n
  8. L49
    apply finite_inverse_choice_prefix_extend
  9. L50
    exact htop
  10. L51
    exact hprevious_witness_witness
13Use earlier factsL52–52

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

  1. L52
    exact hnext

Library-wide reading audit

Original defined command ledger · 52 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004induction n
  5. 0005intro hcover
  6. 0006exists 0
  7. 0007exists 0
  8. 0008intro y
  9. 0009intro hy
  10. 0010exfalso
  11. 0011cases hy
  12. 0012have hsy : S y = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S y)
  15. 0015apply add_eq_zero_right
  16. 0016exact hy_witness
  17. 0017specialize succ_ne_zero y
  18. 0018apply succ_ne_zero
  19. 0019exact hsy
  20. 0020intro hcover
  21. 0021have hcover_all : ∀ fom_value_exists_successor_cover. Lt(fom_value_exists_successor_cover,S n) → ContainsPrefix(b,c,l,fom_value_exists_successor_cover)
    Exact native replay linehave hcover_all : forall fom_value_exists_successor_cover. (exists fom_gap_exists_successor_cover_value_bound. fom_gap_exists_successor_cover_value_bound + S (fom_value_exists_successor_cover) = S n) -> exists fom_index_exists_successor_cover. ((exists fom_gap_exists_successor_cover_index_bound. fom_gap_exists_successor_cover_index_bound + S (fom_index_exists_successor_cover) = l) /\ (((exists fom_beta_height_exists_successor_cover_entry. fom_beta_height_exists_successor_cover_entry + S (fom_value_exists_successor_cover) = S ((S (fom_index_exists_successor_cover)) * c)) /\ exists fom_beta_quotient_exists_successor_cover_entry. b = fom_beta_quotient_exists_successor_cover_entry * S ((S (fom_index_exists_successor_cover)) * c) + (fom_value_exists_successor_cover))))
  22. 0022exact hcover
  23. 0023have hpast : ∀ fom_value_exists_previous_cover. Lt(fom_value_exists_previous_cover,n) → ContainsPrefix(b,c,l,fom_value_exists_previous_cover)
    Exact native replay linehave hpast : forall fom_value_exists_previous_cover. (exists fom_gap_exists_previous_cover_value_bound. fom_gap_exists_previous_cover_value_bound + S (fom_value_exists_previous_cover) = n) -> exists fom_index_exists_previous_cover. ((exists fom_gap_exists_previous_cover_index_bound. fom_gap_exists_previous_cover_index_bound + S (fom_index_exists_previous_cover) = l) /\ (((exists fom_beta_height_exists_previous_cover_entry. fom_beta_height_exists_previous_cover_entry + S (fom_value_exists_previous_cover) = S ((S (fom_index_exists_previous_cover)) * c)) /\ exists fom_beta_quotient_exists_previous_cover_entry. b = fom_beta_quotient_exists_previous_cover_entry * S ((S (fom_index_exists_previous_cover)) * c) + (fom_value_exists_previous_cover))))
  24. 0024intro y
  25. 0025intro hy
  26. 0026specialize hcover_all y
  27. 0027apply hcover_all
  28. 0028specialize le_succ (S y)
  29. 0029specialize le_succ n
  30. 0030apply le_succ
  31. 0031exact hy
  32. 0032have hprevious : ∃ z. ∃ d. ∀ x. Lt(x,n) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))
    Exact native replay linehave hprevious : exists z d. (forall fom_value_exists_previous_choice. (exists fom_gap_exists_previous_choice_value_bound. fom_gap_exists_previous_choice_value_bound + S (fom_value_exists_previous_choice) = n) -> exists fom_index_exists_previous_choice. ((((exists fom_beta_height_exists_previous_choice_choice_entry. fom_beta_height_exists_previous_choice_choice_entry + S (fom_index_exists_previous_choice) = S ((S (fom_value_exists_previous_choice)) * d)) /\ exists fom_beta_quotient_exists_previous_choice_choice_entry. z = fom_beta_quotient_exists_previous_choice_choice_entry * S ((S (fom_value_exists_previous_choice)) * d) + (fom_index_exists_previous_choice))) /\ ((exists fom_gap_exists_previous_choice_index_bound. fom_gap_exists_previous_choice_index_bound + S (fom_index_exists_previous_choice) = l) /\ (((exists fom_beta_height_exists_previous_choice_source_entry. fom_beta_height_exists_previous_choice_source_entry + S (fom_value_exists_previous_choice) = S ((S (fom_index_exists_previous_choice)) * c)) /\ exists fom_beta_quotient_exists_previous_choice_source_entry. b = fom_beta_quotient_exists_previous_choice_source_entry * S ((S (fom_index_exists_previous_choice)) * c) + (fom_value_exists_previous_choice))))))
  33. 0033apply IH
  34. 0034exact hpast
  35. 0035cases hprevious
  36. 0036cases hprevious_witness
  37. 0037have htop : ContainsPrefix(b,c,l,n)
    Exact native replay linehave htop : exists fp_i_exists_top_contains. ((exists fp_gap_exists_top_contains_index. fp_gap_exists_top_contains_index + S fp_i_exists_top_contains = l) /\ (((exists ff_h_exists_top_contains_entry. ff_h_exists_top_contains_entry + S (n) = S ((S (fp_i_exists_top_contains)) * c)) /\ exists ff_q_exists_top_contains_entry. b = ff_q_exists_top_contains_entry * S ((S (fp_i_exists_top_contains)) * c) + (n))))
  38. 0038specialize hcover n
  39. 0039apply hcover
  40. 0040specialize le_refl (S n)
  41. 0041exact le_refl
  42. 0042have hnext : ∃ z. ∃ d. ∀ x. Lt(x,S n) → ∃ y. BetaAt(z,d,x,y) ∧ (Lt(y,l) ∧ BetaAt(b,c,y,x))
    Exact native replay linehave hnext : exists z d. (forall fom_value_exists_successor_choice. (exists fom_gap_exists_successor_choice_value_bound. fom_gap_exists_successor_choice_value_bound + S (fom_value_exists_successor_choice) = S n) -> exists fom_index_exists_successor_choice. ((((exists fom_beta_height_exists_successor_choice_choice_entry. fom_beta_height_exists_successor_choice_choice_entry + S (fom_index_exists_successor_choice) = S ((S (fom_value_exists_successor_choice)) * d)) /\ exists fom_beta_quotient_exists_successor_choice_choice_entry. z = fom_beta_quotient_exists_successor_choice_choice_entry * S ((S (fom_value_exists_successor_choice)) * d) + (fom_index_exists_successor_choice))) /\ ((exists fom_gap_exists_successor_choice_index_bound. fom_gap_exists_successor_choice_index_bound + S (fom_index_exists_successor_choice) = l) /\ (((exists fom_beta_height_exists_successor_choice_source_entry. fom_beta_height_exists_successor_choice_source_entry + S (fom_value_exists_successor_choice) = S ((S (fom_index_exists_successor_choice)) * c)) /\ exists fom_beta_quotient_exists_successor_choice_source_entry. b = fom_beta_quotient_exists_successor_choice_source_entry * S ((S (fom_index_exists_successor_choice)) * c) + (fom_value_exists_successor_choice))))))
  43. 0043specialize finite_inverse_choice_prefix_extend b
  44. 0044specialize finite_inverse_choice_prefix_extend c
  45. 0045specialize finite_inverse_choice_prefix_extend l
  46. 0046specialize finite_inverse_choice_prefix_extend x
  47. 0047specialize finite_inverse_choice_prefix_extend x1
  48. 0048specialize finite_inverse_choice_prefix_extend n
  49. 0049apply finite_inverse_choice_prefix_extend
  50. 0050exact htop
  51. 0051exact hprevious_witness_witness
  52. 0052exact hnext