(*
   LAMBDA FUNFAIR, by Artur Miguel Dias and Luis Caires, April 2000
   
   A LAMBDA CALCULUS INTERPRETER written in Caml Light (version 0.71/mac)


CONVENTIONS:
~~~~~~~~~~~
1. The lambda terms are represented using strings:
            "@x.x", "@xy.fx", "@x.@y.(f x)"
2. The Greek symbol "lambda" is represented by the symbol "@".
3. Macro names are all in upper case:
            "OMEGA", "ID", "ZERO", "ONE", ...
4. A variable is a lower case letter, possibly followed by some digits:
            "a", "x", "v1", "z123", ...

COMMANDS:
~~~~~~~~
lambda  - returns the internal representation of a lambda term
print   - prints a lambda term (given its internal representation)
free    - returns the free names of a lambda term
subst   - prints the result of a substitution
eval    - prints the normal form of lambda term (MAY LOOP)
trace   - prints the individual reduction steps of the evaluation of a term
macro   - adds a macro to the macro table
clear   - clears the macro table
list    - lists the macro table

EXAMPLES:
~~~~~~~~
#macro "OMEGA" "@x.xx" ;;
- : string = "MACRO OMEGA defined"
#lambda "@x.fx" ;;
- : LambdaExpression = Abstraction ("x", Apply (Variable "f", Variable "x"))
#print (lambda "@x.x") ;;
(@x.x)
- : unit = ()
#free "@x.fx" ;;
- : string list = ["f"]
#subst "@x.fx" "f" "y" ;;
(@x.(y x))
- : unit = ()
#eval "ISZERO ZERO" ;;
(@x.(@y.x))
- : unit = ()
#trace "ISZERO ZERO" ;;
(((@x.(@f.x)) (@x.(@y.x))) (@x.(@x.(@y.y))));
((@f.(@x.(@y.x))) (@x.(@x.(@y.y))));
(@x.(@y.x));
- : unit = ()
*)

(******************** ERROR & FAILURE ********************)

exception error ;;
exception fail ;;

let Error str =
    print_string (str ^ ".\n") ;
    raise error
;;

(******************** SET ********************)

let rec Belongs v =
    fun   [] -> false
        | (x::xs) ->
                if v>x then
                    Belongs v xs
                else x=v
;;
let rec Union =
    fun   [] l -> l
        | l [] -> l
        | (x::xs) (y::ys) ->
                if x=y then
                    x::Union xs ys
                else if x<y then
                    x::Union xs (y::ys)
                else y::Union (x::xs) ys
;;
let rec Exclude v =
    fun   [] -> []
        | (x::xs) ->
                if x=v then xs
                else x::Exclude v xs
;;


(******************** DICTIONARY ********************)

let rec Translate key =
    fun   [] -> Error ("MACRO: " ^ key ^ " non existent")
        | ((k,trans)::xs) ->
                if k = key then trans
                else Translate key xs
;;

let rec Update key trans =
    fun   [] -> [(key,trans)]
        | ((k,t)::xs) ->
                if k = key then (k,trans)::xs
                else (k,t)::Update key trans xs
;;


(******************** LAMBDA EXPRESSIONS ********************)

type LambdaExpression =
      Variable of string
    | Abstraction of string * LambdaExpression
    | Apply of LambdaExpression * LambdaExpression
;;


(******************** MACROS ********************)

let lambdaMacros =          (* the macro table *)
    ref []
;;

let macro key trans =       (* add macro to the table *)
    lambdaMacros := Update key trans !lambdaMacros ;
    "MACRO " ^ key ^ " defined"
;;

let clear () =              (* clear macro table *)
    lambdaMacros := []
;;

let list () =               (* list all the macros *)
    !lambdaMacros
;;

macro "ID"      "@x.x" ;;
macro "OMEGA"   "@x.xx" ;;

let rec Size =
    fun (Variable var) ->
            1
      | (Abstraction (var,body)) ->
            1 + Size body
      | (Apply (func,arg)) ->
            1 + Size func + Size arg
;;


(******************** SCANNER ********************)

