## Suggestion Box: The Evaluate Button

The suggestion box contains a button that can automatically evaluate many different kinds of expressions.

• Add (+ (+ (* (10) (10)) (+ (* (6) (10)) (5))) (+ (* (4) (10)) (7))) to the proof stack as explained in the previous tutorial starting from an empty theorem.
• Click "Evaluate" in the suggestion box:

A proof will then be automatically generated that (+ (+ (* (10) (10)) (+ (* (6) (10)) (5))) (+ (* (4) (10)) (7))) /edit/peano/arithmetic.gh/additionExample. The evaluate button works on many different operations. If you give it a true statement like (< (2) (4)), it will generate a proof that (< (2) (4)). If you give it a false statement like (< (4) (2)), it will generate a proof that (< (4) (2)) is false. Below are a list of theorems that were automatically generated using the evaluate button. The left side contains a link to each proof. The right side contains the expression you would type into the editor to generate that proof. Remember that you can use the Add button to help you enter in the formulas.

### Numeric Calculations

• (+ (+ (* (10) (10)) (+ (* (6) (10)) (5))) (+ (* (4) (10)) (7))) /edit/peano/arithmetic.gh/additionExample _______________ (+ (+ (* (10) (10)) (+ (* (6) (10)) (5))) (+ (* (4) (10)) (7)))
• (* (+ (10) (7))(+ (10) (3))) /edit/peano/arithmetic.gh/multiplicationExample _________________ (* (+ (10) (7))(+ (10) (3)))
• (mod (+ (* (3) (* (10) (10))) (+ (* (6) (10)) (7))) (+ (10) (5))) /edit/peano/arithmetic.gh/modExample ____________ (mod (+ (* (3) (* (10) (10))) (+ (* (6) (10)) (7))) (+ (10) (5)))
• (div (+ (* (3) (* (10) (10))) (+ (* (9) (10)) (1))) (+ (* (2) (10)) (3))) /edit/peano/arithmetic.gh/divExample ___________________ (div (+ (* (3) (* (10) (10))) (+ (* (9) (10)) (1))) (+ (* (2) (10)) (3)))
• (.- (+ (* (2) (* (10) (10))) (+ (* (4) (10)) (3))) (+ (* (10) (10)) (+ (* (8) (10)) (6)))) /edit/peano/arithmetic.gh/halfMinusExample ______________ (.- (+ (* (2) (* (10) (10))) (+ (* (4) (10)) (3))) (+ (* (10) (10)) (+ (* (8) (10)) (6))))
• (exp (6) (4)) /edit/peano/arithmetic.gh/exponentExample ____________________ (exp (6) (4))
• (! (9)) /edit/peano/arithmetic.gh/factorialExample _____________________ (! (9))
• (sum (5) (7) (lambda x (+ (exp x (2)) (* (3) x)))) /edit/peano/arithmetic.gh/sumExample __________ (sum (5) (7) (lambda x (+ (exp x (2)) (* (3) x))))
• (product (1) (3) (lambda x (+ (* (2) x) (3)))) /edit/peano/arithmetic.gh/productExample ___________ (product (1) (3) (lambda x (+ (* (2) x) (3))))

### Proving True or False Statements

• (-. (= (+ (10) (8)) (+ (* (6) (10)) (7)))) /edit/peano/arithmetic.gh/notEqualExample ___________________ (= (+ (10) (8)) (+ (* (6) (10)) (7)))
• (< (+ (* (2) (10)) (6)) (+ (* (7) (* (10) (10))) (+ (* (3) (10)) (9)))) /edit/peano/arithmetic.gh/lessThanExample __________________ (< (+ (* (2) (10)) (6)) (+ (* (7) (* (10) (10))) (+ (* (3) (10)) (9))))
• (> (+ (* (3) (* (10) (10))) (* (4) (10))) (+ (* (8) (10)) (1))) /edit/peano/arithmetic.gh/greaterThanExample __________________ (> (+ (* (3) (* (10) (10))) (* (4) (10))) (+ (* (8) (10)) (1)))
• (-. (| (7) (+ (* (2) (10)) (2)))) /edit/peano/arithmetic.gh/notDividesExample _____________________ (| (7) (+ (* (2) (10)) (2)))
• (| (7) (+ (* (3) (* (10) (10))) (+ (* (4) (10)) (3)))) /edit/peano/arithmetic.gh/dividesExample _____________________ (| (7) (+ (* (3) (* (10) (10))) (+ (* (4) (10)) (3))))
• (-. (prime (+ (* (4) (10)) (2)))) /edit/peano/arithmetic.gh/notPrimeExample _____________ (prime (+ (* (4) (10)) (2)))

### Set Calculations

• (e. (3) (u. (u. (u. (u. ({} (1)) ({} (2))) ({} (3))) ({} (4))) ({} (5)))) /edit/peano/arithmetic.gh/elementOfExample ___________ (e. (3) (u. (u. (u. (u. ({} (1)) ({} (2))) ({} (3))) ({} (4))) ({} (5))))
• (-. (e. (3) (u. (u. (u. ({} (1)) ({} (2))) ({} (4))) ({} (5))))) /edit/peano/arithmetic.gh/notElementOfExample _____________ (e. (3) (u. (u. (u. ({} (1)) ({} (2))) ({} (4))) ({} (5))))
• (C. (u. ({} (2)) ({} (4))) (u. (u. (u. ({} (1)) ({} (2))) ({} (4))) ({} (5)))) /edit/peano/arithmetic.gh/properSubsetExample _________ (C. (u. ({} (2)) ({} (4))) (u. (u. (u. ({} (1)) ({} (2))) ({} (4))) ({} (5))))
• (-. (C_ (u. (u. ({} (1)) ({} (3))) ({} (4))) (u. (u. (u. ({} (1)) ({} (2))) ({} (3))) ({} (5))))) /edit/peano/arithmetic.gh/notSubsetExample _______ (C_ (u. (u. ({} (1)) ({} (3))) ({} (4))) (u. (u. (u. ({} (1)) ({} (2))) ({} (3))) ({} (5))))
• (u. (u. (u. ({} (1)) ({} (4))) ({} (5))) (u. (u. ({} (2)) ({} (4))) ({} (8)))) /edit/peano/arithmetic.gh/unionExample _________ (u. (u. (u. ({} (1)) ({} (4))) ({} (5))) (u. (u. ({} (2)) ({} (4))) ({} (8))))

### Substitution

• ([/] A x (< (* (2) x) (exp (+ x y) (3)))) /edit/peano/arithmetic.gh/substitutionExample ________ ([/] A x (< (* (2) x) (exp (+ x y) (3))))
Login to edit