# Theory GExp

subsection ‹Guards Expressions›
text‹
This theory defines the guard language of EFSMs which can be translated directly to and from
contexts. Boolean values true and false respectively represent the guards which are always and never
satisfied. Guards may test for (in)equivalence of two arithmetic expressions or be connected using
\textsc{nor} logic into compound expressions. The use of \textsc{nor} logic reduces the number of
subgoals when inducting over guard expressions.
We also define syntax hacks for the relations less than, less than or equal to, greater than or
equal to, and not equal to as well as the expression of logical conjunction, disjunction, and
negation in terms of nor logic.›
theory GExp
imports AExp Trilean
begin
text_raw‹\snip{gexptype}{1}{2}{%›