type LambdaToken =
    LambdaTK | DotTK | OpenParTK | CloseParTK | VarTK of string
;;

let GetChar str =
    (nth_char str 0, sub_string str 1 ((string_length str) - 1))
;;
let rec GetUpper str =
    if str = "" then ("", "")
    else
      let (ch,rest) = GetChar str in
        match ch with
              `A`..`Z` -> 
                let (upp,rest2) = GetUpper rest in
                    ((char_for_read ch)^upp, rest2)
            | _ -> ("", str)
;;
let rec GetDigits str =
    if str = "" then ("", "")
    else
      let (ch,rest) = GetChar str in
        match ch with
              `0`..`9` -> 
                let (nat,rest2) = GetDigits rest in
                    ((char_for_read ch)^nat, rest2)
            | _ -> ("", str)
;;

let rec Scan str =
    if str = "" then []
    else
      let (ch,rest) = GetChar str in
        match ch with
              ` ` -> Scan rest
            | `@` -> LambdaTK::Scan rest
            | `.` -> DotTK::Scan rest
            | `(` -> OpenParTK::Scan rest
            | `)` -> CloseParTK::Scan rest
            | `a`..`z` ->
                let (digs,rest2) = GetDigits rest in
                    (VarTK ((char_for_read ch)^digs))::Scan rest2
            | `A`..`Z` ->
                let (upp,rest2) = GetUpper str in
                    let trans = Translate upp !lambdaMacros in
                        [OpenParTK]@(Scan trans)@[CloseParTK]@(Scan rest2)
            | _ -> Error ("SCAN: Invalid char '" ^ (char_for_read ch) ^ "'")
;;


(******************** PARSER ********************)

let SkipClosePar =
    fun   [] -> Error "PARSER: Missing close parenthesis"
        | (x::xs) ->
                if x = CloseParTK then xs
                else Error "PARSER: Closing parenthesis missing"
;;
let rec ParseOne =
    fun   (VarTK(var)::xs) ->
            (Variable var, xs)
        | (LambdaTK::VarTK(var)::DotTK::xs) ->
            let (term,rest) = ParseLambda xs in
                (Abstraction (var,term), rest)
        | (OpenParTK::xs) ->
            let (term,rest) = ParseLambda xs in
                (term, SkipClosePar rest)
        | (LambdaTK::VarTK(var)::VarTK(var2)::xs) ->
            let (term,rest) = ParseOne (LambdaTK::VarTK(var2)::xs) in
                (Abstraction (var,term),rest)
        | _ -> raise fail
and ParseApply term rest =
    try
        let (term2,rest2) = ParseOne rest in
            ParseApply (Apply (term,term2)) rest2
    with fail -> (term, rest)
and ParseLambda tks =
    let (term,rest) = ParseOne tks in
        ParseApply term rest
;;

let StrToLambda str =
    try
      match ParseLambda (Scan str) with
          (term,[]) -> term
        | (term,_) -> Error "PARSER: Extra characters at the end"
    with fail ->
        Error "PARSER: Syntax error"
;;

let rec LambdaToString =
    fun   (Variable var) ->
                var
        | (Abstraction (var,body)) ->
                "(@" ^ var ^ "." ^ LambdaToString body ^ ")" ;      
        | (Apply (func,arg)) ->
                "(" ^ LambdaToString func ^ " " ^ LambdaToString arg ^ ")"
;;

let lambda str =
    StrToLambda str
;;
let print term =
    print_string (LambdaToString term) ;
    print_newline()
;;

(* TESTING
#lambda "@x.fx" ;;
- : LambdaExpression = Abstraction ("x", Apply (Variable "f", Variable "x"))
#print (lambda "@x.fx") ;;
(@x.(f x))
- : unit = ()
#print (lambda "@x1.x1x1") ;;
(@x1.(x1 x1))
- : unit = ()
#print (lambda "@xyzw.xy(zw)") ;;
(@x.(@y.(@z.(@w.((x y) (z w))))))
- : unit = ()
#print (lambda "OMEGA") ;;
(@x.(x x))
- : unit = ()
#print (lambda "OMEGA OMEGA") ;;
((@x.(x x)) (@x.(x x)))
- : unit = ()
*)


