In the output, not only we show the upper bound obtained but we also show the results of the intermediate steps performed, which involve computing * ranking functions* and loop invariants.
In order to use the solver, the steps to follow are:

Step 1: Provide a *Cost Equation System*.

- by either typing it in the text-area, or
- uploading a file.

*Entry*. There are three possibilities here:

- manually typing it in the
`Entry`box, - if the CES already contains entries, type in a number in the
`IEntry #`box. - if both boxes are left blank the system will assume that the entry coincides with the first equation as initial entry, with no initial constraint.

*Solve*button.

### Syntax

Equation::= eq(Head, CostExpression, ListOfCalls, ListOfSizeRelations). Head::= Name | Name(Arguments) Arguments ::= Variable | Variable,Arguments ListOfCalls ::= [] |[Head|ListOfCalls] ListOfSizeRelations ::= [] | [SizeRelation|ListOfSizeRelations] SizeRelation ::= Variable Oper LinearExpression Oper ::= >= | <= | = LinearExpression ::= RationalNumber * Variable | RationalNumber * Variable + LinearExpression CostExpression :: = PositiveRationalNumber | nat(LinearExpression) | CostExpression * CostExpression | CostExpression + CostExpression | pow(PositiveRationalNumber,CostExpression) | log(NaturalNumber,CostExpression) | NaturalNumber^CostExpression | max(ListOfCostExpressions) ListOfCostExpressions :: = [] | [CostExpression|ListOfCostExpressions] * A "Name" can be either a sequence of characters between quotes or any sequence of consecutive characters (only letters and numbers) beginning with a lower letter. Examples of valid names are: 'function factorial' factorial factorial1 Examples of invalid names are: Factorial 1factorial function factorial * Variables follows Prolog syntax, i.e., are sequences of characters (letters or numbers) beginning with a capital letter. Examples of valid variables are: X Variable1 * A PositiveRationalNumber has the form NaturalNumber/NaturalNumber * RationalNumber is either a PositiveRationalNumber or -PositiveRationalNumber