diff --git a/src/main/java/inference/InferenceRule.java b/src/main/java/inference/InferenceRule.java index 7c87363..4673023 100644 --- a/src/main/java/inference/InferenceRule.java +++ b/src/main/java/inference/InferenceRule.java @@ -116,10 +116,11 @@ try { Formula res = apply(assumptions, new MatchConstraint(binding, new HashMap<>())); if (res != null) { + // ??? Set constraints = conclusion.isMatchedBy(res); boolean flg = true; for (MatchConstraint constraint : constraints) { - if (! defaultOrderConstraint.check(constraint.getOrderConstraint())) { + if (defaultOrderConstraint != null && ! defaultOrderConstraint.check(constraint.getOrderConstraint())) { flg = false; break; } diff --git a/src/main/java/inference/ProofSystem.java b/src/main/java/inference/ProofSystem.java index 03126a7..1d83544 100644 --- a/src/main/java/inference/ProofSystem.java +++ b/src/main/java/inference/ProofSystem.java @@ -31,160 +31,176 @@ //======================Equality Axioms============================= -// private static final InferenceRule reflexivity = new InferenceRule( -// "Reflexivity", -// List.of(), -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ) -// ); -// -// private static final InferenceRule symmetry = new InferenceRule( -// "Symmetry", -// List.of( -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("se")) -// ) -// ), -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ) -// ); -// -// private static final InferenceRule transitivity = new InferenceRule( -// "Transitivity", -// List.of( -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ), -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ), -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ); -// -// private static final InferenceRule rightSubstitution = new InferenceRule( -// "Right Substitution", -// List.of( -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")) -// ), -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaRDLTerm(new MetaResource(new Variable("r"))) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ), -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ) -// ); -// -// private static final InferenceRule leftSubstitution = new InferenceRule( -// "Left Substitution", -// List.of( -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ), -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")) -// ), -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("ue")), -// new MetaRDLTerm(new MetaResource(new Variable("r"))) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ), -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaResource(new Variable("r")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ) -// ); -// -// private static final InferenceRule identity = new InferenceRule( -// "Identity", -// List.of( -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaRDLTerm(new MetaResource(new Variable("r"))) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaResource(new Variable("r")), -// new MetaResource(new Variable("r")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ) -// ); -// -// private static final InferenceRule mapComposition = new InferenceRule( -// "Map Composition", -// List.of( -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")) -// ), -// new MetaDependencyFormula( -// new MetaResource(new Variable("r")), -// new MetaResource(new Variable("p")) -// ), -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaRDLTerm(new MetaResource(new Variable("p"))) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")), -// new MetaRDLTerm( -// new MetaResource(new Variable("r")), -// new MetaResource(new Variable("p")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ) -// ), -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("p")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ) -// ) -// ); -// -// private static final InferenceRule constantness = new InferenceRule( + public static final InferenceRule reflexivity = new InferenceRule( + "Reflexivity", + List.of(), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + + public static final InferenceRule symmetry = new InferenceRule( + "Symmetry", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("se")) + ) + ), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + + public static final InferenceRule transitivity = new InferenceRule( + "Transitivity", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ), + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ); + + public static final InferenceRule rightSubstitution = new InferenceRule( + "Right Substitution", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("x")), + new MetaEvaluatableTermVariable(new Variable("y")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ) + ); + + public static final InferenceRule leftSubstitution = new InferenceRule( + "Left Substitution", + List.of( + new MetaEquationFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("x")), + new MetaEvaluatableTermVariable(new Variable("y")) + ), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("te")), + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("ue")) + ) + ) + ); + + public static final InferenceRule identity = new InferenceRule( + "Identity", + List.of( + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("x")), + new MetaEvaluatableTermVariable(new Variable("y")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("te")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ); + + public static final InferenceRule mapComposition = new InferenceRule( + "Map Composition", + List.of( + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")) + ), + new MetaDependencyFormula( + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("pe")) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("pe")), + new MetaEvaluatableTermVariable(new Variable("x")), + new MetaEvaluatableTermVariable(new Variable("y")) + ), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaEquationFormula( + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("re")), + new MetaEvaluatableTermVariable(new Variable("pe")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ), + new MetaRDLTerm( + new MetaEvaluatableTermVariable(new Variable("se")), + new MetaEvaluatableTermVariable(new Variable("pe")), + new MetaEvaluatableTermVariable(new Variable("te")) + ) + ) + ); + +// public static final InferenceRule constantness = new InferenceRule( // "Constantness", // List.of( // new MetaInFormula( @@ -347,237 +363,7 @@ new MetaResource(new Variable("p")) ) ); -// -// //======================Set-Theoretic Axioms============================= -// -// private static final InferenceRule memberSubstitution = new InferenceRule( -// "Member Substitution", -// List.of( -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ), -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ) -// ), -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ); -// -// private static final InferenceRule membershipChain = new InferenceRule( -// "Membership Chain", -// List.of( -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ), -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ), -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ); -// -// private static final InferenceRule collectionSubstitution = new InferenceRule( -// "Collection Substitution", -// List.of( -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ), -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("te")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ), -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaEvaluatableTermVariable(new Variable("ue")) -// ) -// ); -// -// private static final InferenceRule setEquivelence = new InferenceRule( -// "Set Equivelence", -// List.of( -// new MetaEquationFormula( -// new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")), -// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))), -// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))) -// ), -// new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0")) -// ); -// -// private static final InferenceRule setHomomorphism = new InferenceRule( -// "Set Homomorphism", -// List.of( -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")) -// ) -// ), -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")), -// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"))) -// ), -// new MetaRDLTerm( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r")), -// new MetaEvaluatableTermVariable(new Variable("te")) -// ) -// ) -// ) -// ); -// -// private static final InferenceRule leftProjection = new InferenceRule( -// "Left Projection", -// List.of( -// new MetaDependencyFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), -// new MetaResource(new Variable("r"), new Variable("m")) -// ), -// new MetaResource(new Variable("q"), new Variable("l")) -// ) -// ), -// new MetaDependencyFormula( -// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))), -// new MetaResource(new Variable("q"), new Variable("l")) -// ) -// ); -// -// private static final InferenceRule rightProjection = new InferenceRule( -// "Right Projection", -// List.of( -// new MetaDependencyFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")), -// new MetaResource(new Variable("r"), new Variable("m")) -// ), -// new MetaResource(new Variable("q"), new Variable("l")) -// ) -// ), -// new MetaDependencyFormula( -// new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))), -// new MetaResource(new Variable("q"), new Variable("l")) -// ) -// ); -// -// private static final InferenceRule domainMembership = new InferenceRule( -// "Domain Membership", -// List.of( -// new MetaEquationFormula( -// new MetaRDLTerm( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r1")), -// new MetaEvaluatableTermVariable(new Variable("t1")) -// ), -// new MetaResource(new Variable("r2")), -// new MetaEvaluatableTermVariable(new Variable("t2")) -// ), -// new MetaResource(new Variable("c")) -// ) -// ), -// new MetaInFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("t1")), -// new MetaResource(new Variable("r2")), -// new MetaEvaluatableTermVariable(new Variable("t2")) -// ), -// new MetaRDLTerm( -// new MetaRDLTerm(new MetaResource(new Variable("r1"))), -// new MetaResource(new Variable("r2")), -// new MetaEvaluatableTermVariable(new Variable("t2")) -// ) -// ) -// ); -// -// private static final InferenceRule codomainMembership = new InferenceRule( -// "Codomain Membership", -// List.of( -// new MetaDependencyFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r1")), -// new MetaEvaluatableTermVariable(new Variable("t1")) -// ), -// new MetaResource(new Variable("r2")) -// ), -// new MetaInFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("t1")), -// new MetaResource(new Variable("r2")), -// new MetaEvaluatableTermVariable(new Variable("t2")) -// ), -// new MetaRDLTerm( -// new MetaRDLTerm( -// new MetaResource(new Variable("r1")) -// ), -// new MetaResource(new Variable("r2")), -// new MetaEvaluatableTermVariable(new Variable("t2")) -// ) -// ) -// ), -// new MetaInFormula( -// new MetaRDLTerm( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r1")), -// new MetaEvaluatableTermVariable(new Variable("t1")) -// ), -// new MetaResource(new Variable("r2")), -// new MetaEvaluatableTermVariable(new Variable("t2")) -// ), -// new MetaRDLTerm( -// new MetaRDLTerm( -// new MetaResource(new Variable("se")) -// ), -// new MetaResource(new Variable("r2")), -// new MetaEvaluatableTermVariable(new Variable("t2")) -// ) -// ) -// ); -// -// private static final InferenceRule codomainMembership2 = new InferenceRule( -// "Codomain Membership2", -// List.of( -// new MetaDependencyFormula( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r1")) -// ), -// new MetaInFormula( -// new MetaEvaluatableTermVariable(new Variable("t1")), -// new MetaRDLTerm( -// new MetaResource(new Variable("r1")) -// ) -// ) -// ), -// new MetaInFormula( -// new MetaRDLTerm( -// new MetaEvaluatableTermVariable(new Variable("se")), -// new MetaResource(new Variable("r1")), -// new MetaEvaluatableTermVariable(new Variable("t1")) -// ), -// new MetaRDLTerm( -// new MetaResource(new Variable("se")) -// ) -// ) -// ); + private static final List axioms = List.of( // reflexivity, diff --git a/src/main/java/models/terms/meta/MetaVariable.java b/src/main/java/models/terms/meta/MetaVariable.java index fdad533..7c8e0fc 100644 --- a/src/main/java/models/terms/meta/MetaVariable.java +++ b/src/main/java/models/terms/meta/MetaVariable.java @@ -169,14 +169,16 @@ @Override public boolean equals(Object another) { - if (another instanceof MetaVariable) { + if (! (another instanceof MetaVariable)) { return false; } MetaVariable anotherVar = (MetaVariable) another; + if (orderVariable != null && !orderVariable.equals(anotherVar.getOrderVariable())) { + return false; + } return super.equals(another) - && variableName.equals(another) + && variableName.equals(anotherVar.getVariableName()) && constraint == anotherVar.getConstraint() - && orderVariable.equals(anotherVar.getOrderVariable()) && orderConstant == anotherVar.getOrderConstant(); } diff --git a/src/test/java/inferencerule/EqualityAxiomTest.java b/src/test/java/inferencerule/EqualityAxiomTest.java new file mode 100644 index 0000000..3d382bc --- /dev/null +++ b/src/test/java/inferencerule/EqualityAxiomTest.java @@ -0,0 +1,107 @@ +package inferencerule; +import static org.junit.jupiter.api.Assertions.*; + +import org.junit.jupiter.api.Test; + +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.Resource; +import utils.Utils; + +public class EqualityAxiomTest { + + Resource a = new Resource("a", Utils.INT, 1); + Resource b = new Resource("b", Utils.INT, 1); + Resource c = new Resource("c", Utils.INT, 1); + Resource d = new Resource("d", Utils.INT, 1); + Resource e = new Resource("e", Utils.INT, 1); + Resource f = new Resource("f", Utils.INT, 1); + Resource g = new Resource("g", Utils.INT, 1); + + @Test + void ReflexivityTest() { + EquationFormula f = new EquationFormula(a, a); + Set results = ProofSystem.reflexivity.apply(List.of(), Set.of(a)); + assertTrue(results.contains(f)); + } + + @Test + void SymmetryTest() { + EquationFormula f1 = new EquationFormula(a, b); + EquationFormula f2 = new EquationFormula(b, a); + assertFalse(f1.equals(f2)); + + Formula result = ProofSystem.symmetry.apply(List.of(f1)); + assertTrue(f2.equals(result)); + } + + @Test + void TransitivitiyTest() { + EquationFormula ab = new EquationFormula(a, b); + EquationFormula bc = new EquationFormula(b, c); + EquationFormula ac = new EquationFormula(a, c); + + Formula result = ProofSystem.transitivity.apply(List.of(ab, bc)); + assertEquals(ac, result); + } + + @Test + void RightSubstitutionTest() { + EquationFormula f1 = new EquationFormula(a, b); + DependencyFormula d1 = new DependencyFormula(c, d); + DependencyTerm t1 = new DependencyTerm(d, f, g); + EquationFormula f2 = new EquationFormula(t1, a); + DependencyTerm t2 = new DependencyTerm(c, d, a); + DependencyTerm t3 = new DependencyTerm(c, d, b); + EquationFormula f3 = new EquationFormula(t2, t3); + Formula result = ProofSystem.rightSubstitution.apply(List.of(f1, d1, f2)); + assertEquals(result, f3); + } + + @Test + void LeftSubstituitionTest() { + EquationFormula f1 = new EquationFormula(a, b); + DependencyFormula d1 = new DependencyFormula(a, c); + DependencyTerm t1 = new DependencyTerm(c, f, g); + EquationFormula f2 = new EquationFormula(t1, d); + DependencyTerm t2 = new DependencyTerm(a, c, d); + DependencyTerm t3 = new DependencyTerm(b, c, d); + EquationFormula f3 = new EquationFormula(t2, t3); + Formula result = ProofSystem.leftSubstitution.apply(List.of(f1, d1, f2)); + assertEquals(result, f3); + } + + @Test + void IdentityTest() { + DependencyTerm t1 = new DependencyTerm(a, f, g); + DependencyTerm t2 = new DependencyTerm(a, a, b); + EquationFormula f1 = new EquationFormula(t1, b); + EquationFormula f2 = new EquationFormula(t2, b); + + Formula result = ProofSystem.identity.apply(List.of(f1)); + assertEquals(f2, result); + } + + @Test + void MapCompositionTest() { + DependencyFormula d1 = new DependencyFormula(a, b); + DependencyFormula d2 = new DependencyFormula(b, c); + DependencyTerm t1 = new DependencyTerm(c, f, g); + EquationFormula f1 = new EquationFormula(t1, d); + + DependencyTerm t2 = new DependencyTerm(b, c, d); + DependencyTerm t3 = new DependencyTerm(a, b, t2); + DependencyTerm t4 = new DependencyTerm(a, c, d); + EquationFormula f2 = new EquationFormula(t3, t4); + + Formula result = ProofSystem.mapComposition.apply(List.of(d1, d2, f1)); + assertEquals(f2, result); + } + +}