(******************** FREE NAMES ********************)

let rec FreeNames =
    fun   (Variable var) ->
                [var]
        | (Abstraction (var,body)) ->
                Exclude var (FreeNames body)
        | (Apply (func,arg)) ->
                Union (FreeNames func) (FreeNames arg)
;;

let free term = FreeNames (lambda term) ;;

(* TESTING
#free "@x.fx" ;;
- : string list = ["f"]
#free "@xy.xy" ;;
- : string list = []
*)


(******************** SUBSTITUITION ********************)

let var_counter =
    ref 0
;;
let UniqueVar () =
    var_counter := !var_counter + 1 ; 
    "v" ^ (string_of_int !var_counter)
;;
let rec Substituition e x t =
    match e with
          (Variable v) ->
            if v = x then t else e
        | (Abstraction (v,b)) ->
            if v = x then
                    (* e has no free ocurrences of x *)
                e
            else if not Belongs v (FreeNames t) then
                    (* no free ocurrences of v in t, so no capture *) 
                Abstraction (v, Substituition b x t)
            else
                    (* there are free ocurrences of v in t and they are
                        all captured -> use alpha equivalence *)
                let z = UniqueVar () in
                    let newBody = Substituition b v (Variable z) in
                        Abstraction (z, Substituition newBody x t)
        | (Apply (f,n)) ->
            Apply (Substituition f x t, Substituition n x t)
;;

let subst e x t =
    print (Substituition (lambda e) x (lambda t))
;;

(* TESTING
#subst "x" "x" "y" ;;
y
- : unit = ()
#subst "x" "x" "x" ;;
x
- : unit = ()
#subst "@x.fx" "x" "y" ;;
(@x.(f x))
- : unit = ()
#subst "@x.fx" "f" "y" ;;
(@x.(y x))
- : unit = ()
#subst "@x.fx" "f" "x" ;;
(@v1.(x v1))
- : unit = ()
*)


(******************** REDUCTION ********************)

(*
CONFLUENCE PROPERTY:
No two orders of evaluation can give different results (some orders may
    possibly fail to terminate).
        EVALUATION = "reduction to normal form".
        RESULT = "normal form" = "irreducible form"

OUT-LEFT ORDER of evaluation (Ordem de avaliação "TOPO-ESQUERDA"):
The outermost-leftmost redex is selected at each step.
This order of evaluation guarantees TERMINATION whenever a term is reducible.

INNER-RIGHT ORDER of evaluation:
The innermost-rightmost redex is selected at each step.
*)

let rec ReductionStepOutLeftOrder =
    fun (Variable var) ->
            raise fail
      | (Abstraction (var,body)) ->
            Abstraction (var, ReductionStepOutLeftOrder body)
      | (Apply (func,arg)) ->
            match func with
                  Abstraction (var,body) -> (* beta reduction *)
                    Substituition body var arg
                | _ ->
                    try Apply (ReductionStepOutLeftOrder func,arg)
                    with fail ->
                            Apply (func, ReductionStepOutLeftOrder arg)
;;
let rec ReductionStepInnerRightOrder =
    fun (Variable var) ->
            raise fail
      | (Abstraction (var,body)) ->
            Abstraction (var, ReductionStepInnerRightOrder body)
      | (Apply (func,arg)) ->
            try Apply (func, ReductionStepInnerRightOrder arg)
            with fail ->
                try Apply (ReductionStepInnerRightOrder func,arg)
                with fail ->
                    match func with
                          Abstraction (var,body) -> (* beta reduction *)
                                    Substituition body var arg
                        | _ -> raise fail
;;

let Evaluate redStep term =     (* MAY LOOP *)
    EvalLoop term
        where rec EvalLoop t =
                    try EvalLoop (redStep t)
                    with fail -> t
;;
let rec Trace redStep term =
    TraceLoop term
        where rec TraceLoop t =
                    try let next = redStep t in
                            print_string (LambdaToString next) ;
                            if read_line () = "q" then ()
                            else TraceLoop next
                    with fail -> ()
;;

