Enter the term ?a+?b using the ``start'' command. Now type the command
The lower occurrence of ?a+?b should be replaced with its right subterm ?b. Now type
up(); (* you should return to the whole term *) left(); (* you should see the left subterm *) left(); (* you should get an error message *) top(); (* takes you back to the top level *)
Enter a more complex term like (?a+?b)+?c+?d and use the movement commands ``right'', ``left'', ``up'', and ``top'' until you have a feeling for how they work. To recover from the Subterm error condition you will have encountered above, either (possibly repeated) use of ``up'' or a single use of ``top'' will work.
The official description of these phenomena follows. The display which you have seen following each application of the ``start'' command shows two terms: the top term is the complete term currently being considered, while the lower term is the ``current subterm'' of that term.
The ``left'' or ``right'' command causes the ``current subterm'' to become the left or right subterm of the erstwhile current subterm. The left or right subterm of an infix term is defined in the obvious way. The left and right subterms of a constant function term [x] are both the subterm x. Atomic identifiers (constant or variable) have no left or right subterms, and so an error condition is reported. Prefix terms do have left subterms (the ``default values'' associated with their prefixes): try entering
start "-?x"; left();
The ``up'' command causes the current subterm to become the smallest subterm of the complete term which properly contains the erstwhile current subterm; if one is at the top level already, an error message is sent. The ``top'' command causes the current subterm to become the complete term under consideration.
The underlying metaphor views terms as (upside-down) trees, with the complete term as the root (at the top!) and each subterm having its immediate subterms growing as branches below it.
The more complex movement commands ``upto'', ``downtoleft'', and ``downtoright'' enable one to move to subterms remote from ones current ``position''; they will be described under the description of individual commands in the Appendix.
If one is in doubt about how to parse a term of the input language, the movement commands provide a way of exploring the structure of a term. For example, the left subterm of ?a+?b+?c+?d is ?a and the right subterm is ?b+?c+?d, which might be a useful discovery if one were uncertain about our associativity convention. Look at the structure of the term ?a*?b+?c (after declaring an operator *); it is not what you might intuitively expect, since there is no precedence of operators in the language.
A command which is often useful is the command
which allows one to see the complete term and the current subterm again; some prover commands leave you not able to see these.