=========================================================
Recognized function symbols in input:

  name                arity   strict-pos  binder-arity        
  ----                -----   -----       -----               

=========================================================

===============================
Input Problem:
===============================
Gamma ={
  (letrec {E1} in (letrec {E2} in (letrec {E3} in S1)))
  =?=
  (letrec {E4} in (letrec {E5} in S2))}
Delta1=  {}
Delta2=  {E1,E2,E3,E4,E5}
Delta3=  {[{E1},(letrec {E2} in [.])],[{E1},(letrec {E3} in [.])],[{E2},(letrec {E3} in [.])],[{E4},(letrec {E5} in [.])]}

===============================
Solution 1:
------------------
Instantiated Expressions:
  (letrec {E1} in (letrec {E2} in (letrec {E3} in S1)))
  =?=
  (letrec {E1} in (letrec {E2} in (letrec {E3} in S1)))
Sol = {
  S2 |-> (letrec {E3} in S1),
  E5 |-> {E2},
  E4 |-> {E1}}
Delta1  = 
  {}
Delta2 = 
  {E1,E2,E3,E4,E5}
Delta3 = 
  {[{E1},(letrec {E2} in [.])],[{E1},(letrec {E3} in [.])],[{E2},(letrec {E3} in [.])],[{E1},(letrec {E2} in [.])]}