let eval str =
    print (Evaluate ReductionStepOutLeftOrder (lambda str))
;;
let trace str =
    Trace ReductionStepOutLeftOrder (lambda str)
;;

(*****)

macro "K" "@yx.y" ;;
macro "I" "@x.x" ;;
macro "F" "@xf.f(fx)" ;;
macro "OMEGA" "@x.xx" ;;

(* TESTING -- Exercícios 8b) i. v. vi. vii. viii.
#trace "Kx" ;;
(@v1.x);
- : unit = ()
#trace "K I F" ;;
((@x.(@x.x)) (@x.(@f.(f (f x)))));
(@x.x);
- : unit = ()
#trace "K(I F)" ;;
(@x.((@x.x) (@x.(@f.(f (f x))))));
(@x.(@x.(@f.(f (f x)))));
- : unit = ()
#trace "OMEGA OMEGA" ;;
((@x.(x x)) (@x.(x x)));
((@x.(x x)) (@x.(x x)));
((@x.(x x)) (@x.(x x)));
((@x.(x x)) (@x.(x x)));
((@x.(x x)) (@x.(x x)))q
- : unit = ()
#trace "Kx(OMEGA OMEGA)" ;;
((@v2.x) ((@x.(x x)) (@x.(x x))));
x;
- : unit = ()
*)


(******************** BOOLEANS ********************)

macro "TRUE" "@xy.x" ;;
macro "FALSE" "@xy.y" ;;
macro "IF" "@abc.abc" ;;
macro "OR" "@ab.IF a TRUE b" ;;
macro "AND" "@ab.IF a b FALSE" ;;
macro "NOT" "@a.IF a FALSE TRUE" ;;

(* TESTING
#eval "IF TRUE OMEGA I" ;;
(@x.(x x))
- : unit = ()
#eval "IF FALSE OMEGA I" ;;
(@x.x)
- : unit = ()
*)


(******************** PAIRS ********************)

macro "PAIR" "@ab.@x.IF x a b" ;;
macro "FST" "@a.a TRUE" ;;
macro "SND" "@a.a FALSE" ;;


(******************** LISTS ********************)

macro "CONS" "PAIR" ;;
macro "HEAD" "FST" ;;
macro "TAIL" "SND" ;;
macro "NIL" "@x.TRUE" ;;
macro "NULL" "@a.a @xy.FALSE" ;;

(* TESTING
#eval "CONS TRUE NIL" ;;
(@x.((x (@x.(@y.x))) (@x.(@x.(@y.x)))))
- : unit = ()
#eval "CONS TRUE (CONS TRUE NIL)" ;;
(@x.((x (@x.(@y.x))) (@x.((x (@x.(@y.x))) (@x.(@x.(@y.x)))))))
- : unit = ()
#eval "NULL NIL" ;;
(@x.(@y.x))
- : unit = ()
#eval "NULL (CONS TRUE NIL)" ;;
(@x.(@y.y))
- : unit = ()
*)

(******************** CHURCH NUMERALS ********************)

macro "ZERO" "@xf.x" ;;
macro "SUCC" "@a.@xf.f(axf)" ;;
macro "PRED" "@a.SND (a (PAIR ZERO ZERO) (@p.PAIR (SUCC (FST p)) (FST p)))" ;;
macro "ISZERO" "@a.a TRUE (@x.FALSE)" ;;
macro "ADD" "@ab.a b SUCC" ;;
macro "SUB" "@ab.a PRED b" ;;
macro "MULT" "@ab.a ZERO (ADD b)" ;;

macro "GE" "@ab.ISZERO (a b PRED)" ;;
macro "LE" "@ab.GE b a" ;;
macro "EQ" "@ab.AND (GE a b) (LE a b)" ;;
macro "GT" "@ab.NOT (LE a b)" ;;
macro "LT" "@ab.NOT (GE a b)" ;;
macro "NE" "@ab.NOT (EQ a b)" ;;

macro "ONE" "SUCC ZERO" ;;
macro "TWO" "SUCC ONE" ;;
macro "THREE" "SUCC TWO" ;;
macro "FOUR" "SUCC THREE" ;;
macro "FIVE" "SUCC FOUR" ;;

