PA00AD

pair_order_iteration_step_room

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

Expose the exact one-orbit room equation in the successor case.

Exact expanded PA statement

forall m k. (k + k) + S (S (S m + S m)) = S (k + k) + S (S (S (m + m)))

Structural proof guide

Generated structural guide

Expose the exact one-orbit room equation in the successor case.

Use the direct prerequisites add_succ_left, add_assoc as previously established PA formulas.

The proof proceeds by certified simplification (1).

Referenced ingredients

PA000E add_succ_left PA0009 add_assoc

Proof neighborhood

Direct dependencies

PA000E add_succ_left PA0009 add_assoc

Direct dependents

PA00B1 prime_pair_order_paired_iteration

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 m
  2. 0002intro k
  3. 0003simp [add_succ_left, add_assoc]