PA00A8

orbit_closed_prefix_zero

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

Orbit closure is vacuous on the empty decoded prefix.

Exact expanded PA statement

forall u v b c. (forall wpo_position_wpoi_zero_closed wpo_source_wpoi_zero_closed wpo_mate_wpoi_zero_closed. (exists wpo_gap_wpoi_zero_closed_position_bound. wpo_gap_wpoi_zero_closed_position_bound + S (wpo_position_wpoi_zero_closed) = 0) -> (((exists wpo_beta_height_wpoi_zero_closed_source_entry. wpo_beta_height_wpoi_zero_closed_source_entry + S (wpo_source_wpoi_zero_closed) = S ((S (wpo_position_wpoi_zero_closed)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_closed_source_entry. b = wpo_beta_quotient_wpoi_zero_closed_source_entry * S ((S (wpo_position_wpoi_zero_closed)) * c) + (wpo_source_wpoi_zero_closed))) -> (((exists wpo_beta_height_wpoi_zero_closed_inverse_entry. wpo_beta_height_wpoi_zero_closed_inverse_entry + S (wpo_mate_wpoi_zero_closed) = S ((S (wpo_source_wpoi_zero_closed)) * v)) /\ exists wpo_beta_quotient_wpoi_zero_closed_inverse_entry. u = wpo_beta_quotient_wpoi_zero_closed_inverse_entry * S ((S (wpo_source_wpoi_zero_closed)) * v) + (wpo_mate_wpoi_zero_closed))) -> exists wpo_mate_position_wpoi_zero_closed. ((exists wpo_gap_wpoi_zero_closed_mate_bound. wpo_gap_wpoi_zero_closed_mate_bound + S (wpo_mate_position_wpoi_zero_closed) = 0) /\ (((exists wpo_beta_height_wpoi_zero_closed_mate_entry. wpo_beta_height_wpoi_zero_closed_mate_entry + S (wpo_mate_wpoi_zero_closed) = S ((S (wpo_mate_position_wpoi_zero_closed)) * c)) /\ exists wpo_beta_quotient_wpoi_zero_closed_mate_entry. b = wpo_beta_quotient_wpoi_zero_closed_mate_entry * S ((S (wpo_mate_position_wpoi_zero_closed)) * c) + (wpo_mate_wpoi_zero_closed)))))

Structural proof guide

Generated structural guide

Orbit closure is vacuous on the empty decoded 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

PA00AA 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 m
  8. 0008intro hq
  9. 0009intro hsource
  10. 0010intro hinverse
  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