Definition

Hopcroft and Ullman say: a finite automaton over an alphabet is a system where is a finite nonempty set of states, is a finite input alphabet, is a mapping of into , is the initial state, and is the set of final states.

In Nuprl this definition is formalized nearly verbatim. The ``system'' is just an element of a product type. We use the notation Automata to denote the type of all automata with input alphabet and states . An automaton is a triple of transition, initial state and final states.

A automata
Automata ==
A DA_act (the first component of )
A DA_init (the initial state, the second component)
A DA_fin (the final states, the third component)
T DA_act_wf Automata
T DA_init_wf Automata
T DA_fin_wf Automata

The first symbol on the line indicates either an abstraction, , or a theorem, .