diff --git a/src/main/java/Main.java b/src/main/java/Main.java
index 5aad8dd..b4a2d4b 100644
--- a/src/main/java/Main.java
+++ b/src/main/java/Main.java
@@ -8,6 +8,7 @@
 import models.algebra.Expression;
 import models.algebra.Type;
 import models.algebra.Variable;
+import models.formulas.meta.MetaEquationFormula;
 import models.terms.Dependency;
 import models.terms.Resource;
 import models.terms.meta.MetaDynamicDependency;
@@ -16,6 +17,7 @@
 import models.terms.meta.MetaRDLTerm;
 import models.terms.meta.MetaResource;
 import models.terms.meta.MetaTermGenerator;
+import utils.ExpressionUtils;
 
 public class Main {
 
@@ -28,6 +30,7 @@
 		sandbox3();
 		sandbox4();
 		sandbox5();
+		sandbox6();
 	}
 	
 	
@@ -103,4 +106,146 @@
 		System.out.println(d3);
 		System.out.println(md1.isMatchedBy(d3, Map.of("maxOrder", 4)));
 	}
+	
+	
+	static void sandbox6() {
+		MetaDynamicDependency d1 =
+				new MetaDynamicDependency(
+						new MetaTermGenerator() {
+							@Override
+							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+								int i = maxDepth - curDepth;
+								context.put("" + curDepth, curIndex);
+								if (curDepth == maxDepth - 1 && curIndex == 0) {
+									return new MetaDynamicDependency(
+											new MetaTermGenerator() {
+												@Override
+												public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
+													curIndex2 -= 2;
+													context2.put("" + curDepth2, curIndex2 + 1);
+													context2.put("depth", curDepth2);
+													return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2), new Variable("n"));
+												}
+											},
+											new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"))
+									);
+								} else if (curIndex == 0) {
+									return new MetaDynamicDependency(this);
+								}
+								curIndex -= 1;
+								return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
+							}
+						}
+				);
+		Map<String, Object> context = new HashMap<>();
+		var tmp = d1.generate(3, 5, context);
+		System.out.println(tmp);
+		System.out.println(context);
+	}
+	
+	void sandbox7() {
+		var d =new MetaEquationFormula(
+				new MetaDynamicDependencyTerm(
+						new MetaTermGenerator() {
+							@Override
+							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+								int i = maxDepth - curDepth;
+								maxIndex = (Integer) context.get("" + curDepth);
+								if (curDepth == maxDepth - 1 && curIndex == 0) {
+									return new MetaDynamicDependency(
+											new MetaTermGenerator() {
+												@Override
+												public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
+													curIndex2 -= 3;
+													maxIndex2 = (Integer) context.get("" + curDepth2);
+													if (curIndex2 >= maxIndex2 * 2) {
+														return null;
+													}
+													if (curIndex2 % 2 == 0) {
+														return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2), new Variable("n"));
+													} 
+													return new MetaEvaluatableTermVariable(new Variable("x" + curDepth2 + "_" + curIndex2), new Variable("n"));
+												}
+											},
+											new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m"))
+									);
+								}
+								if (curIndex == 0) {
+									return new MetaDynamicDependency(this);
+								}
+								curIndex -= 1;
+								if (curIndex >= maxIndex * 2) {
+									return null;
+								}
+								if (curIndex % 2 == 0) {
+									return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
+								}
+								return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
+							}
+						}
+				),
+				new MetaDynamicDependencyTerm(
+						new MetaTermGenerator() {
+							@Override
+							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+								int m = (Integer) context.get("m");
+								int n = (Integer) context.get("n");
+								int i = maxDepth - curDepth;
+								maxIndex = (Integer) context.get("" + curDepth);
+								if (curDepth == maxDepth - 1 && curIndex == 0) {
+									return new MetaDynamicDependency(
+											new MetaTermGenerator() {
+												@Override
+												public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
+													curIndex2 -= 3;
+													maxIndex2 = (Integer) context.get("" + curDepth2);
+													if (curIndex2 >= maxIndex2 * 2) {
+														return null;
+													}
+													if (curIndex2 % 2 == 0) {
+														return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2), new Variable("n"));
+													} 
+													return new MetaEvaluatableTermVariable(new Variable("x" + curDepth2 + "_" + curIndex2), new Variable("n"));
+												}
+											},
+											new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m"))
+									);
+								}
+								if (curIndex == 0) {
+									return new MetaDynamicDependency(this);
+								}
+								curIndex -= 1;
+								if (n - i == m) {
+									if (curIndex == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m"));
+									}
+									if (curIndex == 1) {
+										return new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m"));
+									}
+									curIndex -= 2;
+									if (curIndex >= maxIndex * 2) {
+										return null;
+									}
+									if (curIndex % 2 == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
+									}
+									return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
+								}
+								if (curIndex >= maxIndex * 2) {
+									return null;
+								}
+								if (curIndex % 2 == 0) {
+									return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
+								}
+								return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
+							}
+						}
+				)
+		);
+	}
 }
