This repository contains Coq scripts to prove some fundamental properties on flat LMNtal, a graph rewriting language.
In particular, LMNtalSyntax.v contains the definitions of syntax and semantics of LMNtal on Coq and the proofs on the theorems about reverse execution by inverted rules and admissible rules of structural congruence, i.e., (E4) and (E8).