List of theorems

List of theorems in peano/arithmetic.gh:

EqReplaceEq0 # <title> Substitution </title> # <table> # (= [ A ] ] ] C) # (= [ A ] [ B ] ) # (= [ [ [ B ] C) # </table>
(= A C) , (= A B)(= B C)
1plus1 ---- Automatically generated with GH.ProofGenerator.evaluator.batchEvaluation('+', [1, 10], [1, 10]); # <title> One-digit Addition </title>
(= (+ (1) (1)) (2))
2plus1 # <title> One-digit Addition </title>
(= (+ (2) (1)) (3))
3plus1 # <title> One-digit Addition </title>
(= (+ (3) (1)) (4))
4plus1 # <title> One-digit Addition </title>
(= (+ (4) (1)) (5))
5plus1 # <title> One-digit Addition </title>
(= (+ (5) (1)) (6))
6plus1 # <title> One-digit Addition </title>
(= (+ (6) (1)) (7))
7plus1 # <title> One-digit Addition </title>
(= (+ (7) (1)) (8))
8plus1 # <title> One-digit Addition </title>
(= (+ (8) (1)) (9))
9plus1 # <title> One-digit Addition </title>
(= (+ (9) (1)) (10))
1plus2 # <title> One-digit Addition </title>
(= (+ (1) (2)) (3))
1plus3 # <title> One-digit Addition </title>
(= (+ (1) (3)) (4))
1plus4 # <title> One-digit Addition </title>
(= (+ (1) (4)) (5))
1plus5 # <title> One-digit Addition </title>
(= (+ (1) (5)) (6))
1plus6 # <title> One-digit Addition </title>
(= (+ (1) (6)) (7))
1plus7 # <title> One-digit Addition </title>
(= (+ (1) (7)) (8))
1plus8 # <title> One-digit Addition </title>
(= (+ (1) (8)) (9))
1plus9 # <title> One-digit Addition </title>
(= (+ (1) (9)) (10))
1plus10 # <title> One-digit Addition </title>
(= (+ (1) (10)) (+ (10) (1)))
EqReplaceEq1Add1 # <title> Substitution </title> # <table> # (= A (+ B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (+ B [ [ [ D ] )) # </table>
(= A (+ B C)) , (= C D)(= A (+ B D))
2plus2 # <title> One-digit Addition </title>
(= (+ (2) (2)) (4))
2plus3 # <title> One-digit Addition </title>
(= (+ (2) (3)) (5))
2plus4 # <title> One-digit Addition </title>
(= (+ (2) (4)) (6))
2plus5 # <title> One-digit Addition </title>
(= (+ (2) (5)) (7))
2plus6 # <title> One-digit Addition </title>
(= (+ (2) (6)) (8))
2plus7 # <title> One-digit Addition </title>
(= (+ (2) (7)) (9))
2plus8 # <title> One-digit Addition </title>
(= (+ (2) (8)) (10))
2plus9 # <title> One-digit Addition </title>
(= (+ (2) (9)) (+ (10) (1)))
2plus10 # <title> One-digit Addition </title>
(= (+ (2) (10)) (+ (10) (2)))
EqReplaceEq1Add0 # <title> Substitution </title> # <table> # (= A (+ [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (+ [ [ [ C ] D)) # </table>
(= A (+ B D)) , (= B C)(= A (+ C D))
3plus2 # <title> One-digit Addition </title>
(= (+ (3) (2)) (5))
3plus3 # <title> One-digit Addition </title>
(= (+ (3) (3)) (6))
3plus4 # <title> One-digit Addition </title>
(= (+ (3) (4)) (7))
3plus5 # <title> One-digit Addition </title>
(= (+ (3) (5)) (8))
3plus6 # <title> One-digit Addition </title>
(= (+ (3) (6)) (9))
3plus7 # <title> One-digit Addition </title>
(= (+ (3) (7)) (10))
3plus8 # <title> One-digit Addition </title>
(= (+ (3) (8)) (+ (10) (1)))
3plus9 # <title> One-digit Addition </title>
(= (+ (3) (9)) (+ (10) (2)))
3plus10 # <title> One-digit Addition </title>
(= (+ (3) (10)) (+ (10) (3)))
4plus2 # <title> One-digit Addition </title>
(= (+ (4) (2)) (6))
4plus3 # <title> One-digit Addition </title>
(= (+ (4) (3)) (7))
4plus4 # <title> One-digit Addition </title>
(= (+ (4) (4)) (8))
4plus5 # <title> One-digit Addition 4+5=9 </title> # <summary> # This theorem proves that 4 + 5 = 9. To prove such a basic fact, we must directly use # the definitions of the numbers. The number 2 is defined as 2 = 1 + 1, 3 = 2 + 1, # 4 = 3 + 1, and so on. The theorem uses these definitions along with the # <a href="/edit/peano/peano_thms.gh/addass">associate property</a> to prove 4 + 5 = 9. # </summary>
(= (+ (4) (5)) (9))
4plus6 # <title> One-digit Addition </title>
(= (+ (4) (6)) (10))
4plus7 # <title> One-digit Addition </title>
(= (+ (4) (7)) (+ (10) (1)))
4plus8 # <title> One-digit Addition </title>
(= (+ (4) (8)) (+ (10) (2)))
4plus9 # <title> One-digit Addition </title>
(= (+ (4) (9)) (+ (10) (3)))
4plus10 # <title> One-digit Addition </title>
(= (+ (4) (10)) (+ (10) (4)))
5plus2 # <title> One-digit Addition </title>
(= (+ (5) (2)) (7))
5plus3 # <title> One-digit Addition </title>
(= (+ (5) (3)) (8))
5plus4 # <title> One-digit Addition </title>
(= (+ (5) (4)) (9))
5plus5 # <title> One-digit Addition </title>
(= (+ (5) (5)) (10))
5plus6 # <title> One-digit Addition </title>
(= (+ (5) (6)) (+ (10) (1)))
5plus7 # <title> One-digit Addition </title>
(= (+ (5) (7)) (+ (10) (2)))
5plus8 # <title> One-digit Addition </title>
(= (+ (5) (8)) (+ (10) (3)))
5plus9 # <title> One-digit Addition </title>
(= (+ (5) (9)) (+ (10) (4)))
5plus10 # <title> One-digit Addition </title>
(= (+ (5) (10)) (+ (10) (5)))
6plus2 # <title> One-digit Addition </title>
(= (+ (6) (2)) (8))
6plus3 # <title> One-digit Addition </title>
(= (+ (6) (3)) (9))
6plus4 # <title> One-digit Addition </title>
(= (+ (6) (4)) (10))
6plus5 # <title> One-digit Addition </title>
(= (+ (6) (5)) (+ (10) (1)))
6plus6 # <title> One-digit Addition </title>
(= (+ (6) (6)) (+ (10) (2)))
6plus7 # <title> One-digit Addition </title>
(= (+ (6) (7)) (+ (10) (3)))
6plus8 # <title> One-digit Addition </title>
(= (+ (6) (8)) (+ (10) (4)))
6plus9 # <title> One-digit Addition </title>
(= (+ (6) (9)) (+ (10) (5)))
6plus10 # <title> One-digit Addition </title>
(= (+ (6) (10)) (+ (10) (6)))
7plus2 # <title> One-digit Addition </title>
(= (+ (7) (2)) (9))
7plus3 # <title> One-digit Addition </title>
(= (+ (7) (3)) (10))
7plus4 # <title> One-digit Addition </title>
(= (+ (7) (4)) (+ (10) (1)))
7plus5 # <title> One-digit Addition </title>
(= (+ (7) (5)) (+ (10) (2)))
7plus6 # <title> One-digit Addition </title>
(= (+ (7) (6)) (+ (10) (3)))
7plus7 # <title> One-digit Addition </title>
(= (+ (7) (7)) (+ (10) (4)))
7plus8 # <title> One-digit Addition </title>
(= (+ (7) (8)) (+ (10) (5)))
7plus9 # <title> One-digit Addition </title>
(= (+ (7) (9)) (+ (10) (6)))
7plus10 # <title> One-digit Addition </title>
(= (+ (7) (10)) (+ (10) (7)))
8plus2 # <title> One-digit Addition </title>
(= (+ (8) (2)) (10))
8plus3 # <title> One-digit Addition </title>
(= (+ (8) (3)) (+ (10) (1)))
8plus4 # <title> One-digit Addition </title>
(= (+ (8) (4)) (+ (10) (2)))
8plus5 # <title> One-digit Addition </title>
(= (+ (8) (5)) (+ (10) (3)))
8plus6 # <title> One-digit Addition </title>
(= (+ (8) (6)) (+ (10) (4)))
8plus7 # <title> One-digit Addition </title>
(= (+ (8) (7)) (+ (10) (5)))
8plus8 # <title> One-digit Addition </title>
(= (+ (8) (8)) (+ (10) (6)))
8plus9 # <title> One-digit Addition </title>
(= (+ (8) (9)) (+ (10) (7)))
8plus10 # <title> One-digit Addition </title>
(= (+ (8) (10)) (+ (10) (8)))
9plus2 # <title> One-digit Addition </title>
(= (+ (9) (2)) (+ (10) (1)))
9plus3 # <title> One-digit Addition </title>
(= (+ (9) (3)) (+ (10) (2)))
9plus4 # <title> One-digit Addition </title>
(= (+ (9) (4)) (+ (10) (3)))
9plus5 # <title> One-digit Addition </title>
(= (+ (9) (5)) (+ (10) (4)))
9plus6 # <title> One-digit Addition </title>
(= (+ (9) (6)) (+ (10) (5)))
9plus7 # <title> One-digit Addition </title>
(= (+ (9) (7)) (+ (10) (6)))
9plus8 # <title> One-digit Addition </title>
(= (+ (9) (8)) (+ (10) (7)))
9plus9 # <title> One-digit Addition </title>
(= (+ (9) (9)) (+ (10) (8)))
9plus10 # <title> One-digit Addition </title>
(= (+ (9) (10)) (+ (10) (9)))
EqReplaceEq1Mul0 # <title> Substitution </title> # <table> # (= A (* [ B ] ] ] D)) # (= [ B ] [ C ] ) # (= A (* [ [ [ C ] D)) # </table>
(= A (* B D)) , (= B C)(= A (* C D))
10plus10 # <title> One-digit Addition </title>
(= (+ (10) (10)) (* (2) (10)))

Multiplication Tables

