This cannot be taken for granted, and for a rewrite theory to be sane, one has to ensure that equational application is confluent and terminating. To prove that term-rewriting terminates is not possible in every instance, which we know from studying the halting problem. To be able to prove that term-rewriting (with regards to the equations) terminates, one can usually create some mapping between terms and the natural numbers, and show that application of the equations reduces the associated value of the term. Induction then proves that it is a halting process since the event of finding smaller natural numbers is a halting process. Naturally equation sets that can cause a term-rewrite to contain cycles will not be terminating. To prove confluence is another important aspect since a rewrite theory lacking this ability will be rather flawed. To prove that the equation set is confluent one has to prove that any application of the equations to any belonging term will lead to the same resulting term (termination is a prerequisite). Details for how to prove termination or confluence will not be given here, it just had to be mentioned, since this is where equations and rewrite-rules differ, which is the next topic of this short overview.