diff --git a/src/main/java/inference/axioms/Uncurrying.java b/src/main/java/inference/axioms/Uncurrying.java
index 86d4780..da1d0a2 100644
--- a/src/main/java/inference/axioms/Uncurrying.java
+++ b/src/main/java/inference/axioms/Uncurrying.java
@@ -1,9 +1,246 @@
 package inference.axioms;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+
+import exceptions.SubstituteFailedException;
 import inference.EquationAxiom;
+import models.algebra.Variable;
+import models.formulas.Formula;
+import models.formulas.meta.MetaDependencyFormula;
+import models.formulas.meta.MetaEquationFormula;
+import models.terms.meta.MatchConstraint;
+import models.terms.meta.MetaDependencyTerm;
+import models.terms.meta.MetaDynamicDependency;
+import models.terms.meta.MetaDynamicDependencyTerm;
+import models.terms.meta.MetaEvaluatableTermVariable;
+import models.terms.meta.MetaRDLTerm;
+import models.terms.meta.MetaTermGenerator;
+import utils.ExpressionUtils;
 
 public class Uncurrying extends EquationAxiom {
+	
 	public Uncurrying() {
 		super("Uncurrying");
+		
+		assumptions.add(
+				new MetaDependencyFormula(
+						new MetaDynamicDependency(
+								new MetaTermGenerator() {
+									@Override
+									public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+										int i = maxDepth - curDepth;
+										context.put("" + curDepth, curIndex);
+										context.put("depth", curDepth + 1);
+										if (curDepth == maxDepth - 1 && curIndex == 0) {
+											return new MetaDynamicDependency(
+													new MetaTermGenerator() {
+														@Override
+														public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
+															curIndex2 -= 2;
+															context2.put("" + curDepth2, curIndex2 + 1);
+															context2.put("depth", curDepth2);
+															return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2), new Variable("n"));
+														}
+													},
+													new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
+													new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n"))
+											);
+										} else if (curIndex == 0) {
+											return new MetaDynamicDependency(this);
+										}
+										curIndex -= 1;
+										return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex), ExpressionUtils.parse("n - " + i));
+									}
+								}
+						)
+				)
+		);
+		
+		assumptions.add(
+				new MetaEquationFormula(
+						new MetaDependencyTerm(
+								new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m")),
+								new MetaEvaluatableTermVariable(new Variable("xxx")),
+								new MetaEvaluatableTermVariable(new Variable("yyy"))		
+						),
+						new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m"))
+				)
+		);
+		
+		assumptions.add(
+				new MetaEquationFormula(
+						new MetaDependencyTerm(
+								new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
+								new MetaEvaluatableTermVariable(new Variable("xxxx")),
+								new MetaEvaluatableTermVariable(new Variable("yyyy"))		
+						),
+						new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m"))
+				)
+		);
+		
+		conclusion = new MetaEquationFormula(
+				new MetaDynamicDependencyTerm(
+						new MetaTermGenerator() {
+							@Override
+							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+								int i = maxDepth - curDepth;
+								maxIndex = (Integer) context.get("" + curDepth);
+								if (curDepth == maxDepth - 1 && curIndex == 0) {
+									return new MetaDynamicDependencyTerm(
+											new MetaTermGenerator() {
+												@Override
+												public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
+													curIndex2 -= 3;
+													maxIndex2 = (Integer) context.getOrDefault("" + curDepth2, 0);
+													if (curIndex2 >= maxIndex2 * 2) {
+														return null;
+													}
+													if (curIndex2 % 2 == 0) {
+														return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2 / 2), new Variable("n"));
+													} 
+													return new MetaEvaluatableTermVariable(new Variable("x" + curDepth2 + "_" + curIndex2 / 2), new Variable("n"));
+												}
+											},
+											new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m"))
+									);
+								}
+								if (curIndex == 0) {
+									return new MetaDynamicDependency(this);
+								}
+								curIndex -= 1;
+								if (curIndex >= maxIndex * 2) {
+									return null;
+								}
+								if (curIndex % 2 == 0) {
+									return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
+								}
+								return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
+							}
+						}
+				),
+				new MetaDynamicDependencyTerm(
+						new MetaTermGenerator() {
+							@Override
+							public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+								int m = (Integer) context.get("m");
+								int n = (Integer) context.get("n");
+								int i = maxDepth - curDepth;
+								maxIndex = (Integer) context.get("" + curDepth);
+								if (curDepth == maxDepth - 1 && curIndex == 0) {
+									return new MetaDynamicDependencyTerm(
+											new MetaTermGenerator() {
+												@Override
+												public MetaRDLTerm generate(int curIndex2, int curDepth2, int maxIndex2, int maxDepth2, Map<String, Object> context2) {
+													curIndex2 -= 3;
+													maxIndex2 = (Integer) context.getOrDefault("" + curDepth2, 0);
+													if (curIndex2 >= maxIndex2 * 2) {
+														return null;
+													}
+													if (curIndex2 % 2 == 0) {
+														return new MetaEvaluatableTermVariable(new Variable("v" + curDepth2 + "_" + curIndex2 / 2), new Variable("n"));
+													} 
+													return new MetaEvaluatableTermVariable(new Variable("x" + curDepth2 + "_" + curIndex2 / 2), new Variable("n"));
+												}
+											},
+											new MetaEvaluatableTermVariable(new Variable("s"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("t"), new Variable("n")),
+											new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m"))
+									);
+								}
+								if (curIndex == 0) {
+									return new MetaDynamicDependency(this);
+								}
+								curIndex -= 1;
+								if (n - i == m) {
+									if (curIndex == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("q"), new Variable("m"));
+									}
+									if (curIndex == 1) {
+										return new MetaEvaluatableTermVariable(new Variable("u"), new Variable("m"));
+									}
+									curIndex -= 2;
+									if (curIndex >= maxIndex * 2) {
+										return null;
+									}
+									if (curIndex % 2 == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
+									}
+									return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
+								}
+								if (curIndex >= maxIndex * 2) {
+									return null;
+								}
+								if (curIndex % 2 == 0) {
+									return new MetaEvaluatableTermVariable(new Variable("v" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
+								}
+								return new MetaEvaluatableTermVariable(new Variable("x" + curDepth + "_" + curIndex / 2), ExpressionUtils.parse("n - " + i));
+							}
+						}
+				)
+		);
+		
 	}
