diff --git a/src/inference/ProofSystem.java b/src/inference/ProofSystem.java
index fc8a6d8..9d3d3b4 100644
--- a/src/inference/ProofSystem.java
+++ b/src/inference/ProofSystem.java
@@ -189,10 +189,56 @@
 			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
 	);
 	
-	private final static InferenceRule PSEUDO_IDENTITY_LAW = null;//疑似恒等性??
+	private final static InferenceRule PSEUDO_IDENTITY_LAW = new InferenceRule("pseudo identity law",
+			List.of(
+					new MetaDependencyFormula(
+							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
+							new MetaResourceVariable(new Variable("v"), new Variable("n"))
+					)
+			),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
+							new MetaResourceVariable(new Variable("v"), new Variable("n")),
+							new MetaResourceVariable(new Variable("v"), new Variable("n"))
+					),
+					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
+			),
+			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
+	);//疑似恒等性??
 	
-	private final static InferenceRule SET_EQUIVALENCE = null;//集合同値性??
-	private final static InferenceRule HOMOMORPHISM = null;//準同型性??
+	private final static InferenceRule SET_EQUIVALENCE = new InferenceRule("set equivalence",
+			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 final static InferenceRule HOMOMORPHISM = new InferenceRule("homomorphism",
+			List.of(new MetaDependencyFormula(
+					new MetaEvaluatableTermVariable(new Variable("se")),
+					new MetaResourceVariable(new Variable("v"))
+			)),
+			new MetaEquationFormula(
+					new MetaRDLTerm(
+							new MetaEvaluatableTermVariable(new Variable("se")),
+							new MetaResourceVariable(new Variable("v")),
+							new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te")))
+					),
+					new MetaRDLTerm(
+							new MetaRDLTerm(
+									new MetaEvaluatableTermVariable(new Variable("se")),
+									new MetaResourceVariable(new Variable("v")),
+									new MetaEvaluatableTermVariable(new Variable("te"))
+							)
+					)
+			)
+	);//準同型性??
 	
 	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
 		return false;