rulesubsection23.25ex plus 1ex minus .2ex1.5ex plus .2ex

.`
H >> atom in
by intro
`

`
rulesubsection23.25ex plus
1ex minus .2ex1.5ex plus .2ex`

`"`

`"`

by intro `"`

`"`

.`
H >> "" in atom by intro
`

where `' is any sequence of prl characters.

.`
H >> atom_eq(a;b;t;) in T by intro `

* >> a in atom

* >> b in atom

* a=b in atom >> t in T

* (a=b in atom)->void >> in T

`
rulesubsection23.25ex plus
1ex minus .2ex1.5ex plus .2ex`

.`
H >> atom_eq(a;a;t;)= in T by reduce 1 `

* >> t= in T

whereais a canonical token term.

.`
H >> atom_eq(a;b;t;)= in T by reduce 1 `

* >> = in T

whereaandbare different canonical token terms.

`
`

Thu Sep 14 08:45:18 EDT 1995