HardExpression = { HardCorner } | { HardCorner } e-variable { HardCorner } | { HardCorner } v-variable { HardCorner }. HardCorner = { HardTerm | NamedExpression }. HardTerm = StaticSymbol | s-variable | t-variable | "(" HardExpression ")".
Thus, any subexpression of a hard expression may contain no more that one occurrence of e-variable or v-variable at the top level of parentheses.
A variable may appear in a hard expression no more that once. If two different variables appear in the same hard expression, they must have different indices.
Hard expressions are denoted by
Hard expressions may be regarded as a particular case of pattern expressions. A feature of
hard expressions is that there can exist no more that one way of matching a ground
expression
A judgment
Here are example hard expressions:
Here are examples of matching hard expressions: