Entry Value
Package Name bool-class
Count 41
Theorems
  • BOOL_CASES_AX : !t. (t <=> T) \/ (t <=> F)
  • COND_ABS : !b f g. (\x. if b then f x else g x) = (if b then f else g)
  • COND_ELIM_THM : !p c x y. p (if c then x else y) <=> (c ==> p x) /\ (~c ==> p y)
  • COND_EXPAND : !b t1 t2. (if b then t1 else t2) <=> (~b \/ t1) /\ (b \/ t2)
  • COND_FALSE : !t1 t2. (if F then t1 else t2) = t2
  • COND_ID : !b t. (if b then t else t) = t
  • COND_NOT : !c x y. (if ~c then x else y) = (if c then y else x)
  • COND_RAND : !b f x y. f (if b then x else y) = (if b then f x else f y)
  • COND_RATOR : !b f g x. (if b then f else g) x = (if b then f x else g x)
  • COND_TRUE : !t1 t2. (if T then t1 else t2) = t1
  • CONTRAPOS_THM : !t1 t2. ~t1 ==> ~t2 <=> t2 ==> t1
  • EXCLUDED_MIDDLE : !t. t \/ ~t
  • EXISTS_BOOL_THM : !p. (?b. p b) <=> p T \/ p F
  • EXISTS_NOT_THM : !p. (?x. ~p x) <=> ~(!x. p x)
  • EXISTS_THM : (?) = (\p. p ((@) p))
  • FORALL_BOOL_THM : !p. (!b. p b) <=> p T /\ p F
  • FORALL_NOT_THM : !p. (!x. ~p x) <=> ~(?x. p x)
  • LEFT_EXISTS_IMP_THM : !p q. (?x. p x ==> q) <=> (!x. p x) ==> q
  • LEFT_FORALL_OR_THM : !p q. (!x. p x \/ q) <=> (!x. p x) \/ q
  • LEFT_IMP_FORALL_THM : !p q. (!x. p x) ==> q <=> (?x. p x ==> q)
  • LEFT_OR_FORALL_THM : !p q. (!x. p x) \/ q <=> (!x. p x \/ q)
  • MONO_COND : !b p q r s. (p ==> q) /\ (r ==> s) ==> (if b then p else r) ==> (if b then q else s)
  • NOT_AND_THM : !t1 t2. ~(t1 /\ t2) <=> ~t1 \/ ~t2
  • NOT_EXISTS_THM : !p. ~(?x. p x) <=> (!x. ~p x)
  • NOT_FORALL_THM : !p. ~(!x. p x) <=> (?x. ~p x)
  • NOT_IFF_THM : !t1 t2. (~t1 <=> ~t2) <=> t1 <=> t2
  • NOT_IMP : !t1 t2. ~(t1 ==> t2) <=> t1 /\ ~t2
  • NOT_NOT_THM : !t. ~ ~t <=> t
  • NOT_OR_THM : !t1 t2. ~(t1 \/ t2) <=> ~t1 /\ ~t2
  • RIGHT_EXISTS_IMP_THM : !p q. (?x. p ==> q x) <=> p ==> (?x. q x)
  • RIGHT_FORALL_OR_THM : !p q. (!x. p \/ q x) <=> p \/ (!x. q x)
  • RIGHT_IMP_EXISTS_THM : !p q. p ==> (?x. q x) <=> (?x. p ==> q x)
  • RIGHT_OR_FORALL_THM : !p q. p \/ (!x. q x) <=> (!x. p \/ q x)
  • SELECT_REFL : !x. (@y. y = x) = x
  • SELECT_UNIQUE : !p x. (!y. p y <=> y = x) ==> (@) p = x
  • SKOLEM_THM : !r. (!x. ?y. r x y) <=> (?f. !x. r x (f x))
  • SKOLEM_THM_GEN : !p r. (!x. p x ==> (?y. r x y)) <=> (?f. !x. p x ==> r x (f x))
  • UNIQUE_SKOLEM_ALT : !p. (!x. ?!y. p x y) <=> (?f. !x y. p x y <=> f x = y)
  • UNIQUE_SKOLEM_THM : !p. (!x. ?!y. p x y) <=> (?!f. !x. p x (f x))
  • bool_INDUCT : !p. p F /\ p T ==> (!x. p x)
  • bool_RECURSION : !a b. ?f. f F = a /\ f T = b
    		•
    Back to main package page