#
# Arithmetic KB (Peano Arithmetic, Presburger Arithmetic, etc.)
#

# Source this file to establish the variable settings that
#	make up the definition of the arithemtic theories.


# Guard against using unset variables
	set -u


# Successor (the theory of one successor, Succ [succ])

	PA01="(forall ?X (not (= 0 (succ ?X))))"
	PA02="(forall (?X ?Y) (=> (= (succ ?X) (succ ?Y)) (= ?X ?Y)))"
	PA02V="(forall (?X ?Y) (<=> (= (succ ?X) (succ ?Y)) (= ?X ?Y)))"
	Succ="
		$PA01
		$PA02
		"

# Succ Theorems, Lemmas

	Succ01="(forall ?X (not (= (succ ?X) ?X)))"
	Succ02="(forall ?X (exists ?Y (= ?Y (succ ?X))))"

	SuccLemmaLibrary="
		$Succ01
		$Succ02
		"


# PrA: Presburger Arithmetic = Succ + Addition [+]

# Addition

	PA03="(forall ?X (= (+ ?X 0) ?X))"
	PA03V="(forall (?X ?Y) (<=> (= (+ ?X 0) ?Y) (= ?X ?Y)))"
	PA04="(forall (?X ?Y) (= (+ ?X (succ ?Y)) (succ (+ ?X ?Y))))"
	PA04V="(and (forall (?X ?Y ?Z) (<= (= (+ ?X (succ ?Y)) ?Z) (= (+ (+ ?X ?Y) (succ 0)) ?Z)))
(forall (?X ?Y ?Z) (=> (= (+ ?X (succ ?Y)) ?Z) (= (+ (+ ?X ?Y) (succ 0)) ?Z))))"

	PrA="
		$Succ
		$PA03
		$PA04
		$PA03V
		$PA04V
		"

	PrAV="
		$PA01
		$PA02V
		$PA03V
		$PA04V
		"

# PrA Theorems, Lemmas

	PrA01="(forall ?X (= (+ 0 ?X) ?X))"
	PrA02="(forall ?X (= (+ ?X 0) (+ 0 ?X)))"
	PrA03="(forall ?X (= (succ ?X) (+ ?X (succ 0))))"
	PrA04="(forall ?X (= (succ ?X) (+ (succ 0) ?X)))"
	PrA05="(forall ?Y (= (succ (succ (+ 0 ?Y))) (+ (succ 0) (succ ?Y))))"
	PrA06="(forall ?X (=> (not (exists ?Y (= ?X (+ ?Y ?Y)))) (exists ?Y (= (succ ?X) (+ ?Y ?Y)))))"
	PrA07="(forall (?Y ?X) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))"
	PrA08="(forall (?X ?Y) (=> (= (succ ?X) ?Y) (= ?Y (+ ?X (succ 0)))))"
	PrA09="(forall ?X (= (+ (succ ?X) 0) (succ (+ ?X 0))))"
	PrA10="(forall (?X ?Y) (forall ?Z (=> (and (= ?X (+ ?Y ?Y)) (= ?X (+ ?Z ?Z))) (= ?Y ?Z))))"
	PrA11="(forall (?X ?Y ?Z) (=> (= (succ ?X) (+ (succ ?Y) (succ ?Z))) (= ?X (succ (+ ?Y ?Z)))))"
	PrA12="(forall ?X (= (+ (succ ?X) 0) (succ (+ ?X 0))))"
	PrA13="(forall (?X ?Y) (=> (= ?X ?Y) (= (succ ?X) (succ ?Y))))"
	PrA14="(= (+ 0 0) 0)"
	PrA15="(not (exists ?X (= 0 (+ (succ ?X) (succ ?X)))))"
	PrA16="(forall (?X ?Y) (= (succ (succ (+ ?X ?Y))) (+ (succ ?X) (succ ?Y))))"
	PrA17="(forall (?X ?Y) (= (+ (succ 0) (+ ?X ?Y)) (succ (+ ?X ?Y))))"
	PrA18="(forall (?X ?Y) (=> (= 0 (+ ?X ?Y)) (and (= 0 ?X) (= 0 ?Y))))"
	PrA19="(forall (?X ?Y) (=> (= (+ ?X ?X) (+ ?Y ?Y)) (= ?X ?Y)))"
	PrA20="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) (+ ?X ?Z)) (= ?Y ?Z)))"
	PrA21="(forall (?X ?Y ?Z) (=> (= (+ ?Z ?X) (+ ?Y ?X)) (= ?Z ?Y)))"
	PrA22="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) (+ ?X ?Z)) (= (succ ?Y) (succ ?Z))))"
	PrA24="(= 0 (+ 0 0))"
	PrA25="(forall (?X ?Y) (=> (= (+ 0 ?X) (+ 0 ?Y)) (= ?X ?Y)))"
	PrA26="(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (succ (+ ?X ?Z))) (= ?Y ?Z)))"
	PrA27="(forall (?X ?Y) (= (succ (+ ?X ?Y)) (succ (+ ?Y ?X))))"
	PrA28="(forall (?X ?Y ?Z) (=> (= (+ (succ ?X) ?Y) (+ (succ ?X) ?Z)) (= ?Y ?Z)))"
	PrA29="(forall (?X ?Y) (= (+ (succ ?X) ?Y) (+ ?X (succ ?Y))))"
	PrA30="(forall (?X ?Y ?Z ?W) (<=> (= (+ ?X ?Y) (+ ?Z ?W)) (= (+ (succ ?X) (succ ?Y)) (+ (succ ?Z) (succ ?W)))))"
	PrA31="(forall (?X ?Y) (= (succ (succ (+ ?X ?Y))) (+ (succ ?X) (succ ?Y))))"
	PrA32="(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (+ ?X (succ ?Y)) (succ ?Z))))"
	PrA33="(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) ?Y) (succ ?Z))))"
	PrA34="(forall (?X ?Y) (=> (= (succ (succ ?X)) (succ (succ ?Y))) (= ?X ?Y)))"
	PrA35="(forall (?X ?Y) (= (succ (+ ?X ?Y)) (succ (+ ?Y ?X))))"
#	PrA36=""
	PrA37="(forall (?X ?Y ?Z ?W) (<=> (= (+ ?X ?Y) (+ ?Z ?W)) (= (succ (+ ?X ?Y)) (succ (+ ?Z ?W)))))"
	PrA38="(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) ?Z) (= (succ (+ ?X ?Y)) (succ ?Z))))"
	PrA39="(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (succ (+ ?X ?Z))) (= ?Y ?Z)))"
	PrA40="(forall (?X ?Y ?Z) (<=> (= (+ ?X ?Y) (+ ?X ?Z)) (= (+ ?X (succ ?Y)) (+ ?X (succ ?Z)))))"
	PrA41="(forall (?X ?Y ?Z) (<=> (= (+ ?Y ?X) (+ ?Z ?X)) (= (+ (succ ?Y) ?X) (+ (succ ?Z) ?X))))"
	PrA42="(forall (?X ?Y) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))"
	PrA43="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) ?Y) (succ ?Z))))"
	PrA44="(forall (?Y ?X ?Z) (=> (= (+ (succ ?X) ?Y) (succ ?Z)) (= (+ ?X ?Y) ?Z)))"
	PrA45="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ ?X (succ ?Y)) (succ ?Z))))"
	PrA46="(forall (?X ?Y ?Z) (=> (= (+ ?X (succ ?Y)) (succ ?Z)) (= (+ ?X ?Y) ?Z)))"
	PrA47="(forall (?X ?Y ?Z) (=> (= (+ (succ ?X) (succ ?Y)) (succ (succ ?Z))) (= (+ ?X ?Y) ?Z)))"
	PrA48="(forall (?X ?Y ?Z) (=> (= (+ ?X ?Y) ?Z) (= (+ (succ ?X) (succ ?Y)) (succ (succ ?Z)))))"
