The Theory misc
Parents

init
Children

pair
Constants
Arbitrary
'a
$1
('a BOOL) BOOL
Let
('a 'b) 'a 'b
Cond
BOOL 'a 'a 'a
icl'TS
BOOL BOOL
Aliases
$= : BOOL BOOL BOOL
Fixity


Binder:1 Infix 10:
Terminators

1
Definitions
1
1_def
$1 = ( P t P t ( x P x x = t))
Let
let_def
Let = ( f x f x)
Cond
cond_def
Cond
= ( b x1 x2
x ((b T) x = x1) ((b F) x = x2))
icl'TS
icl'ts_def
x icl'TS x x
Theorems
t_thm
T
_thm
t1 t2 t1 t2 ( b (t1 b) (t2 b) b)
_thm
t t t F
f_thm
F
_t_thm
T F
_thm
t1 t2 t1 t2 ( b (t1 t2 b) b)
_thm1
t t t F
cond_thm
a t1 t2
(if a then t1 else t2)
= ( x ((a T) x = t1) ((a F) x = t2))
__thm
p $ p ( x p x)
__thm
p $ p ( x p x)
1_thm
P $1 P ( t P t ( x P x x = t))
_thm
a b (a b) (a b) (b a)
_thm
a b a b a b
__thm
a a a
__thm
a b (a b) a b
__thm
a b (a b) a b
__thm
a b (a b) a b
__thm
a b (a b) a b b a
_f_thm
F T
_if_thm
a b c
(if a then b else c) (if a then b else c)
if_thm
a b c (if a then b else c) a b a c
eq_rewrite_thm
x x = x T
_rewrite_thm
t
((T t) t)
((t T) t)
((F t) t)
((t F) t)
_rewrite_thm
t ( t t) ( T F) ( F T)
_rewrite_thm
t
(T t t)
(t T t)
(F t)
(t F)
(t t t)
_rewrite_thm
t
(T t)
(t T)
(F t t)
(t F t)
(t t t)
_rewrite_thm
t
(T t t)
(F t T)
(t T T)
(t t T)
(t F t)
if_rewrite_thm
t1 t2
(if T then t1 else t2) = t1
(if F then t1 else t2) = t2
_rewrite_thm
t ( x t) t
_rewrite_thm
t ( x t) t
_rewrite_thm
t1 t2 ( x t1) t2 = t1
one_one_thm
f OneOne f ( x y f x = f y x = y)
ext_thm
f g f = g ( x f x = g x)
type_lemmas_thm
pred
( f TypeDefn pred f)
( abs rep
( a abs (rep a) = a)
( r pred r rep (abs r) = r))
fun_rel_thm
r
( f x y f x = y r x y)
( x y r x y ( z r x z z = y))

up quick index © RBJ