-
+	
+	
+	@Override
+	protected Set<Formula> apply(List<Formula> assumptions, MatchConstraint constraint) {
+		
+		Set<MatchConstraint> result = new HashSet<>();
+		Map<String, Object> context = new HashMap<>();
+		result.add(constraint);
+		if (assumptions.size() < 2) {
+			return new HashSet<>();
+		}
+		
+		for (int i = 0; i < 3; i++) {
+			result = this.assumptions.get(i).isMatchedBy(assumptions.get(i), result, context);
+			if (result.isEmpty()) {
+				return new HashSet<>();
+			}
+		}
+		
+		int count = 3;
+		int depth = (Integer) context.get("depth");
+		for (int d = 1; d < depth + 1; d++) {
+			if (! context.containsKey("" + d)) break;
+			for (int i = 0; i < (Integer) context.getOrDefault("" + d, 0); i++) {
+				Formula assumption = assumptions.get(count);
+				MetaEquationFormula mef = new MetaEquationFormula(
+						new MetaDependencyTerm(
+								new MetaEvaluatableTermVariable(new Variable("v" + d + "_" + i), ExpressionUtils.parse("n-" + (depth - d))),
+								new MetaEvaluatableTermVariable(new Variable("xxx" + d + "_" + i)),
+								new MetaEvaluatableTermVariable(new Variable("yyy" + d + "_" + i))
+						),
+						new MetaEvaluatableTermVariable(new Variable("x" + d + "_" + i), ExpressionUtils.parse("n-" + (depth - d)))
+				);
+				result = mef.isMatchedBy(assumption, result, context);
+				if (result.isEmpty()) {
+					return new HashSet<>();
+				}
+				count++;
+			}
+		}
+		
+		Set<Formula> subRes = new HashSet<>();
+		for (MatchConstraint con: result) {
+			try {
+				int maxIndex = 10000;
+				int maxDepth = depth;
+				context.put("maxIndex", maxIndex);
+				context.put("maxDepth", maxDepth);
+				context.put("m", con.getOrderConstraint().get(new Variable("m")).getOrder());
+				context.put("n", con.getOrderConstraint().get(new Variable("n")).getOrder());
+				subRes.add(conclusion.substitution(con.getBinding(), context));
+			} catch (SubstituteFailedException e) {
+				continue;
+			}
+		}
+		return subRes;
+	}
+	
 }
diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java
index 8536cd6..3c242a6 100644
--- a/src/test/java/inferencerule/EqualityAxiomTest.java
+++ b/src/test/java/inferencerule/EqualityAxiomTest.java
@@ -157,6 +157,20 @@
 	}
 	
 	@Test
+	void UncurryingTest() {
+		DependencyFormula d1 = new DependencyFormula(new Dependency(m, n), a);
+		EquationFormula eq1 = Utils.in(c, n);
+		EquationFormula eq2 = Utils.in(b, c);
+		EquationFormula eq3 = Utils.in(d, a);
+		Set<Formula> result = ProofSystem.uncurrying.apply(d1, eq1, eq2, eq3);
+		EquationFormula eq4 = new EquationFormula(
+				new DependencyTerm(new DependencyTerm(m, n, b), a, d),
+				new DependencyTerm(new DependencyTerm(m, n, c), a, d, c, b)
+		);
+		assertTrue(result.contains(eq4));
+	}
+	
+	@Test
 	void ArgumentDependencyExtractionTest() {
 		Set<Formula> result = ProofSystem.argumentDependencyExtraction.apply(
 				new DependencyFormula(a, b, c),