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))) -> exists a. ((((exists ff_h_last. ff_h_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_last. b = ff_q_last * S ((S (l)) * c) + (a))) /\ (a = 0 \/ a = 1))Structural proof guide
The final entry of a nonempty all-bits prefix is zero or one.
Direct prerequisites: le_refl. The authored body proceeds by equality transport (1).
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.