diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index a34bce9..887d4cb 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -10,6 +10,7 @@
 import models.terms.meta.MetaEvaluatableTermVariable;
 import models.terms.meta.MetaRDLTerm;
 import models.terms.meta.MetaResourceVariable;
+import models.terms.meta.OrderConstraint;
 
 public class ProofSystem {
 
@@ -41,9 +42,43 @@
 			new MetaDependencyFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaResourceVariable(new Variable("w")))
 	);
 	
-	private final static InferenceRule LEFT_PROJECTION = null;
-	private final static InferenceRule RIGHT_PROJECTION = null;
-	private final static InferenceRule CONSTANT_MAPPING = null; // 定値写像??
+	private final static InferenceRule LEFT_PROJECTION = new InferenceRule("left projection", 
+			List.of(new MetaDependencyFormula(
+								new MetaRDLTerm(
+										new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
+										new MetaResourceVariable(new Variable("v"), new Variable("m"))
+								),
+								new MetaResourceVariable(new Variable("w"), new Variable("l"))
+			)),
+			new MetaDependencyFormula(
+					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))),
+					new MetaResourceVariable(new Variable("w"), new Variable("l"))
+			)
+	);
+	
+	private final static InferenceRule RIGHT_PROJECTION = new InferenceRule("left projection", 
+			List.of(new MetaDependencyFormula(
+								new MetaRDLTerm(
+										new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
+										new MetaResourceVariable(new Variable("v"), new Variable("m"))
+								),
+								new MetaResourceVariable(new Variable("w"), new Variable("l"))
+			)),
+			new MetaDependencyFormula(
+					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"), new Variable("m"))),
+					new MetaResourceVariable(new Variable("w"), new Variable("l"))
+			)
+	);
+	
+	private final static InferenceRule CONSTANT_MAPPING = new InferenceRule("constant mapping", 
+			List.of(),
+			new MetaDependencyFormula(
+					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
+					new MetaResourceVariable(new Variable("v"), new Variable("m"))
+			),
+			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
+	); // 定値写像??
+	
 	private final static InferenceRule ORDER_DESCENTING = null; // 階数降下??
 	
 	private final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement",