Logic

Definitions and declarations

	Definition of LHS as syntactically equivalent to RHS.
x : T	Declaration of identifier x to stand for a member of the set T (which may be a type name or any expression yielding a set).
x, y : T	Equivalent to x : T, y : T
( )	Groups terms in expressions

Logic

true, false	Logical constants
not P	Negation: ‘not P’.
	Conjunction: ‘P and Q’
	Disjunction: ‘P or Q’
	Implication: ‘P implies Q’ or ‘if P then Q’
	Equivalence: ‘P is logically equivalent to Q’ or ‘P if and only if Q’
	Conditional: ‘if P then Q else R’.
	Universal quantification: ‘for all x in set S, P holds’.
	Existential quantification: ‘there exists an x in S such that P holds’.
	Unique existence: ‘there exists a unique x in S such that P holds’.
	Equality between terms.

Sets

	Set membership: ‘t is a member of S’.
	* not (t * S)
	Set inclusion: ‘every member of S is also in T’.
{ }	The empty set.
	The set containing the terms t1 through tn
#S	Size of the set S
set of S	Powerset: set of all subsets of S.
	The set containing exactly those x in S for which P holds.
	Given declarations D, the set of t’s for which P holds.
	Given declarations D, the set of t’s.
	Ordered tuple of elements
	Set union.
	Set difference.
	Set intersection.
	Distributed set union. Given SS is a set of sets with members taken from S, ‘the union of all the members of all the sets’
	Cartesian product: The set of all 2-tuples such that the first component is a member of S and the second a member of T.
sum S	The numerical sum all of the elements of the set S. Also defined over sequences and bags.
min S	Minimum of a set (or sequence or bag)
max S	Maximum of a set (or sequence or bag)

Functions

The set of total functions from S to T.

Bags

bag of T	The set of bags whose elements are drawn from set T.
#X	The number of elements in bag X
	The empty bag
	The bag containing x1, x2...,xn with the frequency in which they occur in the list.
members X	The set formed from the elements of bag X.

Sequences

seq of T	The set of sequences whose elements are drawn from set T.
#A	The length of sequence A
	The empty sequence
	The sequence containing a1, a2..., and an
	The sequence formed by concatenating the sequence A with the sequence B.
A(n)	The nth element of sequence A.
members A	The set formed from the elements of A.
items A	The bag of items contained in the sequence A.
head A	The first element of a sequence or nil if the sequence is empty.
last A	The last element of a sequence or nil if the sequence is empty.
tail A	All but the head of a sequence.
front A	All but the last of a sequence.

Sorted sequences

The sorted sequence formed by inserting element e into the sorted sequence S, following the sort rule for S.

Objects