#	PrA49=""
#	PrA50=""
	PrA51="(forall (?X ?Y) (<=> (= (+ 0 0) (+ ?X ?X)) (= 0 ?X)))"
	PrA52="(forall (?X ?Y ?Z) (=> (= ?X ?Y) (= (+ ?X ?Z) (+ ?Y ?Z))))"
	PrA53="(forall (?X ?Y ?Z) (=> (= ?X ?Y) (= (+ ?Z ?X) (+ ?Z ?Y))))"
	PrA54="(forall (?X ?Y) (=> (= (+ ?X ?Y) ?X) (= ?Y 0)))"
	PrA55="(forall ?X (not (= ?X (succ ?X))))"
	PrA56="(forall (?X ?Y ?Z) (=> (= (succ (+ ?X ?Y)) (+ ?X ?Z)) (= (succ ?Y) ?Z)))"
	PrA57="(forall (?X ?Y ?Z) (=> (= (+ ?X (succ ?Y)) (+ ?X ?Z)) (= (succ ?Y) ?Z)))"
#	PrA58=""
	PrA59="(forall (?X ?Y ?Z) (<=> (= (+ (succ ?X) ?Y) (+ (succ ?X) ?Z)) (= (+ ?X ?Y) (+ ?X ?Z))))"
	PrA60="(forall (?X ?Y ?Z) (<=> (= (+ ?Y (succ ?X)) (+ ?Z (succ ?X))) (= (+ ?Y ?X) (+ ?Z ?X))))"
	PrA61="(forall (?X ?Y ?Z) (<=> (= (+ (succ ?X) ?Y) ?Z) (= (+ ?X ?Y) (succ ?Z))))"
#	PrA62=""

# Addition is commutative and associative

	CMAdd="(forall (?X ?Y) (= (+ ?X ?Y) (+ ?Y ?X)))"
	AssocAdd="(forall (?X ?Y ?Z) (= (+ (+ ?X ?Y) ?Z) (+ ?X (+ ?Y ?Z))))"


# Theorems of Presburger Arithmetic

	PrALemmaLibrary="
		$PrA
		$PrA01
		$PrA03
		$PrA04
		$PrA05
		$PrA06
		$PrA07
		$PrA08
		$PrA09
		$PrA10
		$PrA11
		$PrA13
		$PrA15
		$PrA17
		$PrA18
		$PrA19
		$PrA21
		$PrA22
		$PrA24
		$PrA25
		$PrA26
		$PrA28
		$PrA30
		$PrA31
		$PrA32
		$PrA33
		$PrA34
		$PrA35
		$PrA37
		$PrA38
		$PrA39
		$PrA40
		$PrA41
		$PrA42
		$PrA43
		$PrA45
		$PrA46
		$PrA47
		$PrA48
		$PrA51
		$PrA52
		$PrA53
		$PrA54
		$PrA55
		$PrA56
		$PrA57
		$PrA59
		$PrA60
		$PrA61
		$CMAdd
		$AssocAdd
		"


# PrAOE: PrA + Odd/Even

# Evenness

	Even="(forall ?X (<=> (even ?X) (exists ?Y (= ?X (+ ?Y ?Y)))))"
	EvenV="(forall ?X (<=> (even ?X) (not (odd ?X))))"

# Oddness

	OddV="(forall ?X (<=> (odd ?X) (forall ?Y (not (= ?X (+ ?Y ?Y))))))"
	Odd="(forall ?X (<=> (odd ?X) (not (even ?X))))"

	OE="
		$Even
		$Odd
		"

	PrAOE="
		$PrA
		$OE
		"

