Higher-Order Theorems You Can Prove in JITPRO

Five Demo Problems

More Sample Problems

Several Very Easy Problems for Beginners

Theorems about Group Theory

A Property of a Closure Operator

Theorems about Church Numerals

Graph Theory

Five Demo Problems

More Sample Problems

Lemmas are very helpful when proving the Injective Cantor Theorem. (See the CADE 2000 System Description of TPS for more details.)

Several Very Easy Problems For Beginners

(Trivial)

(Trivial)

Group Theory

Theorem 1.2(i) of Hungerford's Algebra

Theorem 1.2(iii) of Hungerford's Algebra

Theorem 1.2(iv) of Hungerford's Algebra using part (iii) proven above

Theorem 1.2(v) of Hungerford's Algebra using part (iii) proven above

A Property of a Closure Operator

Church Numerals

This follows from simply expanding abbreviations.

This uses induction and is relatively difficult.

Graph Theory