Entry	Value
Package Name	bool-int
Count	82
Theorems	ABS_SIMP : !t1 t2. (\x. t1) t2 = t1 AND_FALSE_THM : !t. t /\ F <=> F AND_FORALL_THM : !p q. (!x. p x) /\ (!x. q x) <=> (!x. p x /\ q x) AND_TRUE_THM : !t. t /\ T <=> t BETA_THM : !f y. (\x. f x) y = f y CONJ_ASSOC' : !t1 t2 t3. (t1 /\ t2) /\ t3 <=> t1 /\ t2 /\ t3 CONJ_REFL : !t. t /\ t <=> t CONJ_SYM : !t1 t2. t1 /\ t2 <=> t2 /\ t1 DISJ_ASSOC' : !t1 t2 t3. (t1 \/ t2) \/ t3 <=> t1 \/ t2 \/ t3 DISJ_REFL : !t. t \/ t <=> t DISJ_SYM : !t1 t2. t1 \/ t2 <=> t2 \/ t1 EQ_FALSE_THM : !t. (t <=> F) <=> ~t EQ_IMP : !a b. (a <=> b) ==> a ==> b EQ_REFL : !x. x = x EQ_SYM : !x y. x = y ==> y = x EQ_SYM_EQ : !x y. x = y <=> y = x EQ_TRANS : !x y z. x = y /\ y = z ==> x = z EQ_TRUE_THM : !t. (t <=> T) <=> t EXISTS_OR_THM : !p q. (?x. p x \/ q x) <=> (?x. p x) \/ (?x. q x) EXISTS_REFL : !a. ?x. x = a EXISTS_SIMP : !t. (?x. t) <=> t EXISTS_UNIQUE : !p. (?!x. p x) <=> (?x. p x /\ (!y. p y ==> y = x)) EXISTS_UNIQUE_ALT : !p. (?!x. p x) <=> (?x. !y. p y <=> x = y) EXISTS_UNIQUE_REFL : !a. ?!x. x = a EXISTS_UNIQUE_THM : !p. (?!x. p x) <=> (?x. p x) /\ (!x x'. p x /\ p x' ==> x = x') FALSE_AND_THM : !t. F /\ t <=> F FALSE_EQ_THM : !t. (F <=> t) <=> ~t FALSE_IMP_THM : !t. F ==> t <=> T FALSE_OR_THM : !t. F \/ t <=> t FORALL_AND_THM : !p q. (!x. p x /\ q x) <=> (!x. p x) /\ (!x. q x) FORALL_SIMP : !t. (!x. t) <=> t FORALL_UNWIND_THM1 : !p a. (!x. a = x ==> p x) <=> p a FORALL_UNWIND_THM2 : !p a. (!x. x = a ==> p x) <=> p a IMP_AND_DISTRIB : !p q r. p ==> q /\ r <=> (p ==> q) /\ (p ==> r) IMP_FALSE_THM : !t. t ==> F <=> ~t IMP_IMP : !p q r. p ==> q ==> r <=> p /\ q ==> r IMP_REFL : !t. t ==> t IMP_TRUE_THM : !t. t ==> T <=> T LEFT_AND_DISTRIB : !p q r. p \/ q /\ r <=> (p \/ q) /\ (p \/ r) LEFT_AND_EXISTS_THM : !p q. (?x. p x) /\ q <=> (?x. p x /\ q) LEFT_AND_FORALL_THM : !p q. (!x. p x) /\ q <=> (!x. p x /\ q) LEFT_EXISTS_AND_THM : !p q. (?x. p x /\ q) <=> (?x. p x) /\ q LEFT_FORALL_IMP_THM : !p q. (!x. p x ==> q) <=> (?x. p x) ==> q LEFT_IMP_EXISTS_THM : !p q. (?x. p x) ==> q <=> (!x. p x ==> q) LEFT_OR_DISTRIB : !p q r. p /\ (q \/ r) <=> p /\ q \/ p /\ r LEFT_OR_EXISTS_THM : !p q. (?x. p x) \/ q <=> (?x. p x \/ q) MONO_AND : !p1 p2 q1 q2. (p1 ==> p2) /\ (q1 ==> q2) ==> p1 /\ q1 ==> p2 /\ q2 MONO_EXISTS : !p q. (!x. p x ==> q x) ==> (?x. p x) ==> (?x. q x) MONO_FORALL : !p q. (!x. p x ==> q x) ==> (!x. p x) ==> (!x. q x) MONO_IMP : !p1 p2 q1 q2. (p2 ==> p1) /\ (q1 ==> q2) ==> (p1 ==> q1) ==> p2 ==> q2 MONO_NOT : !p q. (q ==> p) ==> ~p ==> ~q MONO_OR : !p1 p2 q1 q2. (p1 ==> p2) /\ (q1 ==> q2) ==> p1 \/ q1 ==> p2 \/ q2 NOT_FALSE_THM : ~F <=> T NOT_TRUE_THM : ~T <=> F OR_EXISTS_THM : !p q. (?x. p x) \/ (?x. q x) <=> (?x. p x \/ q x) OR_FALSE_THM : !t. t \/ F <=> t OR_IMP_DISTRIB : !p q r. p \/ q ==> r <=> (p ==> r) /\ (q ==> r) OR_TRUE_THM : !t. t \/ T <=> T RIGHT_AND_DISTRIB : !p q r. p /\ q \/ r <=> (p \/ r) /\ (q \/ r) RIGHT_AND_EXISTS_THM : !p q. p /\ (?x. q x) <=> (?x. p /\ q x) RIGHT_AND_FORALL_THM : !p q. p /\ (!x. q x) <=> (!x. p /\ q x) RIGHT_EXISTS_AND_THM : !p q. (?x. p /\ q x) <=> p /\ (?x. q x) RIGHT_FORALL_IMP_THM : !p q. (!x. p ==> q x) <=> p ==> (!x. q x) RIGHT_IMP_FORALL_THM : !p q. p ==> (!x. q x) <=> (!x. p ==> q x) RIGHT_OR_DISTRIB : !p q r. (p \/ q) /\ r <=> p /\ r \/ q /\ r RIGHT_OR_EXISTS_THM : !p q. p \/ (?x. q x) <=> (?x. p \/ q x) SWAP_EXISTS_THM : !p. (?x y. p x y) <=> (?y x. p x y) SWAP_FORALL_THM : !p. (!x y. p x y) <=> (!y x. p x y) TRIV_AND_EXISTS_THM : !p q. (?x. p) /\ (?x. q) <=> (?x. p /\ q) TRIV_EXISTS_AND_THM : !p q. (?x. p /\ q) <=> (?x. p) /\ (?x. q) TRIV_EXISTS_IMP_THM : !p q. (?x. p ==> q) <=> (!x. p) ==> (?x. q) TRIV_FORALL_IMP_THM : !p q. (!x. p ==> q) <=> (?x. p) ==> (!x. q) TRIV_FORALL_OR_THM : !p q. (!x. p \/ q) <=> (!x. p) \/ (!x. q) TRIV_OR_FORALL_THM : !p q. (!x. p) \/ (!x. q) <=> (!x. p \/ q) TRUE_AND_THM : !t. T /\ t <=> t TRUE_EQ_THM : !t. (T <=> t) <=> t TRUE_IMP_THM : !t. T ==> t <=> t TRUE_OR_THM : !t. T \/ t <=> T TRUTH : T UNWIND_THM1 : !p a. (?x. a = x /\ p x) <=> p a UNWIND_THM2 : !p a. (?x. x = a /\ p x) <=> p a WLOG_RELATION : !r p. (!x y. p x y ==> p y x) /\ (!x y. r x y \/ r y x) /\ (!x y. r x y ==> p x y) ==> (!x y. p x y)

Back to main package page