PA009Q

pair_index_left_below_double

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

The left position of an earlier pair lies below the doubled prefix.

Exact expanded PA statement

forall t m. (exists h. h + S t = m) -> exists h. h + S (t + t) = m + m

Structural proof guide

Generated structural guide

The left position of an earlier pair lies below the doubled prefix.

Use the direct prerequisites lt_to_le, add_le_add_right, add_le_add_left, le_trans, add_succ_left as previously established PA formulas.

The proof proceeds by intermediate claims (4), equality transport (1).

Referenced ingredients

PA000X lt_to_le PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA000X lt_to_le PA003J add_le_add_right PA003K add_le_add_left PA000R le_trans PA000E add_succ_left

Direct dependents

PA009S adjacent_scaled_orbit_history_append PA009X scaled_pair_order_successor_lift_adjacent_targets PA00AY paired_inverse_witness_append PA00B7 paired_successor_lift_adjacent_units

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 t
  2. 0002intro m
  3. 0003intro htm
  4. 0004have htle : exists h. h + t = m
  5. 0005specialize lt_to_le t
  6. 0006specialize lt_to_le m
  7. 0007apply lt_to_le
  8. 0008exact htm
  9. 0009have hfirst : exists h. h + (S t + t) = m + t
  10. 0010specialize add_le_add_right (S t)
  11. 0011specialize add_le_add_right m
  12. 0012specialize add_le_add_right t
  13. 0013apply add_le_add_right
  14. 0014exact htm
  15. 0015have hsingle : S t + t = S (t + t)
  16. 0016specialize add_succ_left t
  17. 0017specialize add_succ_left t
  18. 0018exact add_succ_left
  19. 0019rewrite hsingle at hfirst
  20. 0020have hsecond : exists h. h + (m + t) = m + m
  21. 0021specialize add_le_add_left t
  22. 0022specialize add_le_add_left m
  23. 0023specialize add_le_add_left m
  24. 0024apply add_le_add_left
  25. 0025exact htle
  26. 0026specialize le_trans (S (t + t))
  27. 0027specialize le_trans (m + t)
  28. 0028specialize le_trans (m + m)
  29. 0029apply le_trans
  30. 0030exact hfirst
  31. 0031exact hsecond