# PrAOE Theorems, Lemmas

	PrAOE01="(even 0)"
	PrAOE02="(even (+ 0 0))"
	PrAOE03="(not (even (succ 0)))"
	PrAOE04="(even (succ (succ 0)))"
	PrAOE05="(odd (succ 0))"
	PrAOE06="(not (odd 0))"
	PrAOE07="(even (succ (succ (succ (succ (succ (succ (succ (succ 0)))))))))"
	PrAOE08="(odd (succ (succ (succ (succ (succ (succ (succ 0))))))))"
	PrAOE09="(forall ?X (=> (even ?X) (even (+ 0 ?X))))"
	PrAOE10="(forall ?X (even (+ ?X ?X)))"
	PrAOE11="(forall ?X (<=> (even ?X) (not (odd ?X))))"
	PrAOE12="(forall ?X (=> (even ?X) (even (+ ?X ?X))))"
	PrAOE13="(forall ?X (or (even ?X) (odd ?X)))"
	PrAOE14="(forall ?X (=> (even ?X) (even (succ (succ ?X)))))"
	PrAOE15="(forall ?X (=> (even ?X) (even (+ (succ (succ 0)) ?X))))"
	PrAOE16="(forall ?X (=> (even ?X) (odd (succ ?X))))"
	PrAOE17="(forall ?X (<=> (even ?X) (not (odd ?X))))"
	PrAOE18="(forall ?X (=> (odd ?X) (even (succ ?X))))"
	PrAOE19="(forall ?X (=> (odd ?X) (odd (succ (succ ?X)))))"
	PrAOE20="(forall ?X (<=> (odd ?X) (not (even ?X))))"
	PrAOE21="(forall (?X ?Y) (=> (and (even ?X) (even ?Y)) (even (+ ?X ?Y))))"
	PrAOE22="(forall (?X ?Y) (=> (even (+ ?X ?Y)) (even (+ (succ ?X) (succ ?Y)))))"
	PrAOE23="(forall (?X ?Y) (=> (and (odd ?X) (odd ?Y)) (even (+ ?X ?Y))))"
	PrAOE24="(forall (?X ?Y) (=> (and (odd ?X) (even ?Y)) (odd (+ ?X ?Y))))"
	PrAOE25="(forall (?X ?Y) (=> (odd (+ ?X ?Y)) (or (odd ?X) (odd ?Y))))"
	PrAOE26="(forall (?X ?Y) (= (succ (succ (+ ?X ?Y))) (+ (succ ?X) (succ ?Y))))"
	PrAOE27="(forall ?X (=> (even (succ (succ ?X))) (even ?X)))"
	PrAOE28="(forall ?X(or (not (odd ?X)) (not (even ?X))))"
	PrAOE30="(forall ?X (<= (even (succ (succ ?X))) (even ?X)))"
	PrAOE31="(forall (?X ?Y) (<=> (= ?Y (+ (+ ?X ?X) (succ 0))) (odd ?Y)))"
	PrAOE32="(forall (?X ?Y) (=> (even (+ ?X ?Y)) (even (+ ?Y ?X))))"


# Theorems of Presburger arithmetic plus oddness / evenness

	PrAOELemmaLibrary="
		$PrAOE01
		$PrAOE02
		$PrAOE03
		$PrAOE04
		$PrAOE05
		$PrAOE06
	;	$PrAOE07
	;	$PrAOE08
		$PrAOE09
		$PrAOE10
		$PrAOE11
		$PrAOE12
		$PrAOE13
		$PrAOE14
		$PrAOE15
		$PrAOE16
		$PrAOE17
		$PrAOE18
		$PrAOE19
		$PrAOE20
		$PrAOE21
		$PrAOE22
		$PrAOE23
		$PrAOE24
		$PrAOE25
		$PrAOE26
		$PrAOE27
		$PrAOE28
	;	$PrAOE30
		$PrAOE31
		$PrAOE32
		"



# Less Than [<], Less Than Or Equal [=<], etc.

	LT="(forall (?X ?Y) (<=> (< ?X ?Y) (exists ?Z (and (not (= 0 ?Z)) (= (+ ?X ?Z) ?Y)))))"
	LTV="(forall (?X ?Y) (<=> (< ?X ?Y) (forall ?Z (=> (not (= ?Z 0)) (not (= ?X (+ ?Y ?Z)))))))"
	LTV1="(forall (?X ?Y) (<=> (< ?X ?Y) (not (=< ?Y ?X))))"
	LTOrEq="(forall (?X ?Y) (<=> (exists ?Z (= ?X (+ ?Y ?Z))) (=< ?Y ?X)))"
	LTOrEqV1="(forall (?X ?Y) (<=> (=< ?X ?Y) (not (< ?Y ?X))))"

	LessThan="
		$LT
		$LTV
		$LTV1
		"

	LessThanOrEqual="
		$LTOrEq
		$LTOrEqV1
		"


