Linear Indices in Terms

There are two concepts to address an indirect subterm of a term:

TermSelector

One can use a subterm selector navigate through the tree of the term. [1.2] for instance stands for the third subterm (2, starting at 0) in the second subterm (1) the term. [] stands for term itself.

SubtermSelectors can be wrapped in a TermSelector which selects a term from a sequent. S.3.[1.2] would select the above subterm from the fourth (3) term of the succedent (S) of the sequent.

Linear Indices

This can sometimes be tedious, therefore linearisation of the indices is supported. All indirect subterms are then enumerated in a prefix-tree-visitation manner.

Example

Term TermSelector Linear index
f(g(x,y), z) [] 0
g(x,y) [0] 1
x [0.0] 2
y [0.1] 3
z [1] 4