The first three commands in set1.lp declare symbols for use in axiomatizing the properties of sets of elements.

The first declare command introduces names for two sorts,declare sorts E, S declare variables e, e1, e2: E, x, y, z: S declare operators {}: -> S {__}: E -> S insert: E, S -> S __ \union __: S, S -> S __ \in __: E, S -> Bool __ \subseteq __: S, S -> Bool ..

The second command introduces variables ranging over `E`
and `S`. These variables will be used when stating axioms and conjectures.

The third command introduces symbols for the operators whose
properties we will axiomatize. This command uses LP's multi-line input
convention: if the arguments for a command do not
fit on the line containing the command, they can be given on subsequent lines.
Two periods (`..`) mark the end of the command.

The declaration for each operator specifies sorts for the operator's arguments
and the sort of its result. Operators like `{}` with no arguments are
constants. Operators like `insert` are used in functional
notations like `insert(e, x)`. The placeholders in operators like `{__}`
and `__\in__` indicate where their arguments belong in notations like
`{e}` and `e \in x`.