diff --git a/src/main/scala/hb/dhbw/FiniteClosure.scala b/src/main/scala/hb/dhbw/FiniteClosure.scala
index ad41ec8..b61efae 100644
--- a/src/main/scala/hb/dhbw/FiniteClosure.scala
+++ b/src/main/scala/hb/dhbw/FiniteClosure.scala
@@ -7,79 +7,51 @@ final case class RefType(name : String, params : List[Type]) extends Type
 
 class FiniteClosure(val extendsRelations : Set[(RefType, RefType)]){
 
-  def superTypes(of : String) : Set[RefType] = Set(extendsRelations.map(p => (p._1.name, p._2)).toMap.get(of).get)
-  // extendsRelations.filter(p => p._1.name == of).map(p => superTypes(p._1.name)).flatten + extendsRelations.filter(p => p._1.name == of).map(_._1).head
-  def subTypes(of : String) : Set[RefType] =Set(extendsRelations.map(p => (p._1.name, p._2)).toMap.get(of).get)
-    //extendsRelations.filter(p => p._2.name == of).map(p => subTypes(p._2.name)).flatten + extendsRelations.filter(p => p._1.name == of).map(_._1).head
-
-    def getFCType(name : String): RefType ={
-      extendsRelations.map(it => it._1).find(it => it.name == name).get
-    }
-  /*
-
-  def cartesianProduct[A](lists : List[Set[A]]) : Set[List[A]] ={
-
-    def listMultiply[A](inFront: Set[A], list: Set[List[A]]) = list.flatMap(s => inFront.map(element => element :: s))
-
-    if(lists.size == 1) {
-      lists.head.map(it => List(it))
-    }
-    else{
-      listMultiply(lists.head, cartesianProduct(lists.tail))
-    }
-
+  private def calculateSupertypes(of: RefType) ={
+    var rel = Set((of, of))
+    var size = rel.size
+    do {
+      size = rel.size
+      rel = rel ++ reflexiveTypes(rel) ++ transitiveTypes(rel) ++ superClassTypes(rel)
+    }while(rel.size > size)
+    rel.map(_._2)
+  }
+  private def reflexiveTypes(of: Set[(RefType, RefType)]) ={
+    val ref = Set.newBuilder[(RefType, RefType)]
+    ref ++= of.map(pair => (pair._1, pair._1))
+    ref ++= of.map(pair => (pair._2, pair._2))
+    ref.result()
+  }
+  private def transitiveTypes(of: Set[(RefType, RefType)]) ={
+    val ref = Set.newBuilder[(RefType, RefType)]
+    ref ++= of.map(pair => (pair._1, pair._1))
+    ref ++= of.map(pair => (pair._2, pair._2))
+    ref.result()
+  }
+  private def superClassTypes(of: RefType) = {
+    val extendsRelation = extendsRelations.filter(pair => pair._1.name.equals(of.name))
+    extendsRelation.map(p => {
+      val paramMap = p._1.params.zip(of.params).toMap
+      (of,RefType(p._2.name, p._2.params.map(paramMap)))
+    })
+  }
+  private def superClassTypes(of: Set[(RefType, RefType)]) : Set[(RefType, RefType)] ={
+    val sClass = Set.newBuilder[(RefType, RefType)]
+    sClass ++= of.flatMap(pair => Set(pair._2, pair._1)).flatMap(t => superClassTypes(t))
+    sClass.result()
   }
 
-    //Kann wiederverwendet werden:
-    def replaceParams(newType : RefType, replace : RefType): RefType ={
-      val fcType = getFCType(replace.name)
-      val replaceMap : Map[TypeVariable, Type] = fcType.params.map{case t: TypePlaceholder => t}.zip(replace.params).toMap
-      RefType(newType.name, newType.params.map{case t: TypePlaceholder => replaceMap(t) case r: RefType => replaceParams(r, replace) })
-    }
+  def superTypes(of : RefType) : Set[RefType] = calculateSupertypes(of)
 
-    //TODO: Falsche Funktionen
-    def greater(than : SimpleType): Set[SimpleType] = {
-      than match {
-        case RefType(name, params) => {
-          val superTypesNoWildcard = superTypes(name).map(superType => replaceParams(superType, RefType(name, params) ))
-          superTypesNoWildcard
-            .flatMap(superType => {
-              cartesianProduct(superType.params.map(param => greaterArg(param)))
-                .map(parameterList => RefType(superType.name, parameterList))
-            }
-            )
-        }
-        case TypePlaceholder(name) => Set(than)
-      }
+  def isPossibleSupertype(of: String, superType: String): Boolean = {
+    val extendsMap = extendsRelations.map(p => (p._1.name,p._2.name)).toMap
+    var subType = of
+    var isSuperType = false
+    if(subType.equals(superType)) isSuperType = true
+    while(extendsMap.contains(subType)){
+      subType = extendsMap.get(subType).get
+      if(subType.equals(superType)) isSuperType = true
     }
-
-    def smaller(than : SimpleType): Set[SimpleType] = {
-      than match {
-        case RefType(name, params) => {
-          val subTypesNoWildcard = subTypes(name).map(subType => replaceParams(subType, RefType(name, params) ))
-          subTypesNoWildcard
-            .flatMap(subTypes => {
-              cartesianProduct(subTypes.params.map(param => smallerArg(param)))
-                .map(parameterList => RefType(subTypes.name, parameterList))
-            }
-            )
-        }
-        case TypePlaceholder(name) => Set(than)
-      }
-    }
-
-    def greaterArg(t : UnifyType): Set[UnifyType] ={
-      t match { //TODO not recursive yet
-        case RefType(name, params) => Set(t, SuperWildcard(RefType(name, params)), ExtendsWildcard(RefType(name, params)))
-        case other => Set(other)
-      }
-    }
-
-    def smallerArg(t : UnifyType): Set[UnifyType] ={
-      t match { //TODO not recursive yet
-        case RefType(name, params) => Set(t, SuperWildcard(RefType(name, params)), ExtendsWildcard(RefType(name, params)))
-        case other => Set(other)
-      }
-    }
-  */
+    isSuperType
+  }
 }
