package inference;

import java.util.ArrayDeque;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Deque;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Queue;
import java.util.Set;
import java.util.stream.Collectors;

import models.algebra.Constant;
import models.algebra.Variable;
import models.formulas.EquationFormula;
import models.formulas.Formula;
import models.formulas.meta.MetaDependencyFormula;
import models.formulas.meta.MetaEquationFormula;
import models.formulas.meta.MetaInFormula;
import models.terms.EvaluatableTerm;
import models.terms.meta.MetaEvaluatableTermVariable;
import models.terms.meta.MetaRDLTerm;
import models.terms.meta.MetaResourceVariable;
import models.terms.meta.OrderConstraint;
import utils.Product;

public class ProofSystem {

	//MetaExistFormulaのような存在が必要ということを示すFormulaを作ってもいいかも
	//あるいはチェックの時にconclusionのほうから必要なものをあらかじめ抽出しておく
	
	//======================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 MetaResourceVariable(new Variable("r"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaRDLTerm(new MetaResourceVariable(new Variable("r")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(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 MetaResourceVariable(new Variable("r"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("ue")),
							new MetaRDLTerm(new MetaResourceVariable(new Variable("r")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResourceVariable(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 MetaResourceVariable(new Variable("r")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaResourceVariable(new Variable("r")),
							new MetaResourceVariable(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 MetaResourceVariable(new Variable("r"))
					),
					new MetaDependencyFormula(
							new MetaResourceVariable(new Variable("r")),
							new MetaResourceVariable(new Variable("p"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaRDLTerm(new MetaResourceVariable(new Variable("p")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("r")),
							new MetaRDLTerm(
									new MetaResourceVariable(new Variable("r")),
									new MetaResourceVariable(new Variable("p")),
									new MetaEvaluatableTermVariable(new Variable("te"))
							)
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("p")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					)
			)
	);
	
	private static final InferenceRule constantness = new InferenceRule(
			"Constantness",
			List.of(
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("t1")), 
							new MetaRDLTerm(new MetaResourceVariable(new Variable("r1"), new Variable("m")))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n")),
							new MetaResourceVariable(new Variable("r1"), new Variable("m")),
							new MetaEvaluatableTermVariable(new Variable("t1"))
					),
					new MetaEvaluatableTermVariable(new Variable("se"), new Variable("n"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
	);
	
	private static final InferenceRule rightNormalization = new InferenceRule(
			"Right Normalization",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te")),
									new MetaResourceVariable(new Variable("r"), new Variable("n"))
							)
					),
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResourceVariable(new Variable("q"), new Variable("n"))
							)
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te")),
									new MetaResourceVariable(new Variable("r"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("se"))
							),
							new MetaResourceVariable(new Variable("q"), new Variable("n")),
							new MetaEvaluatableTermVariable(new Variable("ue"))
					),
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResourceVariable(new Variable("r"), new Variable("n")),
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResourceVariable(new Variable("q"), new Variable("n")),
									new MetaEvaluatableTermVariable(new Variable("ue"))
							)
					)
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);
	
