Index

A

after, [1] always, [1]

arity atoms

B

bounded model checking

C

commands check commands run commands

E

evaluator

eventually, [1]

F

fields field declaration

H

historically

I

instance

L

lone keyword

M

model checking bounded model checking unbounded model checking multiplicity constraint lone keyword one keyword set keyword some keyword

N

none constant

O

once	one keyword

P

predicates

R

relation abstraction arity bijection entire function injection injective representation simple surjection surjective

relational logic composition transitive closure

S

scopes, [1] exact scopes setting scopes, [1] sig keyword see signature declaration signatures abstract enumeration signatures signature declaration, [1] sub-set signatures top-level signatures variable signatures

solver, [1] some symmetry breaking

T

temporal operator after, [1] always, [1] eventually, [1] historically once

themes customisation, [1] magic layout transition system transitive closure type-system irrelevance error

U

unbounded model checking

V

var keyword variable signatures