ASCII Symbols for the Abstract Machine Notation

Table of relation types

RELATIONS          Mathematical        Cardinality    Optionality
  Symbol            type               Domain/Range   Domain/Range
             
  <->              relation              many/many  optional/optional  

  +->              partial function      many/one   optional/optional

  -->              total function        many/one  mandatory/optional

  +->>             partial surjection    many/one   optional/mandatory

  -->>             total surjection      many/one  mandatory/mandatory

  >+>              partial injection      one/one   optional/optional

  >->              total injection        one/one  mandatory/optional

  >->>             bijection              one/one  mandatory/mandatory

AMN Symbols

  &                logical and, conjunction

  or               logical disjunction

  =>               logical implication, implies

  <=>              logical equivalence, if and only if

  not              logical negation 

  !                universal quantification, for all

  #                existential quantification, there exists 

  =                equality

  /=               inequality  

  ==               rewrite rule

  |->              ordered pair, maplet

  :                set membership, belongs to, element of 

  /:               set non-membership

  <:               set inclusion, subset of

  /<:              set non-inclusion 

  *                Cartesian product 

  \/               set union 

  /\               set intersection 

  -                set difference 

  {}               empty set, null set

  POW              powerset

  POW1             set of all non-empty subsets 

  FIN              set of all finite subsets 

  FIN1             set of all non-empty finite subsets

  {E}              singleton set

  {E,F}            enumerated set        

  union            generalised union

  inter            generalised intersection 

  UNION(z).(P | E) generalised union

  INTER(z).(P | E) generalised intersection

  >                strict inequality, greater than

  <                strict inequality, less than
   
  >=               inequality, greater than or equal

  <=               inequality, less than or equal

  NAT              set of natural numbers  

  NAT1             set of non-zero natural numbers 

  max              maximum

  min              minimum

  +                addition, plus

  -                difference, minus

  *                product

  /                division

  mod              remainder of integer division

  ..               interval

  card             set cardinality

  SIGMA            summation  

  PI               product

  dom              domain of relation           

  ran              co-domain of relation    

  ;                relational composition

  circ             relational composition

  id               identity relation   

  <|               domain-restriction

  |>               range-restriction

  <<|              anti-domain-restriction

  |>>              anti-range-restriction

  r~               inverse 

  r[s]             image    

  <+  +>           overriding 

  ><               direct product

  ||               parallel product

  iterate(r,n)     iteration     

  closure(r)       reflexive transitive closure

  prj1             projection 

  prj2             projection

  %(z).(P | E)     lambda abstraction

  f(x)             function application

  <>               empty sequence

  seq(S)           set of finite sequences over S

  iseq(S)          set of injective sequences over S

  seq1(S)          set of non-empty sequences over S

  perm(S)          set of bijective sequences over S

  ^                sequence concatenation

  ->               prepend   

  <-               append

  [E]              singleton sequence

  [E,F]            sequence enumeration

  size             sequence size

  rev              sequence reverse

  /|\              sequence projection (prefix)

  \|/              sequence projection (suffix)

  first            first sequence element

  last             last sequence element

  tail             sequence tail

  front            sequence front

  conc             generalised concatenation

  x:=E             simple substitution

  x,y:=E,F         simultaneous substitution

  x::E             membership postconditioned substitution

  x: P             general postconditioned substitution

  S ; T            substitution S followed by substitution T

  skip             no-substitution

  oo <-- op(ii)    parameterised substitution with input ii, output oo

Generalised Substitution Language

  [S]P             substitution application to a predicate P

  [x:= E]F         simple substitution on expression F

  z\A              non-freeness of z in A

  P | S            pre-conditioning of S by P

  P ==> S          guarding of S by P

  S [] T           choice between S and T

  @z.S             unbounded choice

A full on-line help listing is available in the Contents Page
Also available in the form of a complete Index.