# PrALT: PrA + LT

	PrALT="
		$PrA
		$LT
		$LessThanOrEqual
		"

# PrALT Theorems, Lemmas

	PrALT01="(< 0 (succ 0))"
	PrALT02="(=< 0 (succ 0))"
	PrALT03="(< (succ 0) (succ (succ 0)))"
	PrALT04="(=< (succ 0) (succ (succ 0)))"
	PrALT05="(forall ?X (=> (< 0 ?X) (< ?X (+ ?X ?X))))"
	PrALT06="(forall ?X (< ?X (succ ?X)))"
	PrALT07="(forall ?X (=< ?X (succ ?X)))"
	PrALT08="(forall ?X (not (< ?X ?X)))"
	PrALT09="(forall ?X (=< ?X ?X))"
	PrALT10="(forall (?X ?Y) (or (=< ?X ?Y) (=< ?Y ?X)))"
	PrALT11="(forall (?X ?Y) (=> (< ?X ?Y) (=< ?X ?Y)))"
	PrALT12="(forall (?X ?Y) (<=> (=< ?X ?Y) (or (= ?X ?Y) (< ?X ?Y))))"
	PrALT13="(forall (?X ?Y) (<=> (=< ?X ?Y) (or (= ?X ?Y) (not (< ?Y ?X)))))"
	PrALT14="(forall (?X ?Y) (=> (and (=< ?X ?Y) (not (= ?X ?Y))) (< ?X ?Y)))"
	PrALT15="(forall (?X ?Y) (=< ?X (+ ?X ?Y)))"
	PrALT16="(forall (?X ?Y) (=> (not (= ?Y 0)) (< ?X (+ ?X ?Y))))"
	PrALT17="(forall (?X ?Y) (=> (< 0 ?Y) (< ?X (+ ?X ?Y))))"
	PrALT18="(forall (?Y ?X ?Z) (=> (and (< ?X ?Y) (< ?Y ?Z)) (< ?X ?Z)))"
	PrALT19="(forall (?Y ?X) (forall ?Z (=> (and (=< ?X ?Y) (=< ?Y ?Z)) (=< ?X ?Z))))"
	PrALT20="(forall ?X (exists ?Y (< ?X ?Y)))"
	PrALT21="(forall ?X (exists ?Y (=< ?X ?Y)))"
	PrALT22="(forall (?X ?Y) (=> (and (=< ?X ?Y) (=< ?Y ?X)) (= ?X ?Y)))"
	PrALT23="(forall (?X ?Y) (=> (= ?X ?Y) (=< ?X ?Y)))"
	PrALT24="(forall ?X (not (=< (succ ?X) ?X)))"
	PrALT25="(forall ?X (=< 0 ?X))"
	PrALT26="(forall (?X ?Y) (<=> (=< ?X ?Y) (=< (succ ?X) (succ ?Y))))"
	PrALT27="(forall ?X (not (< (succ ?X) ?X)))"
	PrALT28="(forall (?X ?Y) (<=> (< ?X ?Y) (< (succ ?X) (succ ?Y))))"
	PrALT29="(forall (?X ?Y) (<=> (< ?X ?Y) (=< (succ ?X) ?Y)))"
	PrALT30="(forall (?X ?Y) (=> (=< (succ ?X) ?Y) (=< ?X ?Y)))"
	PrALT31="(forall (?X ?Y) (=> (=< (succ ?X) ?Y) (< ?X ?Y)))"
	PrALT32="(forall (?X ?Y) (=> (< (succ ?X) ?Y) (< ?X ?Y)))"
	PrALT33="(forall ?X (not (= ?X (succ ?X))))"
	PrALT34="(forall (?X ?Y) (<=> (= ?X ?Y) (= (succ ?X) (succ ?Y))))"
	PrALT35="(forall (?X ?Y ?Z ?W ?T) (=> (and (= (+ ?X ?Y) ?Z) (= (+ ?Z ?W) ?T)) (= (+ ?X (+ ?Y ?W)) ?T)))"
	PrALT36="(forall (?X ?Y) (<=> (= ?X ?Y) (= (+ ?X 0) ?Y)))"
	PrALT37="(forall (?X ?Y ?Z) (= (+ (+ ?X ?Y) (+ ?Y ?Z)) (+ (+ ?X (+ ?Y ?Y)) ?Z)))"
	PrALT38="(forall (?X ?Y) (=> (or (not (= 0 ?X)) (not (= 0 ?Y))) (not (= 0 (+ ?X ?Y)))))"
	PrALT39="(forall (?X ?Y) (=> (< 0 ?Y) (< ?X (+ ?X ?Y))))"
	PrALT40="(forall ?X (not (< ?X 0)))"
	PrALT41="(forall (?X ?Y) (<=> (< ?X (succ ?Y)) (or (= ?X ?Y) (< ?X ?Y))))"
	PrALT42="(forall (?X ?Y) (or (< ?X ?Y) (< ?Y ?X) (= ?X ?Y)))"
	PrALT43="(forall (?X ?Y) (<=> (< ?X ?Y) (and (not (= ?X ?Y)) (not (< ?Y ?X)))))"
	PrALT44="(forall (?X ?Y) (<=> (= ?X ?Y) (and (not (< ?X ?Y)) (not (< ?Y ?X)))))"
	PrALT45="(forall (?X ?Y) (<=> (not (= ?X ?Y)) (or (< ?X ?Y) (< ?Y ?X))))"
	PrALT46="(forall (?X ?Y) (=> (< ?X ?Y) (not (= ?X ?Y))))"
	PrALT47="(forall (?X ?Y) (=> (< (succ ?X) ?Y) (< ?X ?Y)))"
	PrALT48="(forall (?X ?Y) (<=> (not (= ?X ?Y)) (or (< ?X ?Y) (< ?Y ?X))))"
	PrALT49="(forall (?X ?Y) (<=> (< ?X ?Y) (< (succ ?X) (succ ?Y))))"
	PrALT50="(forall (?X ?Y) (<=>  (=< ?X ?Y) (=< (succ ?X) (succ ?Y))))"

