PA004L

finite_bounded_entry_lt

Stable checked-use theorem · independently closed

Every explicitly decoded entry of a bounded prefix satisfies its value bound.

Exact expanded PA statement

forall b c l i x. (forall fp_i_entry_bound. (exists fp_gap_entry_bound_index. fp_gap_entry_bound_index + S fp_i_entry_bound = l) -> exists fp_value_entry_bound. ((((exists ff_h_entry_bound_entry. ff_h_entry_bound_entry + S (fp_value_entry_bound) = S ((S (fp_i_entry_bound)) * c)) /\ exists ff_q_entry_bound_entry. b = ff_q_entry_bound_entry * S ((S (fp_i_entry_bound)) * c) + (fp_value_entry_bound))) /\ (exists fp_gap_entry_bound_value. fp_gap_entry_bound_value + S fp_value_entry_bound = l))) -> (exists h. h + S i = l) -> (((exists ff_h_entry_bound_at. ff_h_entry_bound_at + S (x) = S ((S (i)) * c)) /\ exists ff_q_entry_bound_at. b = ff_q_entry_bound_at * S ((S (i)) * c) + (x))) -> exists h. h + S x = l

Structural proof guide

Generated structural guide

Every explicitly decoded entry of a bounded prefix satisfies its value bound.

Use the direct prerequisites beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (2), intermediate claims (2), equality transport (1).

Referenced ingredients

PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002F beta_at_unique

Direct dependents

PA004M finite_swap_last_bounded

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 l
  4. 0004intro i
  5. 0005intro x
  6. 0006intro hbounded
  7. 0007intro hi
  8. 0008intro hentry
  9. 0009specialize hbounded i
  10. 0010have hdecoded : exists a. (((exists h. h + S a = S ((S i) * c)) /\ exists q. b = q * S ((S i) * c) + a) /\ exists h. h + S a = l)
  11. 0011apply hbounded
  12. 0012exact hi
  13. 0013cases hdecoded
  14. 0014cases hdecoded_witness
  15. 0015have hxa : x = x1
  16. 0016specialize beta_at_unique b
  17. 0017specialize beta_at_unique c
  18. 0018specialize beta_at_unique i
  19. 0019specialize beta_at_unique x
  20. 0020specialize beta_at_unique x1
  21. 0021apply beta_at_unique
  22. 0022exact hentry
  23. 0023exact hdecoded_witness_left
  24. 0024rewrite hxa
  25. 0025exact hdecoded_witness_right