\ No newline at end of file
diff --git a/src/main/scala/hb/dhbw/Main.scala b/src/main/scala/hb/dhbw/Main.scala
index 879b681..c2b699c 100644
--- a/src/main/scala/hb/dhbw/Main.scala
+++ b/src/main/scala/hb/dhbw/Main.scala
@@ -1,6 +1,6 @@
 package hb.dhbw
 
-import hb.dhbw.Unify.LessDot
+import hb.dhbw.Unify.{Constraint, EqualsDot, LessDot}
 ;
 
 object Main {
@@ -14,9 +14,32 @@ object Main {
     val cart = Unify.cartesianProduct(cTest)
     println(cart)
 
+    val superTypes = fc.superTypes(RefType("List", List(RefType("Object", List()))))
+    println(superTypes)
+
     val step1 = Unify.step1(Set(LessDot(TypeVariable("a"), TypeVariable("b")),
       LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List()))))), fc)
     println(step1)
+
+    println(fc.isPossibleSupertype("MyMap", "List"))
+
+    val eqMatchTest = Set(LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List())))), LessDot(TypeVariable("a"), RefType("ArrayList", List(RefType("Object", List())))))
+    println(Unify.matchRule(eqMatchTest.asInstanceOf[Set[Unify.Constraint]], fc))
+
+    val eqEqualsTest : Set[Constraint] = Set(LessDot(TypeVariable("a"), TypeVariable("b")),LessDot(TypeVariable("b"), TypeVariable("c")), LessDot(TypeVariable("c"), TypeVariable("a")))
+    println(Unify.equalsRule(eqEqualsTest))
+
+    //val eqIsLinkedTest = Set(LessDot(TypeVariable("a"), TypeVariable("c")), LessDot(TypeVariable("b"), TypeVariable("c")))
+    //println(Unify.isLinked(TypeVariable("a"), TypeVariable("b"), eqIsLinkedTest))
+
+    val eqAdoptTest = Set(LessDot(TypeVariable("b"), TypeVariable("a")),LessDot(TypeVariable("a"), RefType("List", List(RefType("Object", List())))), LessDot(TypeVariable("b"), RefType("ArrayList", List(RefType("Object", List())))))
+    println(Unify.adoptRule(eqAdoptTest.asInstanceOf[Set[Constraint]], fc))
+
+    val eqAdaptTest: Set[Constraint] = Set(EqualsDot(TypeVariable("a"), TypeVariable("b")),LessDot(RefType("ArrayList",List(RefType("Test",List()))),RefType("List",List(RefType("Object",List())))))
+    println(Unify.adaptRule(eqAdaptTest, fc))
+
+    val eqReduceTest : Set[Constraint] = Set(EqualsDot(RefType("List",List(RefType("Test",List()))),RefType("List",List(RefType("Object",List())))))
+    println(Unify.reduceRule(eqReduceTest))
     //val replacedType = fc.replaceParams(RefType("List", List(TypePlaceholder("A"))), RefType("ArrayList", List(RefType("String", List()))))
     //println(replacedType)
     //val replacedType2 = fc.replaceParams(RefType("Map", List(RefType("String", List(TypePlaceholder("A"))), TypePlaceholder("B"))), RefType("MyMap", List(RefType("String", List()), RefType("Integer", List()))))
diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala
index 4eb70b2..2818419 100644
--- a/src/main/scala/hb/dhbw/Unify.scala
+++ b/src/main/scala/hb/dhbw/Unify.scala
@@ -17,26 +17,154 @@ object Unify {
       case EqualsDot(TypeVariable(_), TypeVariable(_)) => true
       case _ => false
     })
-    val cLessdotACons: Set[Set[Constraint]] = eq.map(c => c match{
+    val cLessdotACons: Set[Set[Set[Constraint]]] = eq.map(c => c match{
       case LessDot(RefType(name,params), TypeVariable(a)) =>
-        fc.superTypes(name)
-        .map(superType => EqualsDot(TypeVariable(a), RefType(superType.name, superType.params.map(fc.getFCType(name).params.zip(params).toMap))).asInstanceOf[Constraint])
+        fc.superTypes(RefType(name,params))
+        .map(superType => Set(EqualsDot(TypeVariable(a), superType).asInstanceOf[Constraint]))
       case _ => null
     }).filter(s => s!=null)
     //val mutatedCLessdotACons = cartesianProduct(cLessdotACons)
-    val aLessdotCCons: Set[Set[Constraint]] = eq.map(c => c match{
-      case LessDot(TypeVariable(a),RefType(name,params)) =>
-        fc.subTypes(name)
-          .map(subTypes => EqualsDot(TypeVariable(a), RefType(subTypes.name, subTypes.params.map(fc.getFCType(name).params.zip(params).toMap))).asInstanceOf[Constraint])
+    val aLessdotCCons: Set[Set[Set[Constraint]]] = eq.map(c => c match{
+      case LessDot(TypeVariable(a),RefType(name,params)) =>{
+        val bs = eq1.filter(c => c match{
+          case LessDot(TypeVariable(leftSide), TypeVariable(_)) => leftSide.equals(a)
+          case _ => false
+        }).map(p => p.asInstanceOf[LessDot].right).asInstanceOf[Set[TypeVariable]]
+        bs.map(b => {
+          val allSuperTypes = fc.superTypes(RefType(name,params))
+            .map(superType => Set(EqualsDot(b, superType).asInstanceOf[Constraint]))
+          Set(Set(LessDot(b, RefType(name,params))) ++ allSuperTypes
+        )
+        })
+        fc.superTypes(RefType(name,params))
+          .map(superType => Set(EqualsDot(TypeVariable(a), superType).asInstanceOf[Constraint]))
+      }
       case _ => null
     }).filter(s => s!=null)
     //val mutadedALessdotCCons = cartesianProduct(aLessdotCCons)
-    val eqSet = cartesianProduct((Set(Set(eq1))+cLessdotACons+aLessdotCCons).filter(s => !s.isEmpty))
+    val eqSet = cartesianProduct(Set(Set(eq1)) ++ aLessdotCCons ++ cLessdotACons)
     eqSet.map( s => s.flatten)
   }
 
-  def cartesianProduct[A](lists : Set[Set[A]]) : Set[Set[A]] ={
+  private def getALessdotC(from: Set[Constraint]) = from.filter(c => c match{
+    case LessDot(TypeVariable(_), RefType(_,_)) => true
+    case _ => false
+  }).asInstanceOf[Set[LessDot]]
 
+  def matchRule(eq : Set[Constraint], fc: FiniteClosure) = {
+    val aLessdotC = getALessdotC(eq)
+    (eq -- aLessdotC) ++ aLessdotC.map(c => {
+      val smallerC = aLessdotC.find(c2 => c2 != c && c2.left.equals(c.left) && fc.isPossibleSupertype(c2.right.asInstanceOf[RefType].name,c.right.asInstanceOf[RefType].name))
+      if(smallerC.isEmpty){
+        c
+      }else{
+        LessDot(smallerC.get.right, c.right)
+      }
+    }
+    )
+  }
+
+  def reduceRule(eq: Set[Constraint]) =  eq.flatMap(c => c match {
+    case EqualsDot(RefType(an, ap), RefType(bn, bp)) => {
+      if(an.equals(bn)){
+        ap.zip(bp).map(p => EqualsDot(p._1, p._2))
+      }else{
+        Set(LessDot(RefType(an, ap), RefType(bn, bp)))
+      }
+    }
+    case x => Set(x)
+  })
+
+  def swapRule(eq : Set[Constraint]) = eq.map(c => c match {
+    case EqualsDot(RefType(an, ap), TypeVariable(a)) => EqualsDot(TypeVariable(a), RefType(an, ap))
+    case x => x
+  })
+
+  def adaptRule(eq: Set[Constraint], fc: FiniteClosure) = {
+    eq.map(c => c match {
+      case LessDot(RefType(an, ap), RefType(bn, bp)) => {
+        if(fc.isPossibleSupertype(an, bn)){
+          EqualsDot(fc.superTypes(RefType(an, ap)).find(r => r.name.equals(bn)).get, RefType(bn, bp))
+        }else{
+          LessDot(RefType(an, ap), RefType(bn, bp))
+        }
+      }
+      case x => x
+    })
+  }
+
+  def adoptRule(eq: Set[Constraint], fc: FiniteClosure) ={
+    val aLessdota = eq.filter(c => c match{
+      case LessDot(TypeVariable(_), TypeVariable(_)) => true
+      case _ => false
+    }).asInstanceOf[Set[LessDot]]
+    val aLessdotC = getALessdotC(eq)
+    (eq -- aLessdotC) ++ aLessdotC.map(c => {
+      val smallerC = aLessdotC.find(c2 => c2 != c
+        && isLinked(c2.left.asInstanceOf[TypeVariable], c.left.asInstanceOf[TypeVariable], aLessdota)
+      && fc.isPossibleSupertype(c2.right.asInstanceOf[RefType].name,c.right.asInstanceOf[RefType].name))
+      if(smallerC.isEmpty){
+        c
+      }else{
+        LessDot(smallerC.get.right, c.right)
+      }
+    }
+    )
+  }
+
+  private def isLinked(a: TypeVariable, b: TypeVariable, aLessdota: Set[LessDot]): Boolean = {
+    def getRightSides(of: TypeVariable) ={
+      aLessdota.filter(c => c.left.asInstanceOf[TypeVariable].name.equals(of.name))
+    }
+    val rightsides = getRightSides(a).map(c => c.right)
+    if(rightsides.isEmpty){
+      false
+    } else if (rightsides.contains(b)){
+      true
+    }else{
+      rightsides.foldLeft(false)((r, c) => r || isLinked(c.asInstanceOf[TypeVariable],b, aLessdota))
+    }
+  }
+
+  private def findCircles(aLessdota: Set[LessDot]) ={
+    def getRightSides(of: TypeVariable) ={
+      aLessdota.filter(c => c.left.asInstanceOf[TypeVariable].name.equals(of.name))
+    }
+    def findCircle(graph: List[LessDot]): List[LessDot] = {
+      val newAdditions = getRightSides(graph.last.right.asInstanceOf[TypeVariable])
+      var circle: List[LessDot] = List()
+      val iterator = newAdditions.iterator
+      while(iterator.hasNext && circle.isEmpty){
+        val newAdd = iterator.next()
+        if(newAdd.right.equals(graph.head.left)){
+          circle = graph ++ List(newAdd)
+        }else{
+          circle = findCircle(graph ++ List(newAdd))
+        }
+      }
+      circle
+    }
+    aLessdota.view.map(c => findCircle(List(c)))
+  }
+
+  def equalsRule(eq: Set[Constraint]) ={
+    val aLessdota = eq.filter(c => c match{
+      case LessDot(TypeVariable(_), TypeVariable(_)) => true
+      case _ => false
+    }).asInstanceOf[Set[LessDot]]
+    val circle = findCircles(aLessdota).find(!_.isEmpty)
+    if(circle.isDefined){
+      val newEq = eq -- circle.get
+      newEq ++ (circle.get.map(c => EqualsDot(c.left, c.right)))
+    }else{
+      eq
+    }
+  }
+
+  def applyRules(fc: FiniteClosure) ={
+  }
+
+  def cartesianProduct[A](lists : Set[Set[A]]) : Set[Set[A]] ={
     def listMultiply[A](inFront: Set[A], list: Set[Set[A]]) = list.flatMap(s => inFront.map(element => s + element))
 
     if(lists.size == 1) {