PA00D2

mod_two_cancel_middle

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

From x == q+x+s modulo two, cancel x and obtain 0 == q+s.

Exact expanded PA statement

forall x q s. (exists fspm_u_cancel_middle_input fspm_v_cancel_middle_input. (x) + 2 * fspm_u_cancel_middle_input = (q + x + s) + 2 * fspm_v_cancel_middle_input) -> (exists fspm_u_cancel_middle_result fspm_v_cancel_middle_result. (0) + 2 * fspm_u_cancel_middle_result = (q + s) + 2 * fspm_v_cancel_middle_result)

Structural proof guide

Generated structural guide

From x == q+x+s modulo two, cancel x and obtain 0 == q+s.

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

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

Referenced ingredients

PA00D1 mod_eq_add_cancel_left PA0009 add_assoc PA000F add_comm

Proof neighborhood

Direct dependencies

PA00D1 mod_eq_add_cancel_left PA0009 add_assoc PA000F add_comm

Direct dependents

PA00D3 gauss_eisenstein_terminal_cancel_magnitude_mod_two

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 x
  2. 0002intro q
  3. 0003intro s
  4. 0004intro hmod
  5. 0005have hreorder : q + x + s = x + (q + s)
  6. 0006simp [add_assoc, add_comm]
  7. 0007rewrite hreorder at hmod
  8. 0008specialize mod_eq_add_cancel_left 2
  9. 0009specialize mod_eq_add_cancel_left x
  10. 0010specialize mod_eq_add_cancel_left 0
  11. 0011specialize mod_eq_add_cancel_left (q + s)
  12. 0012apply mod_eq_add_cancel_left
  13. 0013have hxzero : x + 0 = x
  14. 0014apply PA3
  15. 0015rewrite hxzero
  16. 0016exact hmod