diff --git a/src/de/dhbwstuttgart/syntaxtree/Class.java b/src/de/dhbwstuttgart/syntaxtree/Class.java
index a044a288..e5894526 100755
--- a/src/de/dhbwstuttgart/syntaxtree/Class.java
+++ b/src/de/dhbwstuttgart/syntaxtree/Class.java
@@ -47,7 +47,6 @@ import de.dhbwstuttgart.typeinference.exceptions.DebugException;
 import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException;
 import de.dhbwstuttgart.typeinference.exceptions.TypeinferenceException;
 import de.dhbwstuttgart.typeinference.typedeployment.TypeInsertPoint;
-import de.dhbwstuttgart.typeinference.unify.FC_TTO;
 import de.dhbwstuttgart.typeinference.unify.Unify;
 
 import  org.apache.commons.bcel6.generic.*;
@@ -625,7 +624,7 @@ public class Class extends GTVDeclarationContext implements AClassOrInterface, I
      */
     // ino.end
     // ino.method.TRProg.23110.definition 
-    public ConstraintsSet typeReconstruction(FC_TTO supportData, TypeAssumptions globalAssumptions)
+    public ConstraintsSet typeReconstruction(TypeAssumptions globalAssumptions)
     // ino.end
     // ino.method.TRProg.23110.body 
     {
@@ -637,8 +636,7 @@ public class Class extends GTVDeclarationContext implements AClassOrInterface, I
         //////////////////////////////
         inferencelog.info("Rufe TRStart()...", Section.TYPEINFERENCE);
 
-		typinferenzLog.debug("Erstellte FiniteClosure: "+supportData, Section.TYPEINFERENCE);
-        //////////////////////////////
+		//////////////////////////////
         //  Ab hier ...
         //  @author A10023 - Andreas Stadelmeier:
         //////////////////////////////
diff --git a/src/de/dhbwstuttgart/syntaxtree/SourceFile.java b/src/de/dhbwstuttgart/syntaxtree/SourceFile.java
index cea600d1..18e43236 100755
--- a/src/de/dhbwstuttgart/syntaxtree/SourceFile.java
+++ b/src/de/dhbwstuttgart/syntaxtree/SourceFile.java
@@ -9,6 +9,8 @@ import java.util.Enumeration;
 import java.util.HashMap;
 import java.util.Hashtable;
 import java.util.Iterator;
+import java.util.Set;
+import java.util.function.Function;
 
 import de.dhbwstuttgart.typeinference.Menge;
 
@@ -23,6 +25,7 @@ import de.dhbwstuttgart.myexception.JVMCodeException;
 import de.dhbwstuttgart.myexception.SCClassException;
 import de.dhbwstuttgart.myexception.SCException;
 import de.dhbwstuttgart.parser.JavaClassName;
+import de.dhbwstuttgart.syntaxtree.factory.UnifyTypeFactory;
 import de.dhbwstuttgart.syntaxtree.misc.DeclId;
 import de.dhbwstuttgart.syntaxtree.misc.UsedId;
 import de.dhbwstuttgart.syntaxtree.modifier.Modifiers;
@@ -37,6 +40,7 @@ import de.dhbwstuttgart.typeinference.ByteCodeResult;
 import de.dhbwstuttgart.typeinference.ConstraintsSet;
 import de.dhbwstuttgart.typeinference.FunNInterface;
 import de.dhbwstuttgart.typeinference.FunNMethod;
+import de.dhbwstuttgart.typeinference.KomplexeMenge;
 import de.dhbwstuttgart.typeinference.Pair;
 import de.dhbwstuttgart.typeinference.ResultSet;
 import de.dhbwstuttgart.typeinference.TypeinferenceResultSet;
@@ -48,18 +52,14 @@ import de.dhbwstuttgart.typeinference.assumptions.ParameterAssumption;
 import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions;
 import de.dhbwstuttgart.typeinference.exceptions.DebugException;
 import de.dhbwstuttgart.typeinference.exceptions.TypeinferenceException;
-import de.dhbwstuttgart.typeinference.unify.FC_TTO;
-import de.dhbwstuttgart.typeinference.unify.Unifier;
 import de.dhbwstuttgart.typeinference.unify.Unify;
+import de.dhbwstuttgart.typeinference.unify.model.FiniteClosure;
+import de.dhbwstuttgart.typeinference.unify.model.MPair;
 
 
 
-
-// ino.class.SourceFile.21355.declaration 
 public class SourceFile
  extends SyntaxTreeNode
-// ino.end
-// ino.class.SourceFile.21355.body
 {
     // ino.attribute.LOAD_BASIC_ASSUMPTIONS_FROM_JRE.21358.decldescription type=javadoc
     /**
@@ -170,17 +170,13 @@ public class SourceFile
     	this.KlassenVektor = classDefinitions;
 	}
 
-	// ino.attribute.imports.21382.decldescription type=javadoc
     /**
      * HOTI 4.5.06
      * Beinhaltet alle Imports des aktuell geparsten Files
      * in Form einer UsedId 
      */
-    // ino.end
-    // ino.attribute.imports.21382.declaration 
     private ImportDeclarations imports=new ImportDeclarations();
-    // ino.end
-    // ino.attribute.baseTypeTranslationTable.21385.decldescription type=javadoc
+
     /**
      * Table zum Übersetzen der nicht implementierten Base-Types:
      * Überall im Compiler wird statt bspw. int Integer verwendet
@@ -189,24 +185,13 @@ public class SourceFile
      * der JRE gelieferten Base-Typen (int,char, etc) und die Objekt-
      * Typen umwandeln können 
      */
-    // ino.end
-    // ino.attribute.baseTypeTranslationTable.21385.declaration 
     private Hashtable<String,String> baseTypeTranslationTable;
-    // ino.end
     
-
-    
-    
-    // ino.method.addElement.21394.defdescription type=javadoc
     /**
      * Fuegt ein neues Element (Interface oder Klasse) hinzu.
      * @param c
      */
-    // ino.end
-    // ino.method.addElement.21394.definition 
     public void addElement(AClassOrInterface e)
-    // ino.end
-    // ino.method.addElement.21394.body 
     {
         if (e instanceof Class) {
             KlassenVektor.addElement((Class) e);
@@ -214,447 +199,8 @@ public class SourceFile
             InterfaceVektor.addElement((Interface) e);
         }
     }
-    // ino.end
     
     
-    
-    // ino.method.codegen.21397.defdescription type=javadoc
-    /**
-     * Startet die Bytecodegenerierung fuer alle in der Datei
-     * enthaltenen Klassen und Interfaces.
-     * 
-     
-    // ino.end
-    // ino.method.codegen.21397.definition 
-    public Menge<ClassFile> codegen(ResultSet result)
-    throws JVMCodeException
-    // ino.end
-    // ino.method.codegen.21397.body 
-    {
-    	Menge<ClassFile> ret = new Menge<ClassFile>();
-        codegenlog.info("Anzahl der Interfaces: " 
-                + Integer.toString(InterfaceVektor.size()));
-        for(int i = 0; i < InterfaceVektor.size(); i++) {
-            InterfaceVektor.elementAt(i).codegen(result);
-        }
-    
-        codegenlog.info("Anzahl der Klassen: " 
-                + Integer.toString(KlassenVektor.size()));
-        for(int i = 0; i < KlassenVektor.size(); i++) {
-            ret.add(KlassenVektor.elementAt(i).codegen(result));
-        }
-		return ret;
-    }
-    // ino.end
-     */
-    // ino.method.createPairFromClassAndSuperclass.21400.defdescription type=javadoc
-    /**
-     * Erstellt ein Typ-Paar, welches im 1. Durchlauf in die Menge der Finite Closure  
-     * aufgenommen wird Input: Klassenname, Name der Superklasse, ParameterDerKlasse,  
-     * Parameter der Superklasse 
-     * @return
-     */
-    // ino.end
-    // ino.method.createPairFromClassAndSuperclass.21400.definition 
-    private Pair createPairFromClassAndSuperclass(Class baseClass, Type superclass, Menge classParaOrg, Menge superclassParaOrg, TypeAssumptions ass)
-    // ino.end
-    // ino.method.createPairFromClassAndSuperclass.21400.body 
-    {
-        // Paar erstellen
-        if(classParaOrg!=null && classParaOrg.size()==0){
-            classParaOrg=null;
-        }
-        if(superclassParaOrg!=null && superclassParaOrg.size()==0){
-            superclassParaOrg=null;
-        }
-        /*
-        Pair P = new Pair(                  
-                new RefType( className.toString(), classParaOrg,-1),
-                new RefType( superclassName.toString(), superclassParaOrg,-1) 
-                         );
-        */
-        Pair P = new Pair(baseClass.getType().TYPE(ass, baseClass), superclass.TYPE(ass, baseClass));
-        //PL 04-12-29 freshe Variablen ANFANG
-        RefType r1 = (RefType)P.getTA1Copy();
-        RefType r2 = (RefType)P.getTA2Copy();
-        r1 = (RefType) r1.TYPE(ass, baseClass);
-        r2 = (RefType) r2.TYPE(ass, baseClass);
-        // #JB# 05.04.2005
-        // ###########################################################
-        Hashtable<JavaClassName,Type> substHash = new Hashtable<JavaClassName,Type>(); //fuer jedes Paar komplett neue Variablen
-        Unify.varSubst(r1, substHash);
-        Unify.varSubst(r2, substHash);
-        // ###########################################################
-        P = new Pair(r1, r2);
-        //PL 04-12-29 freshe Variablen ENDE
-    
-        //HIER AUSKOMMENTIERT, SOLLTE MAN AM ENDE WIEDER DAZU NEHMEN PL 04-12-28
-        // gleiches Paar aufnehmen
-        //vFC.add( new Pair( P.getTA1Copy(), P.getTA1Copy() ) );
-        
-        return(P);
-        
-    }
-    // ino.end
-    // ino.method.makeFC.21403.defdescription type=javadoc
-    /**
-     * Erstellt die Finite Closure
-     * @return FC_TTO-Object, welches die Finite Closure repräsentiert
-     */
-    public FC_TTO makeFC( TypeAssumptions ass )
-    {
-        
-        // Menge FC bilden
-        
-        Menge<Pair> vFC = new Menge<Pair>(); // Menge FC
-        TypeAssumptions globalAssumptions = this.makeBasicAssumptionsFromJRE(imports, false);
-        globalAssumptions.add(this.getPublicFieldAssumptions());
-        // 1. Menge <= in FC aufnehmen --> Iteration ueber alle Klassen
-        
-        Menge<Type> ignoreTypes = new Menge<>(); //Enthält die Typen, welche nicht in der FC als Supertypen enthalten sein sollen.
-        ignoreTypes.add(new RefType("Long",null,-1).TYPE(globalAssumptions, parent));
-        ignoreTypes.add(new RefType("Float",null,-1).TYPE(globalAssumptions, parent));
-        ignoreTypes.add(new RefType("Double",null,-1).TYPE(globalAssumptions, parent));
-        ignoreTypes.add(new RefType("String",null,-1).TYPE(globalAssumptions, parent));
-        ignoreTypes.add(new RefType("Integer",null,-1).TYPE(globalAssumptions, parent));
-        ignoreTypes.add(new RefType("Object",null,-1).TYPE(globalAssumptions, parent));
-        
-        Menge<Class> basicAssumptionsClassMenge = new Menge<>(); //die Klassen aus den BasicAssumptions und den Importierten Klassen
-        for(ClassAssumption cAss : ass.getClassAssumptions()){
-        	Type t1 = cAss.getAssumedClass().getType();
-        	Type t2 = cAss.getAssumedClass().getSuperClass();
-        	if(t2 != null){
-        	Pair p = new Pair(t1, t2);
-        	//System.out.println("FCPair: "+p);
-        	if(! t1.equals(t2)){//Um FC_TTO darf kein T <. T stehen.
-        		Type superTypeFromAssumptions = ass.getTypeFor(t2, t2); //In den Assumptions den SuperTyp nachschlagen
-        		if(superTypeFromAssumptions != null && ! ignoreTypes.contains(superTypeFromAssumptions)){//Die Superklasse eines Typs nur anfügen, wenn er auch in den Assumptions vorkommt.
-        			vFC.add(p);
-        		}
-        		basicAssumptionsClassMenge.add(cAss.getAssumedClass());//Klasse ohne die Superklasse anfügen
-        	}else{
-        		//System.out.println("Wurde nicht aufgenommen");
-        	}
-        	}
-        }
-        
-        for( int i = 0; i < KlassenVektor.size(); i++ )
-        {
-            Class tempKlasse = KlassenVektor.elementAt(i);
-            inferencelog.debug("Verarbeite "+tempKlasse.getName(), Section.TYPEINFERENCE);
-            //TODO: SuperKlasse erstellen, dies sollte am besten beim Konstruktoraufruf von Class geschehen. Diese kann dann mit getSuperClass abgefragt werden.
-            if( tempKlasse.superclassid != null ) {  // Klasse hat Superklasse
-                Pair P=createPairFromClassAndSuperclass(tempKlasse,tempKlasse.getSuperClass(),tempKlasse.get_ParaList(),tempKlasse.superclassid.get_ParaList(), globalAssumptions);
-                vFC.add( P );
-            }
-            if(tempKlasse.getSuperInterfaces()!=null){
-                Iterator<Type> interfaceIterator=tempKlasse.getSuperInterfaces().iterator();
-                while(interfaceIterator.hasNext()){
-                    RefType intf=(RefType) interfaceIterator.next();
-                    Pair P=createPairFromClassAndSuperclass(tempKlasse,intf,tempKlasse.get_ParaList(),intf.get_ParaList(),globalAssumptions);
-                    vFC.add( P );
-                    
-                }
-            }
-        } // Schleifenende durch Klassenvektor
-        for(int i=0; i<InterfaceVektor.size();i++){
-            Interface intf= InterfaceVektor.get(i);
-            if(intf.getSuperInterfaces()!=null){
-                Iterator<Type> interfaceIterator=intf.getSuperInterfaces().iterator();
-                while(interfaceIterator.hasNext()){
-                    RefType superintf=(RefType) interfaceIterator.next();
-                    Pair P=createPairFromClassAndSuperclass(intf,superintf,intf.getParaList(), superintf.get_ParaList(),globalAssumptions);
-                    vFC.add( P );
-                    
-                }
-            }
-        }
-        Menge tto = (Menge)vFC.clone(); 
-    
-        Unify.printMenge( "FC", vFC, 6 );
-        /* z.B.
-        *******************************
-        Menge FC = {
-        (Vektor< A >, Vektor< A >),
-        (Vektor< A >, AbstractList< A >),
-        (Matrix< A >, Matrix< A >),
-        (Matrix< A >, Vektor< Vektor< A > >),
-        (ExMatrix< A >, ExMatrix< A >),
-        (ExMatrix< A >, Matrix< A >) }
-        *******************************
-    
-                ODER 
-    
-        *******************************
-        Menge FC = {
-        (BB< A >, BB< A >),
-        (BB< A >, CC< A >),
-        (AA< A, B >, AA< A, B >),
-        (AA< A, B >, BB< DD< B, A > >) }
-        *******************************
-    
-        */        
-    
-        // 2. Regel 2 der Huellendefinition "eingeschraenkt" anwenden
-        // d.h. sinnvolle Substitutionen suchen (nicht alle)
-        
-        boolean bPaarHinzu = true;
-        while( bPaarHinzu )
-        {
-            bPaarHinzu = false; //PL 04-12-29 nur wenn hinzugefuegt auf true setzen
-            // konkret: rechte Seite von FC nach Typkonstruktoren in der Parameterliste durchsuchen
-            for( int n = 0; n < vFC.size(); n++ )
-            {
-                // Elemente in FC k�nnen nur Pair's sein --> Cast ohne Abfrage
-                Pair PTypKonst = vFC.elementAt(n);
-                
-                // Parameter des rechten Typausdrucks des betrachteten Paars extrahieren
-                Menge<Type> vPara = ((RefType)(PTypKonst.TA2)).get_ParaList();
-                Integer Subst = null; // Substitution
-                int nSubstStelle = 0;
-                inferencelog.debug("nSubstStelleStart" + nSubstStelle + " " + n, Section.FINITECLOSURE);
-                
-                // Parameter durchlaufen und nach Typkonstruktor suchen
-                // #JB# 17.05.2005
-                // ###########################################################
-                if(vPara!=null){
-                // ###########################################################
-                    for( ; nSubstStelle < vPara.size(); nSubstStelle++ )
-                    {
-                        inferencelog.debug("nSubstStelle" + nSubstStelle, Section.FINITECLOSURE);
-                        if( vPara.elementAt(nSubstStelle) instanceof RefType && ((RefType)vPara.elementAt(nSubstStelle)).get_ParaList() != null )
-                        {
-                            // Typkonstruktor gefunden -> wird nun als Substitution verwendet
-                            Subst = 1;//new RefType( (RefType)vPara.elementAt(nSubstStelle) ,-1);
-                            inferencelog.debug( "Ausgangstyp:" + ((RefType)PTypKonst.TA2).getName() , Section.FINITECLOSURE);
-                            inferencelog.debug( "RefType = " + ((RefType)vPara.elementAt(nSubstStelle)).getName() , Section.FINITECLOSURE);
-                        break; // Einschraenkung - nur fuer ein RefType wird eine Substitution gesucht
-                        }
-                    }
-                // ###########################################################
-                }
-                // ###########################################################
-                if( Subst != null )
-                {
-                    // Rechter Typ hat einen Typkonstruktor --> sinvolles neues Paar bilden
-                    // d.h. Rechter Typ auf linker Paarseite suchen
-                    // System.out.println("Subststelle = " + nSubstStelle );
-    
-                    for( int t = 0; t < vFC.size(); t++ )
-                    {
-                        Pair PSuchen = vFC.elementAt(t);
-                        if( ((RefType)(PTypKonst.TA2)).getTypeName().equals( ((RefType)PSuchen.TA1).getTypeName() ) )
-                        {
-                            inferencelog.debug(" gefundener Typ links: " + ((RefType)(PSuchen.TA1)).getName(), Section.FINITECLOSURE ); 
-                            inferencelog.debug(" gefundener Typ rechts: " + ((RefType)(PSuchen.TA2)).getName() , Section.FINITECLOSURE); 
-                            // Paar gefunden, das als linken Typ den gleichen Typen enth�lt, der als Parameter einen Typkonstruktor hat
-                            // Substitution
-                            //Pair P = new Pair( PSuchen.getTA1Copy( ), PSuchen.getTA2Copy( ) );
-                //linker Typterm bleibt gleich
-                //rechter Typterm wird aussen auf den Supertyp gesetzt.
-                //restliches FC erfolgt ueber die Transitivitaet
-                //siehe im unteren Teil
-                            Pair P = new Pair( PTypKonst.getTA1Copy( ), PSuchen.getTA2Copy( ) );
-                            // System.out.println(" Subst " + Subst.getName() );
-                            // System.out.println(" Vor: P = " + P.toString() + P.TA1 );
-                            // System.out.println(" Vor: PSuchen = " + PSuchen.toString() + PSuchen.TA1 );
-                            
-                            // Parameter, der substituiert wird, sollte TV sein ???
-                            //TypePlaceholder TV = null;
-                            // if( ((RefType)P.TA1).isTV( nSubstStelle ) )
-    //                                 try
-    //                                 {
-    //                                     TV = new TypePlaceholder( ((RefType)P.TA1).getParaN( nSubstStelle ) );
-    //                                 }
-    //                                 catch( Exception E )
-    //                                 {
-    //                                     continue;
-    //                                 }
-    //                             else
-    //                                 continue;
-    
-                //es werden alle Parameter in einem Typeterm, der
-                //der Argumente hat ersetzt PL 04-12-28
-                Hashtable<JavaClassName,Type> hts = new Hashtable<JavaClassName,Type>();
-                //for(int u = nSubstStelle; u < vPara.size(); u++) {
-                for(int u = 0; u < vPara.size(); u++) {
-                try {
-                    // #JB# 05.04.2005
-                    // ###########################################################
-                    //TV = new TypePlaceholder( ((RefType)PSuchen.TA1).getParaN(u) );
-                    //System.out.println("TV_Name: " + u + TV.Type2String());
-                    // ###########################################################
-                    inferencelog.debug("Typterm_Name: " + vPara.elementAt(u), Section.FINITECLOSURE);
-                    inferencelog.debug("Typterm_Name: " + ((Type)vPara.elementAt(u)).Type2String(), Section.FINITECLOSURE);
-                    hts.put(new JavaClassName(((RefType)PSuchen.TA1).getParaN(u)), vPara.elementAt(u));
-                 }
-                 catch( Exception E ) {
-                     inferencelog.error(E.getMessage(), Section.FINITECLOSURE);
-                     //FIXME Throw Exception or Error instead of exiting!
-                     System.exit(0);
-                 }
-                    
-            //  Subst( P, 
-    //                     2, 
-    //                     TV,
-    //                     new RefType( (RefType)vPara.elementAt(u) ), 
-    //                     false ); // rechte Seite substituieren
-                //Es genuegt die rechte Seite zu substituieren, da
-                //die linke Seite ein Typterm ausschlie�lich mit 
-                //Typvariablen ist
-                }
-                //Unify.SubstHashtableGeneric(((RefType)P.TA1), hts); //funktioniert nicht
-                Unify.SubstHashtableGeneric(((RefType)P.TA2), hts); //funktioniert nicht
-                            // System.out.println(" TV!!!= " + TV.getName() );
-                            //Subst( P, 1, TV, Subst, false ); // linke Seite substituieren
-                            //Subst( P, 2, TV, Subst, false ); // rechte Seite substituieren
-                            // System.out.println(" nach Subst: P = " + P.toString() );
-                            // System.out.println(" Nach: PSuchen = " + PSuchen.toString() );
-                            // System.out.println(" Nach: " + P.toString() );
-    
-                            // Paar einfuegen, falls noch nicht vorhanden
-                            // System.out.println("Paar alt:" + PSuchen.toString() );
-                            // System.out.println("Paar neu:" + P.toString() );
-                            if( !P.isInMenge( vFC ) )
-                            {
-                                vFC.add( P );
-                 Unify.printMenge( "FC", vFC, 6 );
-                                bPaarHinzu = true;
-                            }
-                //PL 04-12-29
-                            // else   //unnoetig, da am Anfang bereits false gesetzt
-    //                             {
-    //                                 bPaarHinzu = false;
-    //                             }
-                            
-                        }
-                    }                
-                } // end if: Substitution gefunden???
-            } // end for: Typkonstruktor suchen
-            
-    
-            // Transitivitaet berechnen      
-            for( int u = 0; u < vFC.size(); u++ )
-            {
-                Pair PTemp = vFC.elementAt(u);
-                
-                // falls rechtes Paar = RefType
-                if( PTemp.TA2 instanceof RefType )
-                {
-                    RefType R = (RefType)PTemp.TA2;
-                    
-                    // rechte Seite auf linker Seite suchen
-                    for( int e = 0; e < vFC.size(); e++ )
-                    {
-                        Pair PSuch = vFC.elementAt(e);
-                        // als linke Paarseite theortisch nur RefType's moeglich --> Cast
-                        RefType RSuch = (RefType)PSuch.TA1;
-                        
-                        //if( R.getName().equals(RSuch.getName()) ) 
-            if (R.is_Equiv(RSuch, new Hashtable<JavaClassName,Type>()))   //eingefuegt PL 05-01-07
-                {
-                // Paar einfuegen, falls noch nicht vorhanden
-                RefType L1 = (RefType)PTemp.getTA1Copy();
-                RefType L2 = (RefType)PTemp.getTA2Copy();
-                RefType R1 = (RefType)PSuch.getTA1Copy();
-                RefType R2 = (RefType)PSuch.getTA2Copy();
-    
-                //zunaechst Variablen disjunkt machen ANFANG
-                // #JB# 05.04.2005
-                // ###########################################################
-                Hashtable<JavaClassName,Type> substHash1 = new Hashtable<JavaClassName,Type>();
-                Unify.varSubst(L1, substHash1);
-                Unify.varSubst(L2, substHash1);
-                Hashtable<JavaClassName,Type> substHash2 = new Hashtable<JavaClassName,Type>();
-                Unify.varSubst(R1, substHash2);
-                Unify.varSubst(R2, substHash2);
-                // ###########################################################
-                //zunaechst Variablen disjunkt machen ENDE
-    
-                //Variablen so umbennen, dass transitiver Abschluss richtige
-                //Namen hat ANFANG
-                
-                // #JB# 05.04.2005
-                // ###########################################################
-                Hashtable<JavaClassName,Type> h = new Hashtable<JavaClassName,Type>();
-                L2.Equiv2Equal(R1, h);
-                Hashtable<JavaClassName,Type> substHash3 = h;
-                Unify.varSubst(L1, substHash3);
-                Unify.varSubst(R2, substHash3);
-                // ###########################################################
-                //Variablen so umbennen, dass transitiver Abschluss richitge
-                //Namen hat ENDE
-    
-                //Pair P = new Pair( (RefType)PTemp.TA1, (RefType)PSuch.TA2 );
-                Pair P = new Pair(L1, R2);
-                if( !P.isInMenge( vFC ) )
-                    {
-                    vFC.add( P );
-                    bPaarHinzu = true;
-                    }
-                else
-                    {
-                    bPaarHinzu = false;
-                    }
-                }
-                    } // end for: linke Seite suchen
-                } // end if: Element ist RefType
-            } // end for: Transitivit�ten berechnen
-        //PL HIER REFLEXIVE HUELLE EINFUEGEN
-        // 05-01-07
-            
-        } // Ende WHILE
-    
-        /* z.B.
-        *******************************
-        Menge nach trans: FC = {
-        (Vektor< A >, Vektor< A >),
-        (Vektor< A >, AbstractList< A >),
-        (Matrix< A >, Matrix< A >),
-        (Matrix< A >, Vektor< Vektor< A > >),
-        (ExMatrix< A >, ExMatrix< A >),
-        (ExMatrix< A >, Matrix< A >),
-        (Vektor< Vektor< A > >, Vektor< Vektor< A > >),
-        (Vektor< Vektor< A > >, AbstractList< Vektor< A > >),
-        (Matrix< A >, AbstractList< Vektor< A > >),
-        (ExMatrix< A >, Vektor< Vektor< A > >),
-        (ExMatrix< A >, AbstractList< Vektor< A > >) }
-        
-            ODER
-            
-        *******************************
-        Menge nach trans: FC = {
-        (BB< A >, BB< A >),
-        (BB< A >, CC< A >),
-        (AA< A, B >, AA< A, B >),
-        (AA< A, B >, BB< DD< B, A > >),
-        (BB< DD< B, A > >, BB< DD< B, A > >),
-        (BB< DD< B, A > >, CC< DD< B, A > >),
-        (AA< A, B >, CC< DD< B, A > >) }
-        *******************************
-    
-        *******************************        */
-        
-        
-        // printMenge( "nach trans: FC", vFC, 6 );
-        
-        Menge<Class> KlassenVektorunImportierteKlassen = new Menge<>();
-        KlassenVektorunImportierteKlassen.addAll(basicAssumptionsClassMenge);
-        KlassenVektorunImportierteKlassen.addAll(KlassenVektor);
-        
-    FC_TTO fctto = new FC_TTO(vFC, tto, KlassenVektorunImportierteKlassen);
-    return fctto;
-    }
-    
-    public TypeAssumptions getPublicFieldAssumptions(){
-    	TypeAssumptions publicAssumptions = new TypeAssumptions(null);
-    	//Alle PublicAssumptions der in dieser SourceFile enthaltenen Klassen sammeln:
-    	for(Class klasse : KlassenVektor){
-    		publicAssumptions.add(klasse.getPublicFieldAssumptions());
-        }
-    	return publicAssumptions;
-    }
-    
     /////////////////////////////////////////////////////////////////////////
     // TypeReconstructionAlgorithmus
     /////////////////////////////////////////////////////////////////////////
@@ -691,24 +237,32 @@ public class SourceFile
     	typinferenzLog.debug("Von JRE erstellte Assumptions: "+importAssumptions, Section.TYPEINFERENCE);
     	
     	//FiniteClosure generieren:
-    	FC_TTO finiteClosure = this.makeFC(globalAssumptions);
+    	FiniteClosure finiteClosure = UnifyTypeFactory.generateFC(globalAssumptions);
     	
     	typinferenzLog.debug("FiniteClosure: \n"+finiteClosure, Section.TYPEINFERENCE);
     	
     	ConstraintsSet oderConstraints = new ConstraintsSet();
     	//Alle Constraints der in dieser SourceFile enthaltenen Klassen sammeln:
         for(Class klasse : KlassenVektor){
-        	oderConstraints.add(klasse.typeReconstruction(finiteClosure, globalAssumptions));
+        	oderConstraints.add(klasse.typeReconstruction(globalAssumptions));
         }
         
+        /*////////////////
+         * Paare in MPairs umwandeln
+         * (Wird zunächst mal weggelassen. Constraints werden erst beim Unifizieren umgewandelt
+         */////////////////
+        //UnifyTypeFactory.convert(oderConstraints);
+        
+        
         ////////////////
         //Karthesisches Produkt bilden:
         ////////////////
         
         //Unmögliche ConstraintsSets aussortieren durch Unifizierung
-        Unifier unifier = (pairs)->{
+        Function<Menge<Pair>,Menge<Menge<Pair>>> unifier = (pairs)->{
         	Menge<Menge<Pair>> retValue = new Menge<>();
-        	retValue = Unify.unify(pairs, finiteClosure);
+        	Set<MPair> convertPairs = UnifyTypeFactory.convert(pairs);
+        	Set<Set<MPair>> unifiedPairs = new Unify().unify(convertPairs, finiteClosure);
         	return retValue;};
         //oderConstraints.filterWrongConstraints(unifier);
         	
@@ -716,17 +270,17 @@ public class SourceFile
         
         typinferenzLog.debug("Übriggebliebene Konstraints:\n"+oderConstraints+"\n", Section.TYPEINFERENCE);
         //Die Constraints in Pair's umwandeln (Karthesisches Produkt bilden):
-        Menge<Menge<Pair>> xConstraints = oderConstraints.cartesianProduct();
+        Set<Set<Pair>> xConstraints = oderConstraints.cartesianProduct();
    
         typinferenzLog.debug("Karthesisches Produkt der Constraints: "+xConstraints, Section.TYPEINFERENCE);
         
-        finiteClosure.generateFullyNamedTypes(globalAssumptions);
+        //finiteClosure.generateFullyNamedTypes(globalAssumptions);
         
         //////////////////////////////
         // Unifizierung der Constraints:
         //////////////////////////////
     	boolean unifyFail = true;
-        for(Menge<Pair> constraints : xConstraints){
+        for(Set<Pair> constraints : xConstraints){
         	//Alle durch das Karthesische Produkt entstandenen Möglichkeiten durchgehen:
             Menge<Menge<Pair>> result = new Menge<Menge<Pair>>();
             
@@ -741,7 +295,7 @@ public class SourceFile
             }
             
             //Erst die Unifizierung erstellen:
-            Menge<Pair> constraintsClone = (Menge<Pair>)constraints.clone();
+            Menge<MPair> constraintsClone = (Menge<MPair>)constraints.clone();
             
           //IDEE: Man bildet Zusammenhangskomponenten von Paaren, die gemeinsame Variablen haben
           //      und unifizert nur die Zusammenhangskomponenten in Schritten 1 - 5
@@ -762,17 +316,17 @@ public class SourceFile
         	
         	//Schritt 3: Umwandlung der Indizes in die zugehoerigen Elemente
         	//           In streamconstraintsclone sind die Mengen von Paar enthalten die unifiziert werden muessen
-        	Stream<Menge<Pair>> streamconstraintsclone = indexeset.stream().map(x -> x.stream()
+        	Stream<Menge<MPair>> streamconstraintsclone = indexeset.stream().map(x -> x.stream()
         			                                                           .map(i -> constraintsClone.elementAt(i))
-        			                                                               .<Menge<Pair>>collect(Menge::new, Menge::add, Menge::addAll));
+        			                                                               .<Menge<MPair>>collect(Menge::new, Menge::add, Menge::addAll));
        	//Menge<Menge<Pair>> vecconstraintsclone = streamconstraintsclone.collect(Menge::new, Menge::add, Menge::addAll);
             //System.out.println();
         	//Schritt 4: Unifikation  
-        	Menge<Menge<Menge<Pair>>> vecunifyResult =
+        	Set<Set<Set<MPair>>> vecunifyResult =
         			//streamconstraintsclone.map(x -> Unify.unify(x, finiteClosure)).collect(Menge::new, Menge::add, Menge::addAll);
         			//DEBUG-Variante
         			streamconstraintsclone.map(x -> 
-        			  	{ 	Menge<Menge<Pair>> z = Unify.unify(x, finiteClosure);
+        			  	{ 	Set<Set<MPair>> z = new Unify().unify(x, finiteClosure);
         					return z;
         			  	}
         					).collect(Menge::new, Menge::add, Menge::addAll);
@@ -785,19 +339,19 @@ public class SourceFile
             //Schritt 5: Bildung des cartesischen Produkts
             //sollte wieder entfernt werden: Weiterarbeit mit: 
         	//[[x_1 -> t_1, x_2 -> t2], [x_1 -> t'_1, x_2 -> t'_2]] x ... x [[x_n -> t_1n], [x_n -> t2n], [x_n -> t3n]] 
-        	Menge<Menge<Pair>> cardprodret_start = new Menge<>();
+        	Set<Set<Pair>> cardprodret_start = new Menge<>();
         	cardprodret_start.add(new Menge<Pair>());
         	
         	//cart. Produkt mit Linkverschiebung
-        	Menge<Menge<Pair>> unifyResult = vecunifyResult.stream().reduce(cardprodret_start, (x, y) -> {
-        		Menge<Menge<Pair>> cardprodret= new Menge<>();
+        	Set<Set<Pair>> unifyResult = vecunifyResult.stream().reduce(cardprodret_start, (x, y) -> {
+        		Set<Set<Pair>> cardprodret= new Menge<>();
         		if (y.size() > 0) {
         			//System.out.println(y);
         			//Menge<Menge<Pair>> cardprodretold = x;
 					//cardprodret = new Menge<>();
 					for(int j = 0; j < x.size(); j++) {
 						for (int k = 0; k < y.size(); k++){
-							Menge<Pair> help = new Menge<>(); 
+							Set<Pair> help = new Menge<>(); 
 							help.addAll(y.elementAt(k));
 							help.addAll(x.elementAt(j));
 							cardprodret.add(help);
diff --git a/src/de/dhbwstuttgart/syntaxtree/factory/UnifyTypeFactory.java b/src/de/dhbwstuttgart/syntaxtree/factory/UnifyTypeFactory.java
index 6d2503f8..5e9d1876 100644
--- a/src/de/dhbwstuttgart/syntaxtree/factory/UnifyTypeFactory.java
+++ b/src/de/dhbwstuttgart/syntaxtree/factory/UnifyTypeFactory.java
@@ -11,7 +11,11 @@ import de.dhbwstuttgart.syntaxtree.type.SuperWildcardType;
 import de.dhbwstuttgart.syntaxtree.type.Type;
 import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
 import de.dhbwstuttgart.syntaxtree.type.WildcardType;
+import de.dhbwstuttgart.typeinference.KomplexeMenge;
 import de.dhbwstuttgart.typeinference.Menge;
+import de.dhbwstuttgart.typeinference.OderMenge;
+import de.dhbwstuttgart.typeinference.Pair;
+import de.dhbwstuttgart.typeinference.UndMenge;
 import de.dhbwstuttgart.typeinference.assumptions.ClassAssumption;
 import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions;
 import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
@@ -24,7 +28,7 @@ import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
 import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
 
 public class UnifyTypeFactory {
-
+	
 	public static FiniteClosure generateFC(TypeAssumptions fromAss){
 		HashSet<MPair> pairs = new HashSet<>();
 		for(ClassAssumption cAss : fromAss.getClassAssumptions()){
@@ -44,7 +48,7 @@ public class UnifyTypeFactory {
 	
 	public static UnifyType convert(Type t){
 		//Es wurde versucht ein Typ umzuwandeln, welcher noch nicht von der Factory abgedeckt ist
-		if(t instanceof GenericTypeVar){
+		if(t instanceof GenericTypeVar){ //WTF ?
 			return UnifyTypeFactory.convert((GenericTypeVar)t);
 		}
 		System.out.println("Der Typ "+t+" kann nicht umgewandelt werden");
@@ -80,4 +84,12 @@ public class UnifyTypeFactory {
 	public static UnifyType convert(GenericTypeVar t){
 		return new SimpleType(t.get_Name());
 	}
+
+	public static UndMenge<MPair> convert(UndMenge<Pair> constraints) {
+		return null;
+	}
+	
+	public static OderMenge<MPair> convert(OderMenge<Pair> constraints) {
+		return null;
+	}
 }
diff --git a/src/de/dhbwstuttgart/syntaxtree/factory/Unify_FC_TTO_Builder.java b/src/de/dhbwstuttgart/syntaxtree/factory/Unify_FC_TTO_Builder.java
index 524e729e..d28992cf 100644
--- a/src/de/dhbwstuttgart/syntaxtree/factory/Unify_FC_TTO_Builder.java
+++ b/src/de/dhbwstuttgart/syntaxtree/factory/Unify_FC_TTO_Builder.java
@@ -22,10 +22,6 @@ public class Unify_FC_TTO_Builder {
 		fc.add(new Pair(t1, t2));
 	}
 	
-	public FC_TTO Get_FC_TTO() {
-		return new FC_TTO(fc, (Menge<?>) fc.clone(), classes);
-	}
-	
 	public void clear() {
 		fc = new Menge<Pair>();
 		classes = new Menge<Class>();
diff --git a/src/de/dhbwstuttgart/syntaxtree/type/RefType.java b/src/de/dhbwstuttgart/syntaxtree/type/RefType.java
index ba03d583..00e808a9 100755
--- a/src/de/dhbwstuttgart/syntaxtree/type/RefType.java
+++ b/src/de/dhbwstuttgart/syntaxtree/type/RefType.java
@@ -29,8 +29,6 @@ import de.dhbwstuttgart.typeinference.TypeinferenceResultSet;
 import de.dhbwstuttgart.typeinference.TypeinferenceResults;
 import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions;
 import de.dhbwstuttgart.typeinference.exceptions.TypeinferenceException;
-import de.dhbwstuttgart.typeinference.unify.CSubstitutionGenVar;
-import de.dhbwstuttgart.typeinference.unify.CSubstitutionSet;
 
 
 
@@ -182,41 +180,6 @@ public class RefType extends ObjectType implements IMatchable
             return name + "<"+para + " >" ;
         }
     }
-    // ino.end
-    
-    /**
-     * Wandelt die Parameter des RefTypes in TPHs um, sofern es sich um Generische Variablen handelt.
-     * @return
-     */
-    // ino.method.GenericTypeVar2TypePlaceholder.26652.definition 
-    public CSubstitutionSet GenericTypeVar2TypePlaceholder ()
-    // ino.end
-    // ino.method.GenericTypeVar2TypePlaceholder.26652.body 
-    {
-    	//throw new NotImplementedException();
-    	///*
-        CSubstitutionSet sub = new CSubstitutionSet();
-        if(parameter != null)
-        {
-        	for (int i = 0; i < parameter.size(); i++)
-        	{
-        		if (parameter.elementAt(i) instanceof GenericTypeVar) 
-        		{
-        			TypePlaceholder tlv = TypePlaceholder.fresh(null);
-        			sub.addElement(new CSubstitutionGenVar((GenericTypeVar)parameter.elementAt(i), tlv));
-        			parameter.set(i, tlv);        
-        		}
-        		if (parameter.elementAt(i) instanceof RefType)
-        		{
-        			CSubstitutionSet parasub = ((RefType)parameter.elementAt(i)).GenericTypeVar2TypePlaceholder();
-        			sub.addAll(parasub);  //korrigiert PL 07=07=29
-        		}
-        	}
-        }
-        return sub;
-    //*/
-    }
-    // ino.end
     
     /**
      * Wandelt die Parameter des RefTypes in TPHs um, sofern es sich um Generische Variablen handelt.
diff --git a/src/de/dhbwstuttgart/typeinference/ConstraintsSet.java b/src/de/dhbwstuttgart/typeinference/ConstraintsSet.java
index 5c8524a8..84475cbf 100755
--- a/src/de/dhbwstuttgart/typeinference/ConstraintsSet.java
+++ b/src/de/dhbwstuttgart/typeinference/ConstraintsSet.java
@@ -1,6 +1,7 @@
 package de.dhbwstuttgart.typeinference;
 
 import java.util.Iterator;
+import java.util.Set;
 import java.util.Vector;
 import de.dhbwstuttgart.logger.Logger;
 import de.dhbwstuttgart.logger.*;
@@ -57,12 +58,12 @@ public class ConstraintsSet extends UndMenge<Pair> implements Iterable<OderConst
 		}
 		this.filterWrongConstraints(
 				(pairs)->{
-					Menge<Pair> undConstraintsUndPairs = new Menge<>();
+					Set<Pair> undConstraintsUndPairs = new Menge<>();
 					undConstraintsUndPairs.addAll(pairs);
 					undConstraintsUndPairs.addAll(alleUndConstraints);
 					log.debug("Versuche Pairs auszusondern:\n"+pairs, Section.TYPEINFERENCE);
 					log.debug("Unifiziere:\n"+undConstraintsUndPairs, Section.TYPEINFERENCE);
-					Menge<Menge<Pair>> unifyResult = unifier.apply(undConstraintsUndPairs);
+					Set<Set<Pair>> unifyResult = unifier.apply(undConstraintsUndPairs);
 					return unifyResult;
 				});
 	}
diff --git a/src/de/dhbwstuttgart/typeinference/KomplexeMenge.java b/src/de/dhbwstuttgart/typeinference/KomplexeMenge.java
index 25ca29e8..f72d991d 100644
--- a/src/de/dhbwstuttgart/typeinference/KomplexeMenge.java
+++ b/src/de/dhbwstuttgart/typeinference/KomplexeMenge.java
@@ -1,6 +1,8 @@
 package de.dhbwstuttgart.typeinference;
 
+import java.util.Set;
+
 public interface KomplexeMenge<A>{
-	Menge<? extends KomplexeMenge<A>> getSet();
-	Menge<Menge<A>> cartesianProduct();
+	Set<? extends KomplexeMenge<A>> getSet();
+	Set<Set<A>> cartesianProduct();
 }
\ No newline at end of file
diff --git a/src/de/dhbwstuttgart/typeinference/OderConstraint.java b/src/de/dhbwstuttgart/typeinference/OderConstraint.java
index 3896b115..7b88223e 100755
--- a/src/de/dhbwstuttgart/typeinference/OderConstraint.java
+++ b/src/de/dhbwstuttgart/typeinference/OderConstraint.java
@@ -1,5 +1,6 @@
 package de.dhbwstuttgart.typeinference;
 
+import java.util.Set;
 import java.util.Vector;
 
 import de.dhbwstuttgart.logger.Logger;
@@ -10,7 +11,7 @@ import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
 import de.dhbwstuttgart.typeinference.unify.Unifier;
 
 public class OderConstraint extends OderMenge<Pair>{
-	private Menge<UndConstraint> oderConstraintPairs;
+	private Set<UndConstraint> oderConstraintPairs;
 	
 	private final static Logger logger = Logger.getLogger(OderConstraint.class.getName());
 	
@@ -70,7 +71,7 @@ public class OderConstraint extends OderMenge<Pair>{
 		return ret+"]";
 	}
 
-	public Vector<UndConstraint> getUndConstraints() {
+	public Set<UndConstraint> getUndConstraints() {
 		return this.oderConstraintPairs;
 		/*
 		Vector<UndConstraint> ret = new Vector<UndConstraint>();
@@ -91,9 +92,9 @@ public class OderConstraint extends OderMenge<Pair>{
 	 * @param unifier - Wird für die Unifizierung benutzt
 	 */
 	void filterWrongConstraints(Unifier unifier) {
-		Menge<UndConstraint> filteredConstraints = new Menge<>();
+		Set<UndConstraint> filteredConstraints = new Menge<>();
 		for(UndConstraint cons : this.getUndConstraints()){
-			Menge<Menge<Pair>> unifierResult = unifier.apply(cons.getConstraintPairs());
+			Set<Set<Pair>> unifierResult = unifier.apply(cons.getConstraintPairs());
 			if(!unifierResult.isEmpty()){
 				filteredConstraints.add(cons);
 			}else{
@@ -111,7 +112,7 @@ public class OderConstraint extends OderMenge<Pair>{
 	}
 
 	@Override
-	public Menge<? extends KomplexeMenge<Pair>> getSet() {
+	public Set<? extends KomplexeMenge<Pair>> getSet() {
 		return this.oderConstraintPairs;
 	}
 	
diff --git a/src/de/dhbwstuttgart/typeinference/OderMenge.java b/src/de/dhbwstuttgart/typeinference/OderMenge.java
index 4781d641..842c78a3 100644
--- a/src/de/dhbwstuttgart/typeinference/OderMenge.java
+++ b/src/de/dhbwstuttgart/typeinference/OderMenge.java
@@ -2,6 +2,7 @@ package de.dhbwstuttgart.typeinference;
 
 import java.util.Collection;
 import java.util.Iterator;
+import java.util.Set;
 
 import de.dhbwstuttgart.typeinference.Menge;
 import de.dhbwstuttgart.logger.Logger;
@@ -13,11 +14,11 @@ import de.dhbwstuttgart.typeinference.unify.Unifier;
 
 public abstract class OderMenge<A> implements KomplexeMenge<A>{
 	
-	public abstract Menge<? extends KomplexeMenge<A>> getSet();
+	public abstract Set<? extends KomplexeMenge<A>> getSet();
 
 	@Override
-	public Menge<Menge<A>> cartesianProduct() {
-		Menge<Menge<A>> ret = new Menge<>();
+	public Set<Set<A>> cartesianProduct() {
+		Set<Set<A>> ret = new Menge<>();
 		for(KomplexeMenge<A> km : this.getSet()){
 			ret.addAll(km.cartesianProduct());
 		}
diff --git a/src/de/dhbwstuttgart/typeinference/UndMenge.java b/src/de/dhbwstuttgart/typeinference/UndMenge.java
index 6771bf18..146121d7 100644
--- a/src/de/dhbwstuttgart/typeinference/UndMenge.java
+++ b/src/de/dhbwstuttgart/typeinference/UndMenge.java
@@ -3,24 +3,25 @@ package de.dhbwstuttgart.typeinference;
 import de.dhbwstuttgart.typeinference.unify.Unify;
 import java.util.Collection;
 import java.util.Iterator;
+import java.util.Set;
 
 //import com.rits.cloning.Cloner;
 
-public abstract class UndMenge<A extends DeepCloneable> implements KomplexeMenge<A>{
+public abstract class UndMenge<A> implements KomplexeMenge<A>{
 
 	public abstract Menge<? extends KomplexeMenge<A>> getSet();
 
 	@Override
-	public Menge<Menge<A>> cartesianProduct() {
-		Menge<Menge<A>> ret = null;
+	public Set<Set<A>> cartesianProduct() {
+		Set<Set<A>> ret = null;
 		//Cloner cloner = new Cloner();
 		for(KomplexeMenge<A> km : this.getSet()){
 			if(ret == null){
 				ret = km.cartesianProduct();
 			}else{
-				Menge<Menge<A>> cartesianProduct = new Menge<>();
-				for(Menge<A> r : ret)for(Menge<A> m : km.cartesianProduct()){ //Für jedes Element aus dem Karthesischen Produkt:
-					Menge<A> undElement = new Menge<A>();
+				Set<Set<A>> cartesianProduct = new Menge<>();
+				for(Set<A> r : ret)for(Set<A> m : km.cartesianProduct()){ //Für jedes Element aus dem Karthesischen Produkt:
+					Set<A> undElement = new Menge<A>();
 					undElement.addAll(Unify.deepClone(r));
 					undElement.addAll(m);
 					cartesianProduct.add(undElement);
@@ -28,7 +29,7 @@ public abstract class UndMenge<A extends DeepCloneable> implements KomplexeMenge
 				ret = cartesianProduct;
 			}
 		}
-		if(ret == null)return new Menge<Menge<A>>();
+		if(ret == null)return new Menge<>();
 		return ret;
 	}
 	
diff --git a/src/de/dhbwstuttgart/typeinference/unify/CSet.java b/src/de/dhbwstuttgart/typeinference/unify/CSet.java
deleted file mode 100755
index 08af741d..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/CSet.java
+++ /dev/null
@@ -1,72 +0,0 @@
-// ino.module.CSet.8698.package 
-package de.dhbwstuttgart.typeinference.unify;
-// ino.end
-
-// ino.module.CSet.8698.import 
-import java.util.Iterator;
-// ino.end
-
-// ino.class.CSet.27435.description type=javadoc
-/**
- * 
- * @author Jrg Buerle
- * @version $date
- */
-// ino.end
-// ino.class.CSet.27435.declaration 
-public abstract class CSet<E> implements Iterable<E>
-// ino.end
-// ino.class.CSet.27435.body
-{
-    // ino.method.addElement.27438.declaration 
-    public abstract void addElement(E element);
-    // ino.end
-    // ino.method.removeElement.27441.declaration 
-    public abstract void removeElement(E element);
-    // ino.end
-    // ino.method.unite.27444.declaration 
-    public abstract void unite(CSet<E> anotherSet);
-    // ino.end
-    // ino.method.subtract.27447.declaration 
-    public abstract void subtract(CSet<E> anotherSet);
-    // ino.end
-    // ino.method.shallowCopy.27450.declaration 
-    public abstract CSet<E> shallowCopy();
-    // ino.end
-    // ino.method.deepCopy.27453.declaration 
-    public abstract CSet<E> deepCopy();
-    // ino.end
-    // ino.method.contains.27456.declaration 
-    public abstract boolean contains(E element);
-    // ino.end
-    // ino.method.getCardinality.27459.declaration 
-    public abstract int getCardinality();
-    // ino.end
-    // ino.method.getIterator.27462.declaration 
-    public abstract Iterator<E> getIterator();
-    // ino.end
-    // ino.method.equals.27465.declaration 
-    public abstract boolean equals(Object obj);
-    // ino.end
-    
-    // ino.method.toString.27468.definition 
-    public String toString()
-    // ino.end
-    // ino.method.toString.27468.body 
-    {
-        StringBuffer sb = new StringBuffer();
-        sb.append("Set {\n");
-        Iterator<E> it = this.getIterator();
-        while(it.hasNext()){
-            sb.append(it.next().toString());
-            sb.append(",\n");
-        }
-        if(this.getCardinality()>0){
-            sb.delete(sb.length()-2, sb.length()-1);
-        }
-        sb.append("}");
-        return sb.toString();
-    }
-    // ino.end
-}
-// ino.end
diff --git a/src/de/dhbwstuttgart/typeinference/unify/CSubstitution.java b/src/de/dhbwstuttgart/typeinference/unify/CSubstitution.java
deleted file mode 100755
index fc9d6705..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/CSubstitution.java
+++ /dev/null
@@ -1,253 +0,0 @@
-// ino.module.CSubstitution.8685.package 
-package de.dhbwstuttgart.typeinference.unify;
-// ino.end
-
-// ino.module.CSubstitution.8685.import 
-import java.util.Iterator;
-import de.dhbwstuttgart.typeinference.Menge;
-
-import de.dhbwstuttgart.logger.Logger;
-// ino.end
-
-
-
-
-
-
-
-
-
-import de.dhbwstuttgart.myexception.CTypeReconstructionException;
-import de.dhbwstuttgart.syntaxtree.type.GenericTypeVar;
-import de.dhbwstuttgart.syntaxtree.type.RefType;
-import de.dhbwstuttgart.syntaxtree.type.Type;
-import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
-import de.dhbwstuttgart.typeinference.Pair;
-
-// ino.class.CSubstitution.27003.description type=javadoc
-/**
- * Implementierung einer Typsubstitution. Bildet eine zu ersetzende                
- * <code>TypePlaceholder</code> auf einen Substitutions-Typ ab. Instanzen dieser   
- * Klasse werden in der Regel aus
- * <code>Pair</code>-Objekten erzeugt.
- * @author J�rg B�uerle
- * @version $Date: 2006/07/10 11:27:04 $
- */
-// ino.end
-// ino.class.CSubstitution.27003.declaration 
-public class CSubstitution
-// ino.end
-// ino.class.CSubstitution.27003.body
-{
-    // ino.attribute.m_TypeVar.27006.declaration 
-    private TypePlaceholder m_TypeVar = null;
-    // ino.end
-    // ino.attribute.m_Type.27009.declaration 
-    protected Type m_Type = null;
-    // ino.end
-    // ino.attribute.inferencelog.27012.declaration 
-    protected static Logger inferencelog = Logger.getLogger("inference");
-    // ino.end
-    // ino.method.CSubstitution.27015.definition 
-    public CSubstitution()
-    // ino.end
-    // ino.method.CSubstitution.27015.body 
-    {
-        this(null, null);
-    }
-    // ino.end
-    
-    // ino.method.CSubstitution.27018.definition 
-    public CSubstitution(TypePlaceholder typeVar, Type type)
-    // ino.end
-    // ino.method.CSubstitution.27018.body 
-    {
-        m_TypeVar = typeVar;
-        m_Type = type;
-    }
-    // ino.end
-    
-    // ino.method.CSubstitution.27021.definition 
-    public CSubstitution(Pair unifier)
-    throws CTypeReconstructionException
-    // ino.end
-    // ino.method.CSubstitution.27021.body 
-    {
-        if(!(unifier.TA1 instanceof TypePlaceholder)){          
-            throw new CTypeReconstructionException("Unifier enth�lt keinen Typeplaceholder",unifier.TA1);
-        }
-        m_TypeVar = (TypePlaceholder)unifier.TA1;
-        m_Type = unifier.TA2;
-    }
-    // ino.end
-    
-    
-    // ino.method.getType.27024.defdescription type=javadoc
-    /**
-     * Author: J�rg B�uerle<br/>
-     * @return Returns the Type.
-     */
-    // ino.end
-    // ino.method.getType.27024.definition 
-    public Type getType()
-    // ino.end
-    // ino.method.getType.27024.body 
-    {
-        return m_Type;
-    }
-    // ino.end
-    
-    // ino.method.setType.27027.defdescription type=javadoc
-    /**
-     * Author: J�rg B�uerle<br/>
-     * @param type The Type to set.
-     */
-    // ino.end
-    // ino.method.setType.27027.definition 
-    public void setType(Type type)
-    // ino.end
-    // ino.method.setType.27027.body 
-    {
-        m_Type = type;
-    }
-    // ino.end
-    
-    // ino.method.getTypeVar.27030.defdescription type=javadoc
-    /**
-     * Author: J�rg B�uerle<br/>
-     * @return Returns the TypeVar.
-     */
-    // ino.end
-    // ino.method.getTypeVar.27030.definition 
-    public Type getTypeVar()
-    // ino.end
-    // ino.method.getTypeVar.27030.body 
-    {
-        return this.m_TypeVar;
-    }
-    // ino.end
-    
-    // ino.method.setTypeVar.27033.defdescription type=javadoc
-    /**
-     * Author: J�rg B�uerle<br/>
-     * @param typeVar The TypeVar to set.
-     */
-    // ino.end
-    // ino.method.setTypeVar.27033.definition 
-    public void setTypeVar(TypePlaceholder typeVar)
-    // ino.end
-    // ino.method.setTypeVar.27033.body 
-    {
-        m_TypeVar = typeVar;
-    }
-    // ino.end
-    
-    // ino.method.equals.27036.definition 
-    public boolean equals(Object obj)
-    // ino.end
-    // ino.method.equals.27036.body 
-    {
-        if(obj instanceof CSubstitution){
-            CSubstitution sub = (CSubstitution)obj;
-            boolean ret = true;
-            ret &= (m_TypeVar.equals(sub.m_TypeVar));
-            ret &= (m_Type.equals(sub.m_Type));
-            return ret;
-        }
-        else{
-            return false;
-        }
-    }
-    // ino.end
-    
-    // ino.method.toString.27039.definition 
-    public String toString()
-    // ino.end
-    // ino.method.toString.27039.body 
-    {
-        //return m_TypeVar.getName() +" --> "+m_Type.getName();
-        return m_TypeVar.toString() +" --> "+m_Type.toString();    	
-    }
-    // ino.end
-    
-    // ino.method.clone.27042.definition 
-    public CSubstitution clone()
-    // ino.end
-    // ino.method.clone.27042.body 
-    {
-        CSubstitution copy = new CSubstitution(m_TypeVar.clone(), m_Type.clone());
-        return copy;
-    }
-    // ino.end
-    
-    
-    // ino.method.applyUnifier.27048.defdescription type=javadoc
-    /**
-     * Wendet den Unifier auf die rechte Seite dieser Substitution an.
-     * <br/>Author: J�rg B�uerle
-     * @param unifier
-     */
-    // ino.end
-    // ino.method.applyUnifier.27048.definition 
-    public void applyUnifier(CSubstitutionSet unifier)
-    // ino.end
-    // ino.method.applyUnifier.27048.body 
-    {
-        Iterator pairIt = unifier.getIterator();
-        while(pairIt.hasNext()){
-            CSubstitution subst = (CSubstitution)pairIt.next();
-    
-        //korrigiert PL 05-07-31 das erste duerfte doch richtig sein.
-            //subst.setType(this.applySubstitution(subst.getType(), subst));
-            this.setType(this.applySubstitution(this.getType(), subst));
-        }
-        
-    }
-    // ino.end
-    
-    // ino.method.applySubstitution.27051.defdescription type=javadoc
-    /**
-     * Wendet die �bergebene Substitution rekursiv auf den �bergebenen Typ an.
-     * <br/>Author: J�rg B�uerle
-     * @param type Der zu untersuchende Typ
-     * @param unifierSub Die anzuwendende Substitution
-     * @return Den ermittelnden Typ
-     */
-    // ino.end
-    // ino.method.applySubstitution.27051.definition 
-    private Type applySubstitution(Type type, CSubstitution unifierSub)
-    // ino.end
-    // ino.method.applySubstitution.27051.body 
-    {
-        if(type instanceof TypePlaceholder){
-            if(type.equals(unifierSub.getTypeVar())){
-                return unifierSub.getType();
-            }
-        }
-        else if(type instanceof GenericTypeVar){
-            if(type.equals(unifierSub.getTypeVar())){
-                return unifierSub.getType();
-            }
-    }
-    else if(type instanceof RefType){
-            Menge<Type> paras = ((RefType)type).get_ParaList();
-            if(paras != null){
-                for(int i=0; i<paras.size(); i++){
-                    paras.setElementAt(this.applySubstitution((Type)paras.elementAt(i), unifierSub), i);
-                }
-            }
-        } 
-        return type;
-    }
-    // ino.end
-
-    // ino.method.applyThisSubstitution.27054.definition 
-    public Type applyThisSubstitution(Type type)
-    // ino.end
-    // ino.method.applyThisSubstitution.27054.body 
-    {
-    return applySubstitution(type, this);
-    }
-    // ino.end
-}
-// ino.end
diff --git a/src/de/dhbwstuttgart/typeinference/unify/CSubstitutionGenVar.java b/src/de/dhbwstuttgart/typeinference/unify/CSubstitutionGenVar.java
deleted file mode 100755
index a93b6eec..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/CSubstitutionGenVar.java
+++ /dev/null
@@ -1,70 +0,0 @@
-// ino.module.CSubstitutionGenVar.8686.package 
-package de.dhbwstuttgart.typeinference.unify;
-
-import de.dhbwstuttgart.syntaxtree.type.GenericTypeVar;
-// ino.end
-import de.dhbwstuttgart.syntaxtree.type.Type;
-
-// ino.class.CSubstitutionGenVar.27057.description type=javadoc
-/**
- * Implementierung einer Typsubstitution der GenVar. Bildet eine zu ersetzende     
- * <code>TypePlaceholder</code> auf einen Substitutions-Typ ab. Instanzen dieser   
- * Klasse werden in der Regel aus
- * <code>Pair</code>-Objekten erzeugt.
- * @author Martin Pl�micke
- * @version $Date: 2006/06/13 10:37:32 $
- */
-// ino.end
-// ino.class.CSubstitutionGenVar.27057.declaration 
-public class CSubstitutionGenVar extends CSubstitution
-// ino.end
-// ino.class.CSubstitutionGenVar.27057.body
-{
-    // ino.attribute.m_TypeVar.27061.declaration 
-    private GenericTypeVar m_TypeVar = null;
-    // ino.end
-    
-    // ino.method.CSubstitutionGenVar.27064.definition 
-    public CSubstitutionGenVar()
-    // ino.end
-    // ino.method.CSubstitutionGenVar.27064.body 
-    {
-        this(null, null);
-    }
-    // ino.end
-    
-    // ino.method.CSubstitutionGenVar.27067.definition 
-    public CSubstitutionGenVar(GenericTypeVar typeVar, Type type)
-    // ino.end
-    // ino.method.CSubstitutionGenVar.27067.body 
-    {
-        m_TypeVar = typeVar;
-        m_Type = type;
-    }
-    // ino.end
-
-     // ino.method.getTypeVar.27070.defdescription type=javadoc
-     /**
-      * Author: J�rg B�uerle<br/>
-      * @return Returns the TypeVar.
-      */
-     // ino.end
-    // ino.method.getTypeVar.27070.definition 
-    public Type getTypeVar()
-    // ino.end
-    // ino.method.getTypeVar.27070.body 
-    {
-        return this.m_TypeVar;
-    }
-    // ino.end
-
-     // ino.method.toString.27073.definition 
-     public String toString()
-     // ino.end
-     // ino.method.toString.27073.body 
-     {
-        return this.m_TypeVar.getName() +" --> "+this.m_Type.getName();
-         }
-     // ino.end
-}
-// ino.end
diff --git a/src/de/dhbwstuttgart/typeinference/unify/CSubstitutionSet.java b/src/de/dhbwstuttgart/typeinference/unify/CSubstitutionSet.java
deleted file mode 100755
index 481ca7cf..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/CSubstitutionSet.java
+++ /dev/null
@@ -1,111 +0,0 @@
-// ino.module.CSubstitutionSet.8699.package 
-package de.dhbwstuttgart.typeinference.unify;
-// ino.end
-
-// ino.module.CSubstitutionSet.8699.import 
-import java.util.Iterator;
-import de.dhbwstuttgart.typeinference.Menge;
-
-import de.dhbwstuttgart.myexception.CTypeReconstructionException;
-import de.dhbwstuttgart.syntaxtree.type.Type;
-import de.dhbwstuttgart.typeinference.Pair;
-
-// ino.class.CSubstitutionSet.27471.description type=javadoc
-/**
- * @author J�rg B�uerle
- * @version $Date: 2013/03/27 18:29:34 $
- */
-// ino.end
-// ino.class.CSubstitutionSet.27471.declaration 
-public class CSubstitutionSet extends CVectorSet<CSubstitution>
-// ino.end
-// ino.class.CSubstitutionSet.27471.body
-{
-    // ino.method.CSubstitutionSet.27475.definition 
-    public CSubstitutionSet()
-    // ino.end
-    // ino.method.CSubstitutionSet.27475.body 
-    {
-        super();
-    }
-    // ino.end
-    
-    // ino.method.CSubstitutionSet.27478.definition 
-    public CSubstitutionSet(Menge<Pair> unifiers)
-    throws CTypeReconstructionException
-    // ino.end
-    // ino.method.CSubstitutionSet.27478.body 
-    {
-        super();
-        for(int i=0; i<unifiers.size(); i++){
-            this.addElement(new CSubstitution(unifiers.elementAt(i)));
-        }
-    }
-    // ino.end
-    
-    // ino.method.shallowCopy.27481.definition 
-    public CSubstitutionSet shallowCopy()
-    // ino.end
-    // ino.method.shallowCopy.27481.body 
-    {
-        CSubstitutionSet copy = new CSubstitutionSet();
-        copy.setMenge((Menge)this.getMenge().clone());
-        return copy;
-    }
-    // ino.end
-    
-    // ino.method.deepCopy.27484.definition 
-    public CSubstitutionSet deepCopy()
-    // ino.end
-    // ino.method.deepCopy.27484.body 
-    {
-        CSubstitutionSet copy = new CSubstitutionSet();
-        Iterator<CSubstitution> substIter = this.getIterator();
-        while(substIter.hasNext()){
-            copy.addElement(substIter.next().clone());
-        }
-        return copy;
-    }
-    // ino.end
-    
-    // ino.method.applyUnifier.27487.defdescription type=javadoc
-    /**
-     * Wendet den Unifier auf die rechten Seiten alle Substitutionen an.
-     * <br/>Author: J�rg B�uerle
-     * @param unifier
-     */
-    // ino.end
-    // ino.method.applyUnifier.27487.definition 
-    public void applyUnifier(CSubstitutionSet unifier)
-    // ino.end
-    // ino.method.applyUnifier.27487.body 
-    {
-        Iterator<CSubstitution> substIt = this.getIterator();
-        
-        while(substIt.hasNext()){
-            substIt.next().applyUnifier(unifier);
-        }
-    }
-    // ino.end
-
-    // ino.method.applyThisSubstitutionSet.27490.definition 
-    public Type applyThisSubstitutionSet(Type type)
-    // ino.end
-    // ino.method.applyThisSubstitutionSet.27490.body 
-    {
-    Iterator<CSubstitution> substIt = this.getIterator();
-    Type ty = type;
-        
-        while(substIt.hasNext()) {
-            ty = substIt.next().applyThisSubstitution(ty);
-        }
-    return ty;
-    }
-    // ino.end
-
-
-	public Iterator<CSubstitution> iterator() {
-		return this.getIterator();
-	}
-}
-// ino.end
diff --git a/src/de/dhbwstuttgart/typeinference/unify/CVectorSet.java b/src/de/dhbwstuttgart/typeinference/unify/CVectorSet.java
deleted file mode 100755
index 5fc6146f..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/CVectorSet.java
+++ /dev/null
@@ -1,165 +0,0 @@
-// ino.module.CMengeSet.8702.package 
-package de.dhbwstuttgart.typeinference.unify;
-// ino.end
-
-// ino.module.CMengeSet.8702.import 
-import java.util.Iterator;
-import de.dhbwstuttgart.typeinference.Menge;
-// ino.end
-
-// ino.class.CMengeSet.27519.description type=javadoc
-/**
- * @author J�rg B�uerle
- * @version $Date: 2013/02/07 05:08:51 $
- */
-// ino.end
-// ino.class.CMengeSet.27519.declaration 
-public abstract class CVectorSet<E> extends CSet<E>
-// ino.end
-// ino.class.CMengeSet.27519.body
-{
-    // ino.attribute.m_Elements.27523.declaration 
-    private Menge<E> m_Elements = null;
-    // ino.end
-    
-    // ino.method.CMengeSet.27526.definition 
-    public CVectorSet()
-    // ino.end
-    // ino.method.CMengeSet.27526.body 
-    {
-        m_Elements = new Menge<E>();
-    }
-    // ino.end
-    
-    // ino.method.addElement.27529.definition 
-    public void addElement(E element)
-    // ino.end
-    // ino.method.addElement.27529.body 
-    {
-        m_Elements.addElement(element);
-    }
-    // ino.end
-    
-    // ino.method.removeElement.27532.definition 
-    public void removeElement(E element)
-    // ino.end
-    // ino.method.removeElement.27532.body 
-    {
-        m_Elements.addElement(element);
-    }
-    // ino.end
-    
-    public void addAll( CVectorSet<E> set ) 
-    {	
-    	for( int i=0;i<set.getCardinality(); i++ ){
-    		m_Elements.addElement(set.m_Elements.elementAt(i));	
-    	}    	
-    }
-    
-    
-    // ino.method.getIterator.27535.definition 
-    public Iterator<E> getIterator()
-    // ino.end
-    // ino.method.getIterator.27535.body 
-    {
-        return m_Elements.iterator();
-    }
-    // ino.end
-    
-    // ino.method.getMenge.27538.definition 
-    public Menge<E> getMenge()
-    // ino.end
-    // ino.method.getMenge.27538.body 
-    {
-        return m_Elements;
-    }
-    // ino.end
-    
-    // ino.method.setMenge.27541.definition 
-    public void setMenge(Menge<E> elements)
-    // ino.end
-    // ino.method.setMenge.27541.body 
-    {
-        m_Elements = elements;
-    }
-    // ino.end
-    
-    /**
-     * Fügt ein CMengeSet an!
-     * Es handelt sich um eine Vereinigung (es werden keine bereits vorhandenen Elemente übernommen)
-     * @param anotherSet Das hinzuzufügende CMengeSet (CSet wird ignoriert)
-     */
-    // ino.method.unite.27544.definition 
-    public void unite(CSet<E> anotherSet)
-    // ino.end
-    // ino.method.unite.27544.body 
-    {
-        if(!(anotherSet instanceof CVectorSet)){
-            return;
-        }
-        CVectorSet<E> MengeSet = (CVectorSet<E>)anotherSet;
-        
-        // Elemente der anderen Menge hinzuf�gen:
-        Iterator<E> it = MengeSet.getIterator();
-        while(it.hasNext()){
-            E elem = it.next();
-            if(!m_Elements.contains(elem)){
-                m_Elements.addElement(elem);
-            }
-        }
-        //m_Elements.addAll(MengeSet.m_Elements);
-    }
-    // ino.end
-
-    // ino.method.subtract.27547.definition 
-    public void subtract(CSet<E> anotherSet)
-    // ino.end
-    // ino.method.subtract.27547.body 
-    {
-        if(!(anotherSet instanceof CVectorSet)){
-            return;
-        }
-        CVectorSet<E> MengeSet = (CVectorSet<E>)anotherSet;
-        
-        // Elemente der anderen Menge entfernen:
-        m_Elements.removeAll(MengeSet.m_Elements);
-    }
-    // ino.end
-    
-    // ino.method.contains.27550.definition 
-    public boolean contains(E element)
-    // ino.end
-    // ino.method.contains.27550.body 
-    {
-        return m_Elements.contains(element);
-    }
-    // ino.end
-    
-    // ino.method.equals.27553.definition 
-    public boolean equals(Object obj)
-    // ino.end
-    // ino.method.equals.27553.body 
-    {
-        if(obj instanceof CVectorSet){
-        	CVectorSet tripSet= (CVectorSet)obj;
-            boolean ret = true;
-            ret &= (m_Elements.containsAll(tripSet.m_Elements));
-            ret &= (tripSet.m_Elements.containsAll(m_Elements));
-            return ret;
-        }
-        else{
-            return false;
-        }
-    }
-    // ino.end
-    
-    // ino.method.getCardinality.27556.definition 
-    public int getCardinality()
-    // ino.end
-    // ino.method.getCardinality.27556.body 
-    {
-        return m_Elements.size();
-    }
-    // ino.end
-}
-// ino.end
diff --git a/src/de/dhbwstuttgart/typeinference/unify/FC_TTO.java b/src/de/dhbwstuttgart/typeinference/unify/FC_TTO.java
deleted file mode 100755
index f27119a6..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/FC_TTO.java
+++ /dev/null
@@ -1,82 +0,0 @@
-// ino.module.FC_TTO.8719.package 
-package de.dhbwstuttgart.typeinference.unify;
-// ino.end
-
-// ino.module.FC_TTO.8719.import 
-import de.dhbwstuttgart.typeinference.Menge;
-
-import de.dhbwstuttgart.syntaxtree.Class;
-import de.dhbwstuttgart.typeinference.Pair;
-import de.dhbwstuttgart.typeinference.assumptions.TypeAssumptions;
-
-// ino.class.FC_TTO.28013.description type=javadoc
-/**
- * Hilfsklasse f�r den Unifizierungsalgorithmus
- * @author Martin Pl�micke
- * @version $Date: 2013/05/12 14:00:05 $
- */
-// ino.end
-// ino.class.FC_TTO.28013.declaration 
-public class FC_TTO
-// ino.end
-// ino.class.FC_TTO.28013.body
-{
-
-    // ino.attribute.FC.28016.declaration 
-    Menge<Pair> FC;
-    // ino.end
-    // ino.attribute.TTO.28019.declaration 
-    Menge TTO;
-    // ino.end
-    
-    Menge<Class> CLASSVEC;
-
-    // ino.method.FC_TTO.28022.definition 
-    public FC_TTO(Menge<Pair> fc, Menge tto, Menge<Class> classv)
-    // ino.end
-    // ino.method.FC_TTO.28022.body 
-    {
-    
-    this.FC = fc;
-    this.TTO = tto;
-    this.CLASSVEC = classv;
-    
-    }
-    // ino.end
-
-    // ino.method.getFC.28025.definition 
-    public Menge<Pair> getFC()
-    // ino.end
-    // ino.method.getFC.28025.body 
-    {
-    return FC;
-    }
-    // ino.end
-
-    // ino.method.getTTO.28028.definition 
-    public Menge getTTO()
-    // ino.end
-    // ino.method.getTTO.28028.body 
-    {
-    return TTO;
-    }
-    // ino.end
-    
-    public Menge<Class> getClasses()
-    {
-    	return CLASSVEC;
-    }
-    
-    @Override
-    public String toString(){
-    	return "FC: "+getFC()+"\nTTO: "+getTTO()+"\nCLASSVEC: "+getClasses();
-    }
-
-	public void generateFullyNamedTypes(TypeAssumptions ass) {
-		for(Pair p : this.FC){
-			p.TA1 = p.TA1.TYPE(ass, p.TA1.getParent());//ass.getTypeFor(p.TA1, p.TA1.getParent()).getType();
-			p.TA2 = p.TA2.TYPE(ass, p.TA2.getParent());//ass.getTypeFor(p.TA2, p.TA2.getParent()).getType();
-		}
-	}
-}
-// ino.end
diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/GuavaSetOperations.java b/src/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java
similarity index 84%
rename from src/de/dhbwstuttgart/typeinference/unifynew/GuavaSetOperations.java
rename to src/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java
index cc4e907c..ba456841 100644
--- a/src/de/dhbwstuttgart/typeinference/unifynew/GuavaSetOperations.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/GuavaSetOperations.java
@@ -1,4 +1,4 @@
-package de.dhbwstuttgart.typeinference.unifynew;
+package de.dhbwstuttgart.typeinference.unify;
 
 import java.util.List;
 import java.util.Set;
diff --git a/src/de/dhbwstuttgart/typeinference/unify/MUB.java b/src/de/dhbwstuttgart/typeinference/unify/MUB.java
deleted file mode 100755
index 42e70c64..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/MUB.java
+++ /dev/null
@@ -1,53 +0,0 @@
-// ino.module.MUB.8720.package 
-package de.dhbwstuttgart.typeinference.unify;
-// ino.end
-
-// ino.module.MUB.8720.import 
-import de.dhbwstuttgart.typeinference.Menge;
-
-import de.dhbwstuttgart.syntaxtree.type.Type;
-import de.dhbwstuttgart.typeinference.Pair;
-
-// ino.class.MUB.28031.declaration 
-public class MUB
-// ino.end
-// ino.class.MUB.28031.body
-{
-    // ino.attribute.Mub.28034.declaration 
-    Menge<? extends Type> Mub;
-    // ino.end
-    // ino.attribute.sigma.28037.declaration 
-    Menge<Pair> sigma;
-    // ino.end
-    
-    // ino.method.MUB.28040.definition 
-    MUB(Menge<? extends Type> M, Menge<Pair> s)
-    // ino.end
-    // ino.method.MUB.28040.body 
-    {
-    Mub = M;
-    sigma = s;
-    }
-    // ino.end
-
-    // ino.method.getUnifier.28043.definition 
-    public Menge<Pair> getUnifier()
-    // ino.end
-    // ino.method.getUnifier.28043.body 
-    {
-    return sigma;
-    }
-    // ino.end
-
-    // ino.method.getMub.28046.definition 
-    public Menge<? extends Type> getMub()
-    // ino.end
-    // ino.method.getMub.28046.body 
-    {
-    return Mub;
-    }
-    // ino.end
-  
-}
-// ino.end
-
diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java b/src/de/dhbwstuttgart/typeinference/unify/Mapping.java
similarity index 96%
rename from src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java
rename to src/de/dhbwstuttgart/typeinference/unify/Mapping.java
index e21bb728..603fb0f7 100644
--- a/src/de/dhbwstuttgart/typeinference/unifynew/Mapping.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/Mapping.java
@@ -1,4 +1,4 @@
-package de.dhbwstuttgart.typeinference.unifynew;
+package de.dhbwstuttgart.typeinference.unify;
 
 import java.util.HashMap;
 import java.util.HashSet;
diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
similarity index 95%
rename from src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java
rename to src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
index 858fd80a..b411e7fe 100644
--- a/src/de/dhbwstuttgart/typeinference/unifynew/MartelliMontanariUnify.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
@@ -1,4 +1,4 @@
-package de.dhbwstuttgart.typeinference.unifynew;
+package de.dhbwstuttgart.typeinference.unify;
 
 import java.util.AbstractMap;
 import java.util.ArrayList;
diff --git a/src/de/dhbwstuttgart/typeinference/unify/ParallelUnify.java b/src/de/dhbwstuttgart/typeinference/unify/ParallelUnify.java
deleted file mode 100644
index fffceb53..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/ParallelUnify.java
+++ /dev/null
@@ -1,44 +0,0 @@
-package de.dhbwstuttgart.typeinference.unify;
-
-import de.dhbwstuttgart.typeinference.Menge;
-import java.util.stream.Stream;
-
-import de.dhbwstuttgart.typeinference.ConstraintsSet;
-import de.dhbwstuttgart.typeinference.Pair;
-
-public class ParallelUnify {
-
-	public ParallelUnify(ConstraintsSet constraints){
-		//constraints.getConstraints();
-	}
-	
-	private CartesianProduct parallelCartProd(){
-		
-		return null;
-	}
-	
-	private UnifyResult parallelUnify(Menge<Pair> pairs, FC_TTO fc){
-		UnifyResult ret = new UnifyResult();
-		return ret;
-	}
-	
-	public UnifyResult unify(){
-		UnifyResult ret = new UnifyResult();
-		return ret;
-	}
-	
-}
-
-class ParallelConstraintSet extends ConstraintsSet{
-	Stream parallelGetConstraints(){
-		return null;
-	}
-}
-
-class UnifyResult{
-	
-}
-
-class CartesianProduct{
-	
-}
\ No newline at end of file
diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java b/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java
similarity index 96%
rename from src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java
rename to src/de/dhbwstuttgart/typeinference/unify/RuleSet.java
index fedccd86..51616be3 100644
--- a/src/de/dhbwstuttgart/typeinference/unifynew/RuleSet.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java
@@ -1,4 +1,4 @@
-package de.dhbwstuttgart.typeinference.unifynew;
+package de.dhbwstuttgart.typeinference.unify;
 
 import java.util.ArrayList;
 import java.util.HashMap;
diff --git a/src/de/dhbwstuttgart/typeinference/unify/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/Unifier.java
deleted file mode 100644
index 19446236..00000000
--- a/src/de/dhbwstuttgart/typeinference/unify/Unifier.java
+++ /dev/null
@@ -1,11 +0,0 @@
-package de.dhbwstuttgart.typeinference.unify;
-
-import de.dhbwstuttgart.typeinference.Menge;
-
-import de.dhbwstuttgart.typeinference.Pair;
-
-public interface Unifier {
-
-	public Menge<Menge<Pair>> apply (Menge<Pair> E);
-
-}
diff --git a/src/de/dhbwstuttgart/typeinference/unify/Unify.java b/src/de/dhbwstuttgart/typeinference/unify/Unify.java
old mode 100755
new mode 100644
index 8cd2baa9..cb2cf3c4
--- a/src/de/dhbwstuttgart/typeinference/unify/Unify.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/Unify.java
@@ -1,3563 +1,480 @@
-//otth/pluemicke2.1.jav funktioniert nicht xxx anschauen
-// ino.module.Unify.8721.package 
-package de.dhbwstuttgart.typeinference.unify;
-import java.util.Collection;
-// ino.end
-// ino.module.Unify.8721.import 
-import java.util.Enumeration;
-import java.util.Hashtable;
-import java.util.Iterator;
-import java.util.function.Function;
-import java.util.stream.Stream;
-
-import de.dhbwstuttgart.logger.Logger;
-import de.dhbwstuttgart.logger.Section;
-import de.dhbwstuttgart.logger.SectionLogger;
-import de.dhbwstuttgart.logger.Timestamp;
-import de.dhbwstuttgart.logger.Timewatch;
-import de.dhbwstuttgart.core.MyCompiler;
-import de.dhbwstuttgart.myexception.CTypeReconstructionException;
-import de.dhbwstuttgart.myexception.MatchException;
-import de.dhbwstuttgart.myexception.SCException;
-import de.dhbwstuttgart.parser.JavaClassName;
-import de.dhbwstuttgart.syntaxtree.Class;
-import de.dhbwstuttgart.syntaxtree.type.BoundedGenericTypeVar;
-import de.dhbwstuttgart.syntaxtree.type.ExtendsWildcardType;
-import de.dhbwstuttgart.syntaxtree.type.FreshExtendsWildcardType;
-import de.dhbwstuttgart.syntaxtree.type.FreshSuperWildcardType;
-import de.dhbwstuttgart.syntaxtree.type.FreshWildcardType;
-import de.dhbwstuttgart.syntaxtree.type.GenericTypeVar;
-import de.dhbwstuttgart.syntaxtree.type.IMatchable;
-import de.dhbwstuttgart.syntaxtree.type.RefType;
-import de.dhbwstuttgart.syntaxtree.type.SuperWildcardType;
-import de.dhbwstuttgart.syntaxtree.type.Type;
-import de.dhbwstuttgart.syntaxtree.type.ObjectType;
-import de.dhbwstuttgart.syntaxtree.type.TypePlaceholder;
-import de.dhbwstuttgart.syntaxtree.type.WildcardType;
-import de.dhbwstuttgart.typeinference.DeepCloneable;
-import de.dhbwstuttgart.typeinference.Menge;
-import de.dhbwstuttgart.typeinference.Pair;
-import de.dhbwstuttgart.typeinference.Pair.PairOperator;
-
-// ino.end
-
-// ino.class.Unify.28049.description type=javadoc
-/**
- * Implementierung des Unifizierungsalgorithmus
- * @author Martin Pl�micke, Thomas Ott
- * @version $Date: 2013/05/22 22:23:50 $
- */
-// ino.end
-// ino.class.Unify.28049.declaration 
-public class Unify
-// ino.end
-// ino.class.Unify.28049.body
-{
-    
-    // ino.attribute.inferencelog.28052.declaration 
-    protected static SectionLogger inferencelog = Logger.getSectionLogger("inference", Section.UNIFY);
-    // ino.end
-    
-    /**
-     * Unifiziert ein Pair mit den Elementen ty1 und ty2  -> (ty1 < ty2)
-     * @param ty1
-     * @param ty2
-     * @param fc_tto
-     * @return
-     */
-    // ino.method.unify.28055.definition 
-    public static Menge<Menge<Pair>> unify(Type ty1, Type ty2, FC_TTO fc_tto )
-    // ino.end
-    // ino.method.unify.28055.body 
-    {
-        Menge<Pair> pairsToUnify = new Menge<Pair>();
-        Pair retTypePair = new Pair(ty1, ty2);
-        pairsToUnify.addElement(retTypePair);
-        return Unify.unify(pairsToUnify, fc_tto);
-    }
-    // ino.end
-    
-
-    /**
-     * Einstieg in die Unifizierung mit Wildcards
-     * 
-     * @param ty1 - Typ 1 der Unifizierung
-     * @param ty2 - Typ 2 der Unifizierung
-     * @param fc_tto - Hilfsklasse mit FC
-     * @return Menge<Menge<Pair>> - Ergebnispaare
-     */
-    public static Menge<Menge<Pair>> unifyWC(Type ty1, Type ty2, FC_TTO fc_tto)
-    {
-    	return unifyWC(new Pair(ty1,ty2),fc_tto);
-    }
-    
-    /**
-     * Einstieg in die Unifizierung mit Wildcards
-     * 
-     * @param P - Paar das unifiziert werden soll.
-     * @param fc_tto - Hilfsklasse mit FC
-     * @return Menge<Menge<Pair>> - Ergebnispaare
-     */
-    public static Menge<Menge<Pair>> unifyWC (Pair P, FC_TTO fc_tto)
-    {
-    	Menge<Pair> tmp = new Menge<Pair>();
-    	tmp.add(P);
-    	return unify(tmp,fc_tto);
-    }
-   
-    /**
-     * Einstieg in die Unifizierung mit Wildcards
-     * 
-     * @param E - Menge von Paaren die unifiziert werden sollen
-     * @param fc_tto - Hilfsklasse mit FC
-     * @return Menge<Menge<Pair>> - Ergebnispaare
-     * Entweder alle Elemente in solved Form [A =. type, B =. type2, ...]
-     * oder alle Elemente in der Form [A <. B, C <. D, ..., E <? F, G <? H, ....  I =. type, J =. type2, ...]
-     * oder [] = fail
-     * F�r den Argumenttype FunN<...> in Typ A<FunN<...> ...> werden keine ? extends-, ? super-Typen erzeugt
-     */
-    //public static Menge<Menge<Pair>> unifyWC (Menge<Pair> E, FC_TTO fc_tto)
-    public static Menge<Menge<Pair>> unify (Menge<Pair> E, FC_TTO fc_tto)
-    {
-    	//Schritt 1: Aufrufen der Regeln durch sub_unify.
-    	Menge<Pair> Eq = sub_unify(E,fc_tto);
-    	/* Schritt 2: Rausfiltern der Typen die entweder beides Typvariablen sind oder nicht.
-    	 * Sobald ein Paar auftauch, bei denen kein Typ mehr eine Typvariable ist, kann dieses Paar
-    	 * nicht mehr unifiziert werden, deshalb abbruch.*/
-    	Menge<Pair> Eq1 = new Menge<Pair>();
-    	for(Pair p : Eq)
-    	{
-    		if(p.TA1 instanceof TypePlaceholder && p.TA2 instanceof TypePlaceholder)
-    		{
-    			Eq1.add(p);
-    		}
-    		else if(!(p.TA1 instanceof TypePlaceholder) && !(p.TA2 instanceof TypePlaceholder))
-    		{
-    			//Diese Paare k�nnen nicht mehr Unifiziert werden. fail.
-    			inferencelog.debug("UNIFY FAIL:" + p.TA1 + " <. " + p.TA2 + " muesste mindestens einen TPH enthalten.");
-    			return new Menge<Menge<Pair>>();
-    		}
-    	}
-    	//Schritt 3: Differenz bilden, in Eq2 landen alle Paare die nicht in Eq1 sind.
-    	Menge<Pair> Eq2 = new Menge<Pair>();
-    	for(Pair p : Eq)
-    	{
-    		if(!Eq1.contains(p))
-    			Eq2.add(p);
-    	}
-    	/* Schritt 4, Teil 1: Einsammeln der Sets f�r das Kartesiche Produkt.
-    	 * Hier werden die Paare verglichen. Je nach Struktur k�nnen neue Paare erzeugt
-    	 * werden, aus denen dann das kartesische Produkt gebildet wird.*/
-    	Menge<Menge<Menge<Pair>>> cartProduktSets = new Menge<Menge<Menge<Pair>>>();
-    	for(Pair p : Eq2)
-    	{
-    		if(p.TA1 instanceof TypePlaceholder)
-    		{
-    			//TPH <. ? super Ty entspricht TPH <. Ty
-                        if (p.TA2 instanceof SuperWildcardType) {
-                               p.TA2 = ((SuperWildcardType)p.TA2).get_SuperType(); 
-                               //HIER GIBT ES EIN PROBLEM, WENN get_SuperType ein TPH LIEFERT PL 15-03-12
-                               //Dann ist THP <. TPH in Eq2 anstatt in Eq1
-                               //Muesste mit folgendem if gel�st sein. PL 15-03-17
-                               if (p.TA2 instanceof TypePlaceholder) {
-                                       Eq1.addElement(p);
-                                       //      Eq2.remove(p);
-                                       continue;
-                               }
-                       }
-
-    			
-    			if(p.OperatorEqual())
-    			{
-    				//Alle Paare die bereits durch sub_unify die richtige Struktur haben einfach durchleiten.
-    				Menge<Menge<Pair>> setofsetofpairs = new Menge<Menge<Pair>>();
-					Menge<Pair> vTmp = new Menge<Pair>();
-					vTmp.add(p);
-					setofsetofpairs.add(vTmp);
-					cartProduktSets.add(setofsetofpairs);
-    			}
-    			else if(p.OperatorSmaller() && (p.TA2 instanceof RefType))
-    			{
-    				RefType p_TA2 = (RefType)p.TA2;
-	    			//1. Menge
-					//Durch alle Paare p_fc laufen und schauen ob diese von der Struktur zu dem Paar p passen.
-					Menge<Pair> fc_refl = copyMengePair(fc_tto.getFC());
-					fc_refl.add(new Pair(p_TA2.clone(), p_TA2.clone())); //Reflexivitaet muss beruecksichtigt werden; ergaenzt PL 07-07-28
-					                                                 //Ist aber in FC nicht enthalten.
-					Menge<Menge<Pair>> ergMenge1 = new Menge<Menge<Pair>>(); //Ergebnismenge der 1. Menge;
-	    			for(Pair p_fc : fc_refl)
-	    			{
-	    				RefType tmp = ((RefType)p_fc.TA2).clone();   //Unifikation vorgezogen, da isRXSimilarRY nicht ausreicht PL 07-07-29
-						CSubstitutionSet gtv2tv = tmp.GenericTypeVar2TypePlaceholder();
-						Menge<ObjectType> greater1elemente;
-						if (tmp.get_ParaList() == null) 
-						{
-							greater1elemente = new Menge<ObjectType>(); //Bei Konstanten liefert greater1 [] zurueck
-							greater1elemente.add(tmp);
-						}
-						else
-						{
-							greater1elemente = greater1(tmp, fc_tto);
-						}
-						Menge<Menge<Pair>> unifyErgs = new Menge<Menge<Pair>>();
-    					for (Type p_TA2_gr : greater1elemente) //Unify alleine reicht nicht, da p_TA2 Wildcards vorkommen koennen
-    					{	                                   //muessen auch alle Typen deren Args Subtypen von p_TA2 sind betrachtet werden.
-    														 //Dies wird durch smaller1elemente bzw. smaller1 erledigt PL 07-07-29
-    						Pair pUnify = new Pair(p_TA2.clone(),p_TA2_gr,PairOperator.Equal);
-    						Menge<Menge<Pair>> unifyErgsElement = unifyWC(pUnify,fc_tto);
-    						if (!unifyErgsElement.isEmpty()) {
-    							unifyErgs.add(unifyErgsElement.firstElement());
-    						}
-    					}
-//    					Nach dem Unifizieren wird das Ergebnis �berpr�ft, und evtl. durch die FC entstandene TPHs werden gel�scht.
-	    				if((p_fc.TA2 instanceof RefType && !unifyErgs.isEmpty())
-	    			       || p_fc.TA2.equals(p_TA2)) //Bedingung fuer Reflexifitaet BRAURHT MAN VERMUTLIRH NIRHT PL 07-08-05
-	    			    {
-	    					//Wenn die Unifizierung erfolgreich war durch jeden Ergebnisvektor der Unifizierung laufen.
-	    					for(Menge<Pair> pVec : unifyErgs)
-	    					{
-//	    						Das Ergebnis in die linke Seite von p_fc einsetzen, und dort Smaller anwenden.
-    	    					Hashtable<JavaClassName,Type> ht = MengePair2SubstHashtableMengePair(pVec);
- 	    						//PL 07-07-04 smallerArg wird auf die linke Seite von p_FC nach subst angewandt  	    							    	    						
-    	    					RefType p_fc_TA1_new = (RefType)p_fc.TA1.clone();
-    	    					gtv2tv.applyThisSubstitutionSet(p_fc_TA1_new); //auf der linken Seite
-    	    					//muessen die GTV durch die gleichen fresh tvs ersetzt werden, wie auf der rechten Seite. PL 07-07-29
-    	    					p_fc_TA1_new.GenericTypeVar2TypePlaceholder();
-    	    					//die uebrigen GTV muessen durch freshe tvs ersetzt werden.
-    	    					SubstHashtable((RefType)p_fc_TA1_new,ht);
-    		    					
-    	    					//smallerArg ersetz durch folgende Zeilen. Durch Transistivitaet von fc kommen sonst
-    	    					//doppelte Elemente rein
-    	    					//Anfang
-    	    					Menge<Type> smallers = new Menge<Type>();
-    		    				Menge<ObjectType> smaller1elemente;
-    		    				if (p_fc_TA1_new.get_ParaList() == null) 
-    		    				{
-    		    					smaller1elemente = new Menge<ObjectType>(); //Bei Konstanten liefert smaller1 [] zurueck
-    		    					smaller1elemente.add(p_fc_TA1_new);
-    		    				}
-    		    				else
-    		    				{
-    		    					smaller1elemente = smaller0(p_fc_TA1_new, fc_tto); //Von Menge 2 kopiert und smaller1 durch smaller0 ersetzt, Luar 07-08-08
-    		    				} 
-    		    					
-    		    				for(ObjectType smele : smaller1elemente) 
-    		    				{
-    		    					smallers.add(smele);
-    		    					smallers.add(new ExtendsWildcardType(smele.getOffset(), smele).clone()); //Auskommentiert luar 07-08-08
-    		    					                                                                         //wieder einkommentiert PL 15-03-11
-    		    				}
-    		    				//Ende
-    		    				
-//    		    				Ersatz fuer testUnifyErg PL 07-08-05
-    		    				//Anfang
-    		    				for(int vec = 0; vec < pVec.size(); vec++)
-    		    				{
-    		    					Pair pTest = pVec.elementAt(vec);
-    		    					if(!(pTest.TA1 instanceof TypePlaceholder) || !isTVinRefType((TypePlaceholder)pTest.TA1,p_TA2))
-    		    					{
-    		    						pVec.remove(vec);
-    		    						vec--;
-    		    					}
-    		    				}
-    		    				//ENDE
-    		    					
-    	    					Menge<Menge<Pair>> cartProduktErg = new Menge<Menge<Pair>>();
-    	    					cartProduktErg.add(pVec);
-    		    					
-    		    				//Mit den kleineren Typen neue Paare bilden, linke Seite Klonen.
-    		    				Menge<Pair> smallerPairs = new Menge<Pair>();
-    		    				for(Type sT : smallers)
-    							{
-    								smallerPairs.add(new Pair(p.TA1.clone(),sT,PairOperator.Equal));
-    							}
-    		    					
-			    				//Hier noch das Kartesische Produkt aus den Greater und den Smaller Ergebnissen bilden.
-			    				Menge<Menge<Pair>> ergs = new Menge<Menge<Pair>>();
-			    				for(Pair PsmP : smallerPairs)
-			    				{
-			    					Menge<Menge<Pair>> dolly = copyMengeMengePair(cartProduktErg);
-			    					if(dolly.isEmpty()) dolly.add(new Menge<Pair>());
-			    					for(Menge<Pair> vecp : dolly)
-			    					{
-			    						vecp.add(PsmP.clone());
-			    					}
-			    					ergs.addAll(dolly);
-			    				}
-			    				if(!ergs.isEmpty())
-			    					for (Menge<Pair> ergele : ergs)				    					
-			    						if (!ergMenge1.contains(ergele))		//ABFRAGE BRAURHT MAN VERMUTLIRH NIRHT, DA DURRH smaller1 keine doppelten Elemente reinkommen koennen		    						
-			    							ergMenge1.add(ergele);
-	    					}
-	    			    }
-	    			}
-	    			
-	    			//aus {ty <. ty'} {? extends ty <. ty'} erzeugen //angefuegt PL 15-03-03
-	    			//DIES IST NICHT RICHTIG GETESTET, ES KOENNTE SEIN, DASS DAS KART. PRODUKT FALSCH GEBILDET WIRD.
-                    //DIES MUEESTE DURCH smallers.add(new ExtendsWildcardType(smele.getOffset(), smele).clone()); weiter ober erledigt sein.
-	       		    //PL 15-03-11
-	    			//Stream<Menge<Pair>> strextergMenge1 = 
-//	    				ergMenge1.stream().map(v -> 
-//	    									   v.stream().map(pa -> 
-//	    									                  new Pair(pa.getTA1Copy(), new ExtendsWildcardType(pa.getTA2Copy().getOffset(), (ObjectType)pa.getTA2Copy()), pa.GetOperator(), pa.bSubst)
-//	    									                  ).collect(Menge::new, Menge::add, Menge::addAll));
-//	    			
-//	    			Menge<Menge<Pair>> extergMenge1 = strextergMenge1.collect(Menge::new, Menge::add, Menge::addAll);
-//	    			ergMenge1.addAll(extergMenge1);
-	    			cartProduktSets.add(ergMenge1);
-    			}
-    			else if(p.OperatorSmaller() && p.TA2 instanceof GenericTypeVar)
-    			{
-    				//Paar unver�ndert lassen, wenn eine GenericTypeVar ist
-    				Menge<Menge<Pair>> setofsetofpairs = new Menge<Menge<Pair>>();
-					Menge<Pair> vTmp = new Menge<Pair>();
-					vTmp.add(p);
-					setofsetofpairs.add(vTmp);
-					cartProduktSets.add(setofsetofpairs);
-    			}
-    			else if(p.OperatorSmallerExtends())
-    			{
-    				if(p.TA2 instanceof ExtendsWildcardType && ((ExtendsWildcardType)p.TA2).get_ExtendsType() instanceof RefType)
-    				{
-    					RefType p_TA2 = (RefType)((ExtendsWildcardType)p.TA2).get_ExtendsType();
-    	    			//2. Menge
-    					//Durch alle Paare p_fc laufen und schauen ob diese von der Struktur zu dem Paar p passen.
-    					Menge<Pair> fc_refl = copyMengePair(fc_tto.getFC());
-    					fc_refl.add(new Pair(p_TA2.clone(), p_TA2.clone())); //Reflexivitaet muss beruecksichtigt werden; ergaenzt PL 07-07-28
-    					                                                 //Ist aber in FC nicht enthalten.
-    					Menge<Menge<Pair>> ergMenge2 = new Menge<Menge<Pair>>(); //Ergebnismenge der 2. Menge; ergaenzt PL 07-07-28
-    					for(Pair p_fc : fc_refl)
-    	    			{
-    						RefType tmp = ((RefType)p_fc.TA2).clone();   //Unifikation vorgezogen, da isRXSimilarRY nicht ausreicht PL 07-07-29
-    						CSubstitutionSet gtv2tv = tmp.GenericTypeVar2TypePlaceholder();
-    						Menge<ObjectType> greater1elemente;
-    						if (tmp.get_ParaList() == null) 
-    						{
-    							greater1elemente = new Menge<ObjectType>(); //Bei Konstanten liefert greater1 [] zurueck
-    							greater1elemente.add(tmp);
-    						}
-    						else
-    						{
-    							greater1elemente = greater1(tmp, fc_tto);
-    						}
-    						Menge<Menge<Pair>> unifyErgs = new Menge<Menge<Pair>>();
-	    					for (Type p_TA2_gr : greater1elemente) //Unify alleine reicht nicht, da p_TA2 Wildcards vorkommen koennen
-	    					{	                                   //muessen auch alle Typen deren Args Subtypen von p_TA2 sind betrachtet werden.
-	    														 //Dies wird durch smaller1elemente bzw. smaller1 erledigt PL 07-07-29
-	    						Pair pUnify = new Pair(p_TA2.clone(),p_TA2_gr,PairOperator.Equal);
-	    						Menge<Menge<Pair>> unifyErgsElement = unifyWC(pUnify,fc_tto);
-	    						if (!unifyErgsElement.isEmpty()) {
-	    							unifyErgs.add(unifyErgsElement.firstElement());
-	    						}
-	    					}
-	    					//Nach dem Unifizieren wird das Ergebnis �berpr�ft, und evtl. durch die FC entstandene TPHs werden gel�scht.
-    	    				if((p_fc.TA2 instanceof RefType && !unifyErgs.isEmpty())
-    	    			       || p_fc.TA2.equals(p_TA2)) //Bedingung fuer Reflexifitaet BRAURHT MAN VERMUTLIRH NIRHT PL 07-08-05
-    	    			    {
-    	    					//Wenn die Unifizierung erfolgreich war durch jeden Ergebnisvektor der Unifizierung laufen.
-    	    					for(Menge<Pair> pVec : unifyErgs) //unifyErgs enthaelt nur einen Unifier STIMMT NIRHT MEHR!!!
-    	    					{
-    	    						//Das Ergebnis in die linke Seite von p_fc einsetzen, und dort Smaller anwenden.
-	    	    					Hashtable<JavaClassName,Type> ht = MengePair2SubstHashtableMengePair(pVec);
-     	    						//PL 07-07-04 smallerArg wird auf die linke Seite von p_FC nach subst angewandt  	    							    	    						
-	    	    					RefType p_fc_TA1_new = (RefType)p_fc.TA1.clone();
-	    	    					gtv2tv.applyThisSubstitutionSet(p_fc_TA1_new); //auf der linken Seite
-	    	    					//muessen die GTV durch die gleichen fresh tvs ersetzt werden, wie auf der rechten Seite. PL 07-07-29
-	    	    					p_fc_TA1_new.GenericTypeVar2TypePlaceholder();
-	    	    					//die uebrigen GTV muessen durch freshe tvs ersetzt werden.
-	    	    					SubstHashtable((RefType)p_fc_TA1_new,ht);
-	    		    					
-	    	    					//smallerArg ersetz durch folgende Zeilen. Durch Transistivitaet von fc kommen sonst
-	    	    					//doppelte Elemente rein
-	    	    					//Anfang
-	    	    					Menge<Type> smallers = new Menge<Type>();
-	    		    				Menge<ObjectType> smaller1elemente;
-	    		    				if (p_fc_TA1_new.get_ParaList() == null) 
-	    		    				{
-	    		    					smaller1elemente = new Menge<ObjectType>(); //Bei Konstanten liefert smaller1 [] zurueck
-	    		    					smaller1elemente.add(p_fc_TA1_new);
-	    		    				}
-	    		    				else
-	    		    				{
-	    		    					smaller1elemente = smaller1(p_fc_TA1_new, fc_tto);
-	    		    				} 
-	    		    					
-	    		    				for(ObjectType smele : smaller1elemente) 
-	    		    				{
-	    		    					smallers.add(smele);
-	    		    					smallers.add(new ExtendsWildcardType(smele.getOffset(), smele).clone());
-	    		    				}
-	    		    				//Ende
-	    		    					
-	    		    				//Ersatz fuer testUnifyErg PL 07-08-05
-	    		    				//Anfang
-	    		    				for(int vec = 0; vec < pVec.size(); vec++)
-	    		    				{
-	    		    					Pair pTest = pVec.elementAt(vec);
-	    		    					if(!(pTest.TA1 instanceof TypePlaceholder) || !isTVinRefType((TypePlaceholder)pTest.TA1,p_TA2))
-	    		    					{
-	    		    						pVec.remove(vec);
-	    		    						vec--;
-	    		    					}
-	    		    				}
-	    		    				//ENDE
-	    		    					
-	    	    					Menge<Menge<Pair>> cartProduktErg = new Menge<Menge<Pair>>();
-	    	    					cartProduktErg.add(pVec);
-	    		    					
-	    		    				//Mit den kleineren Typen neue Paare bilden, linke Seite Klonen.
-	    		    				Menge<Pair> smallerPairs = new Menge<Pair>();
-	    		    				for(Type sT : smallers)
-	    							{
-	    								smallerPairs.add(new Pair(p.TA1.clone(),sT,PairOperator.Equal));
-	    							}
-	    		    					
-	    		    				//Hier noch das Kartesische Produkt aus den Greater und den Smaller Ergebnissen bilden.
-	    		    				Menge<Menge<Pair>> ergs = new Menge<Menge<Pair>>();
-				    				for(Pair PsmP : smallerPairs)
-				    				{
-				    					Menge<Menge<Pair>> dolly = copyMengeMengePair(cartProduktErg);
-				    					if(dolly.isEmpty()) dolly.add(new Menge<Pair>());
-				    					for(Menge<Pair> vecp : dolly)
-				    					{
-				    						vecp.add(PsmP.clone());
-				    					}
-				    					ergs.addAll(dolly);
-				    				}
-				    				if(!ergs.isEmpty())
-				    					for (Menge<Pair> ergele : ergs)				    					
-				    						if (!ergMenge2.contains(ergele))		//ABFRAGE BRAURHT MAN VERMUTLIRH NIRHT, DA DURRH smaller1 keine doppelten Elemente reinkommen koennen		    						
-				    							ergMenge2.add(ergele);
-    	    					}
-    	    				}
-        				}
-    					cartProduktSets.add(ergMenge2);// ergaenzt PL 07-07-28
-    	    		}
-    				else if(p.TA2 instanceof SuperWildcardType)
-    				{
-    					//3. Menge
-    					//Einfach smallerArg auf die Wildcard aufrufen, mit den Ergebnissen neue Paare bilden.
-    					Menge<Type> smErg = smallerArg(p.TA2,fc_tto);
-    					cartProduktSets.add(generateSetOfSetOfPair(p.TA1,smErg));
-    				}
-    				else
-    				{
-    					//4. Menge
-    					//Den Operator des Paares auf = umbiegen und das Paar in einen Menge verpacken.
-    					Menge<Menge<Pair>> setofsetofpairs = new Menge<Menge<Pair>>();
-    					Menge<Pair> vTmp = new Menge<Pair>();
-    					p.SetOperator(PairOperator.Equal);
-    					vTmp.add(p);
-    					setofsetofpairs.add(vTmp);
-    					cartProduktSets.add(setofsetofpairs);
-    				}
-    			}
-    			else {
-    				//kein programmierter Fall konnte angewandt werden. PL 15-03-05
-    				//z.B. TPH <. ? extends Ty
-    				inferencelog.debug("UNIFY FAIL:" + p.TA1 + " <. " + p.TA2 + " Ty wurde kein Fall gefunden");
-    				return new Menge<Menge<Pair>>();
-    			}
-    		}
-    		else if (p.TA2 instanceof TypePlaceholder)
-    		{
-    			if(p.OperatorSmaller())
-    			{
-    				if (p.TA1 instanceof ObjectType) {
-    					//5. Menge
-    					//Greater auf den Typen bilden, und mit den Ergebnissen neue Paare bilden.
-    					Menge<ObjectType> grErg = greater((ObjectType)p.TA1,fc_tto);
-    					cartProduktSets.add(generateSetOfSetOfPair(p.TA2,grErg));
-    				}
-    				else if (p.TA1 instanceof ExtendsWildcardType) { // eingefuegt 15-3-11 PL
-    					Menge<ObjectType> grErg1 = greater(((ExtendsWildcardType)p.TA1).getContainedType(),fc_tto);
-    					Menge<Type> grErg2 = grErg1.stream().map(ty -> new SuperWildcardType(ty.getOffset(), ty.clone())).collect(Menge::new, Menge::add, Menge::addAll);
-    					Menge<Type> grErg = new Menge<>();
-    					grErg.addAll(grErg1);
-    					grErg.addAll(grErg2);
-    					cartProduktSets.add(generateSetOfSetOfPair(p.TA2,grErg));
-    				}
-    				else if (p.TA1 instanceof SuperWildcardType) {// eingefuegt 15-3-11 PL
-    					Menge<Type> erg = new Menge<> ();
-    					erg.addElement(p.TA1);
-    					cartProduktSets.add(generateSetOfSetOfPair(p.TA2,erg));
-    				}
-    			}
-    			else if(p.OperatorSmallerExtends())
-    			{
-    				if(p.TA1 instanceof ExtendsWildcardType)
-    				{
-    					//6. Menge
-    					//GreaterArg auf die Wildcard aufrufen, und mit den Ergebnissen neue Paare bilden.
-    					Menge<Type> grErg = greaterArg(p.TA1,fc_tto);
-    					cartProduktSets.add(generateSetOfSetOfPair(p.TA2,grErg));
-    				}
-    				else if(p.TA1 instanceof SuperWildcardType && ((SuperWildcardType)p.TA1).get_SuperType() instanceof RefType)
-    				{
-        				RefType p_TA1 = (RefType)((SuperWildcardType)p.TA1).get_SuperType();
-    	    			//7. Menge
-    					//Durch alle Paare p_fc laufen und schauen ob diese von der Struktur zu dem Paar p passen.
-    					Menge<Pair> fc_refl = copyMengePair(fc_tto.getFC());
-    					fc_refl.add(new Pair(p_TA1.clone(), p_TA1.clone())); //Reflexivitaet muss beruecksichtigt werden; ergaenzt PL 07-07-28
-    					                                                 //Ist aber in FC nicht enthalten.
-    					Menge<Menge<Pair>> ergMenge1 = new Menge<Menge<Pair>>(); //Ergebnismenge der 1. Menge;
-    	    			for(Pair p_fc : fc_refl)
-    	    			{
-    	    				RefType tmp = ((RefType)p_fc.TA2).clone();   //Unifikation vorgezogen, da isRXSimilarRY nicht ausreicht PL 07-07-29
-    						CSubstitutionSet gtv2tv = tmp.GenericTypeVar2TypePlaceholder();
-    						Menge<ObjectType> greater1elemente;
-    						if (tmp.get_ParaList() == null) 
-    						{
-    							greater1elemente = new Menge<ObjectType>(); //Bei Konstanten liefert greater1 [] zurueck
-    							greater1elemente.add(tmp);
-    						}
-    						else
-    						{
-    							greater1elemente = greater1(tmp, fc_tto);
-    						}
-    						Menge<Menge<Pair>> unifyErgs = new Menge<Menge<Pair>>();
-        					for (Type p_TA2_gr : greater1elemente) //Unify alleine reicht nicht, da p_TA2 Wildcards vorkommen koennen
-        					{	                                   //muessen auch alle Typen deren Args Subtypen von p_TA2 sind betrachtet werden.
-        														 //Dies wird durch smaller1elemente bzw. smaller1 erledigt PL 07-07-29
-        						Pair pUnify = new Pair(p_TA1.clone(),p_TA2_gr,PairOperator.Equal);
-        						Menge<Menge<Pair>> unifyErgsElement = unifyWC(pUnify,fc_tto);
-        						if (!unifyErgsElement.isEmpty()) {
-        							unifyErgs.add(unifyErgsElement.firstElement());
-        						}
-        					}
-//        					Nach dem Unifizieren wird das Ergebnis �berpr�ft, und evtl. durch die FC entstandene TPHs werden gel�scht.
-    	    				if((p_fc.TA2 instanceof RefType && !unifyErgs.isEmpty())
-    	    			       || p_fc.TA2.equals(p_TA1)) //Bedingung fuer Reflexifitaet BRAURHT MAN VERMUTLIRH NIRHT PL 07-08-05
-    	    			    {
-    	    					//Wenn die Unifizierung erfolgreich war durch jeden Ergebnisvektor der Unifizierung laufen.
-    	    					for(Menge<Pair> pVec : unifyErgs)
-    	    					{
-//    	    						Das Ergebnis in die linke Seite von p_fc einsetzen, und dort Smaller anwenden.
-        	    					Hashtable<JavaClassName,Type> ht = MengePair2SubstHashtableMengePair(pVec);
-     	    						//PL 07-07-04 smallerArg wird auf die linke Seite von p_FC nach subst angewandt  	    							    	    						
-        	    					RefType p_fc_TA1_new = (RefType)p_fc.TA1.clone();
-        	    					gtv2tv.applyThisSubstitutionSet(p_fc_TA1_new); //auf der linken Seite
-        	    					//muessen die GTV durch die gleichen fresh tvs ersetzt werden, wie auf der rechten Seite. PL 07-07-29
-        	    					p_fc_TA1_new.GenericTypeVar2TypePlaceholder();
-        	    					//die uebrigen GTV muessen durch freshe tvs ersetzt werden.
-        	    					SubstHashtable((RefType)p_fc_TA1_new,ht);
-        		    					
-        	    					//smallerArg ersetz durch folgende Zeilen. Durch Transistivitaet von fc kommen sonst
-        	    					//doppelte Elemente rein
-        	    					//Anfang
-        	    					Menge<ObjectType> smallers = new Menge<ObjectType>();
-        		    				Menge<ObjectType> smaller1elemente;
-        		    				if (p_fc_TA1_new.get_ParaList() == null) 
-        		    				{
-        		    					smaller1elemente = new Menge<ObjectType>(); //Bei Konstanten liefert smaller1 [] zurueck
-        		    					smaller1elemente.add(p_fc_TA1_new);
-        		    				}
-        		    				else
-        		    				{
-        		    					smaller1elemente = smaller0(p_fc_TA1_new, fc_tto); //Von Menge 2 kopiert und smaller1 durch smaller0 ersetzt, Luar 07-08-08
-        		    				} 
-        		    					
-        		    				for(ObjectType smele : smaller1elemente) 
-        		    				{
-        		    					smallers.add(smele);
-        		    					//smallers.add(new ExtendsWildcardType(smele.getOffset(), smele).clone()); //Auskommentiert luar 07-08-08
-        		    				}
-        		    				//Ende
-        		    				
-//        		    				Ersatz fuer testUnifyErg PL 07-08-05
-        		    				//Anfang
-        		    				for(int vec = 0; vec < pVec.size(); vec++)
-        		    				{
-        		    					Pair pTest = pVec.elementAt(vec);
-        		    					if(!(pTest.TA1 instanceof TypePlaceholder) || !isTVinRefType((TypePlaceholder)pTest.TA1,p_TA1))
-        		    					{
-        		    						pVec.remove(vec);
-        		    						vec--;
-        		    					}
-        		    				}
-        		    				//ENDE
-        		    					
-        	    					Menge<Menge<Pair>> cartProduktErg = new Menge<Menge<Pair>>();
-        	    					cartProduktErg.add(pVec);
-        		    					
-        		    				//Mit den kleineren Typen neue Paare bilden, linke Seite Klonen.
-        		    				Menge<Pair> smallerPairs = new Menge<Pair>();
-        		    				for(ObjectType sT : smallers)
-        							{
-        								smallerPairs.add(new Pair(p.TA2.clone(),new SuperWildcardType(sT.getOffset(),sT),PairOperator.Equal));
-        							}
-        		    					
-    			    				//Hier noch das Kartesische Produkt aus den Greater und den Smaller Ergebnissen bilden.
-    			    				Menge<Menge<Pair>> ergs = new Menge<Menge<Pair>>();
-    			    				for(Pair PsmP : smallerPairs)
-    			    				{
-    			    					Menge<Menge<Pair>> dolly = copyMengeMengePair(cartProduktErg);
-    			    					if(dolly.isEmpty()) dolly.add(new Menge<Pair>());
-    			    					for(Menge<Pair> vecp : dolly)
-    			    					{
-    			    						vecp.add(PsmP.clone());
-    			    					}
-    			    					ergs.addAll(dolly);
-    			    				}
-    			    				if(!ergs.isEmpty())
-    			    					for (Menge<Pair> ergele : ergs)				    					
-    			    						if (!ergMenge1.contains(ergele))		//ABFRAGE BRAURHT MAN VERMUTLIRH NIRHT, DA DURRH smaller1 keine doppelten Elemente reinkommen koennen		    						
-    			    							ergMenge1.add(ergele);
-    	    					}
-    	    			    }
-    	    			}
-    	    			cartProduktSets.add(ergMenge1);
-        			}
-    				else
-    				{
-    					//8. Menge
-    					//GreaterArg auf die Linke Seite Aufrufen, mit den Ergebnissen neue Paare erzeugen
-    					Menge<Type> grErg = greaterArg(p.TA1,fc_tto);
-    					cartProduktSets.add(generateSetOfSetOfPair(p.TA2,grErg));
-    				}
-    			}
-    			else {
-    				//kein programmierter Fall konnte angewandt werden. PL 15-03-05
-    				inferencelog.debug("UNIFY FAIL:" + p.TA1 + " <. " + p.TA2 + " Ty wurde kein Fall gefunden");
-    				return new Menge<Menge<Pair>>();
-    			}
-    		}
-    	}
-    	//Schritt 4, Teil 2: Kartesisches Produkt bilden.
-    	//TODO: Vor der Bildung des Karthesischen Produkts unm�gliche Kombinationen ausfiltern
-    	//Hier wird aus den in Schritt 4, Teil 1 erzeugten Vektoren das Kartesische Produkt gebilden.
-    	Menge<Pair> helpvp;
-    	Menge<Menge<Pair>> bigCartProductErg = new Menge<Menge<Pair>>();
-        bigCartProductErg.addElement(copyMengePair(Eq1));
-        
-        for (Menge<Menge<Pair>> vecvecpair : cartProduktSets)
-        {
-            Menge<Menge<Pair>> bigCartProductErgOld = bigCartProductErg;
-            bigCartProductErg = new Menge<Menge<Pair>>();
-            for(Menge<Pair> vecpair1 : vecvecpair)
-            {
-                for(Menge<Pair> vecpair2 : bigCartProductErgOld)
-                {
-                    helpvp = copyMengePair(vecpair2);
-                    helpvp.addAll(copyMengePair(vecpair1));
-                    bigCartProductErg.addElement(helpvp);
-                }       
-            }
-        }
-        
-        //Schritt 5: Einsetzen der Subst Regel
-        //Hier werden die TPHs substituiert, und dann nach ge�nderten und nicht ge�nderten Sets sortiert.
-        Menge<Menge<Pair>> changedSets = new Menge<Menge<Pair>>();
-        Menge<Menge<Pair>> notChangedSets = new Menge<Menge<Pair>>();
-        for(Menge<Pair> vecpair : bigCartProductErg)
-        {
-        	boolean change = false;	   //eingefuegt PL 13-05-22
-        	Pair substPair = null;
-        	do
-        	{
-        		substPair = null;
-	        	//Einsammeln der Paare von der Signatur a = Typ
-	        	for(Pair p : vecpair)
-	        	{
-	        		if(p.TA1 instanceof TypePlaceholder && p.OperatorEqual() && !p.bSubst)
-	        		{
-	        			substPair = p;
-	        			p.bSubst = true;
-	        			break;
-	        		}
-	        	}
-	        	if(substPair != null)
-	        	{
-		        	//Einsetzen der Typen in die anderen Paare
-		        	//boolean change = false;	   auskommentiert PL 13-05-22
-		        	for(int i = 0; i< vecpair.size();i++)
-		        	{
-		        		Pair p = vecpair.elementAt(i);
-		        		if(!p.instanzeEquals(substPair))
-		        		{
-		        			change |= Subst(p,1,(TypePlaceholder)substPair.TA1,substPair.TA2,true);
-		        			change |= Subst(p,2,(TypePlaceholder)substPair.TA1,substPair.TA2,true);
-		        		}
-		        	}
-		        	//Substitution abgeschlossen. Sortieren.
-		        	//if(change)  auskommentiert PL 13-05-22, da erst nach komplett erfolgter Substitution sortiert wird.
-		        	//{
-		        		//changedSets.add(vecpair);
-		        		//break;   
-		        	//}
-	        	}
-        	}
-        	while(substPair != null);
-        	
-        	if(change)  // NEU PL 13-05-22, da erst nach komplett erfolgter Substitution sortiert wird.
-        	{
-        		changedSets.add(vecpair);
-        	}
-        	else 
-        	//if(substPair == null)
-            {
-        		notChangedSets.add(vecpair);
-            }
-        }
-        
-        //Eq2Set ist das eigentliche Ergebnis, dass zur�ckgegeben wird.
-        Menge<Menge<Pair>> Eq2Set = new Menge<Menge<Pair>>();
-        
-        //Schritt 6A: Beginnen mit Schritt 1 bei den ge�nderten.
-        for(Menge<Pair> vecpair : changedSets)
-        {
-        	Menge<Menge<Pair>> unifyErgs = unify(vecpair,fc_tto);
-        	//Die Ergebnissvektoren sind schon im Schritt 7 von dem Rekursiven Aufruf gepr�ft worden. Sie k�nnen direkt eingef�gt werden.
-        	Eq2Set.addAll(unifyErgs);
-        }
-        
-        //Schritt 6B Einf�gen der nicht ge�nderten.
-        //Schritt 7: Aussortieren der falschen Sets
-        /*
-         * Durch die Rekursion in Schritt 6A sind die Ergebnisse, welche in 6A dazukommen auf jeden Fall korrekt.
-         * Es m�ssen nur die Ergebnisse aus 6B gepr�ft werden.
-         */
-        for(Menge<Pair> vecpair : notChangedSets)
-        {
-        	//�berpr�fen ob Menge in SolvedForm ist.
-        	if(hasSolvedForm(vecpair)) //PL 13-05-22 hasSolvedForm angepasst
-        	{
-        		//�berpr�fung auf FreshTypeVars in den Typen
-        		boolean foundFresh = false;
-        		for(Pair p : vecpair)
-        		{
-        			//EINSRHUB ANFANG UM PAARE A <? B in A = B zu wandeln. Nicht korrekt aber als Vereinfachung
-        			//p.SetOperator(Pair.PairOperator.Equal);//Eigentlich muesste man jetzt nochmals subst aufrufen
-        			//EINSRHUB ENDE  PL 07-08-06
-        			//13-05-22 wieder auskommentiert
-        			
-        			foundFresh |= DelFreshWildcardTypeVar(p.TA1);
-        			foundFresh |= DelFreshWildcardTypeVar(p.TA2);
-        		}
-        		
-        		if(!foundFresh)
-        			Eq2Set.add(vecpair);
-        	}
-        }
-    	
-        //Ergebnis zur�ckgeben.
-    	return Eq2Set;
-    }
-    
-    /**
-     * PL 2014-10-25
-     * schnitt1 checkt ob die Typeplaceholders aus in den Elemeneten aus vars enthalten sind
-     * R�ckgabe ist die Menge der Indizies von vars der Schnittmengen mit var nicht leer sind.
-     * @param var
-     * @param vars
-     * @param indexe
-     * @return
-     */
-    static Menge<Integer> schnitt1 (Menge<TypePlaceholder> var, Menge<Menge<TypePlaceholder>> vars, Menge<Integer> indexe) {
-        int j = -1;
-        for (Menge<TypePlaceholder> varelems : vars) {
-                j++;
-                if (varelems != null) {
-                        if (var.stream().map(x -> varelems.contains(x)).reduce(false, (a,b) -> (a || b))
-                                        && (!indexe.contains(j)))
-                        {
-                                Menge<TypePlaceholder> rekvarelements = vars.elementAt(j);
-                                vars.setElementAt(null, j);//Element erledigt muss nicht nochmals bearbeitet werden.
-                                indexe.addElement(j);
-                                indexe = schnitt1(rekvarelements, vars, indexe);
-                        }
-                }
-        }
-        return indexe;
-    }
-
-    /**
-     * Bildet Schnittmengen der Mengen von Typeplaceholders
-     * Rueckgabe ist die Menge der Menge von Indizies die Schnittmengen sind.
-     * @param vars
-     * @return
-     */
-    public static Menge<Menge<Integer>> schnitt (Menge<Menge<TypePlaceholder>> vars) {
-        Menge<Menge<Integer>> ret = new Menge<>();
-        int i = -1;
-        for (Menge<TypePlaceholder> var : vars) {
-                i++;
-                if (var != null) {//Element wurde noch bearbeitet
-                        Menge<Integer> indexe = new Menge<>();
-                        indexe.add(i);
-                        ret.add(schnitt1(var, vars, indexe));
-                }
-        }
-        return ret;
-    }  
-
-    
-    /**
-     * Diese Methode wird verwendet, um Zuordnungen z.B. TPH a = Integer
-     * aus der Ergebnismenge zu entfernen, wenn im Typ in den die eingesetzt werden sollen kein TPH a vorhanden ist.
-     * Beispiel: unifyERgs = [[a = Integer, b = Number ]], test = Menge<a>
-     * In diesm fall wird b = Number aus dem Menge entfernt.
-     * 
-     * Durch das Entfernen entstehen evtl. Identische Mengeen, diese werden auch gel�scht.
-     * 
-     * @param unifyErgs - Ergebnisse des Unify, die gepr�ft werden sollen.
-     * @param test - RefType gegen den gepr�ft werden soll.
-     */
-    private static void testUnifyErg(Menge<Menge<Pair>> unifyErgs, RefType test)
-    {
-    	for(Menge<Pair> pVec : unifyErgs)
-		for(int vec = 0; vec < pVec.size(); vec++)
-		{
-			Pair pTest = pVec.elementAt(vec);
-			if(!(pTest.TA1 instanceof TypePlaceholder) || !isTVinRefType((TypePlaceholder)pTest.TA1,test))
-			{
-				pVec.remove(vec);
-				vec--;
-			}
-		}
-    	//Gleiche Mengeen l�schen
-    	for(int i = 0; i < unifyErgs.size(); i++)
-    	{
-    		Menge<Pair> p1 = unifyErgs.elementAt(i);
-	    	for(int j = i + 1; j < unifyErgs.size(); j++)
-	    	{
-	    		Menge<Pair> p2 = unifyErgs.elementAt(j);
-	    		if(p1.size() == p2.size())
-	    		{
-	    			boolean equal = true;
-	    			for(Pair p1P : p1)
-	    			{
-	    				boolean found = false;
-	    				for(Pair p2P : p2)
-		    				found |= p2P.equals(p1P);
-	    				
-	    				equal &= found;
-	    			}
-	    			if(equal)
-	    			{
-	    				unifyErgs.remove(j);
-	    				j--;
-	    			}
-	    		}
-	    	}
-    	}
-    }
-    
-    /**
-     * Diese Methode generiert einen Menge<Menge<Pair>> wobei immer der �bergebene TA1 vorne steht, und jeder Typ aus otherPairTypes hinten.
-     * Beispiel: otherPairTypes = [Integer, Number, Menge<Integer>], TA1 = TPH a.
-     * return: [[TPH a = Integer],[TPH a = Number],[TPH a = Menge<Integer>]]
-     * 
-     * @param TA1 - Der Typ der immer vorne steht
-     * @param otherPairTypes - Die anderen Typen
-     * @return - Ein Menge<Menge<Pair>> der alle Paare enth�lt.
-     */
-    private static Menge<Menge<Pair>> generateSetOfSetOfPair(Type TA1, Menge<? extends Type> otherPairTypes)
-    {
-    	Menge<Menge<Pair>> setofsetofpairs = new Menge<Menge<Pair>>();
-		for(Type t : otherPairTypes)
-		{
-			Menge<Pair> vTmp = new Menge<Pair>();
-			vTmp.add(new Pair(TA1.clone(),t,PairOperator.Equal));
-			setofsetofpairs.add(vTmp);
-		}
-		return setofsetofpairs;
-    }
-
-    // ino.method.unify_Mub.28061.definition 
-    public static MUB unify_Mub(Type ty1, Type ty2, FC_TTO fc_tto)
-    throws CTypeReconstructionException
-    // ino.end
-    // ino.method.unify_Mub.28061.body 
-    {
-    Menge<Pair> FC = fc_tto.getFC();
-    if (ty1 instanceof TypePlaceholder) {
-        Menge<Type> Mub = new Menge<Type>();
-        Mub.addElement(ty2);
-        Menge<Pair> sigma = new Menge<Pair>();
-        sigma.addElement(new Pair(ty1, ty2));
-        return new MUB(Mub, sigma);
-    }
-    else if (ty2 instanceof TypePlaceholder) {
-        Menge<Type> Mub = new Menge<Type>();
-        Mub.addElement(ty1);
-        Menge<Pair> sigma = new Menge<Pair>();
-        sigma.addElement(new Pair(ty2, ty1));
-        return new MUB(Mub, sigma);
-    }
-    else {
-        Menge<RefType> ub = new Menge<RefType>(); //alle oberen Schranken
-        Menge<RefType> gr1 = new Menge<RefType>(); //alle Elemente groesser ty1
-        boolean refl_flag1=true;
-        
-        //alle groesseren Elemente in FC
-        for (int i=0; i < FC.size(); i++) {
-        Pair P;
-    
-        // Reflexivitaet, wenn es kein groesseres Element, aber 
-        // kleinere Elemente gibt.
-        P = isInFC((RefType)(FC.elementAt(i).TA1), (RefType)ty1, FC);
-        if (P != null) {
-            gr1.addElement(((RefType)P.TA2).clone()); //Reflexivitaet
-            refl_flag1 = false;
-        }
-    
-        //echt groessere Elemente aus FC suchen
-        P = isInFC((RefType)ty1, (RefType)(FC.elementAt(i).TA2), FC);
-        if (P != null) { 
-            gr1.addElement(((RefType)P.TA2).clone());
-            if (refl_flag1) { 
-            gr1.addElement(((RefType)P.TA1).clone()); //Reflexivitaet
-            }
-        }
-        }
-        
-        Menge<RefType> gr2 = new Menge<RefType>();
-        boolean refl_flag2=true;
-        
-        //alle groesseren Elemente in FC
-        for (int i=0; i < FC.size(); i++) {
-        Pair P;
-    
-        // Reflexivitaet, wenn es kein groesseres Element, aber 
-        // kleinere Elemente gibt.
-        P = isInFC((RefType)(FC.elementAt(i).TA1), (RefType)ty2, FC);
-        if (P != null) {
-            gr2.addElement(((RefType)P.TA2).clone()); //Reflexivitaet
-        }
-    
-        P = isInFC((RefType)ty2, (RefType)(FC.elementAt(i).TA2), FC);
-        if (P != null) { 
-            gr2.addElement(((RefType)P.TA2).clone());
-            if (refl_flag2) { 
-            gr2.addElement(((RefType)P.TA1).clone()); //Reflexivitaet
-            refl_flag1 = false;
-            }
-        }
-        }
-        if (gr1.size()==0) gr1.addElement((RefType)ty1.clone());
-        if (gr2.size()==0) gr2.addElement((RefType)ty2.clone());
-        //MIT Usecase_MUBTest4.jav testen und gr1 und gr2 ueberpruefen
-        
-        for (int i = 0; i < gr1.size(); i++) { //gemeinsame obere Schranken suchen
-            for (int j = 0; j < gr2.size(); j++){
-            if (gr1.elementAt(i).is_Equiv(gr2.elementAt(j), new Hashtable<JavaClassName,Type>())) {
-            ub.addElement(gr1.elementAt(i));
-            break;
-            }
-            }
-        }
-        
-        //Menge wird geclont, Elemente nicht
-        //Menge<RefType> Mub = (Menge<RefType>)ub.clone();
-        
-        //Elemente die nicht kleinste obere Schranken sind, werden gel�scht
-        //FUNKTIONIERT NICHT. SIEHE iftest.java PL 08-08-13
-        for (int i = 0; i < ub.size(); i++) { 
-            for (int j = 0; j < ub.size(); j++) {
-                //PL 05-03-22 alle aequivalenten Elemente sollten auch entfernt werden.
-                if (i != j && 
-                    (isInFC(ub.elementAt(j), ub.elementAt(i), FC) != null
-                     || ub.elementAt(j).equals(ub.elementAt(i)))) {
-                    ub.remove(ub.elementAt(i));
-                    
-                    //durch remove wuerde sonst ein Element 
-                    //nicht geprueft
-                    if (j > i) j--;
-                }
-            }
-        }
-        
-        //es gibt eine kleinste obere Schranke
-        if (ub.size() > 0) {
-        RefType max = ub.elementAt(0);
-        
-        //liefert die Sustitution von Genvars in Typeplaceholders, um
-        //sub dann auf die anderen Elemente von Mub anwenden zu koennen
-        CSubstitutionSet sub = max.GenericTypeVar2TypePlaceholder();
-        //PL 06-03-22 in allen Elementen von Mub muessten die gleichen Typeplaceholders stehen
-        Menge<Pair> sigma = unify(ty1, max, fc_tto).elementAt(0);
-        Menge<Pair> sigma2 = unify(ty2, max, fc_tto).elementAt(0);
-        sigma.addAll(sigma2);
-        Menge<Menge<Pair>> unifiers = unify(sigma, fc_tto);
-        
-        //es gibt keinen Unifier
-        if (unifiers.size()==0) {
-            throw new CTypeReconstructionException("Es gibt keinen Unifier",null);
-        }
-        Iterator<RefType> MubsIt = ub.iterator();
-        while(MubsIt.hasNext()){
-           sub.applyThisSubstitutionSet(MubsIt.next());
-        }
-        return new MUB(ub, unifiers.elementAt(0));
-        }
-        //es gibt keine kleinste obere Schranke
-        else {
-            throw new CTypeReconstructionException("Es existiert kein MUB",null);
-        }
-        
-    }
-    }
-    // ino.end
-    
-// ino.method.match.28064.definition 
-public static Hashtable match(RefType FCtype, RefType tomatch, Hashtable<JavaClassName, Type> ht)
-throws MatchException
-// ino.end
-// ino.method.match.28064.body 
-{ 
-    //PL 05-01-22 
-    //gibt eine Substitution zur�ck, die den Variablen aus FCtype
-    //die Typterme aus tomatch zu ordnet. Es wird davon ausgegangen, dass
-    //FCtype gegen tomatch gematcht werden kann.
-    if (FCtype.getTypeName().equals(tomatch.getTypeName())) {
-        inferencelog.debug("match: " + FCtype.getTypeName());
-        if (FCtype.get_ParaList() != null) {
-        for(int i=0; i < FCtype.get_ParaList().size(); i++) {
-            if (FCtype.get_ParaList().elementAt(i) instanceof GenericTypeVar) {
-                inferencelog.debug("PUT");
-            ht.put(((GenericTypeVar)FCtype.get_ParaList().elementAt(i)).getName(), 
-                   tomatch.get_ParaList().elementAt(i));
-            }
-            else if ((FCtype.get_ParaList().elementAt(i) instanceof RefType) &&
-                (tomatch.get_ParaList().elementAt(i) instanceof TypePlaceholder)) {
-                throw new MatchException("vorne Typterm hinten Typvariable ");
-            }
-            else if((FCtype.get_ParaList().elementAt(i) instanceof RefType) &&
-            		(tomatch.get_ParaList().elementAt(i) instanceof IMatchable) &&
-            		((IMatchable)tomatch.get_ParaList().elementAt(i)).getMatchType() instanceof RefType)
-            {
-            	match((RefType)FCtype.get_ParaList().elementAt(i), (RefType)((IMatchable)tomatch.get_ParaList().elementAt(i)).getMatchType(), ht);
-            }
-        }
-     }
-        return ht;
-    }
-    else {
-        throw new MatchException("different Name 1. " + FCtype.getTypeName()+ " 2. " +  tomatch.getTypeName());
-    }
-    }
-// ino.end
-
-	/* Einstieg in die Unifizierung mit den 4 Regeln. */
-	public static Menge<Pair> sub_unify(Menge<Pair> E, FC_TTO fc_tto)
-	{
-		return sub_unify(E,fc_tto,true);
-	}
-
-    // ino.method.sub_unify.28067.definition 
-    public static Menge<Pair> sub_unify( Menge<Pair> E, FC_TTO fc_tto, boolean useSubst )
-    // ino.end
-    // ino.method.sub_unify.28067.body 
-    {
-    //PL 05-01-21 umbenannt in sub_unify 
-    //Luar boolean useSubst hinzugef�gt, um bei bedarf zu Steuern ob Subst Regel angewendet wird oder nicht.
-        // otth: Unifikation - Versuch 1 :-)
-    
-    //Menge FC = fc_tto.getFC();
-    	Menge TTO = fc_tto.getTTO();
-        Menge<Pair> H = new Menge<Pair>(); // Hilfsmenge
-        boolean bRegel = true; // gibt an, ob eine Regel gepasst hat
-    
-        int n = 0;
-    
-        while( bRegel )
-        {
-            n++;
-    
-            // zum Debuggen
-            printMenge( "E", E, 6 );
-            bRegel = false;
-            for( int i = 0; i < E.size(); i++ )
-            {
-                Pair P = E.elementAt(i);
-                inferencelog.debug("");
-                inferencelog.debug("");                
-                inferencelog.debug("Ausgewaehltes Paar = " + P.toString() + "");
-                inferencelog.debug(  "--------------------------------------------------");
-                
-                // Bei allen Erase erfolgt keine Kopie nach H, dadurch wird das Pair gel�scht.
-                //ERASE3
-                if( P.isEqual() && P.OperatorEqual() )
-                {
-                	inferencelog.debug("  ================================");
-		            inferencelog.debug("  ERASE3");
-		            inferencelog.debug("  ================================");
-		            bRegel = true;
-		            continue;
-                }
-                // ERASE1 luar 15-04-07
-                if(P.OperatorSmaller())
-                {
-                	if (P.TA1 instanceof ObjectType) {
-                		Menge<ObjectType> greaters = greater((ObjectType)P.TA1,fc_tto);
-                		if (greaters.contains(P.TA2))
-	                	{
-	                		inferencelog.debug("  ================================");
-	                        inferencelog.debug("  ERASE1 ObjectType");
-	                        inferencelog.debug("  ================================");
-	                        bRegel = true;
-	                        continue;
-	                	}
-                	}
-                	else if (P.TA1 instanceof ExtendsWildcardType) {
-                		ObjectType pta1 = ((ExtendsWildcardType)P.TA1).getContainedType();
-                		Menge<ObjectType> greaters = greater((ObjectType)pta1,fc_tto);
-                    		if (greaters.contains(P.TA2))
-    	                	{
-    	                		inferencelog.debug("  ================================");
-    	                        inferencelog.debug("  ERASE1 ExtendsWildcardType");
-    	                        inferencelog.debug("  ================================");
-    	                        bRegel = true;
-    	                        continue;
-    	                	}
-                    	}
-                	}
-                	else if (P.TA1 instanceof SuperWildcardType) {
-                		if( P.isEqual()) {
-                			inferencelog.debug("  ================================");
-	                        inferencelog.debug("  ERASE1 SuperWildcardType");
-	                        inferencelog.debug("  ================================");
-	                        bRegel = true;
-	                        continue;
-                		}                	
-                }
-                //ERASE2 luar 15-04-07
-                if(P.OperatorSmallerExtends())
-                {
-                	Menge<Type> greaterArgs = greaterArg(P.TA1,fc_tto);
-                	if(greaterArgs.contains(P.TA2))
-                	{
-                		inferencelog.debug("  ================================");
-                        inferencelog.debug("  ERASE2");
-                        inferencelog.debug("  ================================");
-                        bRegel = true;
-                        continue;
-                	}
-                }
-                
-                //ReduceUp luar 10-04-2007
-                if(P.TA1 instanceof RefType && P.TA2 instanceof SuperWildcardType && P.OperatorSmaller())
-                {
-                	inferencelog.debug("  REDUCEUP");
-                    SuperWildcardType TA2 = ((SuperWildcardType)P.TA2);
-                    
-                    H.add(new Pair(P.TA1,TA2.get_SuperType()));
-                    bRegel = true;
-                    continue;
-                }
-                //ReduceLow luar 10-04-2007
-                if(P.TA1 instanceof ExtendsWildcardType && P.TA2 instanceof RefType && P.OperatorSmaller())
-                {
-                	inferencelog.debug("  REDUCELOW");
-                    ExtendsWildcardType TA1 = ((ExtendsWildcardType)P.TA1);
-                    
-                    H.add(new Pair(TA1.get_ExtendsType(),P.TA2));
-                    bRegel = true;
-                    continue;
-                }
-                //ReduceUpLow luar 10-04-2007
-                if(P.TA1 instanceof ExtendsWildcardType && P.TA2 instanceof SuperWildcardType && P.OperatorSmaller())
-                {
-                	inferencelog.debug("  REDUCEUPLOW");
-                    ExtendsWildcardType TA1 = ((ExtendsWildcardType)P.TA1);
-                	SuperWildcardType TA2 = ((SuperWildcardType)P.TA2);
-                	
-                	H.add(new Pair(TA1.get_ExtendsType(),TA2.get_SuperType()));
-                	bRegel = true;
-                	continue;
-                }
-    
-                //ReduceExt luar 19-04-2007
-                if((P.TA1 instanceof RefType 
-                || (P.TA1 instanceof ExtendsWildcardType && ((ExtendsWildcardType)P.TA1).get_ExtendsType() instanceof RefType)) 
-                && P.TA2 instanceof ExtendsWildcardType && P.OperatorSmallerExtends())
-                {
-                	inferencelog.debug("  REDUCEEXT");
-                	ExtendsWildcardType ExT = (ExtendsWildcardType)P.TA2;
-            		RefType TA1;
-            		if(P.TA1 instanceof RefType)
-            			TA1 = (RefType)P.TA1;
-            		else
-            			TA1 = (RefType)((ExtendsWildcardType)P.TA1).get_ExtendsType();
-            		
-                	if(ExT.get_ExtendsType() instanceof RefType)
-                	{
-                		RefType TA2 = (RefType)ExT.get_ExtendsType();
-                		if(isRealSubClass(TA1.getTypeName(),TA2.getTypeName(),fc_tto) || TA1.getTypeName().equals(TA2.getTypeName()))
-                		{
-	                		if(TA1.get_ParaList() != null && TA2.get_ParaList() != null)
-	                		{
-	                			if(TA1.get_ParaList().size() == TA2.get_ParaList().size())
-	                			{
-	                				try
-	                				{
-	                					reduceExt(H,TA1,TA2,TTO);
-	                					bRegel = true;
-	                					continue;
-	                				}
-	                				catch( SCException Ex )
-	                                {
-	                                    inferencelog.debug("---- Unifikation nicht m�glich: Permutation fehlgeschlagen!");
-	                                    break;
-	                                }
-	                			}
-	                			else
-	                			{
-	                				inferencelog.info("---- Unifikation nicht m�glich: Anzahl der Parameter verschieden!");
-	                                break;
-	                			}
-	                		}
-                		}
-                	}
-                	
-                	inferencelog.debug("  ADAPTEXT");
-                	if(ExT.get_ExtendsType() instanceof RefType)
-                	{
-                		RefType TA2 = (RefType)ExT.get_ExtendsType();
-                		Pair PFC = isInFClinks( TA1, TA2, fc_tto.getFC() );
-                		if(PFC != null)
-                		{
-                			adaptExt(H,PFC,TA1,TA2,fc_tto);
-                			bRegel = true;
-                			continue;
-                		}
-                	}
-                }
-                
-                //ReduceSup luar 19-04-2007
-                if((P.TA1 instanceof RefType 
-                || (P.TA1 instanceof SuperWildcardType && ((SuperWildcardType)P.TA1).get_SuperType() instanceof RefType))
-                && P.TA2 instanceof SuperWildcardType && P.OperatorSmallerExtends())
-                {
-                	inferencelog.debug("  REDUCESUP");
-                	SuperWildcardType SuT = (SuperWildcardType)P.TA2;
-                	RefType TA1;
-            		if(P.TA1 instanceof RefType)
-            			TA1 = (RefType)P.TA1;
-            		else
-            			TA1 = (RefType)((SuperWildcardType)P.TA1).get_SuperType();
-                	
-                	if(SuT.get_SuperType() instanceof RefType)
-                	{
-                		RefType TA2 = (RefType)SuT.get_SuperType();
-                		if(isRealSubClass(TA2.getTypeName(),TA1.getTypeName(),fc_tto) || TA1.getTypeName().equals(TA2.getTypeName()))
-                		{
-	                		if(TA1.get_ParaList() != null && TA2.get_ParaList() != null)
-	                		{
-	                			if(TA1.get_ParaList().size() == TA2.get_ParaList().size())
-	                			{
-	                				try
-	                				{
-	                					reduceSup(H,TA1,TA2,TTO);
-	                					bRegel = true;
-	                					continue;
-	                				}
-	                				catch( SCException Ex )
-	                	            {
-	                	                inferencelog.debug("---- Unifikation nicht m�glich: Permutation fehlgeschlagen!");
-	                	                break;
-	                	            }
-	                			}
-	                			else
-	                			{
-	                				inferencelog.info("---- Unifikation nicht m�glich: Anzahl der Parameter verschieden!");
-	                                break;
-	                			}
-	                		}
-                		}
-                	}
-                	
-                	inferencelog.debug("  ADAPTSUP");
-                	if(SuT.get_SuperType() instanceof RefType)
-                	{
-                		RefType TA2 = (RefType)SuT.get_SuperType();
-                		Pair PFC = isInFClinks( TA2, TA1, fc_tto.getFC() );
-                		if(PFC != null)
-                		{
-                			adaptSup(H,PFC,TA2,TA1,fc_tto);
-                			bRegel = true;
-                			continue;
-                		}
-                	}
-                }
-                //REDUCE2
-                //PL 15-01-20: HIER MUESSEN NOCH ALLE FAELLE MIT EXTENDS UND SUPER GEMISCHT ERGAENZT WERDEN
-                //BEACHTEN: WAS PASSIERT WENN HINTER ? extends/super EINE TYPVAR/KEIN REFTYPE STEHT
-                //erledigt 15-02-03
-                if(P.OperatorEqual())
-                {
-                	if((P.TA1 instanceof ExtendsWildcardType && P.TA2 instanceof ExtendsWildcardType) ||  //PL 15-03-31 eingefuegt
-                			(P.TA1 instanceof SuperWildcardType && P.TA2 instanceof SuperWildcardType))
-                	{
-                		H.add(new Pair(((WildcardType)P.TA1).GetWildcardType(), ((WildcardType)P.TA2).GetWildcardType(), PairOperator.Equal));
-                		bRegel = true;
-                		continue;
-                	}
-                	/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-                	//PL 15-03-05: Ich halte dies fuer falsch
-                	////PL 15-02-08 bisher mit keinem Beispiel getestet
-                	//if(P.TA1 instanceof WildcardType && ((WildcardType)P.TA1).GetWildcardType() instanceof TypePlaceholder 
-                		//&& (P.TA2 instanceof GenericTypeVar || P.TA2 instanceof RefType))
-                	//{
-                		//H.add(new Pair(((WildcardType)P.TA1).GetWildcardType(),P.TA2, PairOperator.Equal));
-                		//bRegel = true;
-                		//continue;
-                	//}
-                	
-                	//PL 15-02-08 bisher mit keinem Beispiel getestet 
-                	//if((P.TA1 instanceof GenericTypeVar || P.TA1 instanceof RefType) 
-                		//&& (P.TA2 instanceof WildcardType && ((WildcardType)P.TA2).GetWildcardType() instanceof TypePlaceholder)) 
-                    //{
-                    	//H.add(new Pair(P.TA1, ((WildcardType)P.TA2).GetWildcardType(), PairOperator.Equal));
-                    	//bRegel = true;
-                    	//continue;
-                    //}
-                	/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-                	
-                	//wenn noetig  extends-wildcards entfernen PL 15-02-03
-                    //korrekt da P.OperatorEqual()
-                	
-                	/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-                	//PL 15-03-05: Ich halte dies fuer falsch
-                	//if(P.TA1 instanceof WildcardType)
-                	//{
-                		//P.TA1 = ((WildcardType)P.TA1).GetWildcardType();
-                	//}
-                	//if(P.TA2 instanceof WildcardType) {
-                		//P.TA2 = ((WildcardType)P.TA2).GetWildcardType();
-                	//}
-                	/////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
-
-         
-                	RefType TA1 = null;
-                	RefType TA2 = null;
-                	//Hier werden die RefTypes gef�llt.
-                	if(P.TA1 instanceof RefType && P.TA2 instanceof RefType)
-                	{
-                		TA1 = (RefType)P.TA1;
-                		TA2 = (RefType)P.TA2;
-                	}
-                	
-	                if(TA1 != null && TA2 != null && TA1.getTypeName().equals(TA2.getTypeName()))
-	                {
-	                    inferencelog.debug("  REDUCE2");
-	                    // REDUCE
-	                    if(TA1.get_ParaList() != null && TA2.get_ParaList() != null && TA1.get_ParaList().size() == TA2.get_ParaList().size())
-	                    {
-	                        try
-	                        {
-	                           	// REDUCE-Regel anwendbar
-	                           	reduce2(H,TA1,TA2,TTO);
-	                           	bRegel = true;
-	                           	continue;
-	                        }
-	                        catch( SCException Ex )
-	                        {
-	                            inferencelog.error("---- Unifikation nicht m�glich: Permutation fehlgeschlagen!");
-	                            break;
-	                        }
-	                    }
-	                }
-                } // end if: Reduce2
-                inferencelog.debug("NACH REDUCE2");
-                
-                // REDUCE1, REDUCEEQ, ADAPT
-        //HIER MUSS BEI PAARBILDUNG NOCH bEqual AUF true GESETZT WERDEN
-        //CONTRAVARIANZ-PROBLEM OO-PROGRAMMIERUNG erlegigt PL 05-01-22
-        //BEISPIEL pl1.1.1.2.java
-                if (P.TA1 instanceof RefType && P.TA2 instanceof RefType)
-                {
-                    inferencelog.debug("  REDUCE1");
-                    RefType TA1 = ((RefType)P.TA1);
-                    RefType TA2 = ((RefType)P.TA2);
-    
-                    // REDUCE1
-                    if((isRealSubClass(TA1.getTypeName(), TA2.getTypeName(), fc_tto) || TA1.getTypeName().equals(TA2.getTypeName())) 
-                           && P.OperatorSmaller())
-                    {
-                        // REDUCE
-                        if(TA1.get_ParaList() != null && TA2.get_ParaList() != null && TA1.get_ParaList().size() == TA2.get_ParaList().size())
-                        {
-                            try
-                            {
-                            	reduce1(H,TA1,TA2,TTO);
-                            	bRegel = true;
-                            	continue;
-                            }
-                            catch( SCException Ex )
-                            {
-                                inferencelog.debug("---- Unifikation nicht m�glich: Permutation fehlgeschlagen!");
-                                break;
-                            }
-                        }
-                    } // end if: Reduce1
-                    inferencelog.debug("NACH REDUCE1");
-                    // REDUCEEQ
-                    if(TA1.getTypeName().equals(TA2.getTypeName()) && P.OperatorSmallerExtends())
-                    {
-                        inferencelog.debug("REDUCEEQ");
-                        if(TA1.get_ParaList() != null && TA2.get_ParaList() != null && TA1.get_ParaList().size() == TA2.get_ParaList().size())
-                        {
-                           	try
-                           	{
-	                           	reduceEq(H,TA1,TA2,TTO);
-	                           	bRegel = true;
-	                           	continue;
-                           	}
-                           	catch( SCException Ex )
-                            {
-                                inferencelog.error("---- Unifikation nicht m�glich: Permutation fehlgeschlagen!");
-                                break;
-                            }
-                        }
-                    } // end if: Reduce2
-                    inferencelog.debug("NACH REDUCEEQ");
-                    // ADAPT
-                    if (P.OperatorSmaller())
-            		{
-            			Pair PFC = isInFClinks( TA1, TA2, fc_tto.getFC() );
-            			inferencelog.debug("  ADAPTStart");
-                    	if( PFC != null )
-                    	{
-                    		inferencelog.debug("isInFCrechtsUnify" + PFC.toString());
-                        	adapt(H,PFC,TA1,TA2,fc_tto);
-                        	bRegel = true;
-                        	continue;
-                        
-                    	} // end if: Ende Adapt bzw. isInFC
-            		} // end if P.OperatorSmaller()
-                } // end if: RefType
-                
-                
-                // Swap
-                if( (P.TA1 instanceof RefType || P.TA1 instanceof GenericTypeVar || P.TA1 instanceof WildcardType) && P.TA2 instanceof TypePlaceholder && P.OperatorEqual())
-                                                    //PL 06-05-16 GenericTypeVar eingefuegt 
-                {
-                    H.addElement( new Pair( P.TA2, P.TA1, PairOperator.Equal ) );
-                    inferencelog.debug("  ================================");
-                    inferencelog.debug("  SWAP");
-                    inferencelog.debug("  ================================");
-                    bRegel = true;
-                    continue;
-                }
-                
-                if (P.OperatorSmallerExtends())    //PL 15-02-17 alle eingefuegt  
-                {	
-                	if(P.TA1 instanceof ExtendsWildcardType && P.TA2 instanceof ExtendsWildcardType)
-                	{                		
-                	
-                		inferencelog.debug("  Extends <? Extends");
-                    
-                		H.add(new Pair(((WildcardType)P.TA1).GetWildcardType(),((WildcardType)P.TA2).GetWildcardType(), PairOperator.Smaller));
-                		bRegel = true;
-                		continue;
-                		
-                	}
-                	
-                	if(!(P.TA1 instanceof WildcardType) && P.TA2 instanceof ExtendsWildcardType)
-                	{                		
-                	
-                		inferencelog.debug("  TA1 <? Extends");
-                    
-                		H.add(new Pair(P.TA1,((WildcardType)P.TA2).GetWildcardType(), PairOperator.Smaller));
-                		bRegel = true;
-                		continue;
-                		
-                	}
-                	
-                	if(P.TA1 instanceof SuperWildcardType && P.TA2 instanceof SuperWildcardType)
-                	{                		
-                	
-                		inferencelog.debug("  Super <? Super");
-                    
-                		H.add(new Pair(((WildcardType)P.TA2).GetWildcardType(),((WildcardType)P.TA1).GetWildcardType(), PairOperator.Smaller));
-                		bRegel = true;
-                		continue;
-                		
-                	}
-                	
-                	if(!(P.TA1 instanceof WildcardType) && P.TA2 instanceof SuperWildcardType)
-                	{                		
-                	
-                		inferencelog.debug(" TA1 <? Super");
-                    
-                		H.add(new Pair(((WildcardType)P.TA2).GetWildcardType(), P.TA1, PairOperator.Smaller));
-                		bRegel = true;
-                		continue;
-                		
-                	}
-                	
-                	if(P.TA1 instanceof ExtendsWildcardType && P.TA2 instanceof SuperWildcardType)
-                	{                		
-                	
-                		inferencelog.debug("  Extends <? Super");
-                    
-                		H.add(new Pair(((WildcardType)P.TA1).GetWildcardType(),((WildcardType)P.TA2).GetWildcardType(), PairOperator.Equal));
-                		bRegel = true;
-                		continue;
-                		
-                	}
-                	
-                	if(P.TA1 instanceof SuperWildcardType && P.TA2 instanceof ExtendsWildcardType)
-                	{                		
-                	
-                		inferencelog.debug("  Super <? Extends");
-                    
-                		H.add(new Pair(((WildcardType)P.TA1).GetWildcardType(),((WildcardType)P.TA2).GetWildcardType(), PairOperator.Equal));
-                		bRegel = true;
-                		continue;
-                		
-                	}
-                	
-                	//PL 15-02-08 angepasst 15-02-17
-                	if(P.TA1 instanceof WildcardType && !(P.TA2 instanceof WildcardType))
-                	{
-                		H.add(new Pair(((WildcardType)P.TA1).GetWildcardType(),P.TA2, PairOperator.Equal));
-                		bRegel = true;
-                		continue;
-                	}
-                	
-                }
-    
-                // Subst --> noch zu pr�fen
-                if( P.TA1 instanceof TypePlaceholder && P.OperatorEqual() && useSubst) //&& P.TA2 instanceof RefType )
-            //PL 05-02-09 P.TA@ duerfen auch TypePlaceholder sein
-            /*  BEISPIEL:
-                *******************************
-            Menge E = {
-            (A, %F%),
-            (A, %F%),
-            (C, %G%) }
-        *******************************
-        */
-                {
-                    inferencelog.debug("  SUBSTITUTE: in ");
-                    // Ersetzungen im Rest von E
-                    inferencelog.debug("  Subst?");
-                    boolean bTempSubst = P.bSubst;
-                    for( int q = i+1; q < E.size(); q++ )
-                    {
-                        if( !P.bSubst )
-                //GIBT ES PROBLEME: WIRD DAS P.bSubst ZURUECKGESETZT?????
-                        {
-                            inferencelog.debug("  ================================");
-                            inferencelog.debug("  SUBSTITUTE: in " + E.elementAt(q).toString() + " alle " + P.TA1.getName() + " durch " + P.TA2.getName());
-                            inferencelog.debug("  ================================");
-                            bRegel  = true;
-                            bTempSubst = true;
-    
-                //PL 05-02-09 Typecast vor P.TA2 entfernt, da auch TypePlaceholder
-                //eingesetzt werden duerfen
-                            Subst( E.elementAt(q), 1, (TypePlaceholder)P.TA1, P.TA2, true );
-                            Subst( E.elementAt(q), 2, (TypePlaceholder)P.TA1, P.TA2, true );
-                        }
-                    }
-                    // Ersetzungen in H
-                    for( int q = 0; q < H.size(); q++ )
-                    {
-                        if( !P.bSubst )
-                        {
-                            inferencelog.debug("  ================================");
-                            inferencelog.debug("  SUBSTITUTE: in " + H.elementAt(q).toString() + " alle " + P.TA1.getName() + " durch " + P.TA2.getName());
-                            inferencelog.debug("  ================================");
-                            bRegel  = true;
-                            bTempSubst = true;
-                            //P.bSubst = true; geloescht PL 06-04-29 darf hire nicht sein, sonst
-                            //wird P nur auf ein Paar in E bzw. H angewandt.
-    
-                            // Ursprungspaar nicht ersetzen
-                //PL 05-02-09 Typecast vor P.TA2 entfernt, da auch TypePlaceholder
-                //eingesetzt werden duerfen
-                            Subst( H.elementAt(q), 1, (TypePlaceholder)P.TA1, P.TA2, true );
-                            Subst( H.elementAt(q), 2, (TypePlaceholder)P.TA1, P.TA2, true );
-                        }
-                    }
-                    
-                    P.bSubst = bTempSubst;
-                    
-                    // falls wirklich was gemacht wurde
-                    H.addElement( E.elementAt(i) );
-                    continue;
-                }
-    
-                // keine Regel --> Element nach H kopieren!
-                H.addElement( E.elementAt(i) );
-                inferencelog.debug("\n--> keine Regel anwendbar --> umkopieren !!!!!!!!!!!!!!!!!!!!!");
-            }
-    
-            // Hilfsvektor nach E kopieren
-            // MyCompiler.printDebugInfo("---- Vektoren kopieren", 6);
-            // MyCompiler.printDebugInfo("---- E = " + E, 6);
-            // MyCompiler.printDebugInfo("---- H = " + H, 6);
-            E.removeAllElements();
-            Menge<Pair> vTemp = E;
-            E = H;
-            H = vTemp;
-        }
-        return E;
-    }
-    // ino.end
-    
-    /**
-     * Implementiert die reduce1 Regel des sub_unify
-     */
-    private static void reduce1(Menge<Pair> H, RefType TA1, RefType TA2, Menge TTO) throws SCException
-    {
-    	  inferencelog.debug("  ================================");
-          inferencelog.debug("  REDUCE1");
-          inferencelog.debug("  ================================");
-
-          Menge<Type> L1 = TA1.get_ParaList();
-          Menge<Type> L2 = TA2.get_ParaList();
-
-          inferencelog.debug("---- Parameteranzahl gleich");
-          inferencelog.debug("---- Reduce !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! (" + L1.size() + ") neue(s) Paar(e)");
-
-          inferencelog.debug("---- PAARBILDUNG ");
-          for( int k = 0; k < L1.size(); k++ )
-          {
-              Pair P2 = new Pair(L1.elementAt( pi(k, TA1.getTypeName(), TA2.getTypeName(), TTO )),L2.elementAt(k), PairOperator.SmallerExtends );
-              inferencelog.debug("---- Paar1: (" + (L1.elementAt( pi(k, TA1.getTypeName(), TA2.getTypeName(), TTO ) )).getName() + ", " + (L2.elementAt(k)).getName() + P2.OperatorEqual() + ")");
-              H.addElement(P2);
-          }
-    }
-    
-    /**
-     * Implementiert die reduceExt Regel des sub_unify
-     */
-    private static void reduceExt(Menge<Pair> H, RefType TA1, RefType TA2, Menge TTO) throws SCException
-    {
-  	  inferencelog.debug("  ================================");
-      inferencelog.debug("  REDUCEEXT");
-      inferencelog.debug("  ================================");
-
-      Menge<Type> L1 = TA1.get_ParaList();
-      Menge<Type> L2 = TA2.get_ParaList();
-      
-      inferencelog.debug("---- Parameteranzahl gleich");
-      inferencelog.debug("---- ReduceExt !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! (" + L1.size() + ") neue(s) Paar(e)");
-
-      inferencelog.debug("---- PAARBILDUNG ");
-      for( int k = 0; k < L1.size(); k++ )
-      {
-         Pair P2 = new Pair( L1.elementAt( pi(k, TA1.getTypeName(), TA2.getTypeName(), TTO )), L2.elementAt(k), PairOperator.SmallerExtends );
-         inferencelog.debug("---- Paar1: (" + (L1.elementAt( pi(k, TA1.getTypeName(), TA2.getTypeName(), TTO ) )).getName() + ", " + (L2.elementAt(k)).getName() + P2.OperatorEqual() + ")");
-         H.addElement(P2);
-          
-      }
-    }
-    
-    /**
-     * Implementiert die reduceSup Regel des sub_unify
-     */
-    private static void reduceSup(Menge<Pair> H, RefType TA1, RefType TA2, Menge TTO) throws SCException
-    {
-    	inferencelog.debug("  ================================");
-        inferencelog.debug("  REDUCEEXT");
-        inferencelog.debug("  ================================");
-
-        Menge<Type> L1 = TA1.get_ParaList();
-        Menge<Type> L2 = TA2.get_ParaList();
-        
-        inferencelog.debug("---- Parameteranzahl gleich");
-        inferencelog.debug("---- ReduceExt !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! (" + L1.size() + ") neue(s) Paar(e)");
-
-        inferencelog.debug("---- PAARBILDUNG ");
-        for( int k = 0; k < L1.size(); k++ )
-        {
-            Pair P2 = new Pair(L2.elementAt(k), L1.elementAt( pi(k, TA2.getTypeName(), TA1.getTypeName(), TTO )), PairOperator.SmallerExtends );
-            inferencelog.debug("---- Paar1: (" + (L1.elementAt( pi(k, TA2.getTypeName(), TA1.getTypeName(), TTO ) )).getName() + ", " + (L2.elementAt(k)).getName() + P2.OperatorEqual() + ")");
-            H.addElement(P2);
-        }
-    }
-    
-    /**
-     * Implementiert die reduceEq Regel des sub_unify
-     * Da in reduce2 unn�tigerweise pi verwendet wird (siehe Kommentar in reduce2), kann reduceEq einfach an reduce2 deligieren.
-     */
-    private static void reduceEq(Menge<Pair> H, RefType TA1, RefType TA2, Menge TTO) throws SCException
-    {
-    	reduce2(H,TA1,TA2,TTO);
-    }
-    
-    /**
-     * Implementiert die reduce2 Regel des sub_unify
-     */
-    private static void reduce2(Menge<Pair> H, RefType TA1, RefType TA2, Menge TTO) throws SCException
-    {
-    	inferencelog.debug("  ================================");
-        inferencelog.debug("  REDUCE2");
-        inferencelog.debug("  ================================");
-
-        Menge<Type> L1 = TA1.get_ParaList();
-        Menge<Type> L2 = TA2.get_ParaList();
-
-        inferencelog.debug("---- Parameteranzahl gleich");
-        inferencelog.debug("---- Reduce !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! (" + L1.size() + ") neue(s) Paar(e)");
-
-        // hier mu� die PERMUTATION erfolgen
-        inferencelog.debug("---- PAARBILDUNG ");
-        for( int k = 0; k < L1.size(); k++ )
-        {
-            // pi eig. bei reduce2 �berfl�ssig, schadet aber hoff. auch nicht :-)
-        	//luar 19-04-2007 durch das pi kann reduce2 auch als reduceEq verwendet werden. Wenn das pi durch k ersetzt wird, muss reduceEq entsprechend ausprogrammiert werden.
-            Pair P2 = new Pair( L1.elementAt( pi(k, TA1.getTypeName(), TA2.getTypeName(), TTO ) ), L2.elementAt(k), PairOperator.Equal );
-            inferencelog.debug("---- Paar1: (" + (L1.elementAt( pi(k, TA1.getTypeName(), TA2.getTypeName(), TTO ) )).getName() + ", " + (L2.elementAt(k)).getName() + P2.OperatorEqual() + ")");
-            H.addElement(P2);
-        }
-    }
-    
-    /**
-     * Implementiert die adapt Regel des sub_unify
-     */
-    private static void adapt(Menge<Pair> H, Pair PFC, RefType TA1, RefType TA2,FC_TTO fc_tto)
-    {
-        Hashtable<JavaClassName,Type> ht = new Hashtable<JavaClassName,Type>();
-        RefType TA1neu = (RefType)Pair.copyType((RefType)PFC.TA2);
-        inferencelog.debug("TA1neu " + TA1neu.Type2String());
-        try 
-        {
-        	match ((RefType)(PFC.TA1), TA1, ht);
-        	ht = CaptureConversionHashtable(ht,fc_tto);
-        	SubstHashtable(TA1neu, ht);
-        	inferencelog.debug("TA1neu " + TA1neu.Type2String());
-        }
-        catch (MatchException e)
-        { 
-        	inferencelog.debug("match im adapt nicht geklappt");
-        	return;
-        } 
-        H.addElement(new Pair(TA1neu, TA2, PairOperator.Smaller));
-        // Paar P ist Element von FC (von der Struktur her)
-        inferencelog.debug("  ================================");
-        inferencelog.debug("  ADAPT");
-        inferencelog.debug("  ================================");
-    }
-    
-    /**
-     * Implementiert die adaptExt Regel des sub_unify
-     */
-    private static void adaptExt(Menge<Pair> H, Pair PFC, RefType TA1, RefType TA2, FC_TTO fc_tto)
-    {
-    	Hashtable<JavaClassName,Type> ht = new Hashtable<JavaClassName,Type>();
-        RefType TA1neu = (RefType)Pair.copyType((RefType)PFC.TA2);
-        inferencelog.debug("TA1neu " + TA1neu.Type2String());
-        try 
-        {
-        	match ((RefType)(PFC.TA1), TA1, ht);
-        	ht = CaptureConversionHashtable(ht,fc_tto);
-        	SubstHashtable(TA1neu, ht);
-        	inferencelog.debug("TA1neu " + TA1neu.Type2String());
-        }
-        catch (MatchException e)
-        { 
-        	inferencelog.debug("match im adapt nicht geklappt");
-        	return;
-        } 
-        H.addElement(new Pair(TA1neu, new ExtendsWildcardType(TA2.getOffset(),TA2), PairOperator.SmallerExtends));
-        // Paar P ist Element von FC (von der Struktur her)
-        inferencelog.debug("  ================================");
-        inferencelog.debug("  ADAPTEXT");
-        inferencelog.debug("  ================================");
-    }
-    
-    /**
-     * Implementiert die adaptSup Regel des sub_unify
-     */
-    private static void adaptSup(Menge<Pair> H, Pair PFC, RefType TA1, RefType TA2, FC_TTO fc_tto)
-    {
-    	Hashtable<JavaClassName,Type> ht = new Hashtable<JavaClassName,Type>();
-        RefType TA1neu = (RefType)Pair.copyType((RefType)PFC.TA2);
-        inferencelog.debug("TA1neu " + TA1neu.Type2String());
-        try 
-        {
-        	match ((RefType)(PFC.TA1), TA1, ht);
-        	ht = CaptureConversionHashtable(ht,fc_tto);
-        	SubstHashtable(TA1neu, ht);
-        	inferencelog.debug("TA1neu " + TA1neu.Type2String());
-        }
-        catch (MatchException e)
-        { 
-        	inferencelog.debug("match im adapt nicht geklappt");
-        	return;
-        } 
-        H.addElement(new Pair(TA1neu, new ExtendsWildcardType(TA2.getOffset(),TA2), PairOperator.SmallerExtends));
-        // Paar P ist Element von FC (von der Struktur her)
-        inferencelog.debug("  ================================");
-        inferencelog.debug("  ADAPTSUP");
-        inferencelog.debug("  ================================");
-    }
-    
-    /* luar 03-05-2007
-     * Diese Methode ersetzt alle Typen in der Hashtable durch deren CaptureConversion
-     */
-    private static Hashtable<JavaClassName,Type> CaptureConversionHashtable(Hashtable<JavaClassName,Type> ht, FC_TTO fc_tto)
-    {
-    	Hashtable<JavaClassName,Type> retHT = new Hashtable<JavaClassName,Type>();
-    	for(JavaClassName s : ht.keySet())
-    	{
-    		Type t = ht.get(s);
-    		Type ccT = CaptureConversion(t,fc_tto);
-    		if(ccT != null)
-    			retHT.put(s,ccT);
-    		else
-    			retHT.put(s,t);
-    	}
-    	return retHT;
-    }
-    
-    private static Pair isInFClinks( RefType RT1, RefType RT2, Menge<Pair> FC)
-    {
-    	for(Pair p : FC)
-    	{
-    		if(p.TA1 instanceof RefType && p.TA2 instanceof RefType)
-    		{
-    			RefType TA1 = (RefType)p.TA1;
-    			RefType TA2 = (RefType)p.TA2;
-    			if(TA1.getTypeName().equals(RT1.getTypeName()) && TA2.getTypeName().equals(RT2.getTypeName()))
-    			{
-    				Pair dolly = p.clone();
-    				//((RefType)dolly.TA1).GenericTypeVar2TypePlaceholder();
-    				MyCompiler.makeGenericTypeVars2TypePlaceHolders(dolly.TA2);
-    				return dolly;
-    			}
-    		}
-    	}
-    	
-    	return null;
-    }
-    
-    
-
-    // ino.method.isRXSimilarRY.28073.defdescription type=line
-    // PL 06-03-16
-    // TypePlaceholder durch GenericTypeVar ersetzt. Das duerfte eigentlich keine      
-    // Fehler ergeben. 
-    // ino.end
-    // ino.method.isRXSimilarRY.28073.definition 
-    public static boolean isRXSimilarRY( RefType RFC, RefType RY, boolean allowTPH )
-    // ino.end
-    // ino.method.isRXSimilarRY.28073.body 
-    {
-        // otth: prueft (rekursiv) ob RFC gleiche Sturktur hat wie RY
-        // RFC: falls Typvariable als Parameterlistenelement vorkommt --> Entsprechung in RY ist egal 
-       
-        // Namen von RFC und RY muessen gleich sein
-        if( RFC.getTypeName().equals( RY.getTypeName() ) )
-        {
-            if( RFC.get_ParaList() == null && RY.get_ParaList() == null )
-            {
-                // beide Typen haben keine Parameter --> nur Typnamen muessen uebereinstimmen
-                return true;
-            }
-            
-            if( RFC.get_ParaList() != null && RY.get_ParaList() != null )
-            {
-                // beide Typen haben Parameter --> Parameterliste durchlaufen
-                Menge px = RFC.get_ParaList();
-                Menge py = RY.get_ParaList();
-                if( px.size() == py.size() )
-                {
-                    for( int i = 0; i < px.size(); i++ )
-                    {
-                        if(px.elementAt(i) instanceof GenericTypeVar || (px.elementAt(i) instanceof TypePlaceholder && allowTPH)) {
-                // Element von RFC ist Typvariable --> Entsprechung von RY kann alles sein
-                            continue;
-                        }
-    
-                        if( px.elementAt(i) instanceof RefType && py.elementAt(i) instanceof RefType )
-                        {
-                            RefType RTempX = (RefType)px.elementAt(i);
-                            RefType RTempY = (RefType)py.elementAt(i);
-                            
-                            if( RTempX.get_ParaList() == null && RTempY.get_ParaList() == null )
-                            {
-                                continue;
-                            }
-                            
-                            // zwei RefTypes --> weiter, rekursiv pruefen
-                            if( isRXSimilarRY( RTempX, RTempY,allowTPH ) )
-                            {
-                                continue;
-                            }
-                        }
-                    
-                        return false;
-                    }
-                    return true;
-                }
-            }
-        }
-    
-        return false;
-    }
-    // ino.end
-
-    // ino.method.SubstHashtable2MengePair.28076.definition 
-    public static Menge<Pair> SubstHashtable2MengePair (Hashtable<JavaClassName, Type> ht)
-    // ino.end
-    // ino.method.SubstHashtable2MengePair.28076.body 
-    {
-    //PL 05-01-23 wandelt eine Hashtable von Substitutionen
-    //PL 05-02-12 true BEI KONSTRUKTOR Pair EINGEFUEGT
-    //in ein Menge von Paaren um.
-    
-    Menge<Pair> ret = new Menge<Pair>();
-    for(Enumeration<JavaClassName> e=ht.keys();e.hasMoreElements();) {
-        String k = e.nextElement().toString();
-        // #JB# 11.04.2005
-        // ###########################################################
-        ret.addElement(new Pair(TypePlaceholder.backdoorCreate(k), (Type)ht.get(k), PairOperator.Equal));
-        //ret.addElement(new Pair(new TypePlaceholder(k), (Type)ht.get(k), true));
-        // ###########################################################
-    }
-    return ret;
-    }
-    // ino.end
-
-    // ino.method.MengePair2SubstHashtableMengePair.28079.definition 
-    public static Hashtable<JavaClassName,Type> MengePair2SubstHashtableMengePair (Menge<Pair> v)
-    // ino.end
-    // ino.method.MengePair2SubstHashtableMengePair.28079.body 
-    {
-    //PL 05-01-23 wandelt einen Menge von Paaren (a, ty) von Substitutionen
-    //in eine Hashtable um.
-    
-    Hashtable<JavaClassName,Type> ret = new Hashtable<JavaClassName,Type>();
-    for(Enumeration<Pair> e=v.elements();e.hasMoreElements();) {
-        Pair p = e.nextElement();
-        ret.put(p.TA1.getName(), p.TA2);
-    }
-    return ret;
-    }
-    // ino.end
-
-    // ino.method.copyMengePair.28082.definition 
-    public static Menge<Pair> copyMengePair (Menge<Pair> vp)
-    // ino.end
-    // ino.method.copyMengePair.28082.body 
-    {
-    //PL 05-01-23 kopiert einen Menge von Typ-Paaren
-    
-    Menge<Pair> ret = new Menge<Pair>();
-    for (int i=0; i < vp.size(); i++) {
-        ret.addElement(vp.elementAt(i).copyPair());
-    }
-    return ret;
-    }
-    // ino.end
-
-    // ino.method.copyMengeMengePair.28085.definition 
-    public static Menge<Menge<Pair>> copyMengeMengePair (Menge<Menge<Pair>> vp)
-    // ino.end
-    // ino.method.copyMengeMengePair.28085.body 
-    {
-    //PL 05-02-08 kopiert einen Menge von Mengeen von Typ-Paaren
-    
-    Menge<Menge<Pair>> ret = new Menge<Menge<Pair>>();
-    for (int i=0; i < vp.size(); i++) {
-        ret.addElement(copyMengePair(vp.elementAt(i)));
-    }
-    return ret;
-    }
-    // ino.end
-        
-
-    
-    // ino.method.instanceSmaller.28088.definition 
-    public static Menge<Menge<Pair>> instanceSmaller(Pair P, FC_TTO fc_tto )
-    // ino.end
-    // ino.method.instanceSmaller.28088.body 
-    {
-    //PL 05-01-23 bekommt als Eingabe ein Paar (a, ty') und bestimmt
-    //die Menge der Menge aller Substitutionen a \leq^* \sigma(ty), wobei
-    //\sigma = unify(ty', \ol{ty}') (ty, \ol{ty}') \in FC
-    
-    Menge<Pair> FC = fc_tto.getFC();
-    Menge<Menge<Pair>> ret = new Menge<Menge<Pair>>();
-    Menge<Pair> element;
-    
-    RefType ty = (RefType)P.TA2;
-    //Menge der \sigma(\theta) bestimmen, die in FC als linke Seite
-    //vorkommt
-    Hashtable<String,RefType> testht = new Hashtable<String,RefType>();
-    for (int i=0; i < FC.size(); i++) {
-    //      try {
-        Hashtable<JavaClassName,Type> ht = new Hashtable<JavaClassName,Type>();
-        //HIER MOEGLICHERWEISE sub_unify MIT true IN DEN PAAREN AUFRUFEN
-        //BEI INSTANZIERTEN TYPEN WEREDN KEINE SUBTYPEN GEBILDET
-        //VERGLEICHE pl1.1.1.3.jav
-        //match(ty, (RefType)(((Pair)FC.elementAt(i)).TA2), ht);
-        Menge<Pair> subunifypair = new Menge<Pair> ();
-        RefType ob = ((RefType)(FC.elementAt(i).TA2)).clone();// !!!oder Pair.copyType!!!
-        CSubstitutionSet sub = ob.GenericTypeVar2TypePlaceholder();
-        sub.applyThisSubstitutionSet(ob);
-        subunifypair.addElement(new Pair(Pair.copyType(ty), ob, PairOperator.Equal));
-        //06-04-27 PL HIER MUSS VERMUTLIRH NORH AUF DAS TA2 ein fresh angewandt werden.
-        //MEHRFACHES UNIFIZIEREN, WENN EIN TYP UND EINE INSTANZ DAVON AUCH IN FC 
-        //LIEGT
-        //erlegigt 06-04-28
-        Menge<Pair> res = sub_unify(subunifypair, fc_tto);
-        if (hasSolvedForm(res)) { //PL 13-05-22: hasSolvedForm geaendert, es nicht gekl�rt, ob es funktioniert.
-            inferencelog.debug("HasSolvedForm: ");
-            printMenge("RES_SMALLER", res, 6);
-            ht = MengePair2SubstHashtableMengePair(res);
-            //RefType tynew = (RefType)Pair.copyType(ty);
-            RefType tynew = (RefType)Pair.copyType((RefType)(FC.elementAt(i).TA1));
-            sub.applyThisSubstitutionSet(tynew);
-            //HIER MUESSEN IM SUBTYPE tynew NEU HINZUGEKOMMENE GENTYPEVARS NOCH DURCH TypePlaceholders VARS ERSETZT WERDEN
-            //pl 06-04-29
-            SubstHashtable(tynew, ht);
-            //falls Typvariablen bei Vererbung hinzugekommen sind. 
-            CSubstitutionSet sub1 = tynew.GenericTypeVar2TypePlaceholder();
-            sub1.applyThisSubstitutionSet(tynew);
-            element = SubstHashtable2MengePair(ht);
-            printMenge("ELEMENT", element, 6);
-            //Menge<RefType> smaller = new Menge<RefType> ();
-            //smaller.addElement(tynew);
-            Menge<RefType> smaller;
-    
-            //DIESER AUFRUF IS MOEGLICHERWEISE UNNOETIG, DA ALLE
-            //KLEINEREN ELEMENTE BEREITS DURCH ANDERE ELEMENTE AUS
-            //FC BESTIMMT WURDEN BZW. WERDEN.
-            smaller = allSmaller(tynew, FC);
-    
-            //wegen Reflexivitaet hinzufuegen, wenn tynew und ty aequivalent
-            //dann wird ganz am Ende hinzugefuet
-            smaller.addElement(tynew);
-    
-            for (int j = 0; j < smaller.size(); j++) {
-            Menge<Pair> newelement = copyMengePair(element);
-            if (smaller.size() >= 1) {
-                RefType testreftype = testht.put(smaller.elementAt(j).Type2Key(), smaller.elementAt(j));
-                if (testreftype == null) 
-                {
-                newelement.addElement(new Pair(P.TA1, smaller.elementAt(j), PairOperator.Equal));
-                printMenge("NEWELEMENT", newelement, 6);
-                ret.addElement(newelement);
-                }
-            }
-            }
-    //      }
-    //      catch (matchException e) {
-    //      System.out.println("matchException " + e.getMessage() + " " + ((RefType)(((Pair)FC.elementAt(i)).TA2)).Type2String());
-    //      //smaller = new Menge<RefType>();
-    //      //element = new Menge<Pair>();
-    //      }
-        }
-    }
-    Menge<Pair> equalElement = new Menge<Pair>();
-    equalElement.addElement(new Pair(P.TA1, P.TA2, PairOperator.Equal));
-    ret.addElement(equalElement);
-    printMengeUnifier("RES_SMALLERend", ret, 6);
-    return ret;
-    }
-    // ino.end
-
-    // ino.method.allSmaller.28091.definition 
-    public static Menge<RefType> allSmaller(RefType ty, Menge<Pair> FC)
-    // ino.end
-    // ino.method.allSmaller.28091.body 
-    {
-    //PL 05-01-22 bestimmt alle Typen die kleiner sind als ty
-    
-    Menge<RefType> ret = new Menge<RefType>();
-    
-    inferencelog.debug("New allSmaller " + ty.Type2String());
-    
-    //doppelte untere Typen von Paaren eleminieren
-    Hashtable<JavaClassName, RefType> hht = new Hashtable<JavaClassName, RefType>(); 
-    
-    for (int i=0; i < FC.size(); i++) {
-        if (hht.put(((RefType)(FC.elementAt(i).TA1)).getName(), (RefType)(FC.elementAt(i).TA1)) != null) { }
-        else {
-            inferencelog.debug("Getestet1: " + (new Pair((RefType)(FC.elementAt(i).TA1), ty)).toString());
-        RefType ty1 = (RefType)Pair.copyType(ty);
-        Pair P = isInFC((RefType)(FC.elementAt(i).TA1), ty1, FC);
-        // RefType FCrselem = (RefType)(((Pair)FC.elementAt(i)).TA2);
-        
-    //      //bestimmt alle Element, die ohne instance kleiner als ty ist
-    //      P = (Pair)FC.elementAt(i); //angenommenes Ergebnis, wird ggfs. geloescht
-    //      if (FCrselem.getTypeName().equals(ty.getTypeName())) {
-    //      if (FCrselem.get_ParaList() != null && ty.get_ParaList() != null) {
-    //          if (FCrselem.get_ParaList().size() == ty.get_ParaList().size()) {
-    //          for (int j = 0; j < FCrselem.get_ParaList().size(); j++) {
-    //              if (!(FCrselem.get_ParaList().elementAt(j) instanceof TypePlaceholder) 
-    //              || !(ty.get_ParaList().elementAt(j) instanceof TypePlaceholder)) {
-    //              P = null;
-    //              break;
-    //              }
-    //          }
-    //          }
-    //      }
-    //      }
-    //      else P = null;
-        inferencelog.debug("Getestet2: " + P);
-        //HIER IN isInFC SCHEINT EIN FEHLER ZU SEIN.
-        
-        if (P != null) {
-        //System.out.println("ISIN");
-        RefType smaller = (RefType)Pair.copyType(P.TA1);
-        Hashtable<JavaClassName,Type> ht = new Hashtable<JavaClassName,Type>();
-        try {
-            match((RefType)P.TA2, ty, ht);
-            //Problem koennte sein, dass ein TypePlaceholder mehrere Typterme
-            //zugeordnet werden.
-            SubstHashtable(smaller, ht);
-            ret.addElement(smaller);
-        }
-        catch (MatchException e) { } 
-        }
-    }
-    }
-    return ret;
-    }
-    // ino.end
-    // ino.method.allGreater.28094.definition 
-    public static Menge<RefType> allGreater (RefType ty, Menge<Pair> FC)
-    // ino.end
-    // ino.method.allGreater.28094.body 
-    {
-    
-    Menge<RefType> ret = new Menge<RefType>();
-    
-    
-    Hashtable<Pair,Pair> testht = new Hashtable<Pair,Pair>();
-    for (int i=0; i < FC.size(); i++) {
-            //System.out.println("Getestet1: " + (new Pair((RefType)(((Pair)FC.elementAt(i)).TA1), ty)).toString());
-        Pair P;
-        P = isInFC(ty, (RefType)(FC.elementAt(i).TA2), FC);
-        if (P != null) {
-        //Testen, ob das mit der Hashtable funktioniert.
-        Pair testreftype = testht.put(P, P);
-        if (testreftype == null) {
-            inferencelog.debug("ISIN" + ty.Type2String() + P.toString()+" "+(FC.elementAt(i)).toString());
-            RefType greater = (RefType)Pair.copyType(P.TA2);
-            Hashtable<JavaClassName,Type> ht = new Hashtable<JavaClassName,Type>();
-            try {
-            	//Hier muessen GTV durch TLV ersetzt werden.
-            	//vgl. searchAndHandleMethod in MethodCall.java
-            match((RefType)P.TA1, ty, ht);
-            //Problem koennte sein, dass ein TypePlaceholder mehrere Typterme
-            //zugeordnet werden.
-            SubstHashtableGeneric(greater, ht);
-            ret.addElement(greater);
-            }
-            catch (MatchException e) { 
-            inferencelog.error("Kein Match im allGreater");
-            }
-        }
-            }
-        }
-        return ret;
-    }
-    // ino.end
-
-    // ino.method.isInFC.28097.definition 
-    public static Pair isInFC( RefType R1, RefType R2, Menge<Pair> FC )
-    // ino.end
-    // ino.method.isInFC.28097.body 
-    {
-        // otth: Funktion, die prueft, ob Paar( R1, R2 ) in FC liegt, 
-        // bzw. deren rechten Seiten, ohne die TypePlaceholder-Variablen zu beachten
-        // z.B. Menge<A> w�re hier gleich wie Menge<Integer>
-        
-        // z.B. FC = { ( AA<a, b> <=* CC< DD<b, a> >  )  ,...}
-        // R1 = AA<Integer, b>
-        // R2 = CC< DD< Char, a> >
-    
-        // FC durchlaufen
-        RefType RFC = null; // temporaer, fuer Element von FC
-        for( int i = 0; i < FC.size(); i++ )
-        {
-            Pair P = FC.elementAt(i);
-            
-            // R1 bzw. linke Seite testen
-            if( P.TA1 instanceof RefType && P.TA2 instanceof RefType )
-            {
-                RFC = (RefType)P.TA1;
-        //System.out.println("SIMILAR1");
-                if( isRXSimilarRY( RFC, R1, false ) )
-                {
-        //System.out.println("SIMILAR2");
-                    // linke Seiten gleich --> rechte Seiten testen
-                    RFC = (RefType)P.TA2;
-                    if( isRXSimilarRY( RFC, R2, false ) )
-                    {
-                        // rechte Seiten gleich
-                        inferencelog.debug("Folgendes Paar ist Element von FC: " + P.toString() + (new Pair(R1, R2)).toString());
-                        return P;
-                    }
-                }
-            }
-            
-            // Paare sind nicht gleich --> FC weiter durchlaufen
-            
-        } // end for: FC durchlaufen
-        
-        // kein passendes Paar in FC gefunden
-        return null;
-    
-    } // end Funktino: isInFC
-    // ino.end
-
-    // ino.method.isInFCrechtsUnify.28100.definition 
-    public static Pair isInFCrechtsUnify( RefType RT1, RefType RT2, FC_TTO fc_tto )
-    // ino.end
-    // ino.method.isInFCrechtsUnify.28100.body 
-    {
-        // otth: Funktion, die prueft, ob Paar( R1, \sigma(R2) ) in FC liegt, 
-        // bzw. deren rechten Seiten, ohne die TypePlaceholders zu beachten
-        // z.B. Menge<A> w�re hier gleich wie Menge<Integer>
-        
-        // z.B. FC = { ( AA<a, b> <=* CC< DD<b, a> >  )  ,...}
-        // R1 = AA<Integer, b>
-        // R2 = CC< DD< Char, a> >
-    
-        // FC durchlaufen
-    Menge<Pair> FC = fc_tto.getFC();
-        RefType RFC = null; // temporaer, fuer Element von FC
-        for( int i = 0; i < FC.size(); i++ )
-        {
-        RefType R1 = (RefType)Pair.copyType(RT1);
-        RefType R2 = (RefType)Pair.copyType(RT2);
-            Pair P = FC.elementAt(i);
-            inferencelog.debug("getestestes Paar" + P.toString());
-            
-            // R1 bzw. linke Seite testen
-            if( P.TA1 instanceof RefType && P.TA2 instanceof RefType )
-            {
-                RFC = (RefType)P.TA1;
-                inferencelog.debug("VOR SIMILAR1" + RFC.Type2String() + " " + R1.Type2String());
-                if( isRXSimilarRY( RFC, R1, false ) )
-                {
-                    inferencelog.debug("SIMILAR1");
-                    // linke Seiten gleich --> rechte Seiten testen
-                    RFC = (RefType)P.TA2;
-            Menge<Pair> R2vec = new Menge<Pair> ();
-            inferencelog.debug("New_Pair" + (new Pair(RFC, R2, PairOperator.Smaller)).toString());
-    
-            //STIMMT DAS copyType???
-            RefType RFC_new = RFC.clone();
-            RFC_new.GenericTypeVar2TypePlaceholder();
-            R2vec.addElement(new Pair(RFC_new, R2.clone(), PairOperator.Smaller));
-    
-            printMenge("R2vec", R2vec, 6);
-            Menge<Pair> vp = sub_unify(R2vec, fc_tto);
-            
-            printMenge("VP", vp, 6);
-            if ( hasSolvedForm(vp) ) //PL 13-05-22: hasSolvedForm geaendert, es nicht gekl�rt, ob es funktioniert.
-            //if( isRXSimilarRY( RFC, R2 ) )
-                    {
-                inferencelog.debug("SIMILAR2");
-                        // rechte Seiten gleich
-                inferencelog.debug("Folgendes Paar ist Element von FC: " + P.toString());
-                        return P;
-                    }
-                }
-            }
-            
-            // Paare sind nicht gleich --> FC weiter durchlaufen
-            
-        } // end for: FC durchlaufen
-        
-        // kein passendes Paar in FC gefunden
-        return null;
-    
-    } // end Funktino: isInFC
-    // ino.end
-
-    // ino.method.isTVinRefType.28103.definition 
-    public static boolean isTVinRefType( TypePlaceholder TV, RefType RT )
-    // ino.end
-    // ino.method.isTVinRefType.28103.body 
-    {
-        // otth: Prueft ob TV in RefType vorkommt, falls ja --> true
-        
-        // Name der Typvariablen
-    	JavaClassName strTV = TV.getName();
-        
-        // Parameterliste extrahieren
-        if( RT.get_ParaList() == null )
-            // keine Parameterliste
-            return false;
-        else
-        {
-            // Parameterliste vorhanden --> durchiterieren
-            Menge P = RT.get_ParaList();
-            for( int i = 0; i < P.size(); i++ )
-            {
-                Type T = (Type)P.elementAt( i );
-                if (T instanceof ExtendsWildcardType) T = ((ExtendsWildcardType)T).get_ExtendsType();
-               
-                if( T instanceof TypePlaceholder )
-                {
-                    // T ist eine Typvariable --> gleiche Namen???
-                    if( strTV.equals(T.getName()) )
-                        return true;
-                }
-                
-                if( T instanceof RefType )
-                {
-                    // T ist wieder ein RefType --> rekursiver Aufruf
-                    if( isTVinRefType( TV, (RefType)T ) )
-                    return true;
-                }
-                       
-            }
-    
-            return false;
-        }
-    }
-    // ino.end
-
-    // ino.method.Subst.28106.defdescription type=line
-    // void Subst( Pair P, int nTypnrInPair, TypePlaceholder a, RefType o, boolean     
-    // bMitVorbedingung ) PL 05-02-10 fuer o sind auch TypePlaceholder moeglich
-    // ino.end
-    // ino.method.Subst.28106.definition 
-    public static boolean Subst( Pair P, int nTypnrInPair, TypePlaceholder a, Type o, boolean bMitVorbedingung )
-    // ino.end
-    // ino.method.Subst.28106.body 
-    {
-        // otth: Hilfsfunktion zur Unifikation
-        // otth: Ersetzen der Typvariablen a durch den RefType o
-        // otth: in dem nTypnrInPair. Type des Paares P
-        // otth: Pair uebergeben, da Zeiger nur by Value kopiert wird, s. TV
-        // otth: bMitVorbedingung: Darf die Typvariable a auf der rechten Seite auch vorkommen oder nicht?
-    
-        inferencelog.debug("SUBST: ");
-        inferencelog.debug("Pair: " + P.toString());
-        inferencelog.debug("Nummer: " + nTypnrInPair);
-        inferencelog.debug("TV: " + a.getName());
-        inferencelog.debug("Bedingung: " + bMitVorbedingung);
-    
-        // richtiger Typ aus Pair raussuchen
-        Type T = null;
-        if( nTypnrInPair == 1 )
-            T = (Type)P.TA1;
-        else
-            T = (Type)P.TA2;
-    
-        // Vorbedingung: in o darf a nicht vorkommen!!!
-    if (o instanceof RefType) {//PL 05-02-09 eingefuegt siehe Methodenkopf
-        if( bMitVorbedingung && isTVinRefType( a, (RefType)o ) )
-        {
-            inferencelog.debug("  Subst nicht m�glich, da TV " + a.getName() + " in RefType " + o.getName());
-            return false;
-        }
-    }
-    
-        // Reftypes substituieren
-        if( T instanceof RefType && ((RefType)T).get_ParaList() != null )
-        {
-            // Parameterliste durchgehen
-            Menge vTemp = ((RefType)T).get_ParaList();
-            Boolean ret = true; //EINGEFUEGT PL 14-01-16: Return darf erst am Ende zur�ckgegeben werden und nicht in den ifs 
-            					//sonst werden nicht alle Elemente der Forschleife durchlaufen
-            for( int i = 0; i < vTemp.size(); i++ )
-            {
-                Type Temp = (Type)vTemp.elementAt(i);
-                
-                // u.U. umwandeln in TypePlaceholders, auskommentiert, da umgestellt auf RefType und TypePlaceholder
-                // if( Temp instanceof RefType && ((RefType)Temp).get_ParaList() == null )
-                // Temp = new TypePlaceholder( ((RefType)Temp).getName() );
-                
-                if( Temp instanceof TypePlaceholder )
-                {
-                    
-                    if( Temp.getName().equals(a.getName()) )
-                    {
-                        // Typvariable ersetzen
-                        Menge<Type> vParaListTemp = ((RefType)T).get_ParaList();
-                        vParaListTemp.set( i, o ); // i. Element ersetzen
-                        ret &= true; //GEAENDERT PL 14-01-17
-                    }
-                }
-                if( (Temp instanceof RefType ) || (Temp instanceof ExtendsWildcardType ) || (Temp instanceof SuperWildcardType ) )
-                	//PL 2015-01-20 eingefuegt: || (Temp instanceof ExtendsWildcardType ) || (Temp instanceof SuperWildcardType )
-                {
-                    Pair PTemp = new Pair( Temp, null);
-                    inferencelog.debug(" TV!!!" + PTemp.toString() );
-                    ret &= Subst( PTemp, 1, a, o, bMitVorbedingung );   //GEAENDERT PL 14-01-17
-                }
-            }
-            return ret;  //EINGEFUEGT PL 14-01-16
-        }
-        
-        // TV substituieren
-        if( T instanceof TypePlaceholder )
-        {
-            if( T.getName().equals( a.getName() ) )
-            {
-                // TV ersetzen
-                if( nTypnrInPair == 1 )
-                    P.TA1 = o;
-                else
-                    P.TA2 = o;
-                
-                return true;
-            }
-        }
-        //Wildcard erg�nzt PL 14-12-05
-        if ( T instanceof ExtendsWildcardType )
-        {
-        	Type Temp = ((ExtendsWildcardType) T).get_ExtendsType();
-        	if( Temp instanceof TypePlaceholder )
-            {
-                
-                if( Temp.getName().equals(a.getName()) )
-                {
-                    // Typvariable ersetzen
-                	((ExtendsWildcardType) T).SetWildcardType(o);
-                    return true;
-                }
-            }
-        }
-        //Wildcard erg�nzt PL 14-12-05
-        if ( T instanceof SuperWildcardType )
-        {
-        	Type Temp = ((SuperWildcardType) T).get_SuperType();
-        	if( Temp instanceof TypePlaceholder )
-            {
-                
-                if( Temp.getName().equals(a.getName()) )
-                {
-                    // Typvariable ersetzen
-                	((SuperWildcardType) T).SetWildcardType(o);
-                    return true;
-                }
-            }
-        }
-        return false;
-    }
-    // ino.end
-    
-    // ino.method.SubstHashtableGeneric.28109.defdescription type=line
-    // SubstHashtableGeneric ersetzt in typterm alle GenericType Variablen aus ht      
-    // durch den zugeordneten Typ.
-    // ht enthaelt Elemente der (String, Type)
-    // ino.end
-    // ino.method.SubstHashtableGeneric.28109.definition 
-    public static void SubstHashtableGeneric(RefType typterm, Hashtable<JavaClassName,Type> ht)
-    // ino.end
-    // ino.method.SubstHashtableGeneric.28109.body 
-    {
-    Menge<Type> para = typterm.get_ParaList();
-    if (para != null) {
-        for (int i=0; i < para.size(); i++) {
-        if (para.elementAt(i) instanceof GenericTypeVar) {
-            if (ht.get(((GenericTypeVar)para.elementAt(i)).getName()) != null) {
-            para.set(i, ht.get(((GenericTypeVar)para.elementAt(i)).getName()));
-            }
-        }
-        else {
-            if (para.elementAt(i) instanceof RefType)
-            SubstHashtableGeneric(((RefType)para.elementAt(i)), ht);
-        }
-        }
-    }
-    }
-    // ino.end
-
-    // ino.method.SubstHashtable.28112.defdescription type=line
-    // SubstHashtable ersetzt in typterm alle TypePlaceholder-Variablen aus ht durch   
-    // den zugeordneten Typ.
-    // ht enthaelt Elemente der (String, Type)
-    // ino.end
-    // ino.method.SubstHashtable.28112.definition 
-    public static void SubstHashtable(RefType typterm, Hashtable<JavaClassName,Type> ht)
-    // ino.end
-    // ino.method.SubstHashtable.28112.body 
-    {
-    Menge<Type> para = typterm.get_ParaList();
-    if (para != null) {
-        for (int i=0; i < para.size(); i++) {
-        if (para.elementAt(i) instanceof TypePlaceholder) {
-            if (ht.get(((TypePlaceholder)para.elementAt(i)).getName()) != null) {
-            para.set(i, ht.get(((TypePlaceholder)para.elementAt(i)).getName()));
-            }
-        }
-        else {
-            if (para.elementAt(i) instanceof RefType)
-            SubstHashtable(((RefType)para.elementAt(i)), ht);
-        }
-        }
-    }
-    }
-    // ino.end
-
-
-    // ino.method.isRealSubClass.28115.definition 
-    public static boolean isRealSubClass( String Basis, String Mutter, FC_TTO fc_tto )
-    // ino.end
-    // ino.method.isRealSubClass.28115.body 
-    {
-    	
-    	
-        // otth: Funktion pr�ft, ob Klasse 'Basis' von Klasse 'Mutter' direkt oder indirekt abgeleitet ist
-    
-        // Basisklasse suchen
-    Menge tto = fc_tto.getTTO();
-        for( int i = 0; i < tto.size(); i++ )
-        {
-            //Class tempKlasse = (Class)KlassenVektor.elementAt(i);
-        Pair tempPair = (Pair)tto.elementAt(i);
-            //if( Basis.equals( tempKlasse.get_classname() ) )
-            if( Basis.equals( ((RefType)tempPair.TA1).getTypeName() ) )
-            {
-                //if( tempKlasse.get_Superclass_Name() != null )
-                {
-                    // Zusatzbedingung: otth - falls Typkonstruktoren in Superklassen auftreten --> ungueltig ??
-                    //Menge s = ((UsedId)tempKlasse.superclassid).vParaOrg;
-                    Menge<Type> s = ((RefType)tempPair.TA2).get_ParaList();
-                    
-                    // HOTI: Bugfixing: Wenn die ParaList leer ist, wird schlich ein neuer Vektor angelegt,der leer ist
-                    
-                    if(s==null){
-                        s=new Menge<Type>();
-                    }
-                    
-                    /* 
-                     * Hier wird �berpr�ft ob in der Paraliste ein anderes Element als ein GTV drinne ist.
-                     * Sollte ein anderes Element gefunden werden ist Reduce nicht m�glich.
-                     * Beispiel: Matrix <. Menge<Menge<Integer>> ist nur durch adapt m�glich.
-                     */
-                    for(Type t : s)
-                    {
-                    	if(!(t instanceof GenericTypeVar))
-                    		return false;
-                    }
-                    
-                    /*for( int l = 0; l < s.size(); l++ )
-                    {
-                        if( s.elementAt(l) instanceof RefType )
-                        {
-                            if( ((RefType)s.elementAt(l)).get_ParaList() != null )
-                            {
-                                inferencelog.debug("Superklasse enthaelt Typkonstruktoren!");
-                                return false;
-                            }
-                        }
-                    }*/
-                    
-                    //if( tempKlasse.get_Superclass_Name().equals( Mutter ) )
-                    if( ((RefType)tempPair.TA2).getTypeName().equals( Mutter ) )
-                        return true; // Basis ist von Mutter abgeleitet
-                    else
-                    {
-                        //return isRealSubClass( tempKlasse.get_Superclass_Name(), Mutter, fc_tto );
-                        return isRealSubClass( ((RefType)tempPair.TA2).getTypeName(), Mutter, fc_tto );
-                    }
-                }
-                //else
-                //{
-                //   return false;
-                //}
-            }
-        }
-        return false;
-    }
-    // ino.end
-
-// ino.method.pi.28118.defdescription type=block
-/*
-    public static void test( )
-    {
-        for( int i = 0; i < KlassenVektor.size(); i++ )
-        {
-            Class tempKlasse = (Class)KlassenVektor.elementAt(i);
-            System.out.println( "Klasse: " + tempKlasse.get_classname() );
-            System.out.println( "P. K.: " + tempKlasse.get_ParaList() );
-            if( tempKlasse.get_Superclass_Name() != null )
-            {
-                Menge s = ((UsedId)tempKlasse.superclassid).vParaOrg;
-                System.out.println( "S. Klasse: " +                             
-tempKlasse.get_Superclass_Name() );                 System.out.println( "P. S.: 
-" + tempKlasse.get_ParaList() );
-            }        
-        }
-    }
-*/
-// ino.end
-
-    /* Alte pi-Methode:
-<<<<<<< HEAD
-    // ino.method.pi.28118.definition 
-    public static int pi( int n, String C, String D, Menge tto )
-    throws SCException
-    // ino.end
-    // ino.method.pi.28118.body 
-    {
-        // otth: Permutation, benoetigt fuer Unifikation
-        // C, D: Namen von Klassen
-        // z.B. class C<A, B> --- class D<B, A>
-        //                             pi(1) = 2
-    
-        // MyCompiler.printDebugInfo("---------------- Permutation: n = " + String.valueOf(n) + " - C = " + C + " - D = " + D, 6);
-        
-        // Klassen suchen
-        //Class KlasseC    = null;
-        //Class KlasseD    = null;
-        //Class tempKlasse = null;
-        // for( int i = 0; i < KlassenVektor.size(); i++ )
-    //         {
-    //             // MyCompiler.printDebugInfo("---------------- Permutation: i = " + String.valueOf(i) + " - Classname = " + ((Class)KlassenVektor.elementAt(i)).get_classname(), 6);
-            
-    //             if( KlasseC != null && KlasseD != null )
-    //                 break;
-            
-    //             tempKlasse = (Class)KlassenVektor.elementAt(i);
-    //             if( C.equals( tempKlasse.get_classname() ) )
-    //             {
-    //                 KlasseC = tempKlasse;
-    //                 // MyCompiler.printDebugInfo("---------------- Permutation: C-Klasse gefunden!", 6);
-    //             }
-    
-    //             if( D.equals( tempKlasse.get_classname() ) )
-    //             {
-    //                 KlasseD = tempKlasse;
-    //                 // MyCompiler.printDebugInfo("---------------- Permutation: D-Klasse gefunden!", 6);                
-    //             }
-    //         }
-    
-    if (C.equals(D)) return n;  //Reduktion mit gleichen Typkonstruktoren
-    
-    else {
-        RefType KlasseC    = null;
-        RefType KlasseD    = null;
-        //RefType tempKlasse = null;
-    
-        for( int i = 0; i < tto.size(); i++ ) {
-        
-        KlasseC = (RefType)((Pair)tto.elementAt(i)).TA1;
-        KlasseD = (RefType)((Pair)tto.elementAt(i)).TA2;
-    
-        if (KlasseC.getTypeName().equals(C) && KlasseD.getTypeName().equals(D)) {
-            break;
-        }
-        else {
-            KlasseC = null;
-            KlasseD = null;
-        }
-    
-        }
-    
-        SCException F = new SCException();
-        if( KlasseC == null && KlasseD == null )
-        throw F; // Fehler
-    
-        // Vektorlisten extrahieren
-        Menge vC = KlasseC.get_ParaList();
-        Menge vD = KlasseD.get_ParaList();
-        
-        if( vC == null || vD == null )
-        throw F;
-    
-        if( n >= vD.size() )
-        throw F;
-    
-        // Permuationswert f�r 'n' berechnen
-        Type TV = (Type)vD.elementAt(n);
-        
-        int nPos = -1;
-    
-        // MyCompiler.printDebugInfo("---------------- Permutation: vC.size() = " + String.valueOf( vC.size() ), 6);
-    
-        for( int i = 0; i < vC.size(); i++ )
-        {
-            // MyCompiler.printDebugInfo("---------------- Permutation: TV = " + ((Type)vC.elementAt(i)).getName_(), 6);
-            if( ((Type)vC.elementAt(i)).getName().equals( TV.getName() ) )
-            {
-                nPos = i;
-                break;
-            }
-        }
-        
-        if (nPos == -1)
-        throw F;
-    
-        // MyCompiler.printDebugInfo("---------------- Permutation: = " + String.valueOf( nPos ), 6);
-            
-        return nPos;
-    }
-    }
-=======
-*/
-	// ino.method.pi.28118.definition
-	public static int pi(int n, String C, String D, Menge tto)
-			throws SCException {
-
-		if (C.equals(D))
-			return n; // Reduktion mit gleichen Typkonstruktoren
-		
-		RefType KlasseC = null;
-		RefType KlasseD = null;
-
-		for (int i = 0; i < tto.size(); i++) {
-
-			KlasseC = (RefType) ((Pair) tto.elementAt(i)).TA1;
-			KlasseD = (RefType) ((Pair) tto.elementAt(i)).TA2;
-
-			if (KlasseC.getTypeName().equals(C)
-					&& KlasseD.getTypeName().equals(D))
-				break;
-			else {
-				KlasseC = null;
-				KlasseD = null;
-			}
-		}
-
-		SCException F = new SCException();
-		if (KlasseC == null && KlasseD == null)
-			throw F; // Fehler
-
-		// Vektorlisten extrahieren
-		Menge vC = KlasseC.get_ParaList();
-		Menge vD = KlasseD.get_ParaList();
-
-		if (vC == null || vD == null)
-			throw F;
-
-		if (n >= vD.size())
-			throw F;
-
-		// Permuationswert f�r 'n' berechnen
-		Type TV = (Type) vD.elementAt(n);
-		int nPos = -1;
-		for (int i = 0; i < vC.size(); i++)
-			if (((Type) vC.elementAt(i)).getName().equals(TV.getName())) {
-				nPos = i;
-				break;
-			}
-
-		return nPos;
-
-	}
+package de.dhbwstuttgart.typeinference.unify;
+
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collection;
+import java.util.HashSet;
+import java.util.LinkedHashSet;
+import java.util.LinkedList;
+import java.util.List;
+import java.util.Map.Entry;
+import java.util.Optional;
+import java.util.Set;
+import java.util.stream.Collectors;
+
+import de.dhbwstuttgart.typeinference.Menge;
+import de.dhbwstuttgart.typeinference.Pair;
+import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException;
+import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
+import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
+import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations;
+import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
+import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
+import de.dhbwstuttgart.typeinference.unify.model.MPair;
+import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
+import de.dhbwstuttgart.typeinference.unify.model.SuperType;
+import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
+import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
+import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
+import de.dhbwstuttgart.typeinference.unify.model.Unifier;
+
+
+/**
+ * Implementation of the type unification algorithm
+ * @author Florian Steurer
+ */
+public class Unify {
+	
+	public Set<Set<MPair>> unify(Set<MPair> eq, IFiniteClosure fc) {		
+		/*
+		 * Step 1: Repeated application of reduce, adapt, erase, swap 
+		 */
+		
+		Set<MPair> eq0 = applyTypeUnificationRules(eq, fc);
+		
+		/*
+		 * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs
+		 */
+		
+		Set<MPair> eq1s = new HashSet<>();
+		Set<MPair> eq2s = new HashSet<>();
+		splitEq(eq0, eq1s, eq2s);
+		
+		/*
+		 * Step 4: Create possible typings
+		 * 
+		 * "Manche Autoren identifizieren die Paare (a, (b,c)) und ((a,b),c) 
+		 * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia
+		 */
+		
+		// There are up to 10 toplevel set. 8 of 10 are the result of the 
+		// cartesian product of the sets created by pattern matching.
+		List<Set<Set<MPair>>> topLevelSets = new ArrayList<>();
+		
+		if(eq1s.size() != 0) {
+			Set<Set<MPair>> wrap = new HashSet<>();
+			wrap.add(eq1s);
+			topLevelSets.add(wrap); // Add Eq1'
+		}
+
+		// Add the set of [a =. Theta | (a=. Theta) in Eq2']
+		Set<MPair> bufferSet = eq2s.stream()
+				.filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType)
+				.collect(Collectors.toSet());
+		
+		if(bufferSet.size() != 0) {
+			Set<Set<MPair>> wrap = new HashSet<>();
+			wrap.add(bufferSet);
+			topLevelSets.add(wrap);
+		}
+		
+		// Sets that originate from pair pattern matching
+		// Sets of the "second level"
+		Set<Set<Set<MPair>>> secondLevelSets = calculatePairSets(eq2s, fc);
+		
+		/* Up to here, no cartesian products are calculated.
+		 * filters for pairs and sets can be applied here */
+		
+		ISetOperations setOps = new GuavaSetOperations();
+		
+		// Sub cartesian products of the second level (pattern matched) sets
+		for(Set<Set<MPair>> secondLevelSet : secondLevelSets) {
+			List<Set<MPair>> secondLevelSetList = new ArrayList<>(secondLevelSet);
+			topLevelSets.add(setOps.cartesianProduct(secondLevelSetList)
+					.stream().map(x -> new HashSet<>(x))
+					.collect(Collectors.toCollection(HashSet::new)));
+		}
+		
+		// Cartesian product over all (up to 10) top level sets 
+		Set<Set<Set<MPair>>> eqPrimeSet = setOps.cartesianProduct(topLevelSets)
+				.stream().map(x -> new HashSet<>(x))
+				.collect(Collectors.toCollection(HashSet::new));
+		//System.out.println(result);
+
+		/*
+		 * Step 5: Substitution
+		 */
+		
+		/*
+		 * TODO hier das ergebnis schonh flach machen? (wird im unify old (glaub ich) so gemacht)
+		 */
+		Set<Set<MPair>> eqPrimeSetFlat = new HashSet<>();
+		for(Set<Set<MPair>> setToFlatten : eqPrimeSet) {
+			Set<MPair> buffer = new HashSet<>();
+			setToFlatten.stream().forEach(x -> buffer.addAll(x));
+			eqPrimeSetFlat.add(buffer);
+		}
+		
+		IRuleSet rules = new RuleSet(fc);
+		Set<Set<MPair>> changed = new HashSet<>();
+		Set<Set<MPair>> eqPrimePrimeSet = new HashSet<>();
+		
+		for(Set<MPair> eqPrime : eqPrimeSetFlat) {
+			Optional<Set<MPair>> eqPrimePrime = rules.subst(eqPrime);
+			
+			if(eqPrimePrime.isPresent())
+				changed.add(eqPrimePrime.get());
+			else
+				eqPrimePrimeSet.add(eqPrime);
+		}
+
+		/*
+		 * Step 6 a) Restart for pairs where subst was applied
+		 * 		  b) Build the union over everything
+		 */
+		
+		for(Set<MPair> eqss : changed) {
+			eqPrimePrimeSet.addAll(this.unify(eqss, fc));
+		}
+		
+		 /*
+		  * Step 7: Filter result for solved pairs
+		  */
+		return eqPrimePrimeSet;
+		
+	}
+	
+	protected Set<MPair> applyTypeUnificationRules(Set<MPair> eq, IFiniteClosure fc) {
+		
+		/*
+		 * Rule Application Strategy:
+		 * 
+		 * 1. 	Swap all pairs and erase all erasable pairs
+		 * 2. 	Apply all possible rules to a single pair, then move it to the result set.
+		 *    	Iterating over pairs first, then iterating over rules prevents the application
+		 *    	of rules to a "finished" pair over and over.
+		 * 2.1 	Apply all rules repeatedly except for erase rules. If
+		 * 		the application of a rule creates new pairs, check immediately
+		 * 		against the erase rules.
+		 */
+		
+		
+		LinkedHashSet<MPair> targetSet = new LinkedHashSet<MPair>();
+		LinkedList<MPair> eqQueue = new LinkedList<>();
+		IRuleSet rules = new RuleSet(fc);
+		
+		/*
+		 * Swap all pairs and erase all erasable pairs
+		 */
+		eq.forEach(x -> swapAddOrErase(x, rules, eqQueue));
+		
+		/*
+		 * Apply rules until the queue is empty
+		 */
+		while(!eqQueue.isEmpty()) {
+			MPair pair = eqQueue.pollFirst();
+
+			// ReduceUp, ReduceLow, ReduceUpLow
+			Optional<MPair> opt = rules.reduceUpLow(pair);
+			opt = opt.isPresent() ? opt : rules.reduceLow(pair);
+			opt = opt.isPresent() ? opt : rules.reduceUp(pair);
+			
+			// One of the rules has been applied
+			if(opt.isPresent()) {
+				swapAddOrErase(opt.get(), rules, eqQueue);
+				continue;
+			}
+			
+			// Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq
+			Optional<Set<MPair>> optSet = rules.reduce1(pair);
+			optSet = optSet.isPresent() ? optSet : rules.reduce2(pair);
+			optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair);
+			optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair);
+			optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair);
+			
+			// One of the rules has been applied
+			if(optSet.isPresent()) {
+				optSet.get().forEach(x -> swapAddOrErase(x, rules, eqQueue));
+				continue;
+			}
+			
+			// Adapt, AdaptExt, AdaptSup
+			opt = rules.adapt(pair);
+			opt = opt.isPresent() ? opt : rules.adaptExt(pair);
+			opt = opt.isPresent() ? opt : rules.adaptSup(pair);
+			
+			// One of the rules has been applied
+			if(opt.isPresent()) {
+				swapAddOrErase(opt.get(), rules, eqQueue);
+				continue;
+			}
+			
+			// None of the rules has been applied
+			targetSet.add(pair);
+		}
+		
+		return targetSet;
+	}
+	
+	protected void swapAddOrErase(MPair pair, IRuleSet rules, Collection<MPair> collection) {
+		Optional<MPair> opt = rules.swap(pair);
+		MPair pair2 = opt.isPresent() ? opt.get() : pair;
+		
+		if(rules.erase1(pair2) || rules.erase3(pair2) || rules.erase2(pair2))
+			return;
+		
+		collection.add(pair2);
+	}
+	
+	protected void splitEq(Set<MPair> eq, Set<MPair> eq1s, Set<MPair> eq2s) {
+		for(MPair pair : eq) 
+			if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType)
+				eq1s.add(pair);
+			else
+				eq2s.add(pair);
+	}
+	
+	
+	protected Set<Set<Set<MPair>>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) {
+		List<Set<Set<MPair>>> result = new ArrayList<>();
+		
+		// Init all 8 cases
+		for(int i = 0; i < 8; i++)
+			result.add(new HashSet<>());
+		
+		for(MPair pair : eq2s) {
+			
+			PairOperator pairOp = pair.getPairOp();
+			UnifyType lhsType = pair.getLhsType();
+			UnifyType rhsType = pair.getRhsType();
+	
+			// Case 1: (a <. Theta')
+			if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType)
+				result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc));
+			
+			// Case 2: (a <.? ? ext Theta')
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
+				result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
+			
+			// Case 3: (a <.? ? sup Theta')
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
+				result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc));
+			
+			// Case 4: (a <.? Theta')
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType)
+				result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc));
+				
+			// Case 5: (Theta <. a)
+			else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType)
+				result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc));
+			
+			// Case 6: (? ext Theta <.? a)
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType)
+				result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc));
+
+			// Case 7: (? sup Theta <.? a)
+			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType)
+				result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc));
+			
+			// Case 8: (Theta <.? a)
+			else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
+				result.get(7).add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc));
+		}
+		
+		return result.stream().filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new));
+	}
+	
+	protected Set<MPair> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		IUnify unify = new MartelliMontanariUnify();
+		
+		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
+		
+		for(UnifyType c : cs) {
+			
+			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
+			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
+			thetaQs.add(c); // reflexive
+			
+			Set<UnifyType> thetaQPrimes = new HashSet<>();
+			TypeParams cParams = c.getTypeParams();
+			if(cParams.size() == 0)
+				thetaQPrimes.add(c);
+			else {
+				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
+				for(UnifyType param : cParams)
+					candidateParams.add(fc.grArg(param));
+			
+				for(TypeParams tp : permuteParams(candidateParams))
+					thetaQPrimes.add(c.setTypeParams(tp));
+			}
+			
+			for(UnifyType tqp : thetaQPrimes) {
+				Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
+				if (!opt.isPresent())
+					continue;
+				
+				Unifier unifier = opt.get();
+				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
+				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
+					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
+				for (UnifyType tq : thetaQs) {
+					Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
+					smaller.stream().map(x -> new MPair(a, x, PairOperator.EQUALSDOT))
+							.forEach(x -> result.add(x));
+				}
+
+			}
+		}
+		
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		IUnify unify = new MartelliMontanariUnify();
+		
+		UnifyType thetaPrime = extThetaPrime.getExtendedType();
+		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
+		
+		for(UnifyType c : cs) {
+			
+			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
+			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
+			thetaQs.add(c); // reflexive
+			
+			Set<UnifyType> thetaQPrimes = new HashSet<>();
+			TypeParams cParams = c.getTypeParams();
+			if(cParams.size() == 0)
+				thetaQPrimes.add(c);
+			else {
+				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
+				for(UnifyType param : cParams)
+					candidateParams.add(fc.grArg(param));
+			
+				for(TypeParams tp : permuteParams(candidateParams))
+					thetaQPrimes.add(c.setTypeParams(tp));
+			}
+			
+			for(UnifyType tqp : thetaQPrimes) {
+				Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
+				if (!opt.isPresent())
+					continue;
+				
+				Unifier unifier = opt.get();
+				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
+				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
+					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
+				for (UnifyType tq : thetaQs) {
+					ExtendsType extTq = new ExtendsType(tq);
+					Set<UnifyType> smaller = fc.smaller(unifier.apply(extTq));
+					smaller.stream().map(x -> new MPair(a, x, PairOperator.EQUALSDOT))
+							.forEach(x -> result.add(x));
+				}
+			}
+		}
+		
+		return result;
+	}
 	
-    // ino.end
-    // ino.method.printMengeUnifier.28121.definition 
-    public static void printMengeUnifier(String strMenge, Menge<Menge<Pair>> Uni, int nDebug )
-    // ino.end
-    // ino.method.printMengeUnifier.28121.body 
-    {
-    //PL 05-01-21
-    //Ruft f�r eine Menge von Unifikatoren die Methode
-    //printMenge auf
-    for (int i = 0; i < Uni.size(); i++) {
-        inferencelog.debug((i+1) + ". Unifier");
-        printMenge(strMenge, Uni.elementAt(i), nDebug);
-        if( hasSolvedForm( Uni.elementAt(i) ) ) { //PL 13-05-22: hasSolvedForm geaendert, es nicht gekl�rt, ob es funktioniert.
-            inferencelog.debug((i+1) + ". Unifier ist in 'Solved form'!\n");
-        }
-        else {
-            inferencelog.debug((i+1) + ". Unifier ist nicht in 'Solved Form'\n");
-        }
-    
-    }
-    }
-    // ino.end
-
-    // ino.method.printMenge.28124.definition 
-    public static void printMenge( String strMenge, Menge<Pair> E, int nDebug )
-    // ino.end
-    // ino.method.printMenge.28124.body 
-    {
-        // otth - zum Debuggen: Menge ausgeben ***********************
-        String strTemp = "";
-        if( E.size() == 0 )
-        {
-            inferencelog.debug("*******************************");
-            inferencelog.debug("Menge " + strMenge + " ist leer!");
-            inferencelog.debug("*******************************");
-            return;
-        }
-    
-        for( int tt = 0; tt < E.size(); tt++ ) {
-        	//luar 13-03-07 If Else Block gel�scht, da sinnlos.
-        	if( tt > 0 )
-        		strTemp = strTemp + ",\n" + E.elementAt(tt).toString();
-            else
-                strTemp = E.elementAt(tt).toString();
-            strTemp = strTemp + (E.elementAt(tt).GetOperator());
-        }
-        inferencelog.debug("*******************************");
-        inferencelog.debug("Menge " + strMenge + " = {" + strTemp + " }");
-        inferencelog.debug("*******************************");
-    }
-    // ino.end
-
-    // ino.method.hasSolvedForm.28127.definition 
-    public static boolean hasSolvedForm( Menge<Pair> E )
-    // ino.end
-    // ino.method.hasSolvedForm.28127.body 
-    {
-        // otth: prueft, ob Menge E in 'Solved form'
-    
-        // TV im Vektor speichern
-        Menge<TypePlaceholder> vTV = new Menge<TypePlaceholder>();
-        for(Pair P : E)
-        {
-            // linke Seite == TypePlaceholder
-            if( !(P.TA1 instanceof TypePlaceholder) )
-            {
-                return false;
-            }
-            else
-            {
-                vTV.add( (TypePlaceholder)P.TA1 ); //wird benoetigt um spaeter zu pruefen, 
-                                                   //ob tlv auf der rechten Seite steht
-            }
-        }
-    
-        for(Pair P : E)
-        {
-            //for( int u = 0; u < vTV.size(); u++ )// geloescht PL 13-05-22
-            {
-              	if (P.TA2 instanceof RefType) 
-              	{ //eingefuegt PL 05-01-30 s.o.
-                    //if( isTVinRefType(vTV.elementAt(u), (RefType)P.TA2 ) )
-              		if (isTVinRefType((TypePlaceholder)P.TA1, (RefType)P.TA2 ))
-                       	return false;
-               	}
-            }
-        }
-        return true;
-    }
-    // ino.end
-    
-    // ino.method.varSubst.28130.defdescription type=line
-    // varSubst ersetzt all TypePlaceholders eines Typterms.
-    // Wenn eine Variable zum ersten Mal auftritt, wird eine freshe generiert 
-    // und diese in ht gespeichert.
-    // Wenn eine Variable auftaucht, die bereits schon einmal ersetzt wurde, wird
-    // sie durch die selbe Variable ersetzt.
-    // ino.end
-    // ino.method.varSubst.28130.definition 
-    public static void varSubst(RefType typterm, Hashtable<JavaClassName,Type> ht)
-    // ino.end
-    // ino.method.varSubst.28130.body 
-    {
-        Menge<Type> para = typterm.get_ParaList();
-        if (para != null) {
-            for (int i=0; i < para.size(); i++) {
-                if (para.elementAt(i) instanceof TypePlaceholder) {
-                    if (ht.get(((TypePlaceholder)para.elementAt(i)).getName()) != null) {
-                    para.set(i, ht.get(((TypePlaceholder)para.elementAt(i)).getName()));
-                    }
-                    else {
-                    // #JB# 11.04.2005
-                    // ###########################################################
-                    ht.put(((TypePlaceholder)para.elementAt(i)).getName(), TypePlaceholder.backdoorFresh());
-                    //ht.put(((TypePlaceholder)para.elementAt(i)).getName(), TypePlaceholder.fresh());
-                    // ###########################################################
-                    para.set(i, ht.get(((TypePlaceholder)para.elementAt(i)).getName()));
-     
-                    }
-                }
-                else {
-                    if (para.elementAt(i) instanceof RefType)
-                    varSubst(((RefType)para.elementAt(i)), ht);
-                }
-            }
-        }
-    }
-    // ino.end
-    
-    
-    /**
-     * Implementiert die CaptureConversion. Wendet diese auf jeden Typ im Menge TVec an.
-     * R�ckgabe ist ein ErgebnisMenge
-     */
-    private static Menge<ObjectType> CaptureConversion(Menge<ObjectType> TVec, FC_TTO fc_tto)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	for(ObjectType t : TVec)
-    	{
-    		ObjectType ccT = (ObjectType)CaptureConversion(t,fc_tto);
-    						//CaptureConversion kann nur ObjectTypes zur�ckliefern, laesst sich aber nicht zurziehen.
-    		if(ccT != null)
-    			retVec.add(ccT);
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * Erzeugt die CaptureConversion von einem Typ.
-     * 
-     * @param T - �bergebener Typ, von welchem die CaptureConversion gemacht werden soll.
-     * @param fc_tto - Hilfsklasse.
-     * @return - CC(T)
-     */
-    private static Type CaptureConversion(Type T, FC_TTO fc_tto)
-    {
-    	if(T instanceof RefType)
-    	{
-    		//Klasse aus Klassenvektor holen.
-    		Class cl = null;
-    		for(Class c : fc_tto.getClasses())
-    		{
-    			if(c.getSimpleName().equals(T.getName()))
-    			{
-    				cl = c;
-    				break;
-    			}
-    		}
-    		if(cl == null) //Keine Klasse gefunden?
-    			return null;
-    		
-    		Menge<Type> ccTypes = new Menge<Type>();
-    		RefType refT = (RefType)T.clone();
-    		boolean ccDone = false;
-    		if(refT.get_ParaList() != null)
-    		{
-    			Menge<Type> paras = refT.get_ParaList();
-    			//Durch jeden Typ in der Paralist des RefTypes laufen.
-    			for(int i = 0; i<paras.size();i++)
-    			{
-    				Type t = paras.get(i);
-    				//Wenn der Typ ein WildcardTyp ist
-    				if(t instanceof WildcardType)
-    				{
-    					FreshWildcardType fwcT = ((WildcardType)t).GetFreshWildcardType();
-    					//Wenn beim Original Typ an der Stelle eine BoundedGenericTypeVar ist werden die Bounds zu der Wildcard hinzugef�gt.
-    					if(cl.get_ParaList().elementAt(i) instanceof BoundedGenericTypeVar)
-    					{
-    						BoundedGenericTypeVar bgv = (BoundedGenericTypeVar)cl.get_ParaList().elementAt(i);
-    						fwcT.set_UpperBounds(copyMengeType(bgv.getBounds()));
-    					}
-    					ccTypes.add(fwcT);
-    					ccDone = true;
-    				}
-    				else
-    					ccTypes.add(t);
-    			}
-    			refT.set_ParaList(ccTypes);
-    		}
-    		//Wenn eine CaptureConversion durchgef�hrt wurde den Typ zur�ckgeben.
-    		if(ccDone)
-    			return refT;
-    		else
-    			return null;
-    	}
-    	
-    	if(T instanceof WildcardType)
-    	{
-    		return ((WildcardType)T).GetFreshWildcardType();
-    	}
-    	return null;
-}
-    	
-    
-    //Von hier an Greater implementierung 28-03-07
-    /**
-     * Der Komplette Ablauf von greater und was die einzelnen Teilschritte machen kann anhand von Aktivit�tsdiagrammen
-     * im Inovator Projekt, oder in der Studienarbeit Arne L�dtke, 2007 nachgelesen werden.
-     */
-    
-    /**
-     * Erzeugt alle Typen die greater sind als T. Gibt diese zur�ck.
-     * F�r den Argumenttype FunN<...> in Typ A<FunN<...> ...> werden keine ? extends-, ? super-Typen erzeugt
-     */
-    private static Menge<ObjectType> greater(ObjectType T, FC_TTO fc_tto)
-    //an die Aenderungen im Skript anpassen 07-11-03
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	Menge<ObjectType> greater0Erg = greater0(T,fc_tto);
-    	for(ObjectType t : greater0Erg)
-    	{
-    		if(!DelFreshWildcardTypeVar(t))
-    			retVec.add(t);
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * greater0 Schritt von greater.
-     */
-    private static Menge<ObjectType> greater0(ObjectType T, FC_TTO fc_tto)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	
-    	//greater1 Erzeugen
-    	Menge<ObjectType> greater1Erg = greater1(T,fc_tto);
-    	
-    	//Reflexivit�t, deshalb T hinzuf�gen.
-    	if(!greater1Erg.contains(T))
-    		greater1Erg.add(T);
-    	
-    	//Falls in greater1Erg Typen doppelt vorhanden sind werden diese nicht in retVec �bernommen.
-    	for(ObjectType t : greater1Erg)
-    		if(!retVec.contains(t))
-    			retVec.add(t);                      
-    	
-    	//Ergebnis von greater1 an greater2 durchreichen, ERgebnisse in retVec einf�gen
-    	Menge<ObjectType> greater2Erg = greater2(greater1Erg,fc_tto);
-    	for(ObjectType t : greater2Erg)
-    		if(!retVec.contains(t))
-    			retVec.add(t);           
-    	
-    	//Ergebnis von greater2 an greater3 durchreichen, ERgebnisse in retVec einf�gen
-    	Menge<ObjectType> greater3Erg = greater3(greater2Erg,fc_tto);
-    	for(ObjectType t : greater3Erg)
-    		if(!retVec.contains(t))
-    			retVec.add(t);
-    	
-    	return retVec;
-    }
-    
-    /**
-     * greater1 Schritt von greater.
-     * F�r den Argumenttype FunN<...> in Typ A<FunN<...> ...> werden keine ? extends-, ? super-Typen erzeugt
-     */
-    private static Menge<ObjectType> greater1(ObjectType T, FC_TTO fc_tto)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	if(T instanceof RefType)
-    	{
-    		RefType refT = (RefType)T;
-    		if(refT.get_ParaList() != null && refT.get_ParaList().size() > 0)
-    		{
-    			Menge<Menge<Type>> types = new Menge<Menge<Type>>();
-    			Menge<Type> paras = refT.get_ParaList();
-    			//Greater Arg von jedem Parameter einsammeln.
-    			for(int i = 0; i<paras.size();i++)
-    			{
-    				types.add(greaterArg(paras.get(i),fc_tto));
-    			}
-    			//Kartesisches Produkt bilden.
-    			Menge<Menge<Type>> kart = cartProductType(types);
-    			//Mit den neuen Parameterlisten neue Typen erzeugen.
-    			for(Menge<Type> t : kart)
-    			{
-    				RefType dolly = refT.clone();
-    				dolly.set_ParaList(t);
-    				retVec.add(dolly);
-    			}
-    		}
-    	}
-    	else if(T instanceof BoundedGenericTypeVar) //PL 15-02-03 angefuegt da BGTV Kleiner als alle seine Bounds ist 
-    	{
-    		BoundedGenericTypeVar bgtv = (BoundedGenericTypeVar)T;
-    		Menge<ObjectType> types = bgtv.getBounds();
-    		retVec = types.stream().map(ty -> greater(ty, fc_tto)).reduce(new Menge<ObjectType>(), (a,b) -> { a.addAll(b); return a;});
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * �berladung der Funktion cartProductType, damit der Programmierer beim ersten Aufruf nicht den 2. Parameter
-     * welcher f�r die rekursion erforderlich ist mit �bergeben muss.
-     */
-    private static Menge<Menge<Type>> cartProductType (Menge<Menge<Type>> vec)
-    {
-    	return cartProductType(vec,0);
-    }
-    
-    /**
-     * Erzeugt das Kartesische Product von mehreren Mengeen von Typen.
-     * F�r den Startaufruf ist der index = 0. Danach ruft sich cartProductType rekursiv auf.
-     */
-    private static Menge<Menge<Type>> cartProductType (Menge<Menge<Type>> vec, int index)
-    {
-    	Menge<Menge<Type>> retVec = new Menge<Menge<Type>>();
-    	if(vec.isEmpty()) return retVec;
-    	
-    	Menge<Type> myTypes = vec.get(index);
-    	
-    	if(index < (vec.size()-1))
-    	{
-    		Menge<Menge<Type>> nextTypes = cartProductType(vec,index+1);
-    		for(Type t : myTypes)
-    		{
-    			for(Menge<Type> tt : nextTypes)
-    			{
-    				Menge<Type> actual = copyMengeType(tt);
-    				actual.insertElementAt(t.clone(),0);
-    				retVec.add(actual);
-    			}
-    		}
-    	}
-    	else
-    	{
-    		for(Type t : myTypes)
-    		{
-    			Menge<Type> tVec = new Menge<Type>();
-    			tVec.insertElementAt(t.clone(),0);
-    			retVec.add(tVec);
-    		}
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * �berladung der Funktion cartProductPair, damit der Programmierer beim ersten Aufruf nicht den 2. Parameter
-     * welcher f�r die rekursion erforderlich ist mit �bergeben muss.
-     */
-    private static Menge<Menge<Pair>> cartProductPair (Menge<Menge<Pair>> vec)
-    {
-    	return cartProductPair(vec,0);
-    }
-    
-    /**
-     * Erzeugt das Kartesische Product von mehreren Mengeen von Paaren.
-     * F�r den Startaufruf ist der index = 0. Danach ruft sich cartProductPair rekursiv auf.
-     */
-    private static Menge<Menge<Pair>> cartProductPair (Menge<Menge<Pair>> vec, int index)
-    {
-    	Menge<Menge<Pair>> retVec = new Menge<Menge<Pair>>();
-    	if(vec.isEmpty()) return retVec;
-    	
-    	Menge<Pair> myPairs = vec.get(index);
-    	
-    	if(index < (vec.size()-1))
-    	{
-    		Menge<Menge<Pair>> nextPairs = cartProductPair(vec,index+1);
-    		for(Pair p : myPairs)
-    		{
-    			for(Menge<Pair> pp : nextPairs)
-    			{
-    				Menge<Pair> actual = copyMengePair(pp);
-    				actual.insertElementAt(p.clone(),0);
-    				retVec.add(actual);
-    			}
-    		}
-    	}
-    	else
-    	{
-    		for(Pair p : myPairs)
-    		{
-    			Menge<Pair> tVec = new Menge<Pair>();
-    			tVec.insertElementAt(p.clone(),0);
-    			retVec.add(tVec);
-    		}
-    	}
-    	return retVec;
-    }
-    /**
-     * Kopiert einen Menge<Type>. Es ist eine Deep Copy, da die Elemente auch kopiert werden.
-     */
-    private static Menge<Type> copyMengeType(Menge<? extends Type> vec)
-    {
-    	Menge<Type> retVec = new Menge<Type>();
-    	for(Type t : vec)
-    		retVec.add(t.clone());
-    		
-    	return retVec;
-    }
-    
-    /**
-     * Kopiert einen Menge<ObjectType>. Es ist eine Deep Copy, da die Elemente auch kopiert werden.
-     * noetig wegen Type-Erasure 
-     */
-    private static Menge<ObjectType> copyMengeObjectType(Menge<ObjectType> vec)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	for(ObjectType t : vec)
-    		retVec.add(t.clone());
-    		
-    	return retVec;
-    }
-    
-    /**
-     * greaterArg Schritt von greater
-     * F�r den Argumenttype FunN<...> werden keine ? extends-, ? super-Typen erzeugt
-     */
-    private static Menge<Type> greaterArg(Type T, FC_TTO fc_tto)
-    {
-    	Menge<Type> retVec = new Menge<Type>();
-    	if(T instanceof ExtendsWildcardType)
-    	{
-    		//Bei einer ExtendsWildcard Rekursiv greater0 aufrufen und neue ExtendsWildcars erzeugen
-    		ExtendsWildcardType exT = (ExtendsWildcardType)T;
-    		Menge<ObjectType> greaterTypes = greater0(exT.get_ExtendsType(),fc_tto);
-    		for(ObjectType t : greaterTypes)
-    			retVec.add(new ExtendsWildcardType(t.getOffset(),t.clone()));
-    	}
-    	else if(T instanceof SuperWildcardType)
-    	{
-    		//Bei einer SuperWildcard Rekursiv smaller0 aufrufen und neue SuperWildcards erzeugen.
-    		SuperWildcardType suT = (SuperWildcardType)T;
-    		Menge<ObjectType> smallerTypes = smaller0(suT.get_SuperType(),fc_tto);
-    		for(ObjectType t : smallerTypes)
-    			retVec.add(new SuperWildcardType(t.getOffset(),t.clone()));
-    	}
-    	
-    	/* PL 15-03-10 
-    	 * Kann meiner Ansicht nach nicht vorkommen
-    	 
-    	else if(T instanceof FreshExtendsWildcardType)
-    	{
-    		//Bei einer FreshExtendsWildcard greaterArg aufrufen, auf Bounds achten.
-    		retVec.add(T);
-    		retVec.add(new ExtendsWildcardType(T.getOffset(),T.clone()));
-    		
-    		FreshExtendsWildcardType fexT = (FreshExtendsWildcardType)T;
-    		ExtendsWildcardType extT = new ExtendsWildcardType(fexT.get_ExtendsBound().getOffset(), fexT.get_ExtendsBound().clone());
-    		
-    		//Menge<Type> tmp = greaterArg(fexT.get_ExtendsBound(),fc_tto); //hier stimmt es nicht PL 07-07-21
-    		Menge<Type> tmp = greaterArg(extT,fc_tto);
-    		//for(int i = 0; i<tmp.size();i++)     nicht mehr noetig, extT immer ? extends ... ist PL 07-07-21
-    		//	if(tmp.get(i).equals(fexT.get_ExtendsBound()))
-    		//		tmp.remove(i--);
-    		                                                               
-    		for(Type tt : tmp)
-				if(!retVec.contains(tt))
-					retVec.add(tt);
-    		
-    		for(Type t : fexT.get_UpperBounds())
-    		{
-    			tmp = greaterArg(t,fc_tto);
-    			for(Type tt : tmp)
-    				if(!retVec.contains(tt))
-    					retVec.add(tt);
-    		}
-    	}
-    	else if(T instanceof FreshSuperWildcardType)
-    	    return new Menge<Type>();
-    	*/
-    	
-    	//Diese Abfrage sorgt f�r grArg(a) = {a} //Luar 07-07-31
-    	else if(T instanceof TypePlaceholder)
-    		retVec.add(T);
-    	//Diese Abfrage verhindert, dass bei FunN Wildcard-Typen generiert werden //PL 13-05-22
-    	else if((T instanceof RefType) && (T.getName().equals("FunN")))
-    			retVec.add(T);
-    	else //RefType oder GTV
-    	{
-    		//Bei allen anderen Typen greater0 und smaller0 aufrufen.
-    		retVec.add((ObjectType)T);
-    		Menge<ObjectType> greaterTypes = greater0((ObjectType)T,fc_tto);
-    		Menge<ObjectType> smallerTypes = smaller0((ObjectType)T,fc_tto);
-    		for(ObjectType t : greaterTypes)
-    			retVec.add(new ExtendsWildcardType(t.getOffset(),t.clone()));
-    		
-    		for(ObjectType t : smallerTypes)
-    			retVec.add(new SuperWildcardType(t.getOffset(),t.clone()));
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * greater2 Schritt von greater
-     */
-    private static Menge<ObjectType> greater2(Menge<ObjectType> greater1Erg, FC_TTO fc_tto)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	/*
-    	 * luar 02-05-07: Beschreibung der Funktion:
-    	 * F�r Jeden Typ aus greater1 durch die FC laufen, und auf der Linken seite einen Match versuchen.
-    	 * Wenn das Funktioniert, dann ist der Typ auf der rechten Seite auch greater.
-    	 * */
-    	Hashtable<JavaClassName,Type> ht = new Hashtable<JavaClassName,Type>();
-    	for(Type t : greater1Erg)
-    	{
-	   		for(Pair p : fc_tto.getFC())
-	   		{
-	   			ht.clear();
-	   			if(p.TA2 instanceof RefType && p.TA1 instanceof RefType && t instanceof RefType)
-	   			{
-	    			try
-	    			{
-	    				match((RefType)p.TA1,(RefType)t,ht);
-	    				ht = CaptureConversionHashtable(ht,fc_tto);
-	    				for(Type tt : ht.values())
-	    				{
-	    					if(tt instanceof WildcardType)
-	    						throw new MatchException("Wildcards not allowed");
-	    				}
-	    				
-	    				//Macht hat funktioniert. In Linker Seite Typen substituieren
-	    				RefType TA2neu = ((RefType)p.TA2).clone();
-	    				SubstHashtableGeneric(TA2neu,ht);
-	    				
-	    				//TA2neu ist greater als T. Einf�gen in retVec
-	    				if(!retVec.contains(TA2neu))
-	    					retVec.add(TA2neu);
-	    			}
-	    			catch(MatchException ex)
-	    			{}
-	   			}
-	   		}
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * greater3 Schritt von greater
-     */
-    private static Menge<ObjectType> greater3(Menge<ObjectType> greater2Erg, FC_TTO fc_tto)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	for(ObjectType t : greater2Erg)
-    	{
-    		Menge<ObjectType> greater1Erg = greater1(t,fc_tto);
-    		for(ObjectType tt : greater1Erg)
-    			if(!retVec.contains(tt))
-    				retVec.add(tt);
-    	}
-    	return retVec;
-    }
-    
-    //Von hier an Smaller implementierung luar 28-03-07
-    /**
-     * Der Komplette Ablauf von smaller und was die einzelnen Teilschritte machen kann anhand von Aktivit�tsdiagrammen
-     * im Inovator Projekt, oder in der Studienarbeit Arne L�dtke, 2007 nachgelesen werden.
-     */
-    
-    /**
-     * Erzeugt alle Typen die smaller sind als T. Gibt diese zur�ck.
-     */
-    private static Menge<ObjectType> smaller(ObjectType T, FC_TTO fc_tto)
-    //an die Aenderungen im Skript anpassen 07-11-03
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	Menge<ObjectType> smaller0Erg = smaller0(T,fc_tto);
-    	for(ObjectType t : smaller0Erg)
-    	{
-    		if(!DelFreshWildcardTypeVar(t))
-    			retVec.add(t);
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * smaller0 Schritt von smaller
-     */
-    private static Menge<ObjectType> smaller0(ObjectType T, FC_TTO fc_tto)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	
-    	Menge<ObjectType> smaller1Erg = smaller1(T,fc_tto);
-    	
-    	
-    	Menge<ObjectType> smaller2Erg = smaller2(smaller1Erg,fc_tto);
-    	
-    	//Unite von smaller 1 und 2 bilden, um dies an smaller 3 weiterzugeben.
-    	Menge<ObjectType> smaller12Erg = copyMengeObjectType(smaller1Erg);
-    	for(ObjectType t : smaller2Erg)
-    		if(!smaller12Erg.contains(t))
-    			smaller12Erg.add(t);
-    	
-    	if(!smaller12Erg.contains(T))
-    		smaller12Erg.add(T);
-    	
-    	//Ergebnise in retVec einf�gen. Doppelte werden gel�scht.
-    	for(ObjectType t : smaller12Erg)
-    		if(!retVec.contains(t))
-    			retVec.add(t);
-    	
-    	//Ergebnis von smaller1 und smaller2 an smaller3 weitergeben, Ergebnisse einf�gen.
-    	Menge<ObjectType> smaller3Erg = smaller3(smaller12Erg,fc_tto);
-    	for(ObjectType t : smaller3Erg)
-    		if(!retVec.contains(t))
-    			retVec.add(t);
-    	
-    	//Ergebnisse von smaller3 an smaller4 weitergeben, Ergebnisse einf�gen.
-    	Menge<ObjectType> smaller4Erg = smaller4(smaller3Erg);
-    	for(ObjectType t : smaller4Erg)
-    		if(!retVec.contains(t))
-    			retVec.add(t);
-    	
-    	return retVec;
-    }
-    
-    /**
-     * smaller1 Schritt von smaller
-     */
-    private static Menge<ObjectType> smaller1(Type T, FC_TTO fc_tto)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	if(T instanceof RefType)
-    	{
-    		RefType refT = (RefType)T;
-    		if(refT.get_ParaList() != null && refT.get_ParaList().size() > 0)
-    		{
-    			Menge<Menge<Type>> types = new Menge<Menge<Type>>();
-    			Menge<Type> paras = refT.get_ParaList();
-    			//Smaller Arg von jedem Parameter einsammeln.
-    			for(int i = 0; i<paras.size();i++)
-    			{
-    				types.add(smallerArg(paras.get(i),fc_tto));
-    			}
-    			//Kartesisches Produkt bilden.
-    			Menge<Menge<Type>> kart = cartProductType(types);
-    			//Mit den neuen Parameterlisten neue Typen klonen, Parameterlisten zuweisen
-    			for(Menge<Type> t : kart)
-    			{
-    				RefType dolly = refT.clone();
-    				dolly.set_ParaList(t);
-    				retVec.add(dolly);
-    			}
-    		}
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * smallerArg Schritt von smaller
-     */
-    private static Menge<Type> smallerArg(Type T, FC_TTO fc_tto)
-    {
-    	Menge<Type> retVec = new Menge<Type>();
-    	if(T instanceof ExtendsWildcardType)
-    	{
-    		//F�r eine ExtendsWildcard rekursiv smaller0 aufrufen, und neue Wildcards erzeugen.
-    		ExtendsWildcardType exT = (ExtendsWildcardType)T;
-    		Menge<ObjectType> smallerTypes = smaller0(exT.get_ExtendsType(),fc_tto);
-    		for(ObjectType t : smallerTypes)
-    		{
-    			retVec.add(new ExtendsWildcardType(t.getOffset(),t.clone()));
-    			retVec.add(t.clone());
-    		}
-    	}
-    	else if(T instanceof SuperWildcardType)
-    	{
-    		//F�r eine SuperWildcard rekursiv greater0 aufrufen, unr neue Wildcards erzeugen.
-    		SuperWildcardType suT = (SuperWildcardType)T;
-    		Menge<ObjectType> greaterTypes = greater0(suT.get_SuperType(),fc_tto);
-    		for(ObjectType t : greaterTypes)
-    		{
-    			retVec.add(new SuperWildcardType(-1,t.clone()));
-    			retVec.add(t.clone());
-    		}
-    	}
-    	else if(T instanceof FreshExtendsWildcardType)
-    		return new Menge<Type>(); //HIER NOCH T EINFUEGEN 07-11-03 PL
-
-    	else if(T instanceof FreshSuperWildcardType)
-    	{//HIER AUCH NUR T EINFUEGEN 07-11-03 PL
-    		FreshSuperWildcardType fsuT = (FreshSuperWildcardType)T;
-    		return smallerArg(fsuT.get_SuperBound(),fc_tto);
-    	}
-    	else
-    		retVec.add(T);
-    	
-    	return retVec;
-    }
-    
-    /**
-     * smaller2 Schritt von smaller
-     */
-    private static Menge<ObjectType> smaller2(Menge<ObjectType> smaller1Erg, FC_TTO fc_tto)
-    {
-    	return CaptureConversion(smaller1Erg,fc_tto);
-    }
-    
-    /**
-     * smaller3 Schritt von smaller
-     */
-    private static Menge<ObjectType> smaller3(Menge<ObjectType> smaller12Erg, FC_TTO fc_tto)
-    {
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	/*
-    	 * luar 02-05-07: Beschreibung der Funktion:
-    	 * F�r Jeden Typ aus Smaller12 durch die FC laufen, und auf der Rechten seite einen Match versuchen.
-    	 * Wenn das Funktioniert, dann ist der Typ auf der linken Seite auch smaller.
-    	 * */
-    	Hashtable<JavaClassName,Type> ht = new Hashtable<JavaClassName,Type>();
-    	for(Type t : smaller12Erg)
-    	{
-	   		for(Pair p : fc_tto.getFC())
-	   		{
-	   			ht.clear();
-	   			if(p.TA2 instanceof RefType && p.TA1 instanceof RefType && t instanceof RefType)
-	   			{
-	    			try
-	    			{
-	    				match((RefType)p.TA2,(RefType)t,ht);    				
-	    				for(Type tt : ht.values())
-	    				{
-	    					if(tt instanceof WildcardType)
-	    						throw new MatchException("Wildcards not allowed");
-	    				}
-	    				
-	    				//Macht hat funktioniert. In Linker Seite Typen substituieren
-	    				RefType TA1neu = ((RefType)p.TA1).clone();
-	    				SubstHashtableGeneric(TA1neu,ht);
-	    				//TA1neu ist smaller als T. Einf�gen in retVec
-	    				if(!retVec.contains(TA1neu))
-	    					retVec.add(TA1neu);
-	    			}
-	    			catch(MatchException ex)
-	    			{}
-	   			}
-	   		}
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * smaller4 Schritt von smaller
-     */
-    private static Menge<ObjectType> smaller4(Menge<ObjectType> smallerErg)
-    {
-    	/* smaller4 ist die inverse CaptureConversion.
-    	 * Alle Typen in smallerErg werden durchlaufen, und evtl. gefundene
-    	 * FreshWildcardTypes werden durch die entsprechenden Wildcards ersetzt.
-    	 * */
-    	Menge<ObjectType> retVec = new Menge<ObjectType>();
-    	for(ObjectType t : smallerErg)
-    	{
-    		if(t instanceof RefType)
-    		{
-    			RefType refT = (RefType)t.clone();
-    			if(refT.get_ParaList() != null)
-    			{
-    				Menge<Type> paras = refT.get_ParaList();
-    				for(int i = 0; i<paras.size();i++)
-    				{
-    					if(paras.get(i) instanceof FreshWildcardType)
-    					{
-    						FreshWildcardType fwct = (FreshWildcardType)paras.get(i);
-    						paras.setElementAt(fwct.get_WildcardType(),i);
-    					}
-    				}
-    			}
-    			retVec.add(refT);
-    		}
-    		else
-    		{
-    			retVec.add(t.clone());
-    		}
-    	}
-    	return retVec;
-    }
-    
-    /**
-     * Gibt True zur�ck, wenn T eine FreshWildcard ist, oder im Falle eines RefTypes oder WildcardTypes eine FreshWildcard enth�lt.
-     */
-    private static boolean DelFreshWildcardTypeVar(Type T)
-    {
-    	//luar 29-05-2007
-    	//�berpr�ft rekursiv ob in dem RefType ein FreshWildcardType enthalten ist.
-    	if(T instanceof RefType)
-    	{
-    		RefType refT = (RefType)T;
-    		if(refT.get_ParaList() != null)
-    			for(Type t : refT.get_ParaList())
-    				if(DelFreshWildcardTypeVar(t))
-    					return true;
-    	}
-    	//Im Falle einer Wildcard, Typen aus der WC rausnehmen und diesen rekursiv pr�fen.
-    	if(T instanceof ExtendsWildcardType)
-    		return DelFreshWildcardTypeVar(((ExtendsWildcardType)T).get_ExtendsType());
-    	
-    	if(T instanceof SuperWildcardType)
-    		return DelFreshWildcardTypeVar(((SuperWildcardType)T).get_SuperType());
-    	
-    	return T instanceof FreshWildcardType;
-    }
-
-    public static <A extends DeepCloneable> Menge<A> deepClone(Menge<A> m){
-        Timewatch watch = Timewatch.getTimewatch();
-        Timestamp timer = watch.start("Unify - deepClone");
-        Menge<A> ret = m.stream().<A>map((Function<A,A>)(x -> x.deepClone())).<Menge<A>>collect(Menge::new, Menge::add, Menge::addAll);
-        timer.stop();
-        return ret;
-    }
-
-    
-}
-// ino.end
+	protected Set<MPair> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		for(UnifyType theta : fc.smArg(subThetaPrime))
+			result.add(new MPair(a, theta, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase4(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		result.add(new MPair(a, thetaPrime, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		for(UnifyType thetaS : fc.greater(theta))
+			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		for(UnifyType thetaS : fc.grArg(extTheta))
+			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		IUnify unify = new MartelliMontanariUnify();
+		
+		UnifyType theta = supTheta.getSuperedType();
+		Set<UnifyType> cs = fc.getAllTypesByName(theta.getName());
+		
+		for(UnifyType c : cs) {
+			
+			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
+			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
+			thetaQs.add(c); // reflexive
+			
+			Set<UnifyType> thetaQPrimes = new HashSet<>();
+			TypeParams cParams = c.getTypeParams();
+			if(cParams.size() == 0)
+				thetaQPrimes.add(c);
+			else {
+				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
+				for(UnifyType param : cParams)
+					candidateParams.add(fc.grArg(param));
+			
+				for(TypeParams tp : permuteParams(candidateParams))
+					thetaQPrimes.add(c.setTypeParams(tp));
+			}
+			
+			for(UnifyType tqp : thetaQPrimes) {
+				Optional<Unifier> opt = unify.unify(tqp, theta);
+				if (!opt.isPresent())
+					continue;
+				
+				Unifier unifier = opt.get();
+				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
+				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
+					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
+				for (UnifyType tq : thetaQs) {
+					Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
+					smaller.stream().map(x -> new MPair(a, new SuperType(x), PairOperator.EQUALSDOT))
+							.forEach(x -> result.add(x));
+				}
+
+			}
+		}
+		
+		return result;
+	}
+	
+	protected Set<MPair> unifyCase8(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
+		Set<MPair> result = new HashSet<>();
+		for(UnifyType thetaS : fc.grArg(theta))
+			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
+		return result;
+	}
+	
+	protected Set<TypeParams> permuteParams(ArrayList<Set<UnifyType>> candidates) {
+		Set<TypeParams> result = new HashSet<>();
+		permuteParams(candidates, 0, result, new UnifyType[candidates.size()]);
+		return result;
+	}
+	
+	private void permuteParams(ArrayList<Set<UnifyType>> candidates, int idx, Set<TypeParams> result, UnifyType[] current) {
+		if(candidates.size() == idx) {
+			result.add(new TypeParams(Arrays.copyOf(current, current.length)));
+			return;
+		}
+		
+		Set<UnifyType> localCandidates = candidates.get(idx);
+		
+		for(UnifyType t : localCandidates) {
+			current[idx] = t;
+			permuteParams(candidates, idx+1, result, current);
+		}
+	}
+}
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
index 757e53d1..3fb48ac9 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
@@ -8,10 +8,10 @@ import java.util.Optional;
 import java.util.Set;
 import java.util.stream.Collectors;
 
+import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
 import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
-import de.dhbwstuttgart.typeinference.unifynew.MartelliMontanariUnify;
 
 public class FiniteClosure implements IFiniteClosure {
 	
diff --git a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java b/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java
deleted file mode 100644
index 1023c852..00000000
--- a/src/de/dhbwstuttgart/typeinference/unifynew/Unify.java
+++ /dev/null
@@ -1,480 +0,0 @@
-package de.dhbwstuttgart.typeinference.unifynew;
-
-import java.util.ArrayList;
-import java.util.Arrays;
-import java.util.Collection;
-import java.util.HashSet;
-import java.util.LinkedHashSet;
-import java.util.LinkedList;
-import java.util.List;
-import java.util.Map.Entry;
-import java.util.Optional;
-import java.util.Set;
-import java.util.stream.Collectors;
-
-import de.dhbwstuttgart.typeinference.Menge;
-import de.dhbwstuttgart.typeinference.Pair;
-import de.dhbwstuttgart.typeinference.exceptions.NotImplementedException;
-import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
-import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
-import de.dhbwstuttgart.typeinference.unify.interfaces.ISetOperations;
-import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
-import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
-import de.dhbwstuttgart.typeinference.unify.model.MPair;
-import de.dhbwstuttgart.typeinference.unify.model.PlaceholderType;
-import de.dhbwstuttgart.typeinference.unify.model.SuperType;
-import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
-import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
-import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
-import de.dhbwstuttgart.typeinference.unify.model.Unifier;
-
-
-/**
- * Implementation of the type unification algorithm
- * @author Florian Steurer
- */
-public class Unify {
-	
-	public Set<Set<MPair>> unify(Set<MPair> eq, IFiniteClosure fc) {		
-		/*
-		 * Step 1: Repeated application of reduce, adapt, erase, swap 
-		 */
-		
-		Set<MPair> eq0 = applyTypeUnificationRules(eq, fc);
-		
-		/*
-		 * Step 2 and 3: Create a subset eq1s of pairs where both sides are TPH and eq2s of the other pairs
-		 */
-		
-		Set<MPair> eq1s = new HashSet<>();
-		Set<MPair> eq2s = new HashSet<>();
-		splitEq(eq0, eq1s, eq2s);
-		
-		/*
-		 * Step 4: Create possible typings
-		 * 
-		 * "Manche Autoren identifizieren die Paare (a, (b,c)) und ((a,b),c) 
-		 * mit dem geordneten Tripel (a,b,c), wodurch das kartesische Produkt auch assoziativ wird." - Wikipedia
-		 */
-		
-		// There are up to 10 toplevel set. 8 of 10 are the result of the 
-		// cartesian product of the sets created by pattern matching.
-		List<Set<Set<MPair>>> topLevelSets = new ArrayList<>();
-		
-		if(eq1s.size() != 0) {
-			Set<Set<MPair>> wrap = new HashSet<>();
-			wrap.add(eq1s);
-			topLevelSets.add(wrap); // Add Eq1'
-		}
-
-		// Add the set of [a =. Theta | (a=. Theta) in Eq2']
-		Set<MPair> bufferSet = eq2s.stream()
-				.filter(x -> x.getPairOp() == PairOperator.EQUALSDOT && x.getLhsType() instanceof PlaceholderType)
-				.collect(Collectors.toSet());
-		
-		if(bufferSet.size() != 0) {
-			Set<Set<MPair>> wrap = new HashSet<>();
-			wrap.add(bufferSet);
-			topLevelSets.add(wrap);
-		}
-		
-		// Sets that originate from pair pattern matching
-		// Sets of the "second level"
-		Set<Set<Set<MPair>>> secondLevelSets = calculatePairSets(eq2s, fc);
-		
-		/* Up to here, no cartesian products are calculated.
-		 * filters for pairs and sets can be applied here */
-		
-		ISetOperations setOps = new GuavaSetOperations();
-		
-		// Sub cartesian products of the second level (pattern matched) sets
-		for(Set<Set<MPair>> secondLevelSet : secondLevelSets) {
-			List<Set<MPair>> secondLevelSetList = new ArrayList<>(secondLevelSet);
-			topLevelSets.add(setOps.cartesianProduct(secondLevelSetList)
-					.stream().map(x -> new HashSet<>(x))
-					.collect(Collectors.toCollection(HashSet::new)));
-		}
-		
-		// Cartesian product over all (up to 10) top level sets 
-		Set<Set<Set<MPair>>> eqPrimeSet = setOps.cartesianProduct(topLevelSets)
-				.stream().map(x -> new HashSet<>(x))
-				.collect(Collectors.toCollection(HashSet::new));
-		//System.out.println(result);
-
-		/*
-		 * Step 5: Substitution
-		 */
-		
-		/*
-		 * TODO hier das ergebnis schonh flach machen? (wird im unify old (glaub ich) so gemacht)
-		 */
-		Set<Set<MPair>> eqPrimeSetFlat = new HashSet<>();
-		for(Set<Set<MPair>> setToFlatten : eqPrimeSet) {
-			Set<MPair> buffer = new HashSet<>();
-			setToFlatten.stream().forEach(x -> buffer.addAll(x));
-			eqPrimeSetFlat.add(buffer);
-		}
-		
-		IRuleSet rules = new RuleSet(fc);
-		Set<Set<MPair>> changed = new HashSet<>();
-		Set<Set<MPair>> eqPrimePrimeSet = new HashSet<>();
-		
-		for(Set<MPair> eqPrime : eqPrimeSetFlat) {
-			Optional<Set<MPair>> eqPrimePrime = rules.subst(eqPrime);
-			
-			if(eqPrimePrime.isPresent())
-				changed.add(eqPrimePrime.get());
-			else
-				eqPrimePrimeSet.add(eqPrime);
-		}
-
-		/*
-		 * Step 6 a) Restart for pairs where subst was applied
-		 * 		  b) Build the union over everything
-		 */
-		
-		for(Set<MPair> eqss : changed) {
-			eqPrimePrimeSet.addAll(this.unify(eqss, fc));
-		}
-		
-		 /*
-		  * Step 7: Filter result for solved pairs
-		  */
-		return eqPrimePrimeSet;
-		
-	}
-	
-	protected Set<MPair> applyTypeUnificationRules(Set<MPair> eq, IFiniteClosure fc) {
-		
-		/*
-		 * Rule Application Strategy:
-		 * 
-		 * 1. 	Swap all pairs and erase all erasable pairs
-		 * 2. 	Apply all possible rules to a single pair, then move it to the result set.
-		 *    	Iterating over pairs first, then iterating over rules prevents the application
-		 *    	of rules to a "finished" pair over and over.
-		 * 2.1 	Apply all rules repeatedly except for erase rules. If
-		 * 		the application of a rule creates new pairs, check immediately
-		 * 		against the erase rules.
-		 */
-		
-		
-		LinkedHashSet<MPair> targetSet = new LinkedHashSet<MPair>();
-		LinkedList<MPair> eqQueue = new LinkedList<>();
-		IRuleSet rules = new RuleSet(fc);
-		
-		/*
-		 * Swap all pairs and erase all erasable pairs
-		 */
-		eq.forEach(x -> swapAddOrErase(x, rules, eqQueue));
-		
-		/*
-		 * Apply rules until the queue is empty
-		 */
-		while(!eqQueue.isEmpty()) {
-			MPair pair = eqQueue.pollFirst();
-
-			// ReduceUp, ReduceLow, ReduceUpLow
-			Optional<MPair> opt = rules.reduceUpLow(pair);
-			opt = opt.isPresent() ? opt : rules.reduceLow(pair);
-			opt = opt.isPresent() ? opt : rules.reduceUp(pair);
-			
-			// One of the rules has been applied
-			if(opt.isPresent()) {
-				swapAddOrErase(opt.get(), rules, eqQueue);
-				continue;
-			}
-			
-			// Reduce1, Reduce2, ReduceExt, ReduceSup, ReduceEq
-			Optional<Set<MPair>> optSet = rules.reduce1(pair);
-			optSet = optSet.isPresent() ? optSet : rules.reduce2(pair);
-			optSet = optSet.isPresent() ? optSet : rules.reduceExt(pair);
-			optSet = optSet.isPresent() ? optSet : rules.reduceSup(pair);
-			optSet = optSet.isPresent() ? optSet : rules.reduceEq(pair);
-			
-			// One of the rules has been applied
-			if(optSet.isPresent()) {
-				optSet.get().forEach(x -> swapAddOrErase(x, rules, eqQueue));
-				continue;
-			}
-			
-			// Adapt, AdaptExt, AdaptSup
-			opt = rules.adapt(pair);
-			opt = opt.isPresent() ? opt : rules.adaptExt(pair);
-			opt = opt.isPresent() ? opt : rules.adaptSup(pair);
-			
-			// One of the rules has been applied
-			if(opt.isPresent()) {
-				swapAddOrErase(opt.get(), rules, eqQueue);
-				continue;
-			}
-			
-			// None of the rules has been applied
-			targetSet.add(pair);
-		}
-		
-		return targetSet;
-	}
-	
-	protected void swapAddOrErase(MPair pair, IRuleSet rules, Collection<MPair> collection) {
-		Optional<MPair> opt = rules.swap(pair);
-		MPair pair2 = opt.isPresent() ? opt.get() : pair;
-		
-		if(rules.erase1(pair2) || rules.erase3(pair2) || rules.erase2(pair2))
-			return;
-		
-		collection.add(pair2);
-	}
-	
-	protected void splitEq(Set<MPair> eq, Set<MPair> eq1s, Set<MPair> eq2s) {
-		for(MPair pair : eq) 
-			if(pair.getLhsType() instanceof PlaceholderType && pair.getRhsType() instanceof PlaceholderType)
-				eq1s.add(pair);
-			else
-				eq2s.add(pair);
-	}
-	
-	
-	protected Set<Set<Set<MPair>>> calculatePairSets(Set<MPair> eq2s, IFiniteClosure fc) {
-		List<Set<Set<MPair>>> result = new ArrayList<>();
-		
-		// Init all 8 cases
-		for(int i = 0; i < 8; i++)
-			result.add(new HashSet<>());
-		
-		for(MPair pair : eq2s) {
-			
-			PairOperator pairOp = pair.getPairOp();
-			UnifyType lhsType = pair.getLhsType();
-			UnifyType rhsType = pair.getRhsType();
-	
-			// Case 1: (a <. Theta')
-			if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType)
-				result.get(0).add(unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), fc));
-			
-			// Case 2: (a <.? ? ext Theta')
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
-				result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), fc));
-			
-			// Case 3: (a <.? ? sup Theta')
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
-				result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, fc));
-			
-			// Case 4: (a <.? Theta')
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType)
-				result.get(3).add(unifyCase4((PlaceholderType) lhsType, rhsType, fc));
-				
-			// Case 5: (Theta <. a)
-			else if(pairOp == PairOperator.SMALLERDOT && rhsType instanceof PlaceholderType)
-				result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, fc));
-			
-			// Case 6: (? ext Theta <.? a)
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof ExtendsType && rhsType instanceof PlaceholderType)
-				result.get(5).add(unifyCase6((ExtendsType) lhsType, (PlaceholderType) rhsType, fc));
-
-			// Case 7: (? sup Theta <.? a)
-			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof SuperType && rhsType instanceof PlaceholderType)
-				result.get(6).add(unifyCase7((SuperType) lhsType, (PlaceholderType) rhsType, fc));
-			
-			// Case 8: (Theta <.? a)
-			else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
-				result.get(7).add(unifyCase8(lhsType, (PlaceholderType) rhsType, fc));
-		}
-		
-		return result.stream().filter(x -> x.size() > 0).collect(Collectors.toCollection(HashSet::new));
-	}
-	
-	protected Set<MPair> unifyCase1(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
-		Set<MPair> result = new HashSet<>();
-		IUnify unify = new MartelliMontanariUnify();
-		
-		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
-		
-		for(UnifyType c : cs) {
-			
-			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
-			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
-			thetaQs.add(c); // reflexive
-			
-			Set<UnifyType> thetaQPrimes = new HashSet<>();
-			TypeParams cParams = c.getTypeParams();
-			if(cParams.size() == 0)
-				thetaQPrimes.add(c);
-			else {
-				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
-				for(UnifyType param : cParams)
-					candidateParams.add(fc.grArg(param));
-			
-				for(TypeParams tp : permuteParams(candidateParams))
-					thetaQPrimes.add(c.setTypeParams(tp));
-			}
-			
-			for(UnifyType tqp : thetaQPrimes) {
-				Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
-				if (!opt.isPresent())
-					continue;
-				
-				Unifier unifier = opt.get();
-				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
-				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
-					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
-				for (UnifyType tq : thetaQs) {
-					Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
-					smaller.stream().map(x -> new MPair(a, x, PairOperator.EQUALSDOT))
-							.forEach(x -> result.add(x));
-				}
-
-			}
-		}
-		
-		return result;
-	}
-	
-	protected Set<MPair> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, IFiniteClosure fc) {
-		Set<MPair> result = new HashSet<>();
-		IUnify unify = new MartelliMontanariUnify();
-		
-		UnifyType thetaPrime = extThetaPrime.getExtendedType();
-		Set<UnifyType> cs = fc.getAllTypesByName(thetaPrime.getName());
-		
-		for(UnifyType c : cs) {
-			
-			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
-			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
-			thetaQs.add(c); // reflexive
-			
-			Set<UnifyType> thetaQPrimes = new HashSet<>();
-			TypeParams cParams = c.getTypeParams();
-			if(cParams.size() == 0)
-				thetaQPrimes.add(c);
-			else {
-				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
-				for(UnifyType param : cParams)
-					candidateParams.add(fc.grArg(param));
-			
-				for(TypeParams tp : permuteParams(candidateParams))
-					thetaQPrimes.add(c.setTypeParams(tp));
-			}
-			
-			for(UnifyType tqp : thetaQPrimes) {
-				Optional<Unifier> opt = unify.unify(tqp, thetaPrime);
-				if (!opt.isPresent())
-					continue;
-				
-				Unifier unifier = opt.get();
-				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
-				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
-					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
-				for (UnifyType tq : thetaQs) {
-					ExtendsType extTq = new ExtendsType(tq);
-					Set<UnifyType> smaller = fc.smaller(unifier.apply(extTq));
-					smaller.stream().map(x -> new MPair(a, x, PairOperator.EQUALSDOT))
-							.forEach(x -> result.add(x));
-				}
-			}
-		}
-		
-		return result;
-	}
-	
-	protected Set<MPair> unifyCase3(PlaceholderType a, SuperType subThetaPrime, IFiniteClosure fc) {
-		Set<MPair> result = new HashSet<>();
-		for(UnifyType theta : fc.smArg(subThetaPrime))
-			result.add(new MPair(a, theta, PairOperator.EQUALSDOT));
-		return result;
-	}
-	
-	protected Set<MPair> unifyCase4(PlaceholderType a, UnifyType thetaPrime, IFiniteClosure fc) {
-		Set<MPair> result = new HashSet<>();
-		result.add(new MPair(a, thetaPrime, PairOperator.EQUALSDOT));
-		return result;
-	}
-	
-	protected Set<MPair> unifyCase5(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
-		Set<MPair> result = new HashSet<>();
-		for(UnifyType thetaS : fc.greater(theta))
-			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
-		return result;
-	}
-	
-	protected Set<MPair> unifyCase6(ExtendsType extTheta, PlaceholderType a, IFiniteClosure fc) {
-		Set<MPair> result = new HashSet<>();
-		for(UnifyType thetaS : fc.grArg(extTheta))
-			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
-		return result;
-	}
-	
-	protected Set<MPair> unifyCase7(SuperType supTheta, PlaceholderType a, IFiniteClosure fc) {
-		Set<MPair> result = new HashSet<>();
-		IUnify unify = new MartelliMontanariUnify();
-		
-		UnifyType theta = supTheta.getSuperedType();
-		Set<UnifyType> cs = fc.getAllTypesByName(theta.getName());
-		
-		for(UnifyType c : cs) {
-			
-			// Wenn die fc nach spezifikation funktioniert ist das hier nicht mehr nötig?
-			Set<UnifyType> thetaQs = fc.smaller(c).stream().filter(x -> x.getTypeParams().arePlaceholders()).collect(Collectors.toCollection(HashSet::new));
-			thetaQs.add(c); // reflexive
-			
-			Set<UnifyType> thetaQPrimes = new HashSet<>();
-			TypeParams cParams = c.getTypeParams();
-			if(cParams.size() == 0)
-				thetaQPrimes.add(c);
-			else {
-				ArrayList<Set<UnifyType>> candidateParams = new ArrayList<>();
-				for(UnifyType param : cParams)
-					candidateParams.add(fc.grArg(param));
-			
-				for(TypeParams tp : permuteParams(candidateParams))
-					thetaQPrimes.add(c.setTypeParams(tp));
-			}
-			
-			for(UnifyType tqp : thetaQPrimes) {
-				Optional<Unifier> opt = unify.unify(tqp, theta);
-				if (!opt.isPresent())
-					continue;
-				
-				Unifier unifier = opt.get();
-				Set<Entry<PlaceholderType, UnifyType>> substitutions = unifier.getSubstitutions();
-				for (Entry<PlaceholderType, UnifyType> sigma : substitutions)
-					result.add(new MPair(sigma.getKey(), sigma.getValue(), PairOperator.EQUALSDOT));
-				for (UnifyType tq : thetaQs) {
-					Set<UnifyType> smaller = fc.smaller(unifier.apply(tq));
-					smaller.stream().map(x -> new MPair(a, new SuperType(x), PairOperator.EQUALSDOT))
-							.forEach(x -> result.add(x));
-				}
-
-			}
-		}
-		
-		return result;
-	}
-	
-	protected Set<MPair> unifyCase8(UnifyType theta, PlaceholderType a, IFiniteClosure fc) {
-		Set<MPair> result = new HashSet<>();
-		for(UnifyType thetaS : fc.grArg(theta))
-			result.add(new MPair(a, thetaS, PairOperator.EQUALSDOT));
-		return result;
-	}
-	
-	protected Set<TypeParams> permuteParams(ArrayList<Set<UnifyType>> candidates) {
-		Set<TypeParams> result = new HashSet<>();
-		permuteParams(candidates, 0, result, new UnifyType[candidates.size()]);
-		return result;
-	}
-	
-	private void permuteParams(ArrayList<Set<UnifyType>> candidates, int idx, Set<TypeParams> result, UnifyType[] current) {
-		if(candidates.size() == idx) {
-			result.add(new TypeParams(Arrays.copyOf(current, current.length)));
-			return;
-		}
-		
-		Set<UnifyType> localCandidates = candidates.get(idx);
-		
-		for(UnifyType t : localCandidates) {
-			current[idx] = t;
-			permuteParams(candidates, idx+1, result, current);
-		}
-	}
-}
diff --git a/test/unify/RuleSetTest.java b/test/unify/RuleSetTest.java
index 1fe1359d..f38d9f2c 100644
--- a/test/unify/RuleSetTest.java
+++ b/test/unify/RuleSetTest.java
@@ -8,13 +8,13 @@ import junit.framework.Assert;
 
 import org.junit.Test;
 
