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

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

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

===============================
Input Problem:
===============================
Gamma ={
  (letrec {EE[Y1,(var Yn)]} in S1) =?= (letrec {y1=(var y2);y2=(var y3)} in S2)}
Delta1=  {}
Delta2=  {}
Delta3=  {((var y2),[.])}

===============================
Solution 1:
------------------
Instantiated Expressions:
  (letrec {y1=(var y2);y2=(var y3)} in S2)
  =?=
  (letrec {y1=(var y2);y2=(var y3)} in S2)
Sol = {
  S1 |-> S2,
  EE[.1,.2]|->{y2=[.2];[.1]=(var y2)},
  Y1 |-> y1,
  EE_#3[.1,.2]|->{[.1]=[.2]},
  X_#2 |-> y2,
  A_#4 |-> [.],
  Yn |-> y3,
  A_#1 |-> [.]}
Delta1  = 
  {}
Delta2 = 
  {}
Delta3 = 
  {((var y2),[.])}