Syntropy  Type view  Object diagrams/mechanisms  Statecharts  Logic  Value types  Glossary 
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 
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.  
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 2tuples 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) 
The set of total functions from S to T. 
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. 
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. 
The sorted sequence formed by inserting element e into the sorted sequence S, following the sort rule for S. 
a in Q  True if the object a is in state Q, false otherwise. 