macro "XADD" "@ab.@xf.a(bxf)f" ;;       (* alternative definitions *)
macro "XMULT" "@ab.@xf.ax(@w.bwf)" ;;

(* TESTING -- Exercício 9a)
#eval "ONE" ;;
(@x.(@f.(f x)))
- : unit = ()
#eval "TWO" ;;
(@x.(@f.(f (f x))))
- : unit = ()
#eval "FIVE" ;;
(@x.(@f.(f (f (f (f (f x)))))))
- : unit = ()
#eval "PRED FIVE" ;;
(@x.(@f.(f (f (f (f x))))))
- : unit = ()
#eval "PRED (MULT TWO FIVE)" ;;
(@x.(@f.(f (f (f (f (f (f (f (f (f x)))))))))))
- : unit = ()
#eval "PRED (MULT FIVE FIVE)" ;;
(@x.(@f.(f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f (f x))))))))))))))))))))))))))
- : unit = ()
#eval "ADD TWO FIVE" ;;
(@x.(@f.(f (f (f (f (f (f (f x)))))))))
- : unit = ()
#eval "MULT TWO THREE" ;;
(@x.(@f.(f (f (f (f (f (f x))))))))
- : unit = ()
#eval "ISZERO ZERO" ;;
(@x.(@y.x))
- : unit = ()
#eval "ISZERO ONE" ;;
(@x.(@y.y))
- : unit = ()
#eval "ISZERO TWO" ;;
(@x.(@y.y))
- : unit = ()
#eval "GE ZERO ONE" ;;
(@x.(@y.y))
- : unit = ()
#eval "GE ONE ONE" ;;
(@x.(@y.x))
- : unit = ()
#eval "GE TWO ONE" ;;
(@x.(@y.x))
- : unit = ()
#eval "EQ ONE ONE" ;;
(@x.(@y.x))
- : unit = ()
#eval "EQ TWO TWO" ;;
(@x.(@y.x))
- : unit = ()
#eval "EQ THREE THREE" ;;
(@x.(@y.x))
- : unit = ()
#eval "EQ FOUR FOUR" ;;
(@x.(@y.x))
- : unit = ()
#eval "EQ FIVE FIVE" ;;
(@x.(@y.x))
- : unit = ()
#eval "EQ THREE FIVE" ;;
(@x.(@y.y))
- : unit = ()
#eval "EQ FIVE THREE" ;;
(@x.(@y.y))
- : unit = ()
#eval "ONE" ;;
(@x.(@f.(f x)))
- : unit = ()
*)


(******************** RECURSION ********************)

macro "REC" "@h.(@x.h(xx))(@x.h(xx))" ;;

macro "SUM" "REC (@fn.IF (ISZERO n) ZERO (ADD n (f (PRED n))))" ;;
    (* let rec sum n = if n = 0 then 0 else n + sum (n-1) ;; *)
macro "FACT" "REC (@fn.IF (ISZERO n) ONE (MULT n (f (PRED n))))" ;;
    (* let rec fact n = if n = 0 then 1 else n * fact (n-1) ;; *)

    (* mutual recursion *)
macro "PSUM" "FST (REC (@f.PAIR (@n.IF (ISZERO n) ZERO (ADD n ((SND f) n))) (@n.((FST f) (PRED n)))))" ;;
    (* let rec psum x = if x = 0 then 0 else x + aux x
            and aux x = psum (x-1) ;;
     IS EQUIVALENT TO
       let rec f = ((fun n ->if n = 0 then 0 else (n + (snd f) n)),
                (fun n ->(fst f) (n-1)))
      let psum = fst f ;; *)

macro "DIV"
  "@ab.(REC (@fmc.IF (GT m a) c (f (ADD b m) (SUCC c)))) b ZERO" ;;

