PA008U

scaled_orbit_closed_prefix_zero

Alpha v16 checked-use theorem · independently closed; not Stable

Shifted orbit closure is vacuous on an empty order prefix.

Exact expanded PA statement

forall u v b c. (forall espo_position_zero_closed espo_source_zero_closed espo_mate_zero_closed. (exists wpo_gap_zero_closed_position_bound. wpo_gap_zero_closed_position_bound + S (espo_position_zero_closed) = 0) -> (((exists wpo_beta_height_zero_closed_source_entry. wpo_beta_height_zero_closed_source_entry + S (espo_source_zero_closed) = S ((S (espo_position_zero_closed)) * c)) /\ exists wpo_beta_quotient_zero_closed_source_entry. b = wpo_beta_quotient_zero_closed_source_entry * S ((S (espo_position_zero_closed)) * c) + (espo_source_zero_closed))) -> (((exists wpo_beta_height_zero_closed_scaled_entry. wpo_beta_height_zero_closed_scaled_entry + S (S espo_mate_zero_closed) = S ((S (espo_source_zero_closed)) * v)) /\ exists wpo_beta_quotient_zero_closed_scaled_entry. u = wpo_beta_quotient_zero_closed_scaled_entry * S ((S (espo_source_zero_closed)) * v) + (S espo_mate_zero_closed))) -> exists espo_mate_position_zero_closed. ((exists wpo_gap_zero_closed_mate_bound. wpo_gap_zero_closed_mate_bound + S (espo_mate_position_zero_closed) = 0) /\ (((exists wpo_beta_height_zero_closed_mate_entry. wpo_beta_height_zero_closed_mate_entry + S (espo_mate_zero_closed) = S ((S (espo_mate_position_zero_closed)) * c)) /\ exists wpo_beta_quotient_zero_closed_mate_entry. b = wpo_beta_quotient_zero_closed_mate_entry * S ((S (espo_mate_position_zero_closed)) * c) + (espo_mate_zero_closed)))))

Structural proof guide

Generated structural guide

Shifted orbit closure is vacuous on an empty order 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

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero

Direct dependents

PA008X scaled_pair_order_state_zero

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.

  1. 0001intro u
  2. 0002intro v
  3. 0003intro b
  4. 0004intro c
  5. 0005intro q
  6. 0006intro s
  7. 0007intro t
  8. 0008intro hq
  9. 0009intro hsource
  10. 0010intro hscaled
  11. 0011exfalso
  12. 0012cases hq
  13. 0013have hsq : S q = 0
  14. 0014specialize add_eq_zero_right x
  15. 0015specialize add_eq_zero_right (S q)
  16. 0016apply add_eq_zero_right
  17. 0017exact hq_witness
  18. 0018specialize succ_ne_zero q
  19. 0019apply succ_ne_zero
  20. 0020exact hsq