Exact expanded PA statement
forall b c l sl. sl = S l -> (forall ff_i_successor. (exists ff_lt_successor_bound. ff_lt_successor_bound + S ff_i_successor = sl) -> exists ff_bit_successor. ((((exists ff_h_successor_decoded. ff_h_successor_decoded + S (ff_bit_successor) = S ((S (ff_i_successor)) * c)) /\ exists ff_q_successor_decoded. b = ff_q_successor_decoded * S ((S (ff_i_successor)) * c) + (ff_bit_successor))) /\ (ff_bit_successor = 0 \/ ff_bit_successor = 1))) -> (forall ff_i_prefix. (exists ff_lt_prefix_bound. ff_lt_prefix_bound + S ff_i_prefix = l) -> exists ff_bit_prefix. ((((exists ff_h_prefix_decoded. ff_h_prefix_decoded + S (ff_bit_prefix) = S ((S (ff_i_prefix)) * c)) /\ exists ff_q_prefix_decoded. b = ff_q_prefix_decoded * S ((S (ff_i_prefix)) * c) + (ff_bit_prefix))) /\ (ff_bit_prefix = 0 \/ ff_bit_prefix = 1)))Structural proof guide
Generated structural guide
Dropping the final entry preserves the all-bits invariant.
Use the direct prerequisites le_succ as previously established PA formulas.
The proof proceeds by equality transport (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
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.