(* TESTING
#trace "RECf";;
((@x.(f (x x))) (@x.(f (x x))));
(f ((@x.(f (x x))) (@x.(f (x x)))));
(f (f ((@x.(f (x x))) (@x.(f (x x))))));
(f (f (f ((@x.(f (x x))) (@x.(f (x x)))))));
(f (f (f (f ((@x.(f (x x))) (@x.(f (x x))))))));
(f (f (f (f (f ((@x.(f (x x))) (@x.(f (x x)))))))));
(f (f (f (f (f (f ((@x.(f (x x))) (@x.(f (x x))))))))));
(f (f (f (f (f (f (f ((@x.(f (x x))) (@x.(f (x x)))))))))));
(f (f (f (f (f (f (f (f ((@x.(f (x x))) (@x.(f (x x))))))))))));
(f (f (f (f (f (f (f (f (f ((@x.(f (x x))) (@x.(f (x x)))))))))))))q
- : unit = ()
#eval "SUM ZERO" ;;
(@x.(@f.x))
- : unit = ()
#eval "SUM ONE" ;;
(@x.(@f.(f x)))
- : unit = ()
#eval "SUM TWO" ;;
(@x.(@f.(f (f (f x)))))
- : unit = ()
#eval "SUM THREE" ;;
(@x.(@f.(f (f (f (f (f (f x))))))))
- : unit = ()
#eval "SUM FOUR" ;;
(@x.(@f.(f (f (f (f (f (f (f (f (f (f x))))))))))))
- : unit = ()
#eval "PSUM ZERO" ;;
(@x.(@f.x))
- : unit = ()
#eval "PSUM ONE" ;;
(@x.(@f.(f x)))
- : unit = ()
#eval "PSUM TWO" ;;
(@x.(@f.(f (f (f x)))))
- : unit = ()
#eval "FACT ZERO" ;;
(@x.(@f.(f x)))
- : unit = ()
#eval "FACT ONE" ;;
(@x.(@f.(f x)))
- : unit = ()
#eval "FACT TWO" ;;
(@x.(@f.(f (f x))))
- : unit = ()
#trace "FACT ZERO" ;;
(((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) (@x.(@f.x)));

(((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) ((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))))) (@x.(@f.x)));

((@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n))))) (@x.(@f.x)));

((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) (@x.(@f.x)))) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) (@x.(@f.x))) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) (@x.(@f.x))))));

(((@b.(@c.((((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) (@x.(@f.x))) b) c))) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) (@x.(@f.x))) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) (@x.(@f.x))))));

((@c.((((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) (@x.(@f.x))) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) c)) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) (@x.(@f.x))) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) (@x.(@f.x))))));

((((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) (@x.(@f.x))) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) (@x.(@f.x))) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) (@x.(@f.x))))));

(((((@x.(@f.x)) (@x.(@y.x))) (@x.(@x.(@y.y)))) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) (@x.(@f.x))) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) (@x.(@f.x))))));

((((@f.(@x.(@y.x))) (@x.(@x.(@y.y)))) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) (@x.(@f.x))) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) (@x.(@f.x))))));

(((@x.(@y.x)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) (@x.(@f.x))) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) (@x.(@f.x))))));

((@y.((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) (@x.(@f.x))) (((@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x))) (@x.((@f.(@n.((((@a.(@b.(@c.((a b) c)))) ((@a.((a (@x.(@y.x))) (@x.(@x.(@y.y))))) n)) ((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)))) (((@a.(@b.((a (@x.(@f.x))) ((@a.(@b.((a b) (@a.(@x.(@f.(f ((a x) f)))))))) b)))) n) (f ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) n)))))) (x x)))) ((@a.((@a.(a (@x.(@y.y)))) ((a (((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) (@x.(@f.x))) (@x.(@f.x)))) (@p.(((@a.(@b.(@x.((((@a.(@b.(@c.((a b) c)))) x) a) b)))) ((@a.(@x.(@f.(f ((a x) f))))) ((@a.(a (@x.(@y.x)))) p))) ((@a.(a (@x.(@y.x)))) p)))))) (@x.(@f.x))))));

((@a.(@x.(@f.(f ((a x) f))))) (@x.(@f.x)));
(@x.(@f.(f (((@x.(@f.x)) x) f))));
(@x.(@f.(f ((@f.x) f))));
(@x.(@f.(f x)));
- : unit = ()
*)