# Theorems of Presburger arithmetic plus less-than

	PrALTLemmaLibrary="
		$PrALT01
		$PrALT02
		$PrALT03
		$PrALT04
		$PrALT05
		$PrALT06
		$PrALT07
		$PrALT08
		$PrALT09
		$PrALT10
		$PrALT11
		$PrALT12
		$PrALT13
		$PrALT14
		$PrALT15
		$PrALT16
		$PrALT17
		$PrALT18
		$PrALT19
		$PrALT20
		$PrALT21
		$PrALT22
		$PrALT23
		$PrALT24
		$PrALT25
		$PrALT26
		$PrALT27
		$PrALT28
		$PrALT29
		$PrALT30
		$PrALT31
		$PrALT32
		$PrALT33
		$PrALT34
		$PrALT35
		$PrALT36
		$PrALT37
		$PrALT38
		$PrALT39
		$PrALT40
		$PrALT41
		$PrALT42
		$PrALT43
		$PrALT44
		$PrALT45
		$PrALT46
		$PrALT47
		$PrALT48
		$PrALT49
		$PrALT50
		"


# PrAOELT: Theorems of Presburger Arithmetic plus oddness / evenness and less-than

	PrAOELT="
		$PrA
		$OE
		$LT
		$LessThanOrEqual
		"

# PrOELT Theorems, Lemmas



# PA: Peano Arithmetic = PrA + Multiplication [*]

