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))