Properties of Arithmetic Prover

Blank Forms

• COMMUTE
  • a + b → b + a
  • a * b → b * a
• ASSOCL
  • a + (b + c) → ( a + b ) + c
  • a * (b * c) → ( a * b ) * c
• ASSOCR
  • (a + b) + c → a + (b + c)
  • (a * b) * c → a * (b * c)

• DISTRIBUTE
  • a * (b + c) → (a * b) + (a * c)
• COLLECT
  • (a * b) + (a * c) → a * (b + c)

• A_IDENT
  • a → (a + 0)
• M_IDENT
  • a → (a * 1)
• COLLAPSE
  • (a + 0) → a
  • (a * 1) → a

• CREATE
  • 0 → (a - a)
  • 1 → (a / a), a ≠ 0
• CANCEL
  • (a - a) → 0
  • (a / a) → 1 , a ≠ 0
• INVERT
  • a - b → a + (-1 * b)
  • a + (-1 * b) → a - b
  • a / b → a * (1 / b)
  • a * (1 / b) → a / b

Exercises

• 1+(2+3) to (3+1)+2
• ((5*4)+3)+2 to (3+(4*5))+2
• (1+2)+(3+4) to (1+4)+(2+3)

• (x+y)*5 to (x*5)+(y*5)
• ((2*x)+(4*y))+(3*x) to ((2+3)*x)+(4*y)
• (7+3)*(r+s) to ((7*r)+(7*s))+((3*r)+(3*s))

• 3+(3*x) to 3*(x+1)
• (x*1)+y to ((y*1)+(0+x))
• (x+y)*(x+y) to ((x*x)+((1+1)*(x*y)))+(y*y)

• (x+2)*(x-2) to (x*x)-(2*2)
• (((x*x)+(3*x))+(3*x)) to (((x+3)*(x+3))-(3*3))
• ((a*b)/c) to (a*(b/c))
• ((1/a)*(1/b)) to (1/(a*b))
• ((a/b)/c) to (a/(b*c))
• ((a/b)*(c/d)) to ((a*c)/(b*d))