We write examples using standard mathematical notation, as it will appear on the screen if you use the ProofGeneral interface under XEamcs. If you want to type formulas, we give the table of special symbols, with their ASCII syntax:
| Symbol | ASCII | |
| Universal quantification |  | /\ |
| Existential quantification |  | \/ |
| Conjunction |  | & |
| Disjunction |  | or |
| Less or equal |  | <= |
| Greater or equal |  | >= |
| Different |  | != |
| Belong (in quantification) |  | /\x:A |
What you have to type to enter a formula, is exactly what is obtained when you replace each mathematical symbol by its ASCII equivalent.
For instance, to type 
,
you just type
/\e>R0 \/a>R0/\y (d x y <= a -> d (f x) (f y) <= e)
We assume you read the previous section ! Moreover, you should report to the appendix A to get a detailed desciption of each command.