# Multiplication

	PA05="(forall ?X (= (* ?X 0) 0))"
	PA05V="(forall (?X ?Y) (<=> (= (* ?X 0) ?Y) (= 0 ?Y)))"
	PA06="(forall (?X ?Y) (= (* ?X (succ ?Y)) (+ (* ?X ?Y) ?X)))"
	PA06V="(forall (?X ?Y ?Z) (<=> (= (* ?X (succ ?Y)) ?Z) (= (+ (* ?X ?Y) ?X) ?Z)))"

	PA="
		$PrA
		$PA05
		$PA06
		$PA05V
		$PA06V
		"

	PAThm01="(forall (?X ?Y ?Z) (=> (and (not (= ?X 0)) (= (* ?X ?Y) (* ?X ?Z))) (= ?Y ?Z)))"
	PAThm02="(forall (?X ?Y ?Z) (=> (and (not (= ?X 0)) (= (* ?Y ?X) (* ?Z ?X))) (= ?Y ?Z)))"
	PAThm03="(forall (?X ?Y ?Z) (= (* ?X (+ ?Y ?Z)) (+ (* ?X ?Y) (* ?X ?Z))))"
	PAThm03V="(forall (?X ?Y ?Z) (= (* (+ ?Y ?Z) ?X) (+ (* ?Y ?X) (* ?Z ?X))))"
	PAThm04="(forall ?X (= ?X (* (succ 0) ?X)))"
	PAThm04V="(forall ?X (= ?X (* ?X (succ 0))))"
	PAThm05="(forall ?X (= (* 0 ?X) 0))"
	PAThm06="(forall (?X ?Y) (= (* (succ ?X) ?Y) (+ (* ?X ?Y) ?Y)))"

# Multiplication is commutative and associative

	CMMult="(forall (?X ?Y) (= (* ?X ?Y) (* ?Y ?X)))"
	AssocMult="(forall (?X ?Y ?Z) (= (* (* ?X ?Y) ?Z) (* ?X (* ?Y ?Z))))"


# PA Theorems, Lemmas

# s(X) = X + s(0)

	PA11="(forall ?X (= (succ ?X) (+ ?X (succ 0))))"
	PA12="(forall ?X (= (succ ?X) (+ (succ 0) ?X)))"


# 0 + X = X
#	(Schaum's prob. 11.17, pg. 290)

	PA13="(forall ?X (= (+ 0 ?X) ?X))"


# s(X) + Y = s(X + Y)
#	(Schaum's prob. 11.18, pg. 291)

	PA14="(forall (?Y ?X) (= (+ (succ ?X) ?Y) (succ (+ ?X ?Y))))"


# X + Y = Y + X
#	(Schaum's prob. 11.19, pg. 292)

	PA15="
		$CMAdd
		"


# 1 * X = X

	PA16="(forall ?X (= (* (succ 0) ?X) ?X))"


# 0 * X = 0

	PA17="(forall ?X (= (* 0 ?X) 0))"
	PA17a="(forall ?X (= 0 (* 0 ?X)))"


# s(X) + Y = s(X + Y)

	PA18="(forall (?Y ?X) (= (* (succ ?X) ?Y) (+ (* ?X ?Y) ?Y)))"


# X * Y = Y * X

	PA19="
		$CMMult
		"

# Theorems of Peano Arithmetic

	PALemmaLibrary="
		$PAThm01
		$PAThm02
		$PAThm03
		$PAThm03V
		$PAThm04
		$PAThm04V
		$PAThm05
		$PAThm06
		$CMMult
		$AssocMult
		"


# PAOE: PA + Odd/Even

