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