diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
index d9de2a3b..2ea63a4a 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/FiniteClosure.java
@@ -81,85 +81,56 @@ public class FiniteClosure implements IFiniteClosure {
 		if(type instanceof FunNType)
 			return computeSmallerFunN((FunNType) type);
 		
-		return computeSmaller(type);
+		Set<UnifyType> ts = new HashSet<>();
+		ts.add(type);
+		return computeSmaller(ts);
 	}
 	
 	/**
 	 * Computes the smaller functions for every type except FunNTypes.
 	 */
-	private Set<UnifyType> computeSmaller(UnifyType type) {
-		// Base Case: The type is in the inheritance tree. Add all children.
-		// This is Case 1 in the definition of the subtyping relation.
-	   	if(inheritanceGraph.containsKey(type)) {
-	   		Set<UnifyType> result = new HashSet<>();
-	   		result.add(type);
-	   		result.addAll(inheritanceGraph.get(type).getContentOfDescendants());
-	   		return result;
-	   	}
-	  
+	private Set<UnifyType> computeSmaller(Set<UnifyType> types) {
+		HashSet<UnifyType> result = new HashSet<>();
+		
 		IUnify unify = new MartelliMontanariUnify();
-		Set<UnifyType> result1 = new HashSet<>();
 		
-		// if T = T' then T <=* T'
-	    result1.add(type); 
-	    
-	    // Permute all params with values that are in smArg() of that type.
-	    // This corresponds to Case 3 in the definition of the subtyping relation.
-		/*{ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
-		for (UnifyType param : type.getTypeParams())
-				paramCandidates.add(smArg(param));
-		permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}*/
-		
-		// This is case 2 of the definition of the subtyping relation.
-		Set<UnifyType> result2 = new HashSet<>();
-		if (strInheritanceGraph.containsKey(type.getName())) {
-			HashSet<UnifyType> candidates = new HashSet<>();
-			// All types with the same name
-			strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent()));
-			//for(UnifyType typePrime : result1) {
-			for (UnifyType theta2 : candidates) {
-				// Find the substitution
-				Optional<Unifier> sigma2Opt = unify.unify(type, theta2);
-				if (!sigma2Opt.isPresent())
-					continue;
-				Unifier sigma2 = sigma2Opt.get();
-				if(sigma2.size() == 0)
-					continue;
-				sigma2.swapPlaceholderSubstitutions(type.getTypeParams());
-				//if(type.equals(theta2))
-				//	continue;
-				Set<UnifyType> theta1s = smaller(theta2);
-				for (UnifyType theta1 : theta1s) {
-					// Because only the most general type is calculated, sigma1 = sigma2
-					UnifyType sigma1Theta1 = sigma2.apply(theta1);
-					result2.add(sigma1Theta1);	
-			     }
-			}
-		}
-		else
-			result2 = result1;
-		
-		// Permute the params again.
-		// This corresponds again to Case 3 of the definition of the subtyping relation.
-		Set<UnifyType> result3 = new HashSet<>();
-		for(UnifyType t : result2) {
-			ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
-			for (UnifyType param : t.getTypeParams())
-				paramCandidates.add(smArg(param));
-	
-			Set<TypeParams> permResult = permuteParams(paramCandidates);
-	
-			for (TypeParams newParams : permResult) {
-				UnifyType tPrime = t.setTypeParams(newParams);
-				if(tPrime.equals(t))
-					result3.add(t);
-				else
-					result3.addAll(smaller(tPrime));
+		for(UnifyType t : types) {
+			
+			// if T = T' then T <* T'
+			result.add(t);
+			
+			// if C<...> <* C<...> then ... (third case in definition of <*)
+			if(t.getTypeParams().size() > 0) {
+				ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
+				for (int i = 0; i < t.getTypeParams().size(); i++)
+					paramCandidates.add(smArg(t.getTypeParams().get(i)));
+				permuteParams(paramCandidates).forEach(x -> result.add(t.setTypeParams(x)));
 			}
 			
-		}	
+			if(!strInheritanceGraph.containsKey(t.getName()))
+				continue;
+			
+			// if T <* T' then sigma(T) <* sigma(T')
+			Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName());
+			for(Node<UnifyType> candidate :  candidates) {
+				UnifyType theta2 = candidate.getContent();
+				Optional<Unifier> optSigma = unify.unify(theta2, t);
+				if(!optSigma.isPresent())
+					continue;
+				
+				Unifier sigma = optSigma.get();
+				sigma.swapPlaceholderSubstitutions(t.getTypeParams());
+				
+				Set<UnifyType> theta1Set = candidate.getContentOfDescendants();
+				
+				for(UnifyType theta1 : theta1Set)
+					result.add(theta1.apply(sigma));
+			}
+		}
 		
