diff --git a/src/main/java/inference/Constantness.java b/src/main/java/inference/Constantness.java
index cc94449..bb8d00d 100644
--- a/src/main/java/inference/Constantness.java
+++ b/src/main/java/inference/Constantness.java
@@ -15,35 +15,43 @@
 import models.terms.meta.MetaResource;
 import models.terms.meta.OrderConstraint;
 import models.terms.meta.OrderVariableConstraint;
+import utils.ExpressionUitls;
 import utils.Permutation;
 
 public class Constantness extends InferenceRule{
 
 	public Constantness() {
 		//todo
-		super("composite mapping", List.of(), null, null);
+		super("composite mapping", List.of(), null, new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m")));
 	}
 	
 	
 	@Override
 	public Set<Formula> apply(List<Formula> assumptions, Set<RDLTerm> existTerms) {
 		Set<Formula> result = new HashSet<>();
-		
 		for (List<Formula> perm : Permutation.permutation(assumptions, assumptions.size())) {
 			Set<MatchConstraint> matchResult = assumptionMatch(perm);
 			for (MatchConstraint constraint: matchResult) {
 				int m = constraint.getOrderConstraint().get(new Variable("m")).getOrder();
-				int n = perm.size() - m;
+				int n = m - perm.size();
+				
+				
+				if (! constraint.getOrderConstraint().containsKey(new Variable("n"))) {
+					constraint.putOrderConstraint(new Variable("n"), new OrderVariableConstraint());
+				}
+				constraint.setOrderConstraint(new Variable("n"), OrderConstraint.EQ, n);
+				
+				if (! this.defaultOrderConstraint.check(constraint.getOrderConstraint())) {
+					continue;
+				}
+				
 				MetaRDLTerm conclusionLsh = createMetaConclusionLsh(0, m-n);
 				MetaEvaluatableTermVariable se = new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"));
 				MetaEquationFormula conclusion = new MetaEquationFormula(conclusionLsh, se);
+				
 				for (RDLTerm term : existTerms) {
-					OrderVariableConstraint orderConst = new OrderVariableConstraint();
-					orderConst.setConstraint(n, OrderConstraint.EQ);
-					MatchConstraint seConst = MatchConstraint.createDefault();
-					seConst.getOrderConstraint().put(new Variable("n"), orderConst);
 					if (! se.isMatchedBy(term).isEmpty()) {
-						constraint.getBinding().put(new Variable("se"), term);
+						constraint.setBinding(new Variable("se"), term);
 						try {
 							result.add(conclusion.substitution(constraint.getBinding()));
 						} catch(SubstituteFailedException e) {
@@ -58,26 +66,37 @@
 	
 	private Set<MatchConstraint> assumptionMatch(List<Formula> assumptions) {
 		Set<MatchConstraint> result = new HashSet<>();
-		result = generateAssumption(0).isMatchedBy(assumptions.get(0));
+		result = generateAssumption(0, false).isMatchedBy(assumptions.get(0));
 		for (int i = 1; i < assumptions.size(); i++) {
-			result = generateAssumption(i).isMatchedBy(assumptions.get(i), result);
+			result = generateAssumption(i, i == assumptions.size() - 1).isMatchedBy(assumptions.get(i), result);
 		}
+		
 		return result;
 	}
 	
-	private MetaEquationFormula generateAssumption(int i) {
-		MetaRDLTerm metaAssumptionLsh = new MetaRDLTerm(
-				new MetaResource(new Variable("r" + i), new Variable("m-" + i)),
-				new MetaEvaluatableTermVariable(new Variable("x" + i)),
-				new MetaEvaluatableTermVariable(new Variable("y" + i))
-		);
-		MetaEvaluatableTermVariable metaAssumptionRsh = new MetaEvaluatableTermVariable(new Variable("t" + i));
-		return new MetaEquationFormula(metaAssumptionLsh, metaAssumptionRsh);
+	private MetaEquationFormula generateAssumption(int i, boolean isLast) {
+		if (isLast) {
+			MetaRDLTerm metaAssumptionLsh = new MetaRDLTerm(
+					new MetaResource(new Variable("r" + i), ExpressionUitls.parse("n + 1")),
+					new MetaEvaluatableTermVariable(new Variable("x" + i)),
+					new MetaEvaluatableTermVariable(new Variable("y" + i))
+			);
+			MetaEvaluatableTermVariable metaAssumptionRsh = new MetaEvaluatableTermVariable(new Variable("t" + i));
+			return new MetaEquationFormula(metaAssumptionLsh, metaAssumptionRsh);
+		} else {
+			MetaRDLTerm metaAssumptionLsh = new MetaRDLTerm(
+					new MetaResource(new Variable("r" + i), ExpressionUitls.parse("m - " + i)),
+					new MetaEvaluatableTermVariable(new Variable("x" + i)),
+					new MetaEvaluatableTermVariable(new Variable("y" + i))
+			);
+			MetaEvaluatableTermVariable metaAssumptionRsh = new MetaEvaluatableTermVariable(new Variable("t" + i));
+			return new MetaEquationFormula(metaAssumptionLsh, metaAssumptionRsh);
+		}
 	}
 	
 	private MetaRDLTerm createMetaConclusionLsh(int depth, int maxRecursion) {
-		int i = maxRecursion - depth;
-		if (depth == maxRecursion) {
+		int i = maxRecursion - depth - 1;
+		if (depth == maxRecursion - 1) {
 			return new MetaRDLTerm(
 					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
 					new MetaResource(new Variable("r" + i), new Variable("m")),
@@ -86,7 +105,7 @@
 		}
 		return new MetaRDLTerm(
 				createMetaConclusionLsh(depth + 1, maxRecursion),
-				new MetaResource(new Variable("r" + i), new Variable("m-"+i)),
+				new MetaResource(new Variable("r" + i),ExpressionUitls.parse("m - " + i)),
 				new MetaEvaluatableTermVariable(new Variable("t" + i))
 		);
 	}
diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java
index ccaf892..eed767d 100644
--- a/src/main/java/inference/InferenceRule.java
+++ b/src/main/java/inference/InferenceRule.java
@@ -27,7 +27,7 @@
 	private final List<MetaFormula> assumptions;
 	@Getter
 	private final MetaFormula conclusion;
-	private final InferenceOrderConstraint defaultOrderConstraint;
+	protected final InferenceOrderConstraint defaultOrderConstraint;
 	
 	private final boolean hasDynamicAssumption;
 	private final AssumptionGenerator generator;
diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java
index 51c6254..aec04d1 100644
--- a/src/main/java/inference/ProofSystem.java
+++ b/src/main/java/inference/ProofSystem.java
@@ -202,38 +202,8 @@
 			)
 	);
 	
-	//todo
-//	public static final InferenceRule constantness = new InferenceRule(
-//			"Constantness",
-//			List.of(),
-//			(i) -> new MetaEquationFormula(
-//					new MetaRDLTerm(
-//							new MetaEvaluatableTermVariable(new Variable("r" + (i + 1)), new Variable("m+" + i)),
-//							new MetaEvaluatableTermVariable(new Variable("x" + (i + 1))),
-//							new MetaEvaluatableTermVariable(new Variable("y" + (i + 1)))
-//					),
-//					new MetaEvaluatableTermVariable(new Variable("t" + (i + 1)))
-//			),
-//			new MetaEquationFormula(
-//					new MetaDynamicTerm(
-//							new MetaTermGenerator() {
-//								@Override
-//								public MetaRDLTerm generate(int index, int depth, boolean isLast) {
-//									if (isLast) {
-//										return new MetaResource(new Variable("se"), new Variable("n"));
-//									} 
-//									return new MetaDynamicTerm(this, new MetaResource(new Variable("r" + (depth + 1)), new Variable("n+" + depth)), new MetaResource(new Variable("t" + (depth + 1))));
-//								}
-//								
-//							},
-//							new MetaResource(new Variable("r1")),
-//							new MetaResource(new Variable("t1"))
-//					),
-//					new MetaResource(new Variable("se"), new Variable("n"))
-//			),
-//			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
-//	);
-//	
+	public static final InferenceRule constantness = new Constantness();
+	
 	public static final InferenceRule rightNormalization = new InferenceRule(
 			"Right Normalization",
 			List.of(
diff --git a/src/main/java/models/terms/meta/MatchConstraint.java b/src/main/java/models/terms/meta/MatchConstraint.java
index 68aa933..5d40446 100644
--- a/src/main/java/models/terms/meta/MatchConstraint.java
+++ b/src/main/java/models/terms/meta/MatchConstraint.java
@@ -25,6 +25,10 @@
 		return new HashMap<>(binding);
 	}
 	
+	public void setBinding(Variable key, RDLTerm value) {
+		this.binding.put(key, value);
+	}
+	
 	public Map<Variable, OrderVariableConstraint> getOrderConstraint() {
 		Map<Variable, OrderVariableConstraint> res = new HashMap<>();
 		for (var key : orderConstraint.keySet()) {
@@ -33,6 +37,14 @@
 		return res;
 	}
 	
+	public void putOrderConstraint(Variable key, OrderVariableConstraint value) {
+		this.orderConstraint.put(key, value);
+	}
+	
+	public void setOrderConstraint(Variable key, OrderConstraint constraint, int value) {
+		this.orderConstraint.get(key).setConstraint(value, constraint);
+	}
+	
 	public static MatchConstraint createDefault() {
 		return new MatchConstraint(new HashMap<>(), new HashMap<>());
 	}
diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java
index 0617ca7..9bd49d2 100644
--- a/src/test/java/inferencerule/EqualityAxiomTest.java
+++ b/src/test/java/inferencerule/EqualityAxiomTest.java
@@ -111,6 +111,44 @@
 	}
 	
 	@Test
+	void ConstantnessTest() {
+		Resource a = new Resource("a", Utils.INT, 3);
+		Resource b = new Resource("b", Utils.INT, 3);
+		Resource c = new Resource("c", Utils.INT, 2);
+		Resource d = new Resource("d", Utils.INT, 2);
+		Resource e = new Resource("e", Utils.INT, 2);
+		Resource f = new Resource("f", Utils.INT, 2);
+		Resource g = new Resource("g", Utils.INT, 1);
+		Resource h = new Resource("h", Utils.INT, 1);
+		
+		DependencyTerm t1 = new DependencyTerm(a, b, c);
+		DependencyTerm t2 = new DependencyTerm(e, f, g);
+		EquationFormula eq1 = new EquationFormula(t1, d);
+		EquationFormula eq2 = new EquationFormula(t2, h);
+		
+		Resource x = new Resource("x", Utils.INT, 2);
+		DependencyTerm t3 = new DependencyTerm(x, a, d);
+		DependencyTerm t4 = new DependencyTerm(t3, e, h);
+		EquationFormula eq3 = new EquationFormula(t4, x);
+		
+		
+		Set<Formula> f1 = ProofSystem.constantness.apply(List.of(eq1, eq2), Set.of(x));
+		assertTrue(f1.contains(eq3));
+		
+		Resource aa = new Resource("a", Utils.INT, 1);
+		Resource bb = new Resource("b", Utils.INT, 1);
+		Resource cc = new Resource("c", Utils.INT, 0);
+		Resource dd = new Resource("d", Utils.INT, 0);
+		Resource yy = new Resource("x", Utils.INT, 0);
+		DependencyTerm t5 = new DependencyTerm(aa, bb, cc);
+		EquationFormula eq4 = new EquationFormula(t5, dd);
+		DependencyTerm t6 = new DependencyTerm(yy, aa, dd);
+		EquationFormula eq5 = new EquationFormula(t6, yy);
+		Set<Formula> f2 = ProofSystem.constantness.apply(List.of(eq4), Set.of(yy));
+		assertTrue(f2.contains(eq5));
+	}
+	
+	@Test
 	void RightNormalizationTest() {
 		Dependency d1 = new Dependency(a, b);
 		Dependency d2 = new Dependency(c, d);