PA0032

beta_range_entry_eq

Stable checked-use theorem · independently closed

A decoded entry of a Range prefix is its start plus its index.

Exact expanded PA statement

forall b c a l i x. (forall ff_i_entry. (exists ff_lt_entry_bound. ff_lt_entry_bound + S ff_i_entry = l) -> (((exists ff_h_entry_decoded. ff_h_entry_decoded + S (a + ff_i_entry) = S ((S (ff_i_entry)) * c)) /\ exists ff_q_entry_decoded. b = ff_q_entry_decoded * S ((S (ff_i_entry)) * c) + (a + ff_i_entry)))) -> (exists h. h + S i = l) -> (((exists ff_h_range_entry_x. ff_h_range_entry_x + S (x) = S ((S (i)) * c)) /\ exists ff_q_range_entry_x. b = ff_q_range_entry_x * S ((S (i)) * c) + (x))) -> x = a + i

Structural proof guide

Generated structural guide

A decoded entry of a Range prefix is its start plus its index.

Use the direct prerequisites beta_at_unique as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA0034 beta_half_range_entry_bounds PA003T beta_range_injective PA0065 factorial_succ_decompose PA006A beta_range_transport_entry PA007C gauss_signed_half_magnitude_injective PA007V gauss_predecessor_half_range_aligned PA008F beta_range_one_entry_eq_succ PA00A1 scaled_pair_order_successor_lift_product_is_factorial PA00BC pair_order_predecessor_range_two_successor_lift_aligned PA00BG beta_range_two_product_is_factorial_succ

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro b
  2. 0002intro c
  3. 0003intro a
  4. 0004intro l
  5. 0005intro i
  6. 0006intro x
  7. 0007intro hrange
  8. 0008intro hi
  9. 0009intro hx
  10. 0010have ha : ((exists h. h + S (a + i) = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + (a + i))
  11. 0011specialize hrange i
  12. 0012apply hrange
  13. 0013exact hi
  14. 0014specialize beta_at_unique b
  15. 0015specialize beta_at_unique c
  16. 0016specialize beta_at_unique i
  17. 0017specialize beta_at_unique x
  18. 0018specialize beta_at_unique (a + i)
  19. 0019apply beta_at_unique
  20. 0020exact hx
  21. 0021exact ha