2times2 ---- Automatically generated with GH.ProofGenerator.evaluator.batchEvaluation('*', [2, 9], [2, 9]); # <title> One-digit Multiplication </title>
(= (* (2) (2)) (4))
2times3 # <title> One-digit Multiplication </title>
(= (* (2) (3)) (6))
2times4 # <title> One-digit Multiplication </title>
(= (* (2) (4)) (8))
2times5 # <title> One-digit Multiplication </title>
(= (* (2) (5)) (10))
2times6 # <title> One-digit Multiplication </title>
(= (* (2) (6)) (+ (10) (2)))
2times7 # <title> One-digit Multiplication </title>
(= (* (2) (7)) (+ (10) (4)))
2times8 # <title> One-digit Multiplication </title>
(= (* (2) (8)) (+ (10) (6)))
2times9 # <title> One-digit Multiplication </title>
(= (* (2) (9)) (+ (10) (8)))
3times2 # <title> One-digit Multiplication </title>
(= (* (3) (2)) (6))
3times3 # <title> One-digit Multiplication </title>
(= (* (3) (3)) (9))
3times4 # <title> One-digit Multiplication </title>
(= (* (3) (4)) (+ (10) (2)))
3times5 # <title> One-digit Multiplication </title>
(= (* (3) (5)) (+ (10) (5)))
3times6 # <title> One-digit Multiplication </title>
(= (* (3) (6)) (+ (10) (8)))
EqReplaceEq1Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ B [ C ] ] ] ) A')) # (= [ C ] [ D ] ) # (= A (+ (+ B [ [ [ D ] ) A')) # </table>
(= A (+ (+ B C) A')) , (= C D)(= A (+ (+ B D) A'))
EqReplaceEq1Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (* [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (+ (* [ [ [ C ] D) A')) # </table>
(= A (+ (* B D) A')) , (= B C)(= A (+ (* C D) A'))
3times7 # <title> One-digit Multiplication </title>
(= (* (3) (7)) (+ (* (2) (10)) (1)))
3times8 # <title> One-digit Multiplication </title>
(= (* (3) (8)) (+ (* (2) (10)) (4)))
3times9 # <title> One-digit Multiplication </title>
(= (* (3) (9)) (+ (* (2) (10)) (7)))
4times2 # <title> One-digit Multiplication </title>
(= (* (4) (2)) (8))
4times3 # <title> One-digit Multiplication </title>
(= (* (4) (3)) (+ (10) (2)))
4times4 # <title> One-digit Multiplication </title>
(= (* (4) (4)) (+ (10) (6)))
4times5 # <title> One-digit Multiplication </title>
(= (* (4) (5)) (* (2) (10)))
4times6 # <title> One-digit Multiplication </title>
(= (* (4) (6)) (+ (* (2) (10)) (4)))
4times7 # <title> One-digit Multiplication </title>
(= (* (4) (7)) (+ (* (2) (10)) (8)))
4times8 # <title> One-digit Multiplication </title>
(= (* (4) (8)) (+ (* (3) (10)) (2)))
4times9 # <title> One-digit Multiplication </title>
(= (* (4) (9)) (+ (* (3) (10)) (6)))
5times2 # <title> One-digit Multiplication </title>
(= (* (5) (2)) (10))
5times3 # <title> One-digit Multiplication </title>
(= (* (5) (3)) (+ (10) (5)))
5times4 # <title> One-digit Multiplication </title>
(= (* (5) (4)) (* (2) (10)))
5times5 # <title> One-digit Multiplication </title>
(= (* (5) (5)) (+ (* (2) (10)) (5)))
5times6 # <title> One-digit Multiplication </title>
(= (* (5) (6)) (* (3) (10)))
5times7 # <title> One-digit Multiplication </title>
(= (* (5) (7)) (+ (* (3) (10)) (5)))
5times8 # <title> One-digit Multiplication </title>
(= (* (5) (8)) (* (4) (10)))
5times9 # <title> One-digit Multiplication </title>
(= (* (5) (9)) (+ (* (4) (10)) (5)))
6times2 # <title> One-digit Multiplication </title>
(= (* (6) (2)) (+ (10) (2)))
6times3 # <title> One-digit Multiplication </title>
(= (* (6) (3)) (+ (10) (8)))
6times4 # <title> One-digit Multiplication </title>
(= (* (6) (4)) (+ (* (2) (10)) (4)))
6times5 # <title> One-digit Multiplication </title>
(= (* (6) (5)) (* (3) (10)))
6times6 # <title> One-digit Multiplication </title>
(= (* (6) (6)) (+ (* (3) (10)) (6)))
6times7 # <title> One-digit Multiplication </title>
(= (* (6) (7)) (+ (* (4) (10)) (2)))
6times8 # <title> One-digit Multiplication </title>
(= (* (6) (8)) (+ (* (4) (10)) (8)))
6times9 # <title> One-digit Multiplication </title>
(= (* (6) (9)) (+ (* (5) (10)) (4)))
7times2 # <title> One-digit Multiplication </title>
(= (* (7) (2)) (+ (10) (4)))
7times3 # <title> One-digit Multiplication </title>
(= (* (7) (3)) (+ (* (2) (10)) (1)))
7times4 # <title> One-digit Multiplication </title>
(= (* (7) (4)) (+ (* (2) (10)) (8)))
7times5 # <title> One-digit Multiplication </title>
(= (* (7) (5)) (+ (* (3) (10)) (5)))
7times6 # <title> One-digit Multiplication </title>
(= (* (7) (6)) (+ (* (4) (10)) (2)))
7times7 # <title> One-digit Multiplication </title>
(= (* (7) (7)) (+ (* (4) (10)) (9)))
7times8 # <title> One-digit Multiplication </title>
(= (* (7) (8)) (+ (* (5) (10)) (6)))
7times9 # <title> One-digit Multiplication </title>
(= (* (7) (9)) (+ (* (6) (10)) (3)))
8times2 # <title> One-digit Multiplication </title>
(= (* (8) (2)) (+ (10) (6)))
8times3 # <title> One-digit Multiplication </title>
(= (* (8) (3)) (+ (* (2) (10)) (4)))
8times4 # <title> One-digit Multiplication </title>
(= (* (8) (4)) (+ (* (3) (10)) (2)))
8times5 # <title> One-digit Multiplication </title>
(= (* (8) (5)) (* (4) (10)))
8times6 # <title> One-digit Multiplication </title>
(= (* (8) (6)) (+ (* (4) (10)) (8)))
8times7 # <title> One-digit Multiplication </title>
(= (* (8) (7)) (+ (* (5) (10)) (6)))
8times8 # <title> One-digit Multiplication </title>
(= (* (8) (8)) (+ (* (6) (10)) (4)))
8times9 # <title> One-digit Multiplication </title>
(= (* (8) (9)) (+ (* (7) (10)) (2)))
9times2 # <title> One-digit Multiplication </title>
(= (* (9) (2)) (+ (10) (8)))
9times3 # <title> One-digit Multiplication </title>
(= (* (9) (3)) (+ (* (2) (10)) (7)))
9times4 # <title> One-digit Multiplication </title>
(= (* (9) (4)) (+ (* (3) (10)) (6)))
9times5 # <title> One-digit Multiplication </title>
(= (* (9) (5)) (+ (* (4) (10)) (5)))
9times6 # <title> One-digit Multiplication </title>
(= (* (9) (6)) (+ (* (5) (10)) (4)))
9times7 # <title> One-digit Multiplication </title>
(= (* (9) (7)) (+ (* (6) (10)) (3)))
9times8 # <title> One-digit Multiplication </title>
(= (* (9) (8)) (+ (* (7) (10)) (2)))
9times9 # <title> One-digit Multiplication </title>
(= (* (9) (9)) (+ (* (8) (10)) (1)))
EqReplaceNot0Eq1 # <title> Substitution </title> # <table> # (-. (= A [ B ] ] ] )) # (= [ B ] [ C ] ) # (-. (= A [ [ [ C ] )) # </table>
(-. (= A B)) , (= B C)(-. (= A C))

Inequalities

0notEqual1 ==================== Equality ===========================# ---- Automatically generated with GH.ProofGenerator.evaluator.batchEvaluation('=', [0, 0], [1, 10]); ---- Automatically generated with GH.ProofGenerator.evaluator.batchEvaluation('=', [1, 10], [0, 0]); # <title> One-Digit Inequality </title>
(-. (= (0) (1)))
0notEqual2 # <title> One-Digit Inequality </title>
(-. (= (0) (2)))
0notEqual3 # <title> One-Digit Inequality </title>
(-. (= (0) (3)))
0notEqual4 # <title> One-Digit Inequality </title>
(-. (= (0) (4)))
0notEqual5 # <title> One-Digit Inequality </title>
(-. (= (0) (5)))
0notEqual6 # <title> One-Digit Inequality </title>
(-. (= (0) (6)))
0notEqual7 # <title> One-Digit Inequality </title>
(-. (= (0) (7)))
0notEqual8 # <title> One-Digit Inequality </title>
(-. (= (0) (8)))
0notEqual9 # <title> One-Digit Inequality </title>
(-. (= (0) (9)))
0notEqual10 # <title> One-Digit Inequality </title>
(-. (= (0) (10)))
1notEqual0 # <title> One-Digit Inequality </title>
(-. (= (1) (0)))
2notEqual0 # <title> One-Digit Inequality </title>
(-. (= (2) (0)))
3notEqual0 # <title> One-Digit Inequality </title>
(-. (= (3) (0)))
4notEqual0 # <title> One-Digit Inequality </title>
(-. (= (4) (0)))
5notEqual0 # <title> One-Digit Inequality </title>
(-. (= (5) (0)))
6notEqual0 # <title> One-Digit Inequality </title>
(-. (= (6) (0)))
7notEqual0 # <title> One-Digit Inequality </title>
(-. (= (7) (0)))
8notEqual0 # <title> One-Digit Inequality </title>
(-. (= (8) (0)))
9notEqual0 # <title> One-Digit Inequality </title>
(-. (= (9) (0)))
10notEqual0 # <title> One-Digit Inequality </title>
(-. (= (10) (0)))
0less1 # <title> One-Digit Inequality </title>
(< (0) (1))
0less2 # <title> One-Digit Inequality </title>
(< (0) (2))
0less3 # <title> One-Digit Inequality </title>
(< (0) (3))
0less4 # <title> One-Digit Inequality </title>
(< (0) (4))
0less5 # <title> One-Digit Inequality </title>
(< (0) (5))
0less6 # <title> One-Digit Inequality </title>
(< (0) (6))
0less7 # <title> One-Digit Inequality </title>
(< (0) (7))
0less8 # <title> One-Digit Inequality </title>
(< (0) (8))
0less9 # <title> One-Digit Inequality </title>
(< (0) (9))
0less10 # <title> One-Digit Inequality </title>
(< (0) (10))
EqReplaceLt0 # <title> Substitution </title> # <table> # (< [ A ] ] ] C) # (= [ A ] [ B ] ) # (< [ [ [ B ] C) # </table>
(< A C) , (= A B)(< B C)
EqReplaceLt1 # <title> Substitution </title> # <table> # (< A [ B ] ] ] ) # (= [ B ] [ C ] ) # (< A [ [ [ C ] ) # </table>
(< A B) , (= B C)(< A C)
1less2 # <title> One-Digit Inequality </title>
(< (1) (2))
1less3 # <title> One-Digit Inequality </title>
(< (1) (3))
1less4 # <title> One-Digit Inequality </title>
(< (1) (4))
1less5 # <title> One-Digit Inequality </title>
(< (1) (5))
1less6 # <title> One-Digit Inequality </title>
(< (1) (6))
1less7 # <title> One-Digit Inequality </title>
(< (1) (7))
1less8 # <title> One-Digit Inequality </title>
(< (1) (8))
1less9 # <title> One-Digit Inequality </title>
(< (1) (9))
1less10 # <title> One-Digit Inequality </title>
(< (1) (10))
1greater0 # <title> One-Digit Inequality </title>
(> (1) (0))
EqReplaceGt0 # <title> Substitution </title> # <table> # (> [ A ] ] ] C) # (= [ A ] [ B ] ) # (> [ [ [ B ] C) # </table>
(> A C) , (= A B)(> B C)
EqReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (= [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (= B C)(> A C)
2greater1 # <title> One-Digit Inequality </title>
(> (2) (1))
2less3 # <title> One-Digit Inequality </title>
(< (2) (3))
2less4 # <title> One-Digit Inequality </title>
(< (2) (4))
2less5 # <title> One-Digit Inequality </title>
(< (2) (5))
2less6 # <title> One-Digit Inequality </title>
(< (2) (6))
2less7 # <title> One-Digit Inequality </title>
(< (2) (7))
2less8 # <title> One-Digit Inequality </title>
(< (2) (8))
2less9 # <title> One-Digit Inequality </title>
(< (2) (9))
2less10 # <title> One-Digit Inequality </title>
(< (2) (10))
2greater0 # <title> One-Digit Inequality </title>
(> (2) (0))
3greater1 # <title> One-Digit Inequality </title>
(> (3) (1))
3greater2 # <title> One-Digit Inequality </title>
(> (3) (2))
3less4 # <title> One-Digit Inequality </title>
(< (3) (4))
3less5 # <title> One-Digit Inequality </title>
(< (3) (5))
3less6 # <title> One-Digit Inequality </title>
(< (3) (6))
3less7 # <title> One-Digit Inequality </title>
(< (3) (7))
3less8 # <title> One-Digit Inequality </title>
(< (3) (8))
3less9 # <title> One-Digit Inequality </title>
(< (3) (9))
3less10 # <title> One-Digit Inequality </title>
(< (3) (10))
3greater0 # <title> One-Digit Inequality </title>
(> (3) (0))
4greater1 # <title> One-Digit Inequality </title>
(> (4) (1))
4greater2 # <title> One-Digit Inequality </title>
(> (4) (2))
4greater3 # <title> One-Digit Inequality </title>
(> (4) (3))
4less5 # <title> One-Digit Inequality </title>
(< (4) (5))
4less6 # <title> One-Digit Inequality </title>
(< (4) (6))
4less7 # <title> One-Digit Inequality </title>
(< (4) (7))
4less8 # <title> One-Digit Inequality </title>
(< (4) (8))
4less9 # <title> One-Digit Inequality </title>
(< (4) (9))
4less10 # <title> One-Digit Inequality </title>
(< (4) (10))
4greater0 # <title> One-Digit Inequality </title>
(> (4) (0))
5greater1 # <title> One-Digit Inequality </title>
(> (5) (1))
5greater2 # <title> One-Digit Inequality </title>
(> (5) (2))
5greater3 # <title> One-Digit Inequality </title>
(> (5) (3))
5greater4 # <title> One-Digit Inequality </title>
(> (5) (4))
5less6 # <title> One-Digit Inequality </title>
(< (5) (6))
5less7 # <title> One-Digit Inequality </title>
(< (5) (7))
5less8 # <title> One-Digit Inequality </title>
(< (5) (8))
5less9 # <title> One-Digit Inequality </title>
(< (5) (9))
5less10 # <title> One-Digit Inequality </title>
(< (5) (10))
5greater0 # <title> One-Digit Inequality </title>
(> (5) (0))
6greater1 # <title> One-Digit Inequality </title>
(> (6) (1))
6greater2 # <title> One-Digit Inequality </title>
(> (6) (2))
6greater3 # <title> One-Digit Inequality </title>
(> (6) (3))
6greater4 # <title> One-Digit Inequality </title>
(> (6) (4))
6greater5 # <title> One-Digit Inequality </title>
(> (6) (5))
6less7 # <title> One-Digit Inequality </title>
(< (6) (7))
6less8 # <title> One-Digit Inequality </title>
(< (6) (8))
6less9 # <title> One-Digit Inequality </title>
(< (6) (9))
6less10 # <title> One-Digit Inequality </title>
(< (6) (10))
6greater0 # <title> One-Digit Inequality </title>
(> (6) (0))
7greater1 # <title> One-Digit Inequality </title>
(> (7) (1))
7greater2 # <title> One-Digit Inequality </title>
(> (7) (2))
7greater3 # <title> One-Digit Inequality </title>
(> (7) (3))
7greater4 # <title> One-Digit Inequality </title>
(> (7) (4))
7greater5 # <title> One-Digit Inequality </title>
(> (7) (5))
7greater6 # <title> One-Digit Inequality </title>
(> (7) (6))
7less8 # <title> One-Digit Inequality </title>
(< (7) (8))
7less9 # <title> One-Digit Inequality </title>
(< (7) (9))
7less10 # <title> One-Digit Inequality </title>
(< (7) (10))
7greater0 # <title> One-Digit Inequality </title>
(> (7) (0))
8greater1 # <title> One-Digit Inequality </title>
(> (8) (1))
8greater2 # <title> One-Digit Inequality </title>
(> (8) (2))
8greater3 # <title> One-Digit Inequality </title>
(> (8) (3))
8greater4 # <title> One-Digit Inequality </title>
(> (8) (4))
8greater5 # <title> One-Digit Inequality </title>
(> (8) (5))
8greater6 # <title> One-Digit Inequality </title>
(> (8) (6))
8greater7 # <title> One-Digit Inequality </title>
(> (8) (7))
8less9 # <title> One-Digit Inequality </title>
(< (8) (9))
8less10 # <title> One-Digit Inequality </title>
(< (8) (10))
8greater0 # <title> One-Digit Inequality </title>
(> (8) (0))
9greater1 # <title> One-Digit Inequality </title>
(> (9) (1))
9greater2 # <title> One-Digit Inequality </title>
(> (9) (2))
9greater3 # <title> One-Digit Inequality </title>
(> (9) (3))
9greater4 # <title> One-Digit Inequality </title>
(> (9) (4))
9greater5 # <title> One-Digit Inequality </title>
(> (9) (5))
9greater6 # <title> One-Digit Inequality </title>
(> (9) (6))
9greater7 # <title> One-Digit Inequality </title>
(> (9) (7))
9greater8 # <title> One-Digit Inequality </title>
(> (9) (8))
9less10 # <title> One-Digit Inequality </title>
(< (9) (10))
9greater0 # <title> One-Digit Inequality </title>
(> (9) (0))
10greater1 # <title> One-Digit Inequality </title>
(> (10) (1))
10greater2 # <title> One-Digit Inequality </title>
(> (10) (2))
10greater3 # <title> One-Digit Inequality </title>
(> (10) (3))
10greater4 # <title> One-Digit Inequality </title>
(> (10) (4))
10greater5 # <title> One-Digit Inequality </title>
(> (10) (5))
10greater6 # <title> One-Digit Inequality </title>
(> (10) (6))
10greater7 # <title> One-Digit Inequality </title>
(> (10) (7))
10greater8 # <title> One-Digit Inequality </title>
(> (10) (8))
10greater9 # <title> One-Digit Inequality </title>
(> (10) (9))
1notEqual2 # <title> One-Digit Inequality </title>
(-. (= (1) (2)))
1notEqual3 # <title> One-Digit Inequality </title>
(-. (= (1) (3)))
1notEqual4 # <title> One-Digit Inequality </title>
(-. (= (1) (4)))
1notEqual5 # <title> One-Digit Inequality </title>
(-. (= (1) (5)))
1notEqual6 # <title> One-Digit Inequality </title>
(-. (= (1) (6)))
1notEqual7 # <title> One-Digit Inequality </title>
(-. (= (1) (7)))
1notEqual8 # <title> One-Digit Inequality </title>
(-. (= (1) (8)))
1notEqual9 # <title> One-Digit Inequality </title>
(-. (= (1) (9)))
1notEqual10 # <title> One-Digit Inequality </title>
(-. (= (1) (10)))
2notEqual1 # <title> One-Digit Inequality </title>
(-. (= (2) (1)))
2notEqual3 # <title> One-Digit Inequality </title>
(-. (= (2) (3)))
2notEqual4 # <title> One-Digit Inequality </title>
(-. (= (2) (4)))
2notEqual5 # <title> One-Digit Inequality </title>
(-. (= (2) (5)))
2notEqual6 # <title> One-Digit Inequality </title>
(-. (= (2) (6)))
2notEqual7 # <title> One-Digit Inequality </title>
(-. (= (2) (7)))
2notEqual8 # <title> One-Digit Inequality </title>
(-. (= (2) (8)))
2notEqual9 # <title> One-Digit Inequality </title>
(-. (= (2) (9)))
2notEqual10 # <title> One-Digit Inequality </title>
(-. (= (2) (10)))
3notEqual1 # <title> One-Digit Inequality </title>
(-. (= (3) (1)))
3notEqual2 # <title> One-Digit Inequality </title>
(-. (= (3) (2)))
3notEqual4 # <title> One-Digit Inequality </title>
(-. (= (3) (4)))
3notEqual5 # <title> One-Digit Inequality </title>
(-. (= (3) (5)))
3notEqual6 # <title> One-Digit Inequality </title>
(-. (= (3) (6)))
3notEqual7 # <title> One-Digit Inequality </title>
(-. (= (3) (7)))
3notEqual8 # <title> One-Digit Inequality </title>
(-. (= (3) (8)))
3notEqual9 # <title> One-Digit Inequality </title>
(-. (= (3) (9)))
3notEqual10 # <title> One-Digit Inequality </title>
(-. (= (3) (10)))
4notEqual1 # <title> One-Digit Inequality </title>
(-. (= (4) (1)))
4notEqual2 # <title> One-Digit Inequality </title>
(-. (= (4) (2)))
4notEqual3 # <title> One-Digit Inequality </title>
(-. (= (4) (3)))
4notEqual5 # <title> One-Digit Inequality </title>
(-. (= (4) (5)))
4notEqual6 # <title> One-Digit Inequality </title>
(-. (= (4) (6)))
4notEqual7 # <title> One-Digit Inequality </title>
(-. (= (4) (7)))
4notEqual8 # <title> One-Digit Inequality </title>
(-. (= (4) (8)))
4notEqual9 # <title> One-Digit Inequality </title>
(-. (= (4) (9)))
4notEqual10 # <title> One-Digit Inequality </title>
(-. (= (4) (10)))
5notEqual1 # <title> One-Digit Inequality </title>
(-. (= (5) (1)))
5notEqual2 # <title> One-Digit Inequality </title>
(-. (= (5) (2)))
5notEqual3 # <title> One-Digit Inequality </title>
(-. (= (5) (3)))
5notEqual4 # <title> One-Digit Inequality </title>
(-. (= (5) (4)))
5notEqual6 # <title> One-Digit Inequality </title>
(-. (= (5) (6)))
5notEqual7 # <title> One-Digit Inequality </title>
(-. (= (5) (7)))
5notEqual8 # <title> One-Digit Inequality </title>
(-. (= (5) (8)))
5notEqual9 # <title> One-Digit Inequality </title>
(-. (= (5) (9)))
5notEqual10 # <title> One-Digit Inequality </title>
(-. (= (5) (10)))
6notEqual1 # <title> One-Digit Inequality </title>
(-. (= (6) (1)))
6notEqual2 # <title> One-Digit Inequality </title>
(-. (= (6) (2)))
6notEqual3 # <title> One-Digit Inequality </title>
(-. (= (6) (3)))
6notEqual4 # <title> One-Digit Inequality </title>
(-. (= (6) (4)))
6notEqual5 # <title> One-Digit Inequality </title>
(-. (= (6) (5)))
6notEqual7 # <title> One-Digit Inequality </title>
(-. (= (6) (7)))
6notEqual8 # <title> One-Digit Inequality </title>
(-. (= (6) (8)))
6notEqual9 # <title> One-Digit Inequality </title>
(-. (= (6) (9)))
6notEqual10 # <title> One-Digit Inequality </title>
(-. (= (6) (10)))
7notEqual1 # <title> One-Digit Inequality </title>
(-. (= (7) (1)))
7notEqual2 # <title> One-Digit Inequality </title>
(-. (= (7) (2)))
7notEqual3 # <title> One-Digit Inequality </title>
(-. (= (7) (3)))
7notEqual4 # <title> One-Digit Inequality </title>
(-. (= (7) (4)))
7notEqual5 # <title> One-Digit Inequality </title>
(-. (= (7) (5)))
7notEqual6 # <title> One-Digit Inequality </title>
(-. (= (7) (6)))
7notEqual8 # <title> One-Digit Inequality </title>
(-. (= (7) (8)))
7notEqual9 # <title> One-Digit Inequality </title>
(-. (= (7) (9)))
7notEqual10 # <title> One-Digit Inequality </title>
(-. (= (7) (10)))
8notEqual1 # <title> One-Digit Inequality </title>
(-. (= (8) (1)))
8notEqual2 # <title> One-Digit Inequality </title>
(-. (= (8) (2)))
8notEqual3 # <title> One-Digit Inequality </title>
(-. (= (8) (3)))
8notEqual4 # <title> One-Digit Inequality </title>
(-. (= (8) (4)))
8notEqual5 # <title> One-Digit Inequality </title>
(-. (= (8) (5)))
8notEqual6 # <title> One-Digit Inequality </title>
(-. (= (8) (6)))
8notEqual7 # <title> One-Digit Inequality </title>
(-. (= (8) (7)))
8notEqual9 # <title> One-Digit Inequality </title>
(-. (= (8) (9)))
8notEqual10 # <title> One-Digit Inequality </title>
(-. (= (8) (10)))
9notEqual1 # <title> One-Digit Inequality </title>
(-. (= (9) (1)))
9notEqual2 # <title> One-Digit Inequality </title>
(-. (= (9) (2)))
9notEqual3 # <title> One-Digit Inequality </title>
(-. (= (9) (3)))
9notEqual4 # <title> One-Digit Inequality </title>
(-. (= (9) (4)))
9notEqual5 # <title> One-Digit Inequality </title>
(-. (= (9) (5)))
9notEqual6 # <title> One-Digit Inequality </title>
(-. (= (9) (6)))
9notEqual7 # <title> One-Digit Inequality </title>
(-. (= (9) (7)))
9notEqual8 # <title> One-Digit Inequality </title>
(-. (= (9) (8)))
9notEqual10 # <title> One-Digit Inequality </title>
(-. (= (9) (10)))
10notEqual1 # <title> One-Digit Inequality </title>
(-. (= (10) (1)))
10notEqual2 # <title> One-Digit Inequality </title>
(-. (= (10) (2)))
10notEqual3 # <title> One-Digit Inequality </title>
(-. (= (10) (3)))
10notEqual4 # <title> One-Digit Inequality </title>
(-. (= (10) (4)))
10notEqual5 # <title> One-Digit Inequality </title>
(-. (= (10) (5)))
10notEqual6 # <title> One-Digit Inequality </title>
(-. (= (10) (6)))
10notEqual7 # <title> One-Digit Inequality </title>
(-. (= (10) (7)))
10notEqual8 # <title> One-Digit Inequality </title>
(-. (= (10) (8)))
10notEqual9 # <title> One-Digit Inequality </title>
(-. (= (10) (9)))
EqReplaceEq1Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (+ (+ [ [ [ C ] D) A')) # </table>
(= A (+ (+ B D) A')) , (= B C)(= A (+ (+ C D) A'))
EqReplaceEq1Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ B (* [ C ] ] ] A')) B')) # (= [ C ] [ D ] ) # (= A (+ (+ B (* [ [ [ D ] A')) B')) # </table>
(= A (+ (+ B (* C A')) B')) , (= C D)(= A (+ (+ B (* D A')) B'))
EqReplaceEq1Add0Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (* [ B ] ] ] D) A') B')) # (= [ B ] [ C ] ) # (= A (+ (+ (* [ [ [ C ] D) A') B')) # </table>
(= A (+ (+ (* B D) A') B')) , (= B C)(= A (+ (+ (* C D) A') B'))
additionExample # <summary> This is an example of multi-digit addition. There is nothing particularly remarkable about these specific numbers. </summary>
(= (+ (+ (* (10) (10)) (+ (* (6) (10)) (5))) (+ (* (4) (10)) (7))) (+ (* (2) (* (10) (10))) (+ (10) (2))))
EqReplaceEq1Add0Add0Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ [ B ] ] ] D) A') B') C')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ (+ [ [ [ C ] D) A') B') C')) # </table>
(= A (+ (+ (+ (+ B D) A') B') C')) , (= B C)(= A (+ (+ (+ (+ C D) A') B') C'))
EqReplaceEq1Add0Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ B [ C ] ] ] ) A') B') C')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ B [ [ [ D ] ) A') B') C')) # </table>
(= A (+ (+ (+ (+ B C) A') B') C')) , (= C D)(= A (+ (+ (+ (+ B D) A') B') C'))
EqReplaceEq1Add0Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ [ B ] ] ] D) A') B')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ [ [ [ C ] D) A') B')) # </table>
(= A (+ (+ (+ B D) A') B')) , (= B C)(= A (+ (+ (+ C D) A') B'))
EqReplaceEq1Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ B [ C ] ] ] ) A') B')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ B [ [ [ D ] ) A') B')) # </table>
(= A (+ (+ (+ B C) A') B')) , (= C D)(= A (+ (+ (+ B D) A') B'))
EqReplaceEq1Add0Add0Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ (+ B [ C ] ] ] ) A') B') C') D')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ (+ B [ [ [ D ] ) A') B') C') D')) # </table>
(= A (+ (+ (+ (+ (+ B C) A') B') C') D')) , (= C D)(= A (+ (+ (+ (+ (+ B D) A') B') C') D'))
EqReplaceEq1Add0Add0Add0Add0Add0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ (+ [ B ] ] ] D) A') B') C') D')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ (+ (+ [ [ [ C ] D) A') B') C') D')) # </table>
(= A (+ (+ (+ (+ (+ B D) A') B') C') D')) , (= B C)(= A (+ (+ (+ (+ (+ C D) A') B') C') D'))
EqReplaceEq1Add0Add0Add0Add0Add0Add1 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ (+ (+ B [ C ] ] ] ) A') B') C') D') A0)) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ (+ (+ B [ [ [ D ] ) A') B') C') D') A0)) # </table>
(= A (+ (+ (+ (+ (+ (+ B C) A') B') C') D') A0)) , (= C D)(= A (+ (+ (+ (+ (+ (+ B D) A') B') C') D') A0))
EqReplaceEq1Add0Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ B (* [ C ] ] ] A')) B') C')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ B (* [ [ [ D ] A')) B') C')) # </table>
(= A (+ (+ (+ B (* C A')) B') C')) , (= C D)(= A (+ (+ (+ B (* D A')) B') C'))
EqReplaceEq1Add0Add0Add0Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (* [ B ] ] ] D) A') B') C')) # (= [ B ] [ C ] ) # (= A (+ (+ (+ (* [ [ [ C ] D) A') B') C')) # </table>
(= A (+ (+ (+ (* B D) A') B') C')) , (= B C)(= A (+ (+ (+ (* C D) A') B') C'))
additionExample2 # <summary> This is an example of multi-digit addition. There is nothing particularly remarkable about these specific numbers. </summary>
(= (+ (+ (* (10) (* (10) (10))) (+ (* (4) (* (10) (10))) (+ (* (9) (10)) (2)))) (+ (* (5) (* (10) (* (10) (10)))) (+ (* (4) (* (10) (10))) (+ (* (8) (10)) (3))))) (+ (* (6) (* (10) (* (10) (10)))) (+ (* (9) (* (10) (10))) (+ (* (7) (10)) (5)))))
multiplicationExample # <summary> This is an example of multi-digit multiplication. There is nothing particularly remarkable about these specific numbers. </summary>
(= (* (+ (10) (7)) (+ (10) (3))) (+ (* (2) (* (10) (10))) (+ (* (2) (10)) (1))))
EqReplaceEq1Add1Add1 # <title> Substitution </title> # <table> # (= A (+ B (+ C [ D ] ] ] ))) # (= [ D ] [ A' ] ) # (= A (+ B (+ C [ [ [ A' ] ))) # </table>
(= A (+ B (+ C D))) , (= D A')(= A (+ B (+ C A')))
EqReplaceEq1Mul1 # <title> Substitution </title> # <table> # (= A (* B [ C ] ] ] )) # (= [ C ] [ D ] ) # (= A (* B [ [ [ D ] )) # </table>
(= A (* B C)) , (= C D)(= A (* B D))
EqReplaceEq1Add1Add0 # <title> Substitution </title> # <table> # (= A (+ B (+ [ C ] ] ] A'))) # (= [ C ] [ D ] ) # (= A (+ B (+ [ [ [ D ] A'))) # </table>
(= A (+ B (+ C A'))) , (= C D)(= A (+ B (+ D A')))
EqReplaceEq1Add0Add0Add0Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ (+ (+ (+ B (* [ C ] ] ] A')) B') C') D')) # (= [ C ] [ D ] ) # (= A (+ (+ (+ (+ B (* [ [ [ D ] A')) B') C') D')) # </table>
(= A (+ (+ (+ (+ B (* C A')) B') C') D')) , (= C D)(= A (+ (+ (+ (+ B (* D A')) B') C') D'))
multiplicationExample2 # <summary> This is an example of multi-digit multiplication. There is nothing particularly remarkable about these specific numbers. </summary>
(= (* (+ (* (3) (* (10) (10))) (+ (* (8) (10)) (7))) (+ (* (2) (* (10) (10))) (3))) (+ (* (7) (* (10) (* (10) (* (10) (10))))) (+ (* (8) (* (10) (* (10) (10)))) (+ (* (5) (* (10) (10))) (+ (* (6) (10)) (1))))))

Modulo Tables

2mod2 # <title> One-digit Modulo </title>
(= (mod (2) (2)) (0))
3mod2 # <title> One-digit Modulo </title>
(= (mod (3) (2)) (1))
4mod2 # <title> One-digit Modulo </title>
(= (mod (4) (2)) (0))
5mod2 # <title> One-digit Modulo </title>
(= (mod (5) (2)) (1))
6mod2 # <title> One-digit Modulo </title>
(= (mod (6) (2)) (0))
7mod2 # <title> One-digit Modulo </title>
(= (mod (7) (2)) (1))
8mod2 # <title> One-digit Modulo </title>
(= (mod (8) (2)) (0))
9mod2 # <title> One-digit Modulo </title>
(= (mod (9) (2)) (1))
10mod2 # <title> One-digit Modulo </title>
(= (mod (10) (2)) (0))
2mod3 # <title> One-digit Modulo </title>
(= (mod (2) (3)) (2))
3mod3 # <title> One-digit Modulo </title>
(= (mod (3) (3)) (0))
4mod3 # <title> One-digit Modulo </title>
(= (mod (4) (3)) (1))
5mod3 # <title> One-digit Modulo </title>
(= (mod (5) (3)) (2))
6mod3 # <title> One-digit Modulo </title>
(= (mod (6) (3)) (0))
7mod3 # <title> One-digit Modulo </title>
(= (mod (7) (3)) (1))
8mod3 # <title> One-digit Modulo </title>
(= (mod (8) (3)) (2))
9mod3 # <title> One-digit Modulo </title>
(= (mod (9) (3)) (0))
10mod3 # <title> One-digit Modulo </title>
(= (mod (10) (3)) (1))
2mod4 # <title> One-digit Modulo </title>
(= (mod (2) (4)) (2))
3mod4 # <title> One-digit Modulo </title>
(= (mod (3) (4)) (3))
4mod4 # <title> One-digit Modulo </title>
(= (mod (4) (4)) (0))
5mod4 # <title> One-digit Modulo </title>
(= (mod (5) (4)) (1))
6mod4 # <title> One-digit Modulo </title>
(= (mod (6) (4)) (2))
7mod4 # <title> One-digit Modulo </title>
(= (mod (7) (4)) (3))
8mod4 # <title> One-digit Modulo </title>
(= (mod (8) (4)) (0))
9mod4 # <title> One-digit Modulo </title>
(= (mod (9) (4)) (1))
10mod4 # <title> One-digit Modulo </title>
(= (mod (10) (4)) (2))
2mod5 # <title> One-digit Modulo </title>
(= (mod (2) (5)) (2))
3mod5 # <title> One-digit Modulo </title>
(= (mod (3) (5)) (3))
4mod5 # <title> One-digit Modulo </title>
(= (mod (4) (5)) (4))
5mod5 # <title> One-digit Modulo </title>
(= (mod (5) (5)) (0))
6mod5 # <title> One-digit Modulo </title>
(= (mod (6) (5)) (1))
7mod5 # <title> One-digit Modulo </title>
(= (mod (7) (5)) (2))
8mod5 # <title> One-digit Modulo </title>
(= (mod (8) (5)) (3))
9mod5 # <title> One-digit Modulo </title>
(= (mod (9) (5)) (4))
10mod5 # <title> One-digit Modulo </title>
(= (mod (10) (5)) (0))
LtReplaceLt1 # <title> Substitution </title> # <table> # (< A [ B ] ] ] ) # (< [ B ] [ C ] ) # (< A [ [ [ C ] ) # </table>
(< A B) , (< B C)(< A C)
(= (mod (+ (* (3) (* (10) (10))) (+ (* (6) (10)) (7))) (+ (10) (5))) (7))
modconExample # <title> Modulo Congruence Example </title> # <summary> 7 and 3 are congruent modulo 4. </summary>
(=mod (7) (3) (4))
modconExample2 # <title> Modulo Congruence Example </title> # <summary> 15 and 7 are congruent modulo 4. </summary>
(=mod (+ (10) (5)) (7) (4))

Whole Number Division Tables

4div2 # <title> Whole Number Division </title>
(= (div (4) (2)) (2))
6div2 # <title> Whole Number Division </title>
(= (div (6) (2)) (3))
8div2 # <title> Whole Number Division </title>
(= (div (8) (2)) (4))
10div2 # <title> Whole Number Division </title>
(= (div (10) (2)) (5))
6div3 # <title> Whole Number Division </title>
(= (div (6) (3)) (2))
9div3 # <title> Whole Number Division </title>
(= (div (9) (3)) (3))
12div3 # <title> Whole Number Division </title>
(= (div (+ (10) (2)) (3)) (4))
15div3 # <title> Whole Number Division </title>
(= (div (+ (10) (5)) (3)) (5))
18div3 # <title> Whole Number Division </title>
(= (div (+ (10) (8)) (3)) (6))
(= (div (7) (4)) (1))
8div4 # <title> Whole Number Division </title>
(= (div (8) (4)) (2))
12div4 # <title> Whole Number Division </title>
(= (div (+ (10) (2)) (4)) (3))
16div4 # <title> Whole Number Division </title>
(= (div (+ (10) (6)) (4)) (4))
20div4 # <title> Whole Number Division </title>
(= (div (* (2) (10)) (4)) (5))
10div5 # <title> Whole Number Division </title>
(= (div (10) (5)) (2))
15div5 # <title> Whole Number Division </title>
(= (div (+ (10) (5)) (5)) (3))
20div5 # <title> Whole Number Division </title>
(= (div (* (2) (10)) (5)) (4))
12div6 # <title> Whole Number Division </title>
(= (div (+ (10) (2)) (6)) (2))
18div6 # <title> Whole Number Division </title>
(= (div (+ (10) (8)) (6)) (3))
14div7 # <title> Whole Number Division </title>
(= (div (+ (10) (4)) (7)) (2))
16div8 # <title> Whole Number Division </title>
(= (div (+ (10) (6)) (8)) (2))
18div9 # <title> Whole Number Division </title>
(= (div (+ (10) (8)) (9)) (2))
(= (div (+ (* (3) (* (10) (10))) (+ (* (9) (10)) (1))) (+ (* (2) (10)) (3))) (+ (10) (7)))

Exponentiation Tables

2power2 # <title> Exponentiation </title>
(= (exp (2) (2)) (4))
2power3 # <title> Exponentiation </title>
(= (exp (2) (3)) (8))
2power4 # <title> Exponentiation </title>
(= (exp (2) (4)) (+ (10) (6)))
2power5 # <title> Exponentiation </title>
(= (exp (2) (5)) (+ (* (3) (10)) (2)))
2power6 # <title> Exponentiation </title>
(= (exp (2) (6)) (+ (* (6) (10)) (4)))
2power7 # <title> Exponentiation </title>
(= (exp (2) (7)) (+ (* (10) (10)) (+ (* (2) (10)) (8))))
2power8 # <title> Exponentiation </title>
(= (exp (2) (8)) (+ (* (2) (* (10) (10))) (+ (* (5) (10)) (6))))
2power9 # <title> Exponentiation </title>
(= (exp (2) (9)) (+ (* (5) (* (10) (10))) (+ (10) (2))))
2power10 # <title> Exponentiation </title>
(= (exp (2) (10)) (+ (* (10) (* (10) (10))) (+ (* (2) (10)) (4))))
3power2 # <title> Exponentiation </title>
(= (exp (3) (2)) (9))
3power3 # <title> Exponentiation </title>
(= (exp (3) (3)) (+ (* (2) (10)) (7)))
3power4 # <title> Exponentiation </title>
(= (exp (3) (4)) (+ (* (8) (10)) (1)))
4power2 # <title> Exponentiation </title>
(= (exp (4) (2)) (+ (10) (6)))
4power3 # <title> Exponentiation </title>
(= (exp (4) (3)) (+ (* (6) (10)) (4)))
4power4 # <title> Exponentiation </title>
(= (exp (4) (4)) (+ (* (2) (* (10) (10))) (+ (* (5) (10)) (6))))
5power2 # <title> Exponentiation </title>
(= (exp (5) (2)) (+ (* (2) (10)) (5)))
5power3 # <title> Exponentiation </title>
(= (exp (5) (3)) (+ (* (10) (10)) (+ (* (2) (10)) (5))))
5power4 # <title> Exponentiation </title>
(= (exp (5) (4)) (+ (* (6) (* (10) (10))) (+ (* (2) (10)) (5))))
6power2 # <title> Exponentiation </title>
(= (exp (6) (2)) (+ (* (3) (10)) (6)))
6power3 # <title> Exponentiation </title>
(= (exp (6) (3)) (+ (* (2) (* (10) (10))) (+ (10) (6))))
7power2 # <title> Exponentiation </title>
(= (exp (7) (2)) (+ (* (4) (10)) (9)))
7power3 # <title> Exponentiation </title>
(= (exp (7) (3)) (+ (* (3) (* (10) (10))) (+ (* (4) (10)) (3))))
8power2 # <title> Exponentiation </title>
(= (exp (8) (2)) (+ (* (6) (10)) (4)))
8power3 # <title> Exponentiation </title>
(= (exp (8) (3)) (+ (* (5) (* (10) (10))) (+ (10) (2))))
9power2 # <title> Exponentiation </title>
(= (exp (9) (2)) (+ (* (8) (10)) (1)))
9power3 # <title> Exponentiation </title>
(= (exp (9) (3)) (+ (* (7) (* (10) (10))) (+ (* (2) (10)) (9))))
10power2 # <title> Exponentiation </title>
(= (exp (10) (2)) (* (10) (10)))
10power3 # <title> Exponentiation </title>
(= (exp (10) (3)) (* (10) (* (10) (10))))
10power4 # <title> Exponentiation </title>
(= (exp (10) (4)) (* (10) (* (10) (* (10) (10)))))

Divisibility Tables

2notdivides3 # <title> Divisibility </title>
(-. (| (2) (3)))
2divides4 # <title> Divisibility </title>
(| (2) (4))
2notdivides5 # <title> Divisibility </title>
(-. (| (2) (5)))
2divides6 # <title> Divisibility </title>
(| (2) (6))
2notdivides7 # <title> Divisibility </title>
(-. (| (2) (7)))
2divides8 # <title> Divisibility </title>
(| (2) (8))
2notdivides9 # <title> Divisibility </title>
(-. (| (2) (9)))
2divides10 # <title> Divisibility </title>
(| (2) (10))
2notdivides11 # <title> Divisibility </title>
(-. (| (2) (+ (10) (1))))
2divides12 # <title> Divisibility </title>
(| (2) (+ (10) (2)))
2notdivides13 # <title> Divisibility </title>
(-. (| (2) (+ (10) (3))))
2divides14 # <title> Divisibility </title>
(| (2) (+ (10) (4)))
2notdivides15 # <title> Divisibility </title>
(-. (| (2) (+ (10) (5))))
2divides16 # <title> Divisibility </title>
(| (2) (+ (10) (6)))
2notdivides17 # <title> Divisibility </title>
(-. (| (2) (+ (10) (7))))
2divides18 # <title> Divisibility </title>
(| (2) (+ (10) (8)))
2notdivides19 # <title> Divisibility </title>
(-. (| (2) (+ (10) (9))))
3notdivides4 # <title> Divisibility </title>
(-. (| (3) (4)))
3notdivides5 # <title> Divisibility </title>
(-. (| (3) (5)))
3divides6 # <title> Divisibility </title>
(| (3) (6))
3notdivides7 # <title> Divisibility </title>
(-. (| (3) (7)))
3notdivides8 # <title> Divisibility </title>
(-. (| (3) (8)))
3divides9 # <title> Divisibility </title>
(| (3) (9))
3notdivides10 # <title> Divisibility </title>
(-. (| (3) (10)))
3notdivides11 # <title> Divisibility </title>
(-. (| (3) (+ (10) (1))))
3divides12 # <title> Divisibility </title>
(| (3) (+ (10) (2)))
3notdivides13 # <title> Divisibility </title>
(-. (| (3) (+ (10) (3))))
3notdivides14 # <title> Divisibility </title>
(-. (| (3) (+ (10) (4))))
3divides15 # <title> Divisibility </title>
(| (3) (+ (10) (5)))
3notdivides16 # <title> Divisibility </title>
(-. (| (3) (+ (10) (6))))
3notdivides17 # <title> Divisibility </title>
(-. (| (3) (+ (10) (7))))
3divides18 # <title> Divisibility </title>
(| (3) (+ (10) (8)))
3notdivides19 # <title> Divisibility </title>
(-. (| (3) (+ (10) (9))))
4notdivides5 # <title> Divisibility </title>
(-. (| (4) (5)))
4notdivides6 # <title> Divisibility </title>
(-. (| (4) (6)))
4notdivides7 # <title> Divisibility </title>
(-. (| (4) (7)))
4divides8 # <title> Divisibility </title>
(| (4) (8))
4notdivides9 # <title> Divisibility </title>
(-. (| (4) (9)))
4notdivides10 # <title> Divisibility </title>
(-. (| (4) (10)))
4notdivides11 # <title> Divisibility </title>
(-. (| (4) (+ (10) (1))))
4divides12 # <title> Divisibility </title>
(| (4) (+ (10) (2)))
4notdivides13 # <title> Divisibility </title>
(-. (| (4) (+ (10) (3))))
4notdivides14 # <title> Divisibility </title>
(-. (| (4) (+ (10) (4))))
4notdivides15 # <title> Divisibility </title>
(-. (| (4) (+ (10) (5))))
4divides16 # <title> Divisibility </title>
(| (4) (+ (10) (6)))
4notdivides17 # <title> Divisibility </title>
(-. (| (4) (+ (10) (7))))
4notdivides18 # <title> Divisibility </title>
(-. (| (4) (+ (10) (8))))
4notdivides19 # <title> Divisibility </title>
(-. (| (4) (+ (10) (9))))
5notdivides6 # <title> Divisibility </title>
(-. (| (5) (6)))
5notdivides7 # <title> Divisibility </title>
(-. (| (5) (7)))
5notdivides8 # <title> Divisibility </title>
(-. (| (5) (8)))
5notdivides9 # <title> Divisibility </title>
(-. (| (5) (9)))
5divides10 # <title> Divisibility </title>
(| (5) (10))
5notdivides11 # <title> Divisibility </title>
(-. (| (5) (+ (10) (1))))
5notdivides12 # <title> Divisibility </title>
(-. (| (5) (+ (10) (2))))
5notdivides13 # <title> Divisibility </title>
(-. (| (5) (+ (10) (3))))
5notdivides14 # <title> Divisibility </title>
(-. (| (5) (+ (10) (4))))
5divides15 # <title> Divisibility </title>
(| (5) (+ (10) (5)))
5notdivides16 # <title> Divisibility </title>
(-. (| (5) (+ (10) (6))))
5notdivides17 # <title> Divisibility </title>
(-. (| (5) (+ (10) (7))))
5notdivides18 # <title> Divisibility </title>
(-. (| (5) (+ (10) (8))))
5notdivides19 # <title> Divisibility </title>
(-. (| (5) (+ (10) (9))))
6notdivides7 # <title> Divisibility </title>
(-. (| (6) (7)))
6notdivides8 # <title> Divisibility </title>
(-. (| (6) (8)))
6notdivides9 # <title> Divisibility </title>
(-. (| (6) (9)))
6notdivides10 # <title> Divisibility </title>
(-. (| (6) (10)))
6notdivides11 # <title> Divisibility </title>
(-. (| (6) (+ (10) (1))))
6divides12 # <title> Divisibility </title>
(| (6) (+ (10) (2)))
6notdivides13 # <title> Divisibility </title>
(-. (| (6) (+ (10) (3))))
7notdivides8 # <title> Divisibility </title>
(-. (| (7) (8)))
7notdivides9 # <title> Divisibility </title>
(-. (| (7) (9)))
7notdivides10 # <title> Divisibility </title>
(-. (| (7) (10)))
7notdivides11 # <title> Divisibility </title>
(-. (| (7) (+ (10) (1))))
7notdivides12 # <title> Divisibility </title>
(-. (| (7) (+ (10) (2))))
7notdivides13 # <title> Divisibility </title>
(-. (| (7) (+ (10) (3))))
8notdivides9 # <title> Divisibility </title>
(-. (| (8) (9)))
8notdivides10 # <title> Divisibility </title>
(-. (| (8) (10)))
8notdivides11 # <title> Divisibility </title>
(-. (| (8) (+ (10) (1))))
8notdivides12 # <title> Divisibility </title>
(-. (| (8) (+ (10) (2))))
8notdivides13 # <title> Divisibility </title>
(-. (| (8) (+ (10) (3))))
9notdivides10 # <title> Divisibility </title>
(-. (| (9) (10)))
9notdivides11 # <title> Divisibility </title>
(-. (| (9) (+ (10) (1))))
9notdivides12 # <title> Divisibility </title>
(-. (| (9) (+ (10) (2))))
9notdivides13 # <title> Divisibility </title>
(-. (| (9) (+ (10) (3))))
10notdivides11 # <title> Divisibility </title>
(-. (| (10) (+ (10) (1))))
10notdivides12 # <title> Divisibility </title>
(-. (| (10) (+ (10) (2))))
10notdivides13 # <title> Divisibility </title>
(-. (| (10) (+ (10) (3))))
11notdivides12 # <title> Divisibility </title>
(-. (| (+ (10) (1)) (+ (10) (2))))
11notdivides13 # <title> Divisibility </title>
(-. (| (+ (10) (1)) (+ (10) (3))))
12notdivides13 # <title> Divisibility </title>
(-. (| (+ (10) (2)) (+ (10) (3))))
SeqReplaceSeq1 # <title> Substitution </title> # <table> # (=_ S [ T ] ] ] ) # (=_ [ T ] [ U ] ) # (=_ S [ [ [ U ] ) # </table>
(=_ S T) , (=_ T U)(=_ S U)
SeqReplaceSeq1Un1 # <title> Substitution </title> # <table> # (=_ S (u. T [ U ] ] ] )) # (=_ [ U ] [ V ] ) # (=_ S (u. T [ [ [ V ] )) # </table>
(=_ S (u. T U)) , (=_ U V)(=_ S (u. T V))
EqReplaceSeq1Un1Sn0 # <title> Substitution </title> # <table> # (=_ S (u. T ({} [ A ] ] ] ))) # (= [ A ] [ B ] ) # (=_ S (u. T ({} [ [ [ B ] ))) # </table>
(=_ S (u. T ({} A))) , (= A B)(=_ S (u. T ({} B)))
SeqReplaceSeq1Un0 # <title> Substitution </title> # <table> # (=_ S (u. [ T ] ] ] V)) # (=_ [ T ] [ U ] ) # (=_ S (u. [ [ [ U ] V)) # </table>
(=_ S (u. T V)) , (=_ T U)(=_ S (u. U V))
2interval3 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (3)) (u. ({} (2)) ({} (3))))
2interval4 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (4)) (u. (u. ({} (2)) ({} (3))) ({} (4))))
2interval5 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (5)) (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))))
2interval6 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (6)) (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))))
2interval7 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (7)) (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))))
2interval8 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (8)) (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))))
2interval9 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (9)) (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))))
2interval10 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (10)) (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))))
2interval11 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (1))) (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))))
2interval12 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (2))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))))
2interval13 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (3))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))))

