BT00XB

add_lt_add

Alpha body-checked · checked-use disabled

Strict inequalities add componentwise.

Exact expanded PA statement

forall a b c d. (exists bcf_lt_gap_b5alaa_left. bcf_lt_gap_b5alaa_left + S (a) = b) -> (exists bcf_lt_gap_b5alaa_right. bcf_lt_gap_b5alaa_right + S (c) = d) -> (exists bcf_lt_gap_b5alaa_result. bcf_lt_gap_b5alaa_result + S (a + c) = b + d)

Structural proof guide

Strict inequalities add componentwise.

Direct prerequisites: add_succ_left, add_shuffle_middle. The authored body proceeds by case analysis (2), equality transport (2).

Proof neighborhood

Direct dependencies

BT0001 add_succ_left BT00MY add_shuffle_middle

Direct dependents

BT00XG division_double_quotient_bit

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro hab
  6. 0006intro hcd
  7. 0007cases hab
  8. 0008cases hcd
  9. 0009exists S (x + x1)
  10. 0010rewrite <- hab_witness
  11. 0011rewrite <- hcd_witness
  12. 0012trans S ((x + x1) + S (a + c))
  13. 0013apply add_succ_left
  14. 0014trans S (S ((x + x1) + (a + c)))
  15. 0015congr
  16. 0016apply PA4
  17. 0017trans S (S ((x + a) + (x1 + c)))
  18. 0018congr
  19. 0019congr
  20. 0020apply add_shuffle_middle
  21. 0021trans S ((x + a) + S (x1 + c))
  22. 0022congr
  23. 0023symm
  24. 0024apply PA4
  25. 0025trans S ((x + a) + (x1 + S c))
  26. 0026congr
  27. 0027congr
  28. 0028refl
  29. 0029symm
  30. 0030apply PA4
  31. 0031trans S (x + a) + (x1 + S c)
  32. 0032symm
  33. 0033apply add_succ_left
  34. 0034congr
  35. 0035symm
  36. 0036apply PA4
  37. 0037refl