FootNote
An example of such benefits arising from use a theorem prover can be found in
[6]
.