(define aor
  [lambda V [E V]] -> E	where (not (free? V E))
  [lambda X Y] -> [lambda X (aor Y)]
  [[lambda X Y] Z] -> (let Alpha (alpha [lambda X Y])
                                     (aor (beta Alpha (aor Z))))
  [X Y] -> (let AOR [(aor X) (aor Y)]
                    (if (= AOR [X Y])
                        AOR
                        (aor AOR)))
  X -> X)

(define free?
   V V -> true
   V [lambda V _] -> false
   V [lambda _ Y] -> (free? V Y)
   V [X Y] -> (or (free? V X) (free? V Y))
   _ _ -> false)

(define alpha
  [lambda X Y] -> (let V (gensym x)
                             [lambda V (replace X (alpha Y) V)])
  [X Y] -> [(alpha X) (alpha Y)]
  X -> X)

(define beta
  [lambda X Y] Z -> (replace X Y Z))

(define replace
  X [lambda X Y] _ -> [lambda X Y]
  X X Z -> Z
  X [Y Y*] Z -> [(replace X Y Z) (replace X Y* Z)]
  X [lambda Y Y*] Z -> [lambda Y (replace X Y* Z)]
  _ Y _ -> Y)     

(define t
  -> [lambda x [lambda y x]])

(define f
  -> [lambda x [lambda y y]])

(define if*
   -> [lambda z [lambda x [lambda y [[z x] y]]]])

(aor [[[(if*) (t)] a] b])

(aor [[[(if*) (f)] a] b])

(define curry
  [lambda X Y] -> [lambda X (curry Y)]
  [W X Y | Z] ->  (curry [[W X] Y | Z])
  [X Y] -> [(curry X) (curry Y)]
  X -> X)

(define aor+
   X -> (aor (curry X)))

(aor+ [(if*) (f) a b])   

(define aor
  [[lambda X Y] Z] -> (aor (replace X Y Z))
  [X Y] -> (let AOR [(aor X) (aor Y)]
                    (if (= AOR [X Y]) AOR  (aor AOR)))
  X -> X)

(define replace
  X [lambda X Y] _ -> [lambda X Y]
  X X Z -> Z
  X [Y Y'] Z -> [(replace X Y Z) (replace X Y* Z)]
  X [lambda Y Y*] Z -> [lambda Y (replace X Y* Z)]
  _ Y _ -> Y)