Exact expanded PA statement
forall b c m. (exists f g. (forall wsl_index_wsl_lift wsl_value_wsl_lift. (exists wpo_gap_wsl_lift_bound. wpo_gap_wsl_lift_bound + S (wsl_index_wsl_lift) = m + m) -> (((exists wpo_beta_height_wsl_lift_source. wpo_beta_height_wsl_lift_source + S (wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * c)) /\ exists wpo_beta_quotient_wsl_lift_source. b = wpo_beta_quotient_wsl_lift_source * S ((S (wsl_index_wsl_lift)) * c) + (wsl_value_wsl_lift))) -> (((exists wpo_beta_height_wsl_lift_target. wpo_beta_height_wsl_lift_target + S (S wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * g)) /\ exists wpo_beta_quotient_wsl_lift_target. f = wpo_beta_quotient_wsl_lift_target * S ((S (wsl_index_wsl_lift)) * g) + (S wsl_value_wsl_lift)))))Structural proof guide
Generated structural guide
Every zero-based pair order has a beta code of successor-valued factors.
Use the direct prerequisites beta_successor_lift_exists as previously established PA formulas.
The proof proceeds by direct introduction and elimination.
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 Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.