PA0091

euler_pair_iteration_step_short

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

Expose a strict-prefix witness whenever at least one pair remains.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Expose a strict-prefix witness whenever at least one pair remains.

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

The proof proceeds by certified simplification (1).

Referenced ingredients

PA000E add_succ_left PA000F add_comm

Proof neighborhood

Direct dependencies

PA000E add_succ_left PA000F add_comm

Direct dependents

PA009V scaled_inverse_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_comm]