# PAOE Theorems, Lemmas

	PAOE01="(odd (* (succ 0) (succ 0)))"
	PAOE02="(even (* 0 0))"
	PAOE03="(forall ?X (even (* 0 ?X)))"
	PAOE04="(forall ?X (=> (even ?X) (even (* ?X ?X))))"
	PAOE05="(forall (?X ?Y) (=> (even ?X) (even (* ?X ?Y))))"
	PAOE06="(forall (?X ?Y) (=> (and (even ?X) (odd ?Y)) (even (* ?X ?Y))))"
	PAOE07="(forall (?X ?Y) (=> (and (odd ?X) (odd ?Y)) (odd (* ?X ?Y))))"
	PAOE08="(forall (?X ?Y) (=> (even (* ?X ?Y)) (even (* ?Y ?X))))"
	PAOE09="(forall (?X ?Y) (<=> (even (* ?X ?Y)) (even (* (succ ?X) (succ ?Y)))))"
	PAOE10="(forall (?X ?Y) (=> (odd (* ?X ?Y)) (even (* (succ ?X) ?Y))))"
	PAOE11="(forall (?X ?Y) (=> (odd (* ?X ?Y)) (even (* ?X (succ ?Y)))))"
	PAOE12="(forall (?X ?Y) (=> (even (* ?X ?Y)) (or (even ?X) (even ?Y))))"

	PAOE="
		$PA
		$OE
		"

	PAOELemmaLibrary="
		$PAOE01
		$PAOE02
		$PAOE03
		$PAOE04
		$PAOE05
	;	$PAOE06
		$PAOE07
		$PAOE08
		$PAOE09
		$PAOE10
		$PAOE11
		$PAOE12
		"



# PALT: PA + LT

	PALT="
		$PA
		$LT
		$LessThanOrEqual
		"

# PALT Theorems, Lemmas

	PALT01="(forall (?X ?Y) (=> (and (< 0 ?X) (< 0 ?Y)) (=< (+ ?X ?Y) (* ?X ?Y))))"
	PALT02="(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (+ ?X ?Y) (* ?X ?Y))))"
	PALT03="(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (succ ?X) (* ?X ?Y))))"
	PALT04="(forall (?X ?Y) (=> (and (< (succ 0) ?X) (< (succ 0) ?Y)) (< (succ (+ ?X ?Y)) (* ?X ?Y))))"
	PALT05="(forall (?X ?Y) (=> (< 0 ?Y) (< (* ?X ?Y) (* (succ ?X) ?Y))))"
	PALT06="(forall (?X ?Y) (=> (< 0 ?X) (< (* ?X ?Y) (* ?X (succ ?Y)))))"
	PALT07="(forall (?X ?Y) (=> (and (< 0 ?X) (< 0 ?Y)) (< (succ (+ ?X ?Y)) (succ (* ?X ?Y)))))"
	PALT08="(forall (?X ?Y ?Z) (=> (and (< (succ 0) ?Z) (< 0 ?X) (< 0 ?Y)) (< (* ?X ?Y) (* ?X (* ?Y ?Z)))))"



# PALT Lemma Library
	PALTLemmaLibrary="
		$PALT01
		$PALT02
		$PALT03
		$PALT04
		$PALT05
		$PALT06
		$PALT07
		$PALT08
		"


# PAOELT: PA + OE + LT

	PAOELT="
		$PAOE
		$LT
		$LessThanOrEqual
		"

# PAOELT Theorems, Lemmas


# PALTMinus:

	MinusX0="(forall ?X (= (- ?X 0) ?X))"
	MinusXX="(forall ?X (= (- ?X ?X) 0))"
	Minus="(forall ?X (A))"
	MinusLTSucc="(forall (?X ?Y) (=> (< ?Y ?X) (= (succ (- ?X ?Y)) (- (succ ?X) ?Y))))"
	MinusLT0X="(forall (?X ?Y) (or (= ?X 0) (< 0 ?X)))"
	MinusLTSucc="(forall (?X ?Y) (< (- ?X ?Y) (- (succ ?X) ?Y)))"

	PrALTMinus="
		$PrA
		$LT
		$MinusX0
		$MinusLTSucc
		$MinusLT0X
		"

	PrALTMinus01="(= (- (succ 0) 0) (succ 0))"
	PrALTMinus02="(= (- (succ (succ (succ 0))) (succ (succ 0))) (succ 0))"


# Arithmetic
	ArithmeticLibrary="
		$PA
		$LT
		$LessThanOrEqual
		$OE
		$SuccLemmaLibrary
		$PrALemmaLibrary
		$PrALTLemmaLibrary
		$PrAOELemmaLibrary
		$PALemmaLibrary
		$PALTLemmaLibrary
		$PAOELemmaLibrary
		"