LP, the Larch Prover -- Sample proof: declarations

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

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 first declare command introduces names for two sorts, E and S. LP predefines the boolean sort 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.