+import de.dhbwstuttgart.typeinference.unify.RuleSet;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IRuleSet;
 import de.dhbwstuttgart.typeinference.unify.model.ExtendsType;
 import de.dhbwstuttgart.typeinference.unify.model.MPair;
 import de.dhbwstuttgart.typeinference.unify.model.SimpleType;
 import de.dhbwstuttgart.typeinference.unify.model.SuperType;
 import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
-import de.dhbwstuttgart.typeinference.unifynew.RuleSet;
 
 
 public class RuleSetTest {
diff --git a/test/unify/StandardUnifyTest.java b/test/unify/StandardUnifyTest.java
index e75bf38c..ac6e5c0c 100644
--- a/test/unify/StandardUnifyTest.java
+++ b/test/unify/StandardUnifyTest.java
@@ -7,11 +7,11 @@ import junit.framework.Assert;
 
 import org.junit.Test;
 
+import de.dhbwstuttgart.typeinference.unify.MartelliMontanariUnify;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IUnify;
 import de.dhbwstuttgart.typeinference.unify.model.MPair;
 import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
 import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
-import de.dhbwstuttgart.typeinference.unifynew.MartelliMontanariUnify;
 
 public class StandardUnifyTest {
 	
diff --git a/test/unify/UnifyTest.java b/test/unify/UnifyTest.java
index e9bed425..8a6f2f32 100644
--- a/test/unify/UnifyTest.java
+++ b/test/unify/UnifyTest.java
@@ -6,12 +6,12 @@ import java.util.Set;
 
 import org.junit.Test;
 
+import de.dhbwstuttgart.typeinference.unify.Unify;
 import de.dhbwstuttgart.typeinference.unify.interfaces.IFiniteClosure;
 import de.dhbwstuttgart.typeinference.unify.model.MPair;
 import de.dhbwstuttgart.typeinference.unify.model.MPair.PairOperator;
 import de.dhbwstuttgart.typeinference.unify.model.UnifyType;
 import de.dhbwstuttgart.typeinference.unify.model.TypeParams;
-import de.dhbwstuttgart.typeinference.unifynew.Unify;
 
 public class UnifyTest extends Unify {