PA0090

euler_pair_iteration_previous_balance

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

Move the newest pair from stored count to remaining count.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Move the newest pair from stored count to remaining count.

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

The proof proceeds by certified simplification (1).

Referenced ingredients

PA000E add_succ_left PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA000E add_succ_left PA0009 add_assoc 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_assoc, add_comm]