	private static final InferenceRule pseudoConstantness = new InferenceRule(
			"Pseudo-Constantness",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
									new MetaResourceVariable(new Variable("r"), new Variable("n"))
							)
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
							new MetaResourceVariable(new Variable("r"), new Variable("n")),
							new MetaResourceVariable(new Variable("r"), new Variable("n"))
					),
					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.GT, new Constant("0"))
	);
	
	//======================Dependency Axioms=============================
	
	private static final InferenceRule identityMapping = new InferenceRule(
			"Identity Mapping",
			List.of(
					new MetaEquationFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResourceVariable(new Variable("r"))
					)
			),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaResourceVariable(new Variable("r"))
			)
	);
	
	private static final InferenceRule compositeMapping = new InferenceRule(
			"Composite Mapping",
			List.of(
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResourceVariable(new Variable("r"))
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("r")),
							new MetaResourceVariable(new Variable("q"))
					)
			),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te")),
					new MetaResourceVariable(new Variable("q"))
			)
	);
	
	private static final InferenceRule constantMapping = new InferenceRule(
			"Constant Mapping",
			List.of(),
			new MetaDependencyFormula(
					new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n")),
					new MetaResourceVariable(new Variable("r"), new Variable("m"))
			),
			new InferenceOrderConstraint(new Variable("n"), OrderConstraint.LT, new Variable("m"))
	);
	
	private static final InferenceRule slicedMapping = new InferenceRule(
			"Sliced Mapping",
			List.of(
					new MetaDependencyFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResourceVariable(new Variable("r"))
							),
							new MetaResourceVariable(new Variable("p"))
					),
					new MetaDependencyFormula(
							new MetaEvaluatableTermVariable(new Variable("te")),
							new MetaResourceVariable(new Variable("p"))
					)
			),
			new MetaDependencyFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("r")),
							new MetaEvaluatableTermVariable(new Variable("te"))
					),
					new MetaResourceVariable(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 MetaResourceVariable(new Variable("r"))
					)
			),
			new MetaEquationFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("r")),
							new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te")))
					),
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResourceVariable(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 MetaResourceVariable(new Variable("r"), new Variable("m"))
							),
							new MetaResourceVariable(new Variable("q"), new Variable("l"))
					)
			),
			new MetaDependencyFormula(
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("te"), new Variable("n"))),
					new MetaResourceVariable(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 MetaResourceVariable(new Variable("r"), new Variable("m"))
							),
							new MetaResourceVariable(new Variable("q"), new Variable("l"))
					)
			),
			new MetaDependencyFormula(
					new MetaRDLTerm(new MetaEvaluatableTermVariable(new Variable("r"), new Variable("m"))),
					new MetaResourceVariable(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 MetaResourceVariable(new Variable("r1")),
										new MetaEvaluatableTermVariable(new Variable("t1"))
								),
								new MetaResourceVariable(new Variable("r2")),
								new MetaEvaluatableTermVariable(new Variable("t2"))
							),
							new MetaResourceVariable(new Variable("c"))
					)
			),
			new MetaInFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("t1")),
							new MetaResourceVariable(new Variable("r2")),
							new MetaEvaluatableTermVariable(new Variable("t2"))
					),
					new MetaRDLTerm(
							new MetaRDLTerm(new MetaResourceVariable(new Variable("r1"))),
							new MetaResourceVariable(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 MetaResourceVariable(new Variable("r1")),
									new MetaEvaluatableTermVariable(new Variable("t1"))
							),
							new MetaResourceVariable(new Variable("r2"))
					),
					new MetaInFormula(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("t1")),
									new MetaResourceVariable(new Variable("r2")),
									new MetaEvaluatableTermVariable(new Variable("t2"))
							),
							new MetaRDLTerm(
									new MetaRDLTerm(
											new MetaResourceVariable(new Variable("r1"))
									),
									new MetaResourceVariable(new Variable("r2")),
									new MetaEvaluatableTermVariable(new Variable("t2"))
							)
					)
			),
			new MetaInFormula(
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaEvaluatableTermVariable(new Variable("se")),
									new MetaResourceVariable(new Variable("r1")),
									new MetaEvaluatableTermVariable(new Variable("t1"))
							),
							new MetaResourceVariable(new Variable("r2")),
							new MetaEvaluatableTermVariable(new Variable("t2"))
					),
					new MetaRDLTerm(
							new MetaRDLTerm(
									new MetaResourceVariable(new Variable("se"))
							),
							new MetaResourceVariable(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 MetaResourceVariable(new Variable("r1"))
					),
					new MetaInFormula(
							new MetaEvaluatableTermVariable(new Variable("t1")),
							new MetaRDLTerm(
									new MetaResourceVariable(new Variable("r1"))
							)
					)
			),
			new MetaInFormula(
					new MetaRDLTerm(
							new MetaEvaluatableTermVariable(new Variable("se")),
							new MetaResourceVariable(new Variable("r1")),
							new MetaEvaluatableTermVariable(new Variable("t1"))
					),
					new MetaRDLTerm(
							new MetaResourceVariable(new Variable("se"))
					)
			)
	);

	private static final List<InferenceRule> axioms = List.of(
			reflexivity, 
//			symmetry, 
			transitivity,
			rightSubstitution, 
			leftSubstitution, 
			identity, 
			mapComposition, 
			constantness,
			rightNormalization,
			pseudoConstantness,
			identityMapping,
			compositeMapping,
			constantMapping,
			slicedMapping,
			memberSubstitution, 
			membershipChain, 
			collectionSubstitution,
			setEquivelence,
			setHomomorphism,
			leftProjection,
			rightProjection,
			domainMembership,
			codomainMembership,
			codomainMembership2
	);
	
	public static void debug() {
		for (var axiom : axioms) {
			System.out.println(axiom);
			System.out.println("==================================================================================================");
		}
	}
	
	record AxiomResult(InferenceRule axiom, List<Formula> formulas) {}
	
	public static boolean check(Collection<Formula> assumptions, Formula conclusion) {
		
		Map<Formula, AxiomResult> proofGraph = new HashMap<>();
		Map<InferenceRule, Set<List<Formula>>> appliedFormulas = new HashMap<>(); 
		for (InferenceRule axiom : axioms) {
			appliedFormulas.put(axiom, new HashSet<>());
		}
		
		Set<Formula> appearFormulas = new HashSet<>(assumptions);
		int prevAppearFormulasSize = appearFormulas.size();
		while (! appearFormulas.contains(conclusion)) {
			Set<Formula> derivedFormulas = new HashSet<>();
			for(InferenceRule axiom : axioms) {
				derivedFormulas.addAll(applyAxiom(axiom, appearFormulas, appliedFormulas.get(axiom), proofGraph));
			}
			if (derivedFormulas.size() == 0) {
				return false;
			}
			appearFormulas.addAll(derivedFormulas);
			if (appearFormulas.size() == prevAppearFormulasSize) {
				return false;
			}
			prevAppearFormulasSize = appearFormulas.size();
		}
		
		Queue<Formula> formulaQueue = new ArrayDeque<>();
		Queue<Integer> depthQueue = new ArrayDeque<>();
		List<Formula> formulaResult = new ArrayList<>();
		List<Integer> depthResult = new ArrayList<>();
		Map<Integer, Set<InferenceRule>> usedAxioms = new HashMap<>();
		
		formulaQueue.add(conclusion);
		depthQueue.add(0);
		
		while (formulaQueue.size() != 0) {
			Formula currentFormula = formulaQueue.poll();
			int currentDepth = depthQueue.poll();
			formulaResult.add(currentFormula);
			depthResult.add(currentDepth);
			if (! proofGraph.containsKey(currentFormula)) continue;
			for (Formula nextFormula : proofGraph.get(currentFormula).formulas) {
				formulaQueue.add(nextFormula);
				depthQueue.add(currentDepth + 1);
				if (! usedAxioms.containsKey(currentDepth + 1)) {
					usedAxioms.put(currentDepth + 1, new HashSet<>());
				}
				usedAxioms.get(currentDepth + 1).add(proofGraph.get(currentFormula).axiom);
			}
		}
		int prevDepth = depthResult.get(depthResult.size() - 1);
		List<Formula> sameDepthFormulas = new ArrayList<>();
		for (int i = formulaResult.size() - 1; i >= 0; i--) {
			int currentDepth = depthResult.get(i);
			Formula currentFormula = formulaResult.get(i);
			if (currentDepth != prevDepth) {
				String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(", "));
				String axioms = usedAxioms.get(prevDepth).stream().map(InferenceRule::getName).collect(Collectors.joining(", "));
				System.out.println(out);
				System.out.println("==============================================================(" + axioms + ")");
				sameDepthFormulas.clear();
			}
			prevDepth = currentDepth;
			sameDepthFormulas.add(currentFormula);
			
		}
		String out = sameDepthFormulas.stream().map(String::valueOf).collect(Collectors.joining(","));
		System.out.println(out);
		return true;
	}
	
	private static Set<Formula> applyAxiom(InferenceRule axiom, Set<Formula> formulas, Set<List<Formula>> appliedFormulas,  Map<Formula, AxiomResult> proofGraph) {
		Set<Formula> result = new HashSet<>();
		List<List<Formula>> matchedFormulas = new ArrayList<>();
		for (int i = 0; i < axiom.getAssumptionSize(); i++) {
			matchedFormulas.add(new ArrayList<>());
			for (Formula formula : formulas) {
				if (axiom.getAssumptions().get(i).isMatchedBy(formula)) {
					matchedFormulas.get(i).add(formula);
				}
			}
		}
		for(List<Formula> applyFormulas : Product.product(matchedFormulas)) {
			if (appliedFormulas.contains(applyFormulas)) continue;
			Formula applied = axiom.apply(applyFormulas);
			if (applied != null) {
				result.add(axiom.apply(applyFormulas));
				appliedFormulas.add(applyFormulas);
				proofGraph.put(applied, new AxiomResult(axiom, applyFormulas));
			}
		}
		return result;
	}
	
	private static boolean equationTransitionCheck(Collection<Formula> assumptions, Formula conclusion) {
		if (! (conclusion instanceof EquationFormula)) {
			return false;
		}
		EquationFormula equationConclusion = (EquationFormula) conclusion;
		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = constructEquationGraph(assumptions);
		Deque<EvaluatableTerm> que = new ArrayDeque<>();
		Set<EvaluatableTerm> visited = new HashSet<>();
		que.add(equationConclusion.getLeftSideHand());
		while (! que.isEmpty()) {
			EvaluatableTerm curNode = que.pollFirst();
			if (curNode.equals(equationConclusion.getRightSideHand())) {
				return true;
			}
			for (EvaluatableTerm nextNode : graph.getOrDefault(curNode, new ArrayList<>())) {
				if (visited.contains(nextNode)) {
					continue;
				}
				visited.add(nextNode);
				que.add(nextNode);
			}
		}
		return false;
	}
	
	private static Map<EvaluatableTerm, List<EvaluatableTerm>> constructEquationGraph(Collection<Formula> assumptions) {
		List<EquationFormula> equations = new ArrayList<>();
		for (Formula assumption : assumptions) {
			if (assumption instanceof EquationFormula) {
				equations.add((EquationFormula) assumption);
			}
		}
		
		Map<EvaluatableTerm, List<EvaluatableTerm>> graph = new HashMap<>();
		for (EquationFormula equation : equations) {
			EvaluatableTerm lsh = equation.getLeftSideHand();
			EvaluatableTerm rsh = equation.getRightSideHand();
			if (! graph.containsKey(lsh)) {
				graph.put(lsh, new ArrayList<>());
			}
			if (! graph.containsKey(rsh)) {
				graph.put(rsh, new ArrayList<>());
			}
			graph.get(lsh).add(rsh);
			graph.get(rsh).add(lsh);
		}
		return graph;
	}
}