diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index 887d4cb..fc8a6d8 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -3,10 +3,13 @@
 import java.util.Collection;
 import java.util.List;
 
+import models.algebra.Constant;
 import models.algebra.Variable;
 import models.formulas.Formula;
 import models.formulas.meta.MetaDependencyFormula;
 import models.formulas.meta.MetaEquationFormula;
+import models.formulas.meta.MetaInFormula;
+import models.terms.meta.MetaDependencyVariable;
 import models.terms.meta.MetaEvaluatableTermVariable;
 import models.terms.meta.MetaRDLTerm;
 import models.terms.meta.MetaResourceVariable;
@@ -79,8 +82,12 @@
 			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
 	); // 定値写像??
 	
-	private final static InferenceRule ORDER_DESCENTING = null; // 階数降下??
-	
+	private final static InferenceRule ORDER_DESCENTING = new InferenceRule("order descenting", 
+			List.of(new MetaDependencyFormula(new MetaDependencyVariable(new Variable("d"), new Variable("n")))),
+			new MetaDependencyFormula(new MetaRDLTerm(new MetaDependencyVariable(new Variable("d"), new Variable("n")))),
+			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
+	); // 階数降下??
+		
 	private final static InferenceRule RIGHT_REPLACEMENT = new InferenceRule("right replacement",
 			List.of(new MetaEquationFormula(new MetaEvaluatableTermVariable(new Variable("te")), new MetaEvaluatableTermVariable(new Variable("ue")))),
 			new MetaEquationFormula(
@@ -97,7 +104,20 @@
 			)
 	);
 	
-	private final static InferenceRule IDENTITY_LAW = null;
+	private final static InferenceRule IDENTITY_LAW = new InferenceRule("identity law", 
+			List.of(new MetaInFormula(
+					new MetaEvaluatableTermVariable(new Variable("te")), 
+					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"))))
+			),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaResourceVariable(new Variable("v")),
+							new MetaResourceVariable(new Variable("v")),
+							new MetaEvaluatableTermVariable(new Variable("te"))
+					),
+					new MetaEvaluatableTermVariable(new Variable("te"))
+			)
+	);
 	
 	private final static InferenceRule JOIN = new InferenceRule("join",
 			List.of(new MetaEquationFormula(new MetaResourceVariable(new Variable("v")), new MetaResourceVariable(new Variable("w")))),
@@ -119,9 +139,58 @@
 			)
 	);
 	
-	private final static InferenceRule CONSTANT_VALUE_LAW = null;//定値性??
-	private final static InferenceRule LINEAR_RIGHT_NORMALIZE = null;
+	private final static InferenceRule CONSTANT_VALUE_LAW = new InferenceRule("constant value law", 
+			List.of(new MetaInFormula(
+					new MetaEvaluatableTermVariable(new Variable("t")), 
+					new MetaRDLTerm(new MetaResourceVariable(new Variable("v"), new Variable("m"))))
+			),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
+							new MetaResourceVariable(new Variable("v"), new Variable("m")),
+							new MetaEvaluatableTermVariable(new Variable("t"))
+					),
+					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
+			),
+			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
+	);//定値性??
+	
+	private final static InferenceRule RIGHT_NORMALIZE = new InferenceRule("right normalize", 
+			List.of(
+					new MetaDependencyFormula(
+							new MetaEvaluatableTermVariable(new Variable("te")),
+							new MetaResourceVariable(new Variable("v"), new Variable("n"))
+					),
+					new MetaDependencyFormula(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("w"), new Variable("n"))
+					)
+			),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaRDLTerm(
+									new MetaEvaluatableTermVariable(new Variable("te")),
+									new MetaResourceVariable(new Variable("v"), new Variable("n")),
+									new MetaEvaluatableTermVariable(new Variable("se"))
+							),
+							new MetaResourceVariable(new Variable("w"), new Variable("n")),
+							new MetaEvaluatableTermVariable(new Variable("ue"))
+					),
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("te")),
+							new MetaResourceVariable(new Variable("v"), new Variable("n")),
+							new MetaRDLTerm(
+									new MetaEvaluatableTermVariable(new Variable("se")),
+									new MetaResourceVariable(new Variable("w"), new Variable("n")),
+									new MetaEvaluatableTermVariable(new Variable("ue"))
+							)
+					)
+			),
+			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
+	);
+	
 	private final static InferenceRule PSEUDO_IDENTITY_LAW = null;//疑似恒等性??
+	
 	private final static InferenceRule SET_EQUIVALENCE = null;//集合同値性??
 	private final static InferenceRule HOMOMORPHISM = null;//準同型性??