type lambda = Var of string | App of (lambda * lambda) | Abs of (string * lambda) | Nil type sk = S of sk list | K of sk list val s : lambda val k : lambda val i : lambda val w : lambda val y_term : lambda val pair_term : lambda -> lambda -> lambda val if_term : lambda val true_term : lambda val false_term : lambda val fst_term : lambda val snd_term : lambda val iszero_term : lambda val incr_term : lambda val paral_term : lambda val paral_term2 : lambda val string_of_lambda : lambda -> string val ( /- ) : 'a -> 'a list -> bool val exclude : 'a -> 'a list -> 'a list val unique : 'a list -> 'a list val union : 'a list -> 'a list -> 'a list val intersect : 'a list -> 'a list -> 'a list val fv : lambda -> string list val cx : lambda -> string -> string list val all_vars : lambda -> string list val replace : lambda -> string -> lambda -> lambda val bound_replace : lambda -> string -> string -> lambda val ( =@ ) : lambda -> lambda -> bool val new_name : string -> string list -> string val conv_red : lambda -> string -> lambda -> lambda val redex_reduction : lambda -> lambda val energetic_reduction : lambda -> lambda val parallel_reduction : lambda -> lambda list val parallel_reduction_full : lambda -> lambda val normal_reduction : lambda -> bool * lambda val all_reductions : lambda -> lambda list val normal_form : lambda -> int -> lambda val normal_forming : lambda -> lambda list val sk_comb : lambda -> lambda val lambda_of_sk : sk -> lambda val check_term : string -> int val output : (lambda -> 'a) -> ('a -> unit) -> lambda -> unit