![]() |
CSR |
![]() |
AProVE Help System → User Interface → Graphical User Interface → Selecting Options → User Defined → | CSR |
For input type CSR (Context-Sensitive Rewriting) some special settings are available in user defined mode.
The Context-Sensitive strategy offers the selection of the strategy(1) the prover should show the termination for.
If the Orthogonal checker(2) is active the prover checks whether CSR is orthogonal and in that case it switches to innermost termination.
The CSR to TRS Transformations are selectable
with the Transformations combobox(3) and are added with add.
Every transformation could only be added once.
The prover could only be started with a non-empty list of transformations.
Also the order of them are selectable with
and
.
  removes the selected transformation and
  clears the list of transformations(4).
If the prover is started for a CSR target
the prover tries the first transformation if it succeeds
it goes on with the technique selected in the
TRS Configuration(6)
and Scc Configuration.
If parallel(5) is active the transformations
are processed in parallel and the first proof is shown in the Result tab.