Prime Numbers

1elementsInSubset # <title> 1 Elements Inside Subset </title>
(e. A S)(C_ ({} A) S)
SeqReplaceSs0 # <title> Substitution </title> # <table> # (C_ [ S ] ] ] U) # (=_ [ S ] [ T ] ) # (C_ [ [ [ T ] U) # </table>
(C_ S U) , (=_ S T)(C_ T U)
3prime # <title> Prime Number Calculation </title>
(prime (3))
4notprime # <title> Prime Number Calculation </title>
(-. (prime (4)))
3elementsInSubset # <title> 3 Elements Inside Subset </title>
(e. A S) , (e. B S) , (e. C S)(C_ (u. (u. ({} A) ({} B)) ({} C)) S)
5prime # <title> Prime Number Calculation </title>
(prime (5))
6notprime # <title> Prime Number Calculation </title>
(-. (prime (6)))
5elementsInSubset # <title> 5 Elements Inside Subset </title>
(e. A S) , (e. B S) , (e. C S) , (e. D S) , (e. A' S)(C_ (u. (u. (u. (u. ({} A) ({} B)) ({} C)) ({} D)) ({} A')) S)
7prime # <title> Prime Number Calculation </title>
(prime (7))
8notprime # <title> Prime Number Calculation </title>
(-. (prime (8)))
9notprime # <title> Prime Number Calculation </title>
(-. (prime (9)))
10notprime # <title> Prime Number Calculation </title>
(-. (prime (10)))
9elementsInSubset # <title> 9 Elements Inside Subset </title>
(e. A S) , (e. B S) , (e. C S) , (e. D S) , (e. A' S) , (e. B' S) , (e. C' S) , (e. D' S) , (e. A0 S)(C_ (u. (u. (u. (u. (u. (u. (u. (u. ({} A) ({} B)) ({} C)) ({} D)) ({} A')) ({} B')) ({} C')) ({} D')) ({} A0)) S)
11prime # <title> Prime Number Calculation </title>
(prime (+ (10) (1)))
12notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (10) (2))))
11elementsInSubset # <title> 11 Elements Inside Subset </title>
(e. A S) , (e. B S) , (e. C S) , (e. D S) , (e. A' S) , (e. B' S) , (e. C' S) , (e. D' S) , (e. A0 S) , (e. A1 S) , (e. A2 S)(C_ (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} A) ({} B)) ({} C)) ({} D)) ({} A')) ({} B')) ({} C')) ({} D')) ({} A0)) ({} A1)) ({} A2)) S)
13prime # <title> Prime Number Calculation </title>
(prime (+ (10) (3)))
14notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (10) (4))))
15notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (10) (5))))
16notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (10) (6))))
SeqReplaceEl1 ---------------------------------------------------- Sets -------------------------------------------------# # <title> Substitution </title> # <table> # (e. A [ S ] ] ] ) # (=_ [ S ] [ T ] ) # (e. A [ [ [ T ] ) # </table>
(e. A S) , (=_ S T)(e. A T)
(e. (3) (u. (u. (u. (u. ({} (1)) ({} (2))) ({} (3))) ({} (4))) ({} (5))))
notIn4set # <title> Element Not Inside 4-Set </title>
(-. (= A B)) , (-. (= A C)) , (-. (= A D)) , (-. (= A A'))(-. (e. A (u. (u. (u. ({} B) ({} C)) ({} D)) ({} A'))))
(-. (e. (3) (u. (u. (u. ({} (1)) ({} (2))) ({} (4))) ({} (5)))))
SeqReplaceSeq1Un0Un0 # <title> Substitution </title> # <table> # (=_ S (u. (u. [ T ] ] ] V) S0)) # (=_ [ T ] [ U ] ) # (=_ S (u. (u. [ [ [ U ] V) S0)) # </table>
(=_ S (u. (u. T V) S0)) , (=_ T U)(=_ S (u. (u. U V) S0))
SeqReplaceSeq1Un0Un0Un0 # <title> Substitution </title> # <table> # (=_ S (u. (u. (u. [ T ] ] ] V) S0) S1)) # (=_ [ T ] [ U ] ) # (=_ S (u. (u. (u. [ [ [ U ] V) S0) S1)) # </table>
(=_ S (u. (u. (u. T V) S0) S1)) , (=_ T U)(=_ S (u. (u. (u. U V) S0) S1))
SeqReplaceSeq1Un0Un0Un1 # <title> Substitution </title> # <table> # (=_ S (u. (u. (u. T [ U ] ] ] ) S0) S1)) # (=_ [ U ] [ V ] ) # (=_ S (u. (u. (u. T [ [ [ V ] ) S0) S1)) # </table>
(=_ S (u. (u. (u. T U) S0) S1)) , (=_ U V)(=_ S (u. (u. (u. T V) S0) S1))
SeqReplaceSeq1Un0Un1 # <title> Substitution </title> # <table> # (=_ S (u. (u. T [ U ] ] ] ) S0)) # (=_ [ U ] [ V ] ) # (=_ S (u. (u. T [ [ [ V ] ) S0)) # </table>
(=_ S (u. (u. T U) S0)) , (=_ U V)(=_ S (u. (u. T V) S0))
SeqReplaceSeq1Un0Un0Un0Un1 # <title> Substitution </title> # <table> # (=_ S (u. (u. (u. (u. T [ U ] ] ] ) S0) S1) S2)) # (=_ [ U ] [ V ] ) # (=_ S (u. (u. (u. (u. T [ [ [ V ] ) S0) S1) S2)) # </table>
(=_ S (u. (u. (u. (u. T U) S0) S1) S2)) , (=_ U V)(=_ S (u. (u. (u. (u. T V) S0) S1) S2))
SeqReplaceSeq1Un1Un1 # <title> Substitution </title> # <table> # (=_ S (u. T (u. U [ V ] ] ] ))) # (=_ [ V ] [ S0 ] ) # (=_ S (u. T (u. U [ [ [ S0 ] ))) # </table>
(=_ S (u. T (u. U V))) , (=_ V S0)(=_ S (u. T (u. U S0)))
SeqReplaceSeq1Un1Un1Un0 # <title> Substitution </title> # <table> # (=_ S (u. T (u. U (u. [ V ] ] ] S1)))) # (=_ [ V ] [ S0 ] ) # (=_ S (u. T (u. U (u. [ [ [ S0 ] S1)))) # </table>
(=_ S (u. T (u. U (u. V S1)))) , (=_ V S0)(=_ S (u. T (u. U (u. S0 S1))))
(=_ (u. (u. (u. ({} (1)) ({} (4))) ({} (5))) (u. (u. ({} (2)) ({} (4))) ({} (8)))) (u. (u. (u. (u. ({} (1)) ({} (2))) ({} (4))) ({} (5))) ({} (8))))
EqReplaceEq0Fact0 # <title> Substitution </title> # <table> # (= (! [ A ] ] ] ) C) # (= [ A ] [ B ] ) # (= (! [ [ [ B ] ) C) # </table>
(= (! A) C) , (= A B)(= (! B) C)
factorial2 # <title> Factorial </title>
(= (! (2)) (2))
factorial3 # <title> Factorial </title>
(= (! (3)) (6))
factorial4 # <title> Factorial </title>
(= (! (4)) (+ (* (2) (10)) (4)))
factorial5 # <title> Factorial </title>
(= (! (5)) (+ (* (10) (10)) (* (2) (10))))
factorial6 # <title> Factorial </title>
(= (! (6)) (+ (* (7) (* (10) (10))) (* (2) (10))))
factorial7 # <title> Factorial </title>
(= (! (7)) (+ (* (5) (* (10) (* (10) (10)))) (* (4) (10))))
factorial8 # <title> Factorial </title>
(= (! (8)) (+ (* (4) (* (10) (* (10) (* (10) (10))))) (+ (* (3) (* (10) (10))) (* (2) (10)))))
(-. (| (7) (+ (* (2) (10)) (2))))
(| (7) (+ (* (3) (* (10) (10))) (+ (* (4) (10)) (3))))
(-. (= (+ (10) (8)) (+ (* (6) (10)) (7))))
exponentExample # <title> Exponentiation </title>
(= (exp (6) (4)) (+ (* (10) (* (10) (10))) (+ (* (2) (* (10) (10))) (+ (* (9) (10)) (6)))))
factorialExample # <title> Factorial </title>
(= (! (9)) (+ (* (3) (* (10) (* (10) (* (10) (* (10) (10)))))) (+ (* (6) (* (10) (* (10) (* (10) (10))))) (+ (* (2) (* (10) (* (10) (10)))) (+ (* (8) (* (10) (10))) (* (8) (10)))))))
(= (.- (+ (* (2) (* (10) (10))) (+ (* (4) (10)) (3))) (+ (* (10) (10)) (+ (* (8) (10)) (6)))) (+ (* (5) (10)) (7)))
EqReplaceEq1Add1Mul0 # <title> Substitution </title> # <table> # (= A (+ B (* [ C ] ] ] A'))) # (= [ C ] [ D ] ) # (= A (+ B (* [ [ [ D ] A'))) # </table>
(= A (+ B (* C A'))) , (= C D)(= A (+ B (* D A')))
(= (.- (+ (* (10) (10)) (+ (* (8) (10)) (6))) (+ (* (2) (* (10) (10))) (+ (* (4) (10)) (3)))) (0))
(<= (+ (* (4) (10)) (2)) (+ (* (6) (* (10) (10))) (+ (* (3) (10)) (9))))
(< (+ (* (2) (10)) (6)) (+ (* (7) (* (10) (10))) (+ (* (3) (10)) (9))))
GtReplaceGt1 # <title> Substitution </title> # <table> # (> A [ B ] ] ] ) # (> [ B ] [ C ] ) # (> A [ [ [ C ] ) # </table>
(> A B) , (> B C)(> A C)
10greater0 # <title> One-Digit Inequality </title>
(> (10) (0))
(> (+ (* (3) (* (10) (10))) (* (4) (10))) (+ (* (8) (10)) (1)))
EqReplaceEq1Mul0Product1 # <title> Substitution </title> # <table> # (= A (* (product B [ C ] ] ] S) A')) # (= [ C ] [ D ] ) # (= A (* (product B [ [ [ D ] S) A')) # </table>
(= A (* (product B C S) A')) , (= C D)(= A (* (product B D S) A'))
EqReplaceEq1Mul0Mul0 # <title> Substitution </title> # <table> # (= A (* (* [ B ] ] ] D) A')) # (= [ B ] [ C ] ) # (= A (* (* [ [ [ C ] D) A')) # </table>
(= A (* (* B D) A')) , (= B C)(= A (* (* C D) A'))
EqReplaceEq1Mul0Mul1 # <title> Substitution </title> # <table> # (= A (* (* B [ C ] ] ] ) A')) # (= [ C ] [ D ] ) # (= A (* (* B [ [ [ D ] ) A')) # </table>
(= A (* (* B C) A')) , (= C D)(= A (* (* B D) A'))
(= (product (1) (3) (lambda x (+ (* (2) x) (3)))) (+ (* (3) (* (10) (10))) (+ (10) (5))))
EqReplaceEq1Add0Sum1 # <title> Substitution </title> # <table> # (= A (+ (sum B [ C ] ] ] S) A')) # (= [ C ] [ D ] ) # (= A (+ (sum B [ [ [ D ] S) A')) # </table>
(= A (+ (sum B C S) A')) , (= C D)(= A (+ (sum B D S) A'))
(= (sum (5) (7) (lambda x (+ (exp x (2)) (* (3) x)))) (+ (* (10) (10)) (+ (* (6) (10)) (4))))
notPrimeExample # <title> Prime Number Calculation </title>
(-. (prime (+ (* (4) (10)) (2))))
SeqReplaceSs1 # <title> Substitution </title> # <table> # (C_ S [ T ] ] ] ) # (=_ [ T ] [ U ] ) # (C_ S [ [ [ U ] ) # </table>
(C_ S T) , (=_ T U)(C_ S U)
notIn2set # <title> Element Not Inside 2-Set </title>
(-. (= A B)) , (-. (= A C))(-. (e. A (u. ({} B) ({} C))))
(C. (u. ({} (2)) ({} (4))) (u. (u. (u. ({} (1)) ({} (2))) ({} (4))) ({} (5))))
(-. (C_ (u. (u. ({} (1)) ({} (3))) ({} (4))) (u. (u. (u. ({} (1)) ({} (2))) ({} (3))) ({} (5)))))
6notdivides17 # <title> Divisibility </title>
(-. (| (6) (+ (10) (7))))
7notdivides17 # <title> Divisibility </title>
(-. (| (7) (+ (10) (7))))
8notdivides17 # <title> Divisibility </title>
(-. (| (8) (+ (10) (7))))
9notdivides17 # <title> Divisibility </title>
(-. (| (9) (+ (10) (7))))
10notdivides17 # <title> Divisibility </title>
(-. (| (10) (+ (10) (7))))
11notdivides17 # <title> Divisibility </title>
(-. (| (+ (10) (1)) (+ (10) (7))))
12notdivides17 # <title> Divisibility </title>
(-. (| (+ (10) (2)) (+ (10) (7))))
13notdivides17 # <title> Divisibility </title>
(-. (| (+ (10) (3)) (+ (10) (7))))
14notdivides17 # <title> Divisibility </title>
(-. (| (+ (10) (4)) (+ (10) (7))))
15notdivides17 # <title> Divisibility </title>
(-. (| (+ (10) (5)) (+ (10) (7))))
16notdivides17 # <title> Divisibility </title>
(-. (| (+ (10) (6)) (+ (10) (7))))
2interval14 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (4))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))))
2interval15 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (5))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))) ({} (+ (10) (5)))))
2interval16 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (6))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))) ({} (+ (10) (5)))) ({} (+ (10) (6)))))
17prime # <title> Prime Number Calculation </title>
(prime (+ (10) (7)))
18notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (10) (8))))
6notdivides19 # <title> Divisibility </title>
(-. (| (6) (+ (10) (9))))
7notdivides19 # <title> Divisibility </title>
(-. (| (7) (+ (10) (9))))
8notdivides19 # <title> Divisibility </title>
(-. (| (8) (+ (10) (9))))
9notdivides19 # <title> Divisibility </title>
(-. (| (9) (+ (10) (9))))
10notdivides19 # <title> Divisibility </title>
(-. (| (10) (+ (10) (9))))
11notdivides19 # <title> Divisibility </title>
(-. (| (+ (10) (1)) (+ (10) (9))))
12notdivides19 # <title> Divisibility </title>
(-. (| (+ (10) (2)) (+ (10) (9))))
13notdivides19 # <title> Divisibility </title>
(-. (| (+ (10) (3)) (+ (10) (9))))
14notdivides19 # <title> Divisibility </title>
(-. (| (+ (10) (4)) (+ (10) (9))))
15notdivides19 # <title> Divisibility </title>
(-. (| (+ (10) (5)) (+ (10) (9))))
16notdivides19 # <title> Divisibility </title>
(-. (| (+ (10) (6)) (+ (10) (9))))
17notdivides19 # <title> Divisibility </title>
(-. (| (+ (10) (7)) (+ (10) (9))))
18notdivides19 # <title> Divisibility </title>
(-. (| (+ (10) (8)) (+ (10) (9))))
2interval17 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (7))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))) ({} (+ (10) (5)))) ({} (+ (10) (6)))) ({} (+ (10) (7)))))
2interval18 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (8))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))) ({} (+ (10) (5)))) ({} (+ (10) (6)))) ({} (+ (10) (7)))) ({} (+ (10) (8)))))
19prime # <title> Prime Number Calculation </title>
(prime (+ (10) (9)))
20notprime # <title> Prime Number Calculation </title>
(-. (prime (* (2) (10))))
2notdivides23 # <title> Divisibility </title>
(-. (| (2) (+ (* (2) (10)) (3))))
3notdivides23 # <title> Divisibility </title>
(-. (| (3) (+ (* (2) (10)) (3))))
4notdivides23 # <title> Divisibility </title>
(-. (| (4) (+ (* (2) (10)) (3))))
5notdivides23 # <title> Divisibility </title>
(-. (| (5) (+ (* (2) (10)) (3))))
6notdivides23 # <title> Divisibility </title>
(-. (| (6) (+ (* (2) (10)) (3))))
7notdivides23 # <title> Divisibility </title>
(-. (| (7) (+ (* (2) (10)) (3))))
8notdivides23 # <title> Divisibility </title>
(-. (| (8) (+ (* (2) (10)) (3))))
9notdivides23 # <title> Divisibility </title>
(-. (| (9) (+ (* (2) (10)) (3))))
10notdivides23 # <title> Divisibility </title>
(-. (| (10) (+ (* (2) (10)) (3))))
11notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (1)) (+ (* (2) (10)) (3))))
12notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (2)) (+ (* (2) (10)) (3))))
13notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (3)) (+ (* (2) (10)) (3))))
14notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (4)) (+ (* (2) (10)) (3))))
15notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (5)) (+ (* (2) (10)) (3))))
16notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (6)) (+ (* (2) (10)) (3))))
17notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (7)) (+ (* (2) (10)) (3))))
18notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (8)) (+ (* (2) (10)) (3))))
19notdivides23 # <title> Divisibility </title>
(-. (| (+ (10) (9)) (+ (* (2) (10)) (3))))
20notdivides23 # <title> Divisibility </title>
(-. (| (* (2) (10)) (+ (* (2) (10)) (3))))
21notdivides23 # <title> Divisibility </title>
(-. (| (+ (* (2) (10)) (1)) (+ (* (2) (10)) (3))))
22notdivides23 # <title> Divisibility </title>
(-. (| (+ (* (2) (10)) (2)) (+ (* (2) (10)) (3))))
2interval19 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (10) (9))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))) ({} (+ (10) (5)))) ({} (+ (10) (6)))) ({} (+ (10) (7)))) ({} (+ (10) (8)))) ({} (+ (10) (9)))))
2interval20 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (* (2) (10))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))) ({} (+ (10) (5)))) ({} (+ (10) (6)))) ({} (+ (10) (7)))) ({} (+ (10) (8)))) ({} (+ (10) (9)))) ({} (* (2) (10)))))
2interval21 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (* (2) (10)) (1))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))) ({} (+ (10) (5)))) ({} (+ (10) (6)))) ({} (+ (10) (7)))) ({} (+ (10) (8)))) ({} (+ (10) (9)))) ({} (* (2) (10)))) ({} (+ (* (2) (10)) (1)))))
2interval22 # <title> Interval of Natural Numbers </title>
(=_ ({...} (2) (+ (* (2) (10)) (2))) (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. (u. ({} (2)) ({} (3))) ({} (4))) ({} (5))) ({} (6))) ({} (7))) ({} (8))) ({} (9))) ({} (10))) ({} (+ (10) (1)))) ({} (+ (10) (2)))) ({} (+ (10) (3)))) ({} (+ (10) (4)))) ({} (+ (10) (5)))) ({} (+ (10) (6)))) ({} (+ (10) (7)))) ({} (+ (10) (8)))) ({} (+ (10) (9)))) ({} (* (2) (10)))) ({} (+ (* (2) (10)) (1)))) ({} (+ (* (2) (10)) (2)))))
23prime # <title> Prime Number Calculation </title>
(prime (+ (* (2) (10)) (3)))
2divides24 # <title> Divisibility </title>
(| (2) (+ (* (2) (10)) (4)))
24notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (* (2) (10)) (4))))
5divides25 # <title> Divisibility </title>
(| (5) (+ (* (2) (10)) (5)))
25notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (* (2) (10)) (5))))
2divides26 # <title> Divisibility </title>
(| (2) (+ (* (2) (10)) (6)))
26notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (* (2) (10)) (6))))
3divides27 # <title> Divisibility </title>
(| (3) (+ (* (2) (10)) (7)))
27notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (* (2) (10)) (7))))
2divides28 # <title> Divisibility </title>
(| (2) (+ (* (2) (10)) (8)))
28notprime # <title> Prime Number Calculation </title>
(-. (prime (+ (* (2) (10)) (8))))
EqReplaceEq0Fibonacci0 # <title> Substitution </title> # <table> # (= (fibonacci [ A ] ] ] ) C) # (= [ A ] [ B ] ) # (= (fibonacci [ [ [ B ] ) C) # </table>
(= (fibonacci A) C) , (= A B)(= (fibonacci B) C)
EqReplaceEq1Add1Fibonacci0 # <title> Substitution </title> # <table> # (= A (+ B (fibonacci [ C ] ] ] ))) # (= [ C ] [ D ] ) # (= A (+ B (fibonacci [ [ [ D ] ))) # </table>
(= A (+ B (fibonacci C))) , (= C D)(= A (+ B (fibonacci D)))
fibonacci2 # <title> Fibonacci </title>
(= (fibonacci (2)) (1))
fibonacci3 # <title> Fibonacci </title>
(= (fibonacci (3)) (2))
fibonacci4 # <title> Fibonacci </title>
(= (fibonacci (4)) (3))
fibonacci5 # <title> Fibonacci </title>
(= (fibonacci (5)) (5))
fibonacci6 # <title> Fibonacci </title>
(= (fibonacci (6)) (8))
fibonacci7 # <title> Fibonacci </title>
(= (fibonacci (7)) (+ (10) (3)))
fibonacci8 # <title> Fibonacci </title>
(= (fibonacci (8)) (+ (* (2) (10)) (1)))
fibonacci9 # <title> Fibonacci </title>
(= (fibonacci (9)) (+ (* (3) (10)) (4)))
fibonacci10 # <title> Fibonacci </title>
(= (fibonacci (10)) (+ (* (5) (10)) (5)))
fibonacci11 # <title> Fibonacci </title>
(= (fibonacci (+ (10) (1))) (+ (* (8) (10)) (9)))
fibonacci12 # <title> Fibonacci </title>
(= (fibonacci (+ (10) (2))) (+ (* (10) (10)) (+ (* (4) (10)) (4))))
fibonacci13 # <title> Fibonacci </title>
(= (fibonacci (+ (10) (3))) (+ (* (2) (* (10) (10))) (+ (* (3) (10)) (3))))
fibonacci14 # <title> Fibonacci </title>
(= (fibonacci (+ (10) (4))) (+ (* (3) (* (10) (10))) (+ (* (7) (10)) (7))))
fibonacci15 # <title> Fibonacci </title>
(= (fibonacci (+ (10) (5))) (+ (* (6) (* (10) (10))) (10)))
EqReplaceEq0Tri0 # <title> Substitution </title> # <table> # (= (tri [ A ] ] ] ) C) # (= [ A ] [ B ] ) # (= (tri [ [ [ B ] ) C) # </table>
(= (tri A) C) , (= A B)(= (tri B) C)
triangle1 # <title> Triangle </title>
(= (tri (1)) (1))
triangle2 # <title> Triangle </title>
(= (tri (2)) (3))
triangle3 # <title> Triangle </title>
(= (tri (3)) (6))
triangle4 # <title> Triangle </title>
(= (tri (4)) (10))
triangle5 # <title> Triangle </title>
(= (tri (5)) (+ (10) (5)))
triangle6 # <title> Triangle </title>
(= (tri (6)) (+ (* (2) (10)) (1)))
triangle7 # <title> Triangle </title>
(= (tri (7)) (+ (* (2) (10)) (8)))
triangle8 # <title> Triangle </title>
(= (tri (8)) (+ (* (3) (10)) (6)))
triangle9 # <title> Triangle </title>
(= (tri (9)) (+ (* (4) (10)) (5)))
triangle10 # <title> Triangle </title>
(= (tri (10)) (+ (* (5) (10)) (5)))
substitutionExample # <summary> # This gives an example of the variable A being substituted into an expression # in place of the variable x. Substitutions can be performed automatically using # the evaluate button. # </summary>
(<-> ([/] A x (< (* (2) x) (exp (+ x y) (3)))) (< (* (2) A) (exp (+ A y) (3))))
emptyThm # <summary> This is used just for convenience to get an empty theorem. </summary>
(T)