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

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

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

===============================
Input Problem:
===============================
Gamma ={
  (letrec {E1;E10;E2;E3;E4;E5;E6;E7;E8;E9} in S1) =?= (letrec {EE[Y,S]} in S2)}
Delta1=  {}
Delta2=  {E1,E2,E3,E4,E5}
Delta3=  {}

===============================
Solution 1:
------------------
Instantiated Expressions:
  (letrec {E_#1;E_#10;E_#2;E_#3;E_#4;E_#5;E_#6;E_#7;E_#8;E_#9} in S2)
  =?=
  (letrec {EE[Y,S]} in S2)
Sol = {
  S1 |-> S2,
  E10 |-> {E_#10},
  E9 |-> {E_#9},
  E8 |-> {E_#8},
  E7 |-> {E_#7},
  E6 |-> {E_#6},
  E5 |-> {E_#5},
  E4 |-> {E_#4},
  E3 |-> {E_#3},
  E2 |-> {E_#2},
  E1 |-> {E_#1}}
Delta1  = 
  {}
Delta2 = 
  {E1,E2,E3,E4,E5,E_#1,E_#2,E_#3,E_#4,E_#5}
Delta3 = 
  {}
Delta4 = {
  {E_#1;E_#10;E_#2;E_#3;E_#4;E_#5;E_#6;E_#7;E_#8;E_#9} =?= {EE[Y,S]} }