PA008F — beta_range_one_entry_eq

Exact expanded PA statement

forall b c l i x. (forall ff_i_frp_range_entry. (exists ff_lt_frp_range_entry_bound. ff_lt_frp_range_entry_bound + S ff_i_frp_range_entry = l) -> (((exists ff_h_frp_range_entry_decoded. ff_h_frp_range_entry_decoded + S (1 + ff_i_frp_range_entry) = S ((S (ff_i_frp_range_entry)) * c)) /\ exists ff_q_frp_range_entry_decoded. b = ff_q_frp_range_entry_decoded * S ((S (ff_i_frp_range_entry)) * c) + (1 + ff_i_frp_range_entry)))) -> (exists frp_gap_entry_bound. frp_gap_entry_bound + S i = l) -> (((exists ff_h_frp_entry. ff_h_frp_entry + S (x) = S ((S (i)) * c)) /\ exists ff_q_frp_entry. b = ff_q_frp_entry * S ((S (i)) * c) + (x))) -> x = S i

Structural proof guide

Generated structural guide

A decoded entry of the range 1,...,l is the successor of its index.

Use the direct prerequisites beta_range_entry_eq, add_succ_left, zero_add as previously established PA formulas.

The proof proceeds by intermediate claims (2).

Referenced ingredients

PA0032 beta_range_entry_eq PA000E add_succ_left PA0001 zero_add

Proof neighborhood

Direct dependencies

PA0032 beta_range_entry_eq PA000E add_succ_left PA0001 zero_add

Direct dependents

PA008G beta_successor_range_reindex_aligned PA008H beta_successor_range_scale_mod PA008K prime_range_product_coprime

Formal native tactic body

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