-		return result3;
+		if(result.equals(types))
+			return result;
+		return computeSmaller(result);
 	}
 	
 	/**
@@ -190,82 +161,58 @@ public class FiniteClosure implements IFiniteClosure {
 	public Set<UnifyType> greater(UnifyType type) {
 		if(type instanceof FunNType)
 			return computeGreaterFunN((FunNType) type); 
-		return computeGreater(type);
+		
+		Set<UnifyType> ts = new HashSet<>();
+		ts.add(type);
+		return computeGreater(ts);
 	}
  
 	/**
 	 * Computes the greater function for all types except function types.
 	 */
-	protected Set<UnifyType> computeGreater(UnifyType type) {
+	protected Set<UnifyType> computeGreater(Set<UnifyType> types) {
+		HashSet<UnifyType> result = new HashSet<>();
+		
 		IUnify unify = new MartelliMontanariUnify();
-		Set<UnifyType> result1 = new HashSet<>();
 		
-		// The type is in the inheritance tree. Add all children.
-		// This is Case 1 in the definition of the subtyping relation.
-	   	if(inheritanceGraph.containsKey(type))
-	   		result1.addAll(inheritanceGraph.get(type).getContentOfPredecessors());
-		
-		// if T = T' then T <=* T'
-	    result1.add(type); 
-	    
-	    // Permute all params with values that are in smArg() of that type.
-	    // This corresponds to Case 3 in the definition of the subtyping relation.
-		/*{ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
-		for (UnifyType param : type.getTypeParams())
-				paramCandidates.add(grArg(param));
-		permuteParams(paramCandidates).forEach(x -> result1.add(type.setTypeParams(x)));}*/
-		
-		// This is case 2 of the definition of the subtyping relation.
-		Set<UnifyType> result2 = new HashSet<>();
-		if (strInheritanceGraph.containsKey(type.getName()) && !inheritanceGraph.containsKey(type)) {
-			HashSet<UnifyType> candidates = new HashSet<>();
-			// All types with the same name
-			strInheritanceGraph.get(type.getName()).forEach(x -> candidates.add(x.getContent()));
-
-			// for(UnifyType typePrime : result1)
-			for (UnifyType theta2 : candidates) {
-				// Find the substitution
-				Optional<Unifier> sigma2Opt = unify.unify(type, theta2);
-				if (!sigma2Opt.isPresent())
-					continue;
-				//if (type.equals(theta2))
-				//	continue;
-				Unifier sigma2 = sigma2Opt.get();
-				if(sigma2.size() == 0) // type.equals(theta2)
-					continue;
-				sigma2.swapPlaceholderSubstitutionsReverse(type.getTypeParams());
-				Set<UnifyType> theta1s = greater(theta2);
-				for (UnifyType theta1 : theta1s) {
-					// Because only the most general type is calculated, sigma1
-					// = sigma2
-					UnifyType sigma1Theta1 = sigma2.apply(theta1);
-					result2.add(sigma1Theta1);
-				}
-			// }
-			}
-		}
-		
-		result2.addAll(result1);
-		
-		// Permute the params again.
-		// This corresponds again to Case 3 of the definition of the subtyping relation.
-		Set<UnifyType> result3 = new HashSet<>();
-		for(UnifyType t : result2) {
-			ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
-			for (UnifyType param : t.getTypeParams())
-				paramCandidates.add(grArg(param));
-	
-			for (TypeParams newParams : permuteParams(paramCandidates)) {
-				UnifyType tPrime = t.setTypeParams(newParams);
-				if(tPrime.equals(t))
-					result3.add(t);
-				else
-					result3.addAll(greater(tPrime));
+		for(UnifyType t : types) {
+			
+			// if T = T' then T <=* T'
+			result.add(t);
+			
+			// if C<...> <* C<...> then ... (third case in definition of <*)			
+			if(t.getTypeParams().size() > 0) {
+				ArrayList<Set<UnifyType>> paramCandidates = new ArrayList<>();
+				for (int i = 0; i < t.getTypeParams().size(); i++)
+					paramCandidates.add(grArg(t.getTypeParams().get(i)));
+				permuteParams(paramCandidates).forEach(x -> result.add(t.setTypeParams(x)));
 			}
 			
-		}	
+			if(!strInheritanceGraph.containsKey(t.getName()))
+				continue;
+			
+			// if T <* T' then sigma(T) <* sigma(T')
+			Set<Node<UnifyType>> candidates = strInheritanceGraph.get(t.getName());
+			for(Node<UnifyType> candidate :  candidates) {
+				UnifyType theta1 = candidate.getContent();
+				Optional<Unifier> optSigma = unify.unify(theta1, t);
+				if(!optSigma.isPresent())
+					continue;
+				
+				Unifier sigma = optSigma.get();
+				sigma.swapPlaceholderSubstitutionsReverse(theta1.getTypeParams());
+				
+				Set<UnifyType> theta2Set = candidate.getContentOfPredecessors();
+				
+				for(UnifyType theta2 : theta2Set)
+					result.add(theta2.apply(sigma));
+			}
+			
+		}
 		
-		return result3;
+		if(result.equals(types))
+			return result;
+		return computeGreater(result);
 	}
 
 	/**