diff --git a/src/main/java/inference/rewrite/RewriteInferenceSystem.java b/src/main/java/inference/rewrite/RewriteInferenceSystem.java
index e7749c2..1e01814 100644
--- a/src/main/java/inference/rewrite/RewriteInferenceSystem.java
+++ b/src/main/java/inference/rewrite/RewriteInferenceSystem.java
@@ -353,6 +353,20 @@
 		return new ResourceTree(resultTree, resultResourceMap);
 	} 
 	
+	private boolean definitionFormulaCheck(Formula formula) {
+		if (formula instanceof EquationFormula equation) {
+			EvaluatableTerm left = equation.getLeftSideHand();
+			return left.getSize() <= 3;
+		} else if (formula instanceof Then then) {
+			Formula f1 = then.getCondition();
+			Formula f2 = then.getResult();
+			if (f1 instanceof EquationFormula eq1 && f2 instanceof EquationFormula eq2) {
+				return eq1.getLeftSideHand().getSize() <= 3 && eq2.getLeftSideHand().getSize() <= 3;
+			}
+		}
+		return false;
+	}
+	
 	private boolean inputFormulaCheck(Formula formula) {
 		if (! (formula instanceof EquationFormula equation)) {
 			return false;
@@ -384,4 +398,5 @@
 	}
 	
 	
+	
 }