LP, the Larch Prover -- Syntax descriptions

The syntax of LP is described using equations of the form 
<term> ::= <simpleId> | <simpleId> "(" <term>+, ")"
that are interpreted according to the following conventions to mean that a <term> is either a simple identifier or a simple identifier followed by a parenthesized list of terms separated by commas.
chars or "chars"
A terminal symbol
<chars>
A construct defined by a syntax equation
e f
An e followed by (whitespace and) an f
e | f
An e or an f
e ~ f
An e that is not an f
(e)
An e as a syntactic unit, as in (e | f) e. Without parentheses, e | f e is interpreted as e | (f e).
[e]
An optional e
e* or e*, or e*[,]
Zero or more e's, separated respectively by nothing, commas, or optional commas.
e+ or e+, or e+[,]
One or more e's, separated respectively by nothing, commas, or optional commas.