diff --git a/src/main/java/inference/EquationAxiom.java b/src/main/java/inference/EquationAxiom.java
index 29a216b..9d85181 100644
--- a/src/main/java/inference/EquationAxiom.java
+++ b/src/main/java/inference/EquationAxiom.java
@@ -27,27 +27,39 @@
 		super(name, assumptions, conclusion);
 	}
 	
-	public Set<EquationFormula> apply(List<Formula>assumptions,  EvaluatableTerm leftSideHand) {
-		Set<EquationFormula> result = new HashSet<>();
+	public Set<EvaluatableTerm> apply(List<Formula>assumptions,  EvaluatableTerm leftSideHand) {
+		Set<EvaluatableTerm> result = new HashSet<>();
+		boolean isLeft = true;
 		if (assumptions.size() < this.assumptions.size()) {
 			return new HashSet<>();
 		}
-		MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion;
-		Set<MatchConstraint> matchResult = ((MetaRDLTerm) metaConclusion.getLeftSideHand()).isMatchedBy(leftSideHand);
-		if (result.isEmpty()) {
-			return new HashSet<>();
-		}
+		Set<MatchConstraint> matchResult = new HashSet<>();
+		matchResult.add(MatchConstraint.createDefault());
 		for (int i = 0; i < assumptions.size(); i++) {
 			Formula assumption = assumptions.get(i);
 			MetaFormula metaAssumption = this.assumptions.get(i);
 			matchResult = metaAssumption.isMatchedBy(assumption, matchResult);
-			if (result.isEmpty()) {
+			if (matchResult.isEmpty()) {
 				return new HashSet<>();
 			}
 		}
-		for (MatchConstraint matchRes: matchResult) {
+		MetaEquationFormula metaConclusion = (MetaEquationFormula) this.conclusion;
+		Set<MatchConstraint> conclusionMatchResult = ((MetaRDLTerm) metaConclusion.getLeftSideHand()).isMatchedBy(leftSideHand, matchResult);
+		if (conclusionMatchResult.isEmpty()) {
+			isLeft = false;
+			conclusionMatchResult = ((MetaRDLTerm) metaConclusion.getRightSideHand()).isMatchedBy(leftSideHand, matchResult);
+			if (conclusionMatchResult.isEmpty()) {
+				return new HashSet<>();
+			}
+		}
+		for (MatchConstraint matchRes: conclusionMatchResult) {
 			try {
-				result.add(metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext()));
+				EquationFormula eq = metaConclusion.substitution(matchRes.getBinding(), matchRes.getContext());
+				if (isLeft) {
+					result.add(eq.getRightSideHand());
+				} else {
+					result.add(eq.getLeftSideHand());
+				}
 			} catch (SubstituteFailedException e) {
 				continue;
 			}
diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java
index a1fea57..c7a2f34 100644
--- a/src/main/java/inference/ProofSystem.java
+++ b/src/main/java/inference/ProofSystem.java
@@ -22,7 +22,7 @@
 
 	//======================Equality Axioms=============================
 	
-	public static final InferenceRule reflexivity = new InferenceRule(
+	public static final EquationAxiom reflexivity = new EquationAxiom(
 			"Reflexivity",
 			List.of(),
 			new MetaEquationFormula(
@@ -31,7 +31,7 @@
 			)
 	);
 	
-	public static final InferenceRule symmetry = new InferenceRule(
+	public static final EquationAxiom symmetry = new EquationAxiom(
 			"Symmetry",
 			List.of(
 					new MetaEquationFormula(
@@ -45,7 +45,7 @@
 			)
 	);
 	
-	public static final InferenceRule transitivity = new InferenceRule(
+	public static final EquationAxiom transitivity = new EquationAxiom(
 			"Transitivity",
 			List.of(
 					new MetaEquationFormula(
@@ -64,7 +64,7 @@
 			
 	);
 	
-	public static final InferenceRule rightSubstitution = new InferenceRule(
+	public static final EquationAxiom rightSubstitution = new EquationAxiom(
 			"Right Substitution",
 			List.of(
 					new MetaEquationFormula(
@@ -120,7 +120,8 @@
 	);
 	
 	
-	public static final InferenceRule leftSubstitution = new InferenceRule(
+	
+	public static final InferenceRule leftSubstitution = new EquationAxiom(
 			"Left Substitution",
 			List.of(
 					new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("se")), new MetaEvaluatableTermVariable(new Variable("te")))
@@ -156,7 +157,7 @@
 	);
 
 	
-	public static final InferenceRule identity = new InferenceRule(
+	public static final EquationAxiom identity = new EquationAxiom(
 			"Identity",
 			List.of(),
 			new MetaEquationFormula(
@@ -178,8 +179,88 @@
 					new MetaEvaluatableTermVariable(new Variable("te"))
 			)
 	);
-//	
-//	public static final InferenceRule mapComposition = new MapComposition();
+	
+	public static final EquationAxiom mapComposition = new EquationAxiom(
+			"Map Composition",
+			List.of(
+					new MetaDependencyFormula(
+							new MetaDynamicDependency(
+									new MetaTermGenerator() {
+										@Override
+										public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+											curIndex -= 2;
+											return new MetaEvaluatableTermVariable(new Variable("te" + curIndex));
+										}
+									},
+									new MetaEvaluatableTermVariable(new Variable("se")),
+									new MetaEvaluatableTermVariable(new Variable("te"))
+							)
+					),
+					new MetaDependencyFormula(
+							new MetaDynamicDependency(
+									new MetaTermGenerator() {
+										@Override
+										public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+											curIndex -= 1;
+											context.put("uIndex", curIndex);
+											return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex));
+										}
+									},
+									new MetaEvaluatableTermVariable(new Variable("te"))
+							)
+					)
+			),
+			new MetaEquationFormula(
+					new MetaDynamicDependencyTerm(
+							new MetaTermGenerator() {
+								@Override
+								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+									curIndex -= 3;
+									if (curIndex % 2 == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
+									} else {
+										return new MetaEvaluatableTermVariable(new Variable("tex" + curIndex / 2));
+									}
+								}
+							},
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaEvaluatableTermVariable(new Variable("te")),
+							new MetaDynamicDependencyTerm(
+									new MetaTermGenerator() {
+										@Override
+										public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+											curIndex -= 1;
+											if (curIndex % 2 == 0) {
+												return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
+											} else {
+												return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
+											}
+										}
+									},
+									new MetaEvaluatableTermVariable(new Variable("te"))
+							)
+					),
+					new MetaDynamicDependencyTerm(
+							new MetaTermGenerator() {
+								@Override
+								public MetaRDLTerm generate(int curIndex, int curDepth, int maxIndex, int maxDepth, Map<String, Object> context) {
+									curIndex -= 1;
+									int uIndex = (Integer) context.get("uIndex");
+									if (curIndex % 2 == 0 && curIndex < uIndex) {
+										return new MetaEvaluatableTermVariable(new Variable("ue" + curIndex / 2));
+									} else if (curIndex < uIndex ){
+										return new MetaEvaluatableTermVariable(new Variable("ve" + curIndex / 2));
+									} else if (curIndex % 2 == 0) {
+										return new MetaEvaluatableTermVariable(new Variable("te" + curIndex / 2));
+									} else {
+										return new MetaEvaluatableTermVariable(new Variable("tex" + curIndex / 2));
+									}
+								}
+							},
+							new MetaEvaluatableTermVariable(new Variable("se"))
+					)
+			)
+	);
 //	
 //	public static final InferenceRule constantness = new Constantness();
 //	
diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java
index abb46b3..f01d76a 100644
--- a/src/test/java/inferencerule/EqualityAxiomTest.java
+++ b/src/test/java/inferencerule/EqualityAxiomTest.java
@@ -1,16 +1,17 @@
 package inferencerule;
 import static org.junit.jupiter.api.Assertions.*;
 
-import java.util.HashSet;
-import java.util.Set;
-
 import org.junit.jupiter.api.Test;
 
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+
 import inference.ProofSystem;
 import models.formulas.DependencyFormula;
 import models.formulas.EquationFormula;
 import models.formulas.Formula;
-import models.terms.DependencyTerm;
+import models.terms.EvaluatableTerm;
 import models.terms.RDLTerm;
 import models.terms.Resource;
 import utils.Utils;
@@ -37,16 +38,16 @@
 		Set<RDLTerm> terms = new HashSet<>();
 		terms.add(a);
 		terms.add(b);
-		Set<Formula> formulas = ProofSystem.reflexivity.apply(new HashSet<>(), terms);
-		assertTrue(formulas.contains(new EquationFormula(a, a)));
-		assertTrue(formulas.contains(new EquationFormula(b, b)));
+		Set<EvaluatableTerm> formulas = ProofSystem.reflexivity.apply(List.of(), a);
+		assertTrue(formulas.contains(a));
 	}
 	
 	@Test
 	void SymmetryTest() {
-		Set<Formula> formulas = ProofSystem.symmetry.apply(Set.of(new EquationFormula(a, b), new EquationFormula(new DependencyTerm(a, b, c), d)), Set.of());
-		assertTrue(formulas.contains(new EquationFormula(b, a)));
-		assertTrue(formulas.contains(new EquationFormula(d, new DependencyTerm(a, b, c))));
+		Set<EvaluatableTerm> formulas = ProofSystem.symmetry.apply(List.of(new EquationFormula(a, b)), a);
+		assertTrue(formulas.contains(b));
+		formulas = ProofSystem.symmetry.apply(List.of(new EquationFormula(a, b)), b);
+		assertTrue(formulas.contains(a));
 	}
 	
 	@Test