PA004G

eq_decidable

Stable checked-use theorem · independently closed

Equality of natural numbers is constructively decidable.

Exact expanded PA statement

forall a b. a = b \/ ~(a = b)

Structural proof guide

Generated structural guide

Equality of natural numbers is constructively decidable.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by structural induction (3), case analysis (1).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA004H finite_contains_decidable PA004M finite_swap_last_bounded PA004N beta_prefix_swap_last_reflect PA005J mod_eq_decidable_from_remainders PA00A2 prime_two_or_terminal_odd_shape

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro a
  2. 0002induction a
  3. 0003intro b
  4. 0004induction b
  5. 0005left
  6. 0006refl
  7. 0007right
  8. 0008intro h
  9. 0009apply PA1
  10. 0010symm
  11. 0011exact h
  12. 0012intro b
  13. 0013induction b
  14. 0014right
  15. 0015intro h
  16. 0016apply PA1
  17. 0017exact h
  18. 0018specialize IH b
  19. 0019cases IH
  20. 0020left
  21. 0021congr
  22. 0022exact IH_left
  23. 0023right
  24. 0024intro h
  25. 0025apply IH_right
  26. 0026apply PA2
  27. 0027exact h