Encode simplify rule with a term rewriting systems

[NotBad4U]

The crate term-rewriting-rs could be use to defined some rewriting rules specified in Alethe. This lib is a Rust implementation of first-order term rewriting systems (TRS).

Here is an example of utilisation from the documentation on doc.rs:

let mut sig = Signature::default();

let t = parse_trs(&mut sig,
"A = B;
C = D | E;
F(x_) = G;").expect("parse of A = B; C = D | E; F(x_) = G;");

let term = parse_term(&mut sig, "J(F(C) K(C A))").expect("parse of J(F(C) K(C A))");

let rewritten_terms = &t.rewrite(&term, Strategy::Normal).unwrap();
assert_eq!(rewritten_terms.len(), 1);
assert_eq!(rewritten_terms[0].display(), "J(G K(C A))");

It could be a good alternative to writing all the simplification by hand in simplification.rs and having an algorithm that tries to compose them.