Exact expanded PA statement
forall b c n. (forall wpo_position_wpoi_zero_nonendpoint wpo_value_wpoi_zero_nonendpoint. (exists wpo_gap_wpoi_zero_nonendpoint_position_bound. wpo_gap_wpoi_zero_nonendpoint_position_bound + S (wpo_position_wpoi_zero_nonendpoint) = 0) -> (((exists wpo_beta_height_wpoi_zero_nonendpoint_entry. wpo_beta_height_wpoi_zero_nonendpoint_entry + S (wpo_value_wpoi_zero_nonendpoint) = S ((S (wpo_position_wpoi_zero_nonendpoint)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_nonendpoint_entry. b = wpo_beta_quotient_wpoi_zero_nonendpoint_entry * S ((S (wpo_position_wpoi_zero_nonendpoint)) * c) + (wpo_value_wpoi_zero_nonendpoint))) -> (~(wpo_value_wpoi_zero_nonendpoint = 0) /\ ~((S wpo_value_wpoi_zero_nonendpoint) = n)))Structural proof guide
Generated structural guide
The nonendpoint range invariant is vacuous on the empty prefix.
Use the direct prerequisites add_eq_zero_right, succ_ne_zero as previously established PA formulas.
The proof proceeds by case analysis (1), intermediate claims (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 Alpha-v16 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
- 0001
intro b - 0002
intro c - 0003
intro n - 0004
intro q - 0005
intro s - 0006
intro hq - 0007
intro hentry - 0008
exfalso - 0009
cases hq - 0010
have hsq : S q = 0 - 0011
specialize add_eq_zero_right x - 0012
specialize add_eq_zero_right (S q) - 0013
apply add_eq_zero_right - 0014
exact hq_witness - 0015
specialize succ_ne_zero q - 0016
apply succ_ne_zero - 0017
exact hsq