PA009U

pair_order_double_succ_length

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

Normalize the two-entry successor length into the next doubled pair count.

Exact expanded PA statement

forall l m. l = m + m -> S (S l) = S m + S m

Structural proof guide

Generated structural guide

Normalize the two-entry successor length into the next doubled pair count.

Use the direct prerequisites add_succ_left as previously established PA formulas.

The proof proceeds by equality transport (1), certified simplification (1).

Referenced ingredients

PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA000E add_succ_left

Direct dependents

PA009V scaled_inverse_pair_order_paired_iteration 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 l
  2. 0002intro m
  3. 0003intro hl
  4. 0004rewrite hl
  5. 0005symm
  6. 0006simp [add_succ_left]