General
This site provides supporting material for the paper Formalizing Jordan Normal Forms in Isabelle/HOL by René Thiemann and Akihisa Yamada.In automated complexity analysis of term rewriting, estimating the growth rate of the values in Ak - for a fixed matrix A and increasing k - is of fundamental interest. This growth rate can be exactly characterized via A's Jordan normal form (JNF). We formalize this result in our library IsaFoR and our certifier CeTA, and thereby improve the support for certifying polynomial bounds derived by (untrusted) complexity analysis tools.
To this end, we develop a new library for matrices that admits to conveniently work with block matrices. Besides the mentioned complexity result, we formalize Gram-Schmidt's orthogonalization algorithm and Schur decomposition in order to prove existence of JNFs. We also provide a uniqueness result for JNFs which allows us to compute Jordan blocks for individual eigenvalues. In order to determine eigenvalues automatically, we moreover formalize Yun's square-free factorization algorithm.
Formalization
The relevant theories are in the Matrix directory of the sources of IsaFoR/CeTA v2.23.
A compilation of the Isabelle sources requires Isabelle 2015 and the corresponding archive of formal proofs (version afp–2015–08–23 or later). There are also binaries for CeTA available.
To conveniently inspect theories like Matrix.thy, one has to add the following lines into ~/.isabelle/Isabelle2015/etc/settings:
init_component “/the/path/to/afp–2015–08–23” init_component “/the/path/to/CeTA-v2.23”
Afterwards one can navigate into the /the/path/to/CeTA-v2.23/thys/Matrix directory and invoke
/the/path/to/Isabelle2015/bin/isabelle jedit -l QTRS Matrix.thy
For further compilation instructions, we refer to the README-file within the IsaFoR-sources.
Examples
In Section 10 we explicitly mention three examples. The following table contains all the generated proofs for these examples.| Input | CaT-old | CaT-old++ | CaT-new | CaT-new++ | TCT-old | TCT-old++ | TCT-new | TCT-new++ | Old | New++ | ||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| ICFP_2010/96086 | O(k4) | O(k2) | O(k4) | O(k2) | O(k4) | O(k2) | ||||||||
| Mixed_SRS/3 | O(k2) | O(k2) | ||||||||||||
| Transformed_CSR_04/Ex4_7_77_Bor03_iGM | O(k4) | O(k3) | O(k4) | O(k3) | O(k5) | O(k3) | O(k4) | O(k3) | O(k4) | O(k3) |
Experiments - Derivational Complexity
For the following experiments we ran two configurations of CaT (version 1.5) and TCT (version 3.0) on all problems for derivational complexity within TPDB 10.3 The proofs have been generated on a PC with a 3,5 GHz 6-Core Intel Xeon E5 and 32 GB of RAM, using a timeout of 60 seconds. All proofs have been certified by CeTA (version 2.23).
- CaT was configured with two different strategies. Here, CaT-old uses only matrix interpretations of upper-triangular shape, and it infers the complexity by the dimension of the matrix. In contrast, CaT-new combines the various strategies that are described in [15, 17] except for those which are based on joint-spectral radius theory or weighted automata in combination with multiple matrices.
- TCT was configured with two different strategies. Here, TCT-old uses only matrix interpretations of upper-triangular shape, and it infers the complexity by the dimension of the matrix. In contrast, TCT-new determines the complexity by counting ones on the diagonal.
- In the ++-versions, CeTA 2.23 is used as post-processor to optimize the complexity bound: the given bound in the proof is reduced until CeTA no longer accepts the proof.
- The Old-column corresponds to the union of CaT-old and TCT-old, and New++ corresponds to the union of all generated proofs, including CeTA post-processing.
The overview of the results is depicted in the following table.
| Complexity | CaT-old | CaT-old++ | CaT-new | CaT-new++ | TCT-old | TCT-old++ | TCT-new | TCT-new++ | Old | New++ | ||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| O(1) | 0 | 0 | 1 | 1 | 0 | 1 | 1 | 1 | 0 | 1 | ||||
| O(k) | 51 | 83 | 99 | 105 | 46 | 68 | 68 | 68 | 51 | 106 | ||||
| O(k2) | 178 | 202 | 212 | 215 | 160 | 173 | 173 | 174 | 178 | 215 | ||||
| O(k3) | 204 | 219 | 223 | 227 | 177 | 185 | 185 | 186 | 206 | 227 | ||||
| O(k4) | 224 | 224 | 232 | 232 | 184 | 186 | 187 | 187 | 224 | 232 | ||||
| O(k5) | 224 | 224 | 232 | 232 | 186 | 186 | 187 | 187 | 224 | 232 |
In the upcoming table, the detailed results are displayed, where we only list those examples where at least one tool was successful. Moreover, for the ++-configurations, we only display a proof, if it actually improves the initial bound. The best result in each row is displayed with a green background, whereas non-optimal results have a yellow background. All of the proofs are links.
| Input | CaT-old | CaT-old++ | CaT-new | CaT-new++ | TCT-old | TCT-old++ | TCT-new | TCT-new++ | Old | New++ | ||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| AG01/#3.15 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.24 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| AG01/#3.33 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| AG01/#3.35 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.37 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| AG01/#3.56 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.7 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| AotoYamada_05/005 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| AotoYamada_05/017 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| AotoYamada_05/023 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| AotoYamada_05/025 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Applicative_05/Ex2_6_1Composition | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| AProVE_04/Liveness6.2 | O(k4) | O(k2) | O(k4) | O(k2) | ||||||||||
| AProVE_04/Liveness8 | O(k4) | O(k2) | O(k2) | O(k4) | O(k2) | |||||||||
| AProVE_04/Liveness_WRS | O(k3) | O(k2) | O(k2) | O(k3) | O(k2) | |||||||||
| AProVE_10/ex5 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Bouchare_06/02 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| CiME_04/dpqs | O(k2) | O(k2) | ||||||||||||
| Der95/01 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Der95/02 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Der95/03 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Der95/04 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Der95/07 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Der95/09 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Der95/27 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Endrullis_06/direct | O(k4) | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | |||||||
| Endrullis_06/quadruple2 | O(k3) | O(k2) | O(k2) | O(k3) | O(k2) | O(k2) | O(k3) | O(k2) | ||||||
| HirokawaMiddeldorp_04/t006 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| HirokawaMiddeldorp_04/t007 | O(k2) | O(k) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | |||||||
| HirokawaMiddeldorp_04/t010 | O(k2) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | ||||||||
| HirokawaMiddeldorp_04/t011 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| ICFP_2010/159731 | O(k3) | O(k) | O(k) | O(k3) | O(k) | |||||||||
| ICFP_2010/211471 | O(k2) | O(k) | O(k2) | O(k) | O(k2) | O(k) | ||||||||
| ICFP_2010/211857 | O(k4) | O(k3) | O(k3) | O(k4) | O(k3) | |||||||||
| ICFP_2010/212693 | O(k2) | O(k) | O(k2) | O(k) | ||||||||||
| ICFP_2010/213281 | O(k3) | O(k2) | O(k2) | O(k3) | O(k2) | |||||||||
| ICFP_2010/213407 | O(k3) | O(k3) | O(k3) | O(k3) | ||||||||||
| ICFP_2010/230819 | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||||
| ICFP_2010/231480 | O(k2) | O(k) | O(k2) | O(k) | O(k2) | O(k) | ||||||||
| ICFP_2010/25192 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| ICFP_2010/264033 | O(k3) | O(k) | O(k) | O(k3) | O(k) | |||||||||
| ICFP_2010/264370 | O(k2) | O(k) | O(k) | O(k2) | O(k) | |||||||||
| ICFP_2010/264405 | O(k2) | O(k) | O(k) | O(k2) | O(k2) | O(k) | ||||||||
| ICFP_2010/3268 | O(k3) | O(k2) | O(k) | O(k3) | O(k2) | O(k2) | O(k3) | O(k) | ||||||
| ICFP_2010/3336 | O(k3) | O(k) | O(k3) | O(k3) | O(k3) | O(k) | ||||||||
| ICFP_2010/3385 | O(k4) | O(k4) | ||||||||||||
| ICFP_2010/3770 | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||||
| ICFP_2010/4046 | O(k3) | O(k3) | O(k3) | O(k3) | ||||||||||
| ICFP_2010/4970 | O(k3) | O(k2) | O(k3) | O(k2) | O(k3) | O(k2) | ||||||||
| ICFP_2010/54532 | O(k2) | O(k) | O(k2) | O(k) | O(k2) | O(k) | ||||||||
| ICFP_2010/54622 | O(k2) | O(k) | O(k2) | O(k) | O(k2) | O(k) | ||||||||
| ICFP_2010/96086 | O(k4) | O(k2) | O(k4) | O(k2) | O(k4) | O(k2) | ||||||||
| Mixed_SRS/3 | O(k2) | O(k2) | ||||||||||||
| Mixed_SRS/s6 | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||||
| Mixed_SRS/turing_add | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Mixed_TRS/jones1 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Mixed_TRS/jones4 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Mixed_TRS/jones6 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Rubio_04/aoto | O(k2) | O(k) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | |||||||
| Rubio_04/bintrees | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Rubio_04/koen | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Rubio_04/lescanne | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Rubio_04/lindau | O(k3) | O(k2) | O(k) | O(k3) | O(k2) | O(k2) | O(k3) | O(k) | ||||||
| Rubio_04/mfp90b | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Rubio_04/mfp95 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Rubio_04/p266 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Rubio_04/test4 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Rubio_04/test829 | O(k2) | O(k2) | O(k2) | O(k) | O(k) | O(k2) | O(k) | |||||||
| Secret_05_SRS/matchbox2 | O(k4) | O(k3) | O(k) | O(k4) | O(k) | |||||||||
| Secret_05_SRS/torpa3 | O(k2) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | ||||||||
| Secret_06_TRS/6 | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | ||||||||
| Secret_06_TRS/9 | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | ||||||||
| SK90/2.01 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.03 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.04 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.06 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.09 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.11 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.31 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.33 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.36 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.38 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.41 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.46 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.47 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.48 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/2.49 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/2.53 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.54 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.55 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/2.56 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/2.60 | O(k2) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | ||||||||
| SK90/2.61 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/4.01 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/4.04 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.07 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.08 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.11 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.12 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.15 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.16 | O(k2) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | ||||||||
| SK90/4.19 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/4.25 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.29 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.30 | O(k3) | O(k2) | O(k3) | O(k2) | O(k3) | O(k2) | O(k2) | O(k3) | O(k2) | |||||
| SK90/4.33 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/4.35 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| SK90/4.36 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| SK90/4.37 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/4.38 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.39 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.44 | O(k2) | O(k) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | |||||||
| SK90/4.45 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/4.46 | O(k2) | O(k) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | |||||||
| SK90/4.47 | O(k2) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | ||||||||
| SK90/4.48 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| SK90/4.51 | O(k3) | O(k2) | O(k) | O(k3) | O(k2) | O(k2) | O(k3) | O(k) | ||||||
| SK90/4.52 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| SK90/4.56 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Strategy_removed_AG01/#4.20 | O(k2) | O(k) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | |||||||
| Strategy_removed_AG01/#4.20a | O(k2) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | |||||||
| Strategy_removed_AG01/#4.21 | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Strategy_removed_AG01/#4.37 | O(k2) | O(k) | O(k2) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | ||||||
| Strategy_removed_AG01/#4.37a | O(k2) | O(k) | O(k2) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | ||||||
| Strategy_removed_mixed_05/test830 | O(k2) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | |||||||
| Trafo_06/dup16 | O(k) | O(k) | O(k) | O(k) | ||||||||||
| Transformed_CSR_04/Ex15_Luc06_C | O(k4) | O(k4) | O(k4) | O(k4) | ||||||||||
| Transformed_CSR_04/Ex15_Luc06_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex15_Luc06_GM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex15_Luc06_iGM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex15_Luc06_Z | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex18_Luc06_C | O(k4) | O(k3) | O(k4) | O(k3) | O(k4) | O(k3) | ||||||||
| Transformed_CSR_04/Ex18_Luc06_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex18_Luc06_GM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex18_Luc06_iGM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex18_Luc06_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex18_Luc06_Z | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex1_Zan97_C | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex1_Zan97_GM | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex1_Zan97_iGM | O(k2) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | |||||||
| Transformed_CSR_04/Ex23_Luc06_C | O(k4) | O(k4) | ||||||||||||
| Transformed_CSR_04/Ex23_Luc06_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex23_Luc06_GM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex23_Luc06_iGM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex23_Luc06_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex23_Luc06_Z | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex25_Luc06_C | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex25_Luc06_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex25_Luc06_GM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex25_Luc06_iGM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex25_Luc06_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex25_Luc06_Z | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex26_Luc03b_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex2_Luc03b_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex3_3_25_Bor03_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex4_4_Luc96b_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_GM | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | ||||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_iGM | O(k4) | O(k3) | O(k3) | |||||||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_L | O(k2) | O(k) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_Z | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex4_7_77_Bor03_FR | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex4_7_77_Bor03_GM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex4_7_77_Bor03_iGM | O(k4) | O(k3) | O(k4) | O(k3) | O(k5) | O(k3) | O(k4) | O(k3) | O(k4) | O(k3) | ||||
| Transformed_CSR_04/Ex5_Zan97_Z | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex6_GM04_C | O(k4) | O(k3) | O(k3) | O(k4) | O(k3) | |||||||||
| Transformed_CSR_04/Ex6_GM04_GM | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex6_GM04_iGM | O(k2) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | |||||||
| Transformed_CSR_04/Ex6_GM04_L | O(k) | O(1) | O(k) | O(1) | O(1) | O(k) | O(1) | |||||||
| Transformed_CSR_04/Ex6_Luc98_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex9_BLR02_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/Ex9_Luc06_GM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/Ex9_Luc06_iGM | O(k4) | O(k2) | O(k3) | O(k3) | O(k3) | O(k2) | ||||||||
| Transformed_CSR_04/ExConc_Zan97_C | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/ExConc_Zan97_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/ExConc_Zan97_GM | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/ExConc_Zan97_iGM | O(k3) | O(k2) | O(k2) | O(k3) | O(k3) | O(k3) | O(k2) | |||||||
| Transformed_CSR_04/ExConc_Zan97_L | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Transformed_CSR_04/ExIntrod_GM04_GM | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | O(k3) | ||||||||
| Transformed_CSR_04/ExProp7_Luc06_L | O(k2) | O(k2) | ||||||||||||
| Transformed_CSR_04/PALINDROME_nokinds-noand_Z | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/PALINDROME_nokinds_Z | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/PALINDROME_nosorts-noand_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/PALINDROME_nosorts-noand_L | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/PALINDROME_nosorts_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/PEANO_nosorts-noand_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/PEANO_nosorts_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Various_04/07 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Various_04/23 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Various_04/25 | O(k2) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | |||||||
| Various_04/27 | O(k2) | O(k) | O(k) | O(k2) | O(k2) | O(k2) | O(k) | |||||||
| Waldmann_06_SRS/pi | O(k4) | O(k4) | O(k4) | O(k4) | O(k4) | O(k4) | ||||||||
| Zantema_04/z002 | O(k4) | O(k2) | O(k2) | O(k5) | O(k2) | O(k2) | O(k4) | O(k2) | ||||||
| Zantema_04/z006 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_04/z007 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_04/z009 | O(k4) | O(k4) | O(k4) | O(k4) | ||||||||||
| Zantema_04/z024 | O(k3) | O(k) | O(k) | O(k4) | O(k2) | O(k2) | O(k3) | O(k) | ||||||
| Zantema_04/z025 | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||||
| Zantema_04/z049 | O(k4) | O(k2) | O(k2) | O(k4) | O(k2) | O(k2) | O(k4) | O(k2) | ||||||
| Zantema_04/z050 | O(k4) | O(k2) | O(k2) | O(k4) | O(k2) | O(k2) | O(k4) | O(k2) | ||||||
| Zantema_04/z055 | O(k2) | O(k2) | ||||||||||||
| Zantema_04/z061 | O(k4) | O(k3) | O(k) | O(k4) | O(k3) | O(k3) | O(k4) | O(k) | ||||||
| Zantema_04/z062 | O(k4) | O(k2) | O(k) | O(k4) | O(k2) | O(k3) | O(k2) | O(k4) | O(k) | |||||
| Zantema_04/z063 | O(k3) | O(k) | O(k3) | O(k3) | O(k3) | O(k) | ||||||||
| Zantema_04/z064 | O(k4) | O(k2) | O(k2) | O(k4) | O(k2) | |||||||||
| Zantema_04/z066 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_04/z067 | O(k3) | O(k2) | O(k3) | O(k2) | ||||||||||
| Zantema_04/z084 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_04/z085 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Zantema_04/z087 | O(k2) | O(k2) | ||||||||||||
| Zantema_04/z092 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_04/z093 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_04/z101 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Zantema_04/z102 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Zantema_04/z104 | O(k) | O(k) | O(k) | O(k) | ||||||||||
| Zantema_04/z107 | O(k) | O(k) | O(k) | O(k) | ||||||||||
| Zantema_04/z108 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Zantema_04/z109 | O(k) | O(k) | O(k) | O(k) | ||||||||||
| Zantema_04/z112 | O(k) | O(k) | O(k) | O(k) | ||||||||||
| Zantema_04/z115 | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||||
| Zantema_04/z116 | O(k) | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||||
| Zantema_04/z124 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_04/z126 | O(k3) | O(k) | O(k) | O(k3) | O(k) | O(k) | O(k3) | O(k) | ||||||
| Zantema_05/jw43 | O(k3) | O(k2) | O(k) | O(k3) | O(k) | O(k) | O(k3) | O(k) | ||||||
| Zantema_05/jw44 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_05/jw47 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_05/jw50 | O(k3) | O(k) | O(k) | O(k3) | O(k) | O(k) | O(k3) | O(k) | ||||||
| Zantema_05/z26 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||||
| Zantema_06/16 | O(k3) | O(k2) | O(k) | O(k3) | O(k) | |||||||||
| Zantema_06/17 | O(k2) | O(k) | O(k2) | O(k) | ||||||||||
| Zantema_06/18 | O(k3) | O(k2) | O(k2) | O(k3) | O(k2) | |||||||||
| Zantema_06/while2 | O(k4) | O(k3) | O(k2) | O(k4) | O(k3) | O(k3) | O(k4) | O(k2) |
Experiments - Innermost Runtime Complexity
In addition to experiment on derivational complexity, we also investigated innermost runtime complexity proofs. To this end, we ran two configurations of AProVE (version termCOMP 2015) and TCT (version 3.0) on all corresponding problems within TPDB 10.3. We used the same hardware and timeouts as for derivational complexity.
- TCT was configured with two different strategies as before, where again TCT-old uses only matrix interpretations of upper-triangular shape, and it infers the complexity by the dimension of the matrix; and as before, TCT-new determines the complexity by counting ones on the diagonal. However, there is one difference to the derivational complexity category, namely that specific technique for runtime complexity have been added to both configurations, e.g., weak dependency pairs, usable rules, non-linear polynomial orders, etc.
- AProVE is only available in one configuration, AProVE-old, which corresponds to the old version of CeTA. There is no AProVE-new, since currently AProVE has only basic support for complexity of matrix interpretations. Still, we included AProVE in the experiments, as also here the ++-version with CeTA post-processing is available.
- The Old-column corresponds to the union of AProVE-old and TCT-old, and New++ corresponds to the union of all generated proofs, including CeTA post-processing.
The overview of the results is depicted in the following table. Here, the impact of our development is smaller as in the derivational complexity category. This is mainly caused by the strength of the other complexity analysis techniques that are available solely for runtime complexity analysis. Still, the experiments show that the results of our paper can mildly improve the generated complexity bounds, e.g., by admitting a 5 % increase for linear bounds.
| Complexity | AProVE-old | AProVE-old++ | TcT-old | TcT-old++ | TcT-new | TcT-new++ | Old | New++ | |||
|---|---|---|---|---|---|---|---|---|---|---|---|
| O(1) | 1 | 1 | 22 | 26 | 26 | 26 | 22 | 26 | |||
| O(k) | 174 | 180 | 202 | 218 | 217 | 221 | 227 | 239 | |||
| O(k2) | 237 | 240 | 260 | 263 | 265 | 265 | 295 | 299 | |||
| O(k3) | 253 | 253 | 266 | 266 | 267 | 267 | 311 | 312 | |||
| O(k4) | 253 | 253 | 266 | 266 | 267 | 267 | 311 | 312 | |||
| O(k5) | 253 | 253 | 267 | 267 | 268 | 268 | 312 | 313 |
The detailed results can be observed in the following table.
| Input | AProVE-old | AProVE-old++ | TcT-old | TcT-old++ | TcT-new | TcT-new++ | Old | New++ | |||
|---|---|---|---|---|---|---|---|---|---|---|---|
| AG01/#3.1 | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.12 | O(k3) | O(k3) | O(k3) | ||||||||
| AG01/#3.15 | O(k) | O(k) | O(k) | ||||||||
| AG01/#3.16 | O(k3) | O(k3) | O(k3) | ||||||||
| AG01/#3.2 | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.23 | O(k) | O(k) | O(k) | ||||||||
| AG01/#3.24 | O(k) | O(k) | O(k) | ||||||||
| AG01/#3.29 | O(k) | O(k) | O(k) | ||||||||
| AG01/#3.33 | O(k) | O(k) | O(k) | ||||||||
| AG01/#3.35 | O(k) | O(k) | O(k) | ||||||||
| AG01/#3.37 | O(k) | O(k) | O(k) | ||||||||
| AG01/#3.42 | O(k3) | O(k2) | O(k3) | O(k2) | |||||||
| AG01/#3.47 | O(k2) | O(k) | O(k2) | O(k) | |||||||
| AG01/#3.48 | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.5 | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.51 | O(k) | O(k) | O(k) | ||||||||
| AG01/#3.52 | O(k2) | O(k) | O(k2) | O(k) | |||||||
| AG01/#3.53 | O(k3) | O(k3) | O(k3) | ||||||||
| AG01/#3.53a | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| AG01/#3.53b | O(k2) | O(k) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||
| AG01/#3.56 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| AG01/#3.5a | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.5b | O(k3) | O(k3) | O(k3) | ||||||||
| AG01/#3.6 | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.6a | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| AG01/#3.6b | O(k3) | O(k3) | O(k3) | ||||||||
| AG01/#3.7 | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| AG01/#3.8a | O(k2) | O(k2) | O(k2) | ||||||||
| AG01/#3.8b | O(k3) | O(k3) | O(k3) | ||||||||
| AProVE_04/JFP_Ex51 | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| AProVE_04/Liveness6.3 | O(k) | O(k) | O(k) | O(k) | |||||||
| AProVE_07/kabasci03 | O(1) | O(1) | O(1) | O(1) | |||||||
| CiME_04/append | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| CiME_04/dpqs | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| CiME_04/intersect | O(k2) | O(k2) | O(k2) | ||||||||
| CiME_04/lse | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Der95/06 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Der95/07 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Der95/08 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Der95/11 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Der95/18 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Der95/27 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Der95/31 | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| Der95/32 | O(k2) | O(k2) | O(k2) | ||||||||
| Endrullis_06/direct | O(k) | O(k2) | O(k) | O(k2) | O(k) | O(k) | O(k) | ||||
| Frederiksen_Glenstrup/add | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/addlists | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/anchored | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/append | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/assrewrite | O(k) | O(k) | O(k) | O(k) | |||||||
| Frederiksen_Glenstrup/decrease | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/deeprev_typed | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/duplicate | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/evenodd | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/fold | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/game | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/int | O(k) | O(k) | O(k) | O(k) | |||||||
| Frederiksen_Glenstrup/lambdaint_typed | O(k) | O(k) | O(k) | O(k) | |||||||
| Frederiksen_Glenstrup/list | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/lte | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/map0 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/member | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/mergelists | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/mergesort | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Frederiksen_Glenstrup/mul | O(k3) | O(k3) | O(k3) | ||||||||
| Frederiksen_Glenstrup/mul_better | O(k3) | O(k3) | O(k3) | ||||||||
| Frederiksen_Glenstrup/naiverev | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Frederiksen_Glenstrup/nestdec | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/nolexicord | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/ordered | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| Frederiksen_Glenstrup/overlap | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Frederiksen_Glenstrup/revapp | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Glenstrup/select | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Frederiksen_Glenstrup/shuffle | O(k3) | O(k3) | O(k3) | ||||||||
| Frederiksen_Glenstrup/turing_typed | O(k) | O(k) | O(k) | O(k) | |||||||
| Frederiksen_Others/add | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/boolprog | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| Frederiksen_Others/bubblesort | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Frederiksen_Others/disj2_typed | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/div2 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/dup1_typed | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/dup2_typed | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/eq | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/ex6 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/gexgcd | O(k) | O(k) | O(k) | ||||||||
| Frederiksen_Others/gexgcd2 | O(k) | O(k) | O(k) | O(k) | |||||||
| Frederiksen_Others/inssort | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Frederiksen_Others/inssort_better | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Frederiksen_Others/match | O(k2) | O(1) | O(1) | O(1) | O(1) | ||||||
| Frederiksen_Others/ocall-safe | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/ocall-unsafe | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/oddeven | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/permut | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Frederiksen_Others/quicksortPtime | O(k2) | O(k2) | O(k2) | ||||||||
| Frederiksen_Others/strmatch | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Frederiksen_Others/thetrickSize | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| HirokawaMiddeldorp_04/t011 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| HirokawaMiddeldorp_04/t014 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Mixed_TRS/hydra | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Mixed_TRS/jones1 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Mixed_TRS/jones2 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Mixed_TRS/jones4 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Mixed_TRS/jones6 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Mixed_TRS/perfect | O(k) | O(k) | O(k) | O(k) | |||||||
| raML/appendAll.raml | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| raML/clevermmult.raml | O(k2) | O(k2) | O(k2) | ||||||||
| raML/duplicates.raml | O(k2) | O(k2) | O(k2) | ||||||||
| raML/dyade.raml | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| raML/flatten.raml | O(k2) | O(k2) | O(k2) | ||||||||
| raML/minsort.raml | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| raML/rationalPotential.raml | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| raML/subtrees.raml | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Rubio_04/bintrees | O(k) | O(k2) | O(k) | O(k) | O(k) | O(k) | |||||
| Rubio_04/bn122 | O(k2) | O(k2) | O(k) | O(k) | O(k2) | O(k) | |||||
| Rubio_04/division | O(k3) | O(k3) | O(k3) | ||||||||
| Rubio_04/elimdupl | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Rubio_04/enno | O(k2) | O(k2) | O(k2) | ||||||||
| Rubio_04/gcd | O(k2) | O(k2) | O(k2) | ||||||||
| Rubio_04/gm | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| Rubio_04/gmnp | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Rubio_04/koen | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Rubio_04/logarquot | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Rubio_04/mfp95 | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| Rubio_04/p266 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Rubio_04/polo2 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Rubio_04/prov | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Rubio_04/test4 | O(k) | O(k2) | O(k) | O(k) | O(k) | O(k) | |||||
| Rubio_04/test829 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Rubio_04/wst99 | O(k2) | O(k2) | O(k2) | ||||||||
| Secret_05_TRS/cime2 | O(k) | O(k) | O(k) | O(k) | |||||||
| Secret_05_TRS/cime4 | O(k) | O(k) | O(k) | O(k) | |||||||
| Secret_05_TRS/ttt1 | O(1) | O(1) | O(1) | O(1) | |||||||
| Secret_06_TRS/10 | O(k) | O(k) | O(k) | O(k) | |||||||
| Secret_06_TRS/4 | O(k) | O(k) | O(k) | ||||||||
| Secret_06_TRS/6 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Secret_06_TRS/gen-1 | O(k) | O(k) | O(k) | O(k) | |||||||
| Secret_06_TRS/gen-17 | O(k3) | O(k) | O(1) | O(1) | O(1) | O(1) | |||||
| Secret_07_TRS/3 | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Secret_07_TRS/secret5 | O(k) | O(k) | O(k) | O(k) | |||||||
| SK90/2.02 | O(k) | O(k) | O(k) | ||||||||
| SK90/2.03 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.07 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.09 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.11 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.12 | O(k3) | O(k3) | O(k3) | ||||||||
| SK90/2.13 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.14 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.16 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| SK90/2.17 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.18 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| SK90/2.19 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| SK90/2.20 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.22 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| SK90/2.29 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.30 | O(1) | O(1) | O(1) | O(1) | O(1) | ||||||
| SK90/2.31 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.36 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.37 | O(k) | O(k) | O(1) | O(1) | O(k) | O(1) | |||||
| SK90/2.38 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.39 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| SK90/2.40 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.41 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.42 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.44 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.45 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.47 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.48 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.49 | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| SK90/2.50 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.53 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.54 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.55 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.59 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/2.61 | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.05 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| SK90/4.07 | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| SK90/4.09 | O(k2) | O(1) | O(1) | O(1) | O(1) | ||||||
| SK90/4.10 | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| SK90/4.12 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.13 | O(k3) | O(k2) | O(k2) | O(k3) | O(k2) | ||||||
| SK90/4.16 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.17 | O(k3) | O(k2) | O(k3) | O(k2) | |||||||
| SK90/4.18 | O(k2) | O(1) | O(1) | O(1) | O(1) | ||||||
| SK90/4.25 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.26 | O(k) | O(k) | O(k) | ||||||||
| SK90/4.28 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.29 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.30 | O(k) | O(k2) | O(k) | O(k) | O(k) | O(k) | |||||
| SK90/4.35 | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| SK90/4.38 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.45 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.47 | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| SK90/4.48 | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| SK90/4.51 | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.53 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| SK90/4.57 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Strategy_removed_AG01/#4.14 | O(k) | O(k) | O(k) | O(k) | |||||||
| Strategy_removed_AG01/#4.16 | O(k) | O(k) | O(k) | O(k) | |||||||
| Strategy_removed_AG01/#4.17 | O(k) | O(k) | O(k) | O(k) | |||||||
| Strategy_removed_AG01/#4.2 | O(k) | O(k) | O(k) | O(k) | |||||||
| Strategy_removed_AG01/#4.20a | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Strategy_removed_AG01/#4.28 | O(k3) | O(k2) | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||
| Strategy_removed_AG01/#4.32 | O(k2) | O(k) | O(k3) | O(k) | O(k2) | O(k) | O(k2) | O(k) | |||
| Strategy_removed_AG01/#4.34 | O(k2) | O(k) | O(k2) | O(k) | O(k2) | O(k) | O(k2) | O(k) | |||
| Strategy_removed_AG01/#4.37 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Strategy_removed_AG01/#4.37a | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Strategy_removed_AG01/#4.7 | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| Strategy_removed_CSR_05/Ex49_GM04 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Strategy_removed_mixed_05/test830 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Strategy_removed_mixed_05/tricky1 | O(k2) | O(1) | O(1) | O(1) | O(1) | ||||||
| TCT_12/polycounter-5 | O(k5) | O(k5) | O(k5) | O(k5) | |||||||
| TCT_12/sat | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Transformed_CSR_04/Ex14_AEGL02_GM | O(k3) | O(k3) | O(k3) | O(k3) | |||||||
| Transformed_CSR_04/Ex15_Luc06_FR | O(k) | O(k2) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex15_Luc06_GM | O(k) | O(k2) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex15_Luc06_Z | O(k) | O(k2) | O(k) | O(k) | O(k) | O(k) | |||||
| Transformed_CSR_04/Ex15_Luc98_GM | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex18_Luc06_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex18_Luc06_GM | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex18_Luc06_Z | O(k) | O(k) | O(1) | O(1) | O(k) | O(1) | |||||
| Transformed_CSR_04/Ex1_2_AEL03_FR | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex1_2_AEL03_Z | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Transformed_CSR_04/Ex1_2_Luc02c_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex1_2_Luc02c_Z | O(k) | O(k) | O(1) | O(1) | O(k) | O(1) | |||||
| Transformed_CSR_04/Ex1_GL02a_GM | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex1_GM03_FR | O(k3) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex1_Luc02b_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/Ex1_Luc02b_Z | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex1_Zan97_GM | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex23_Luc06_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex23_Luc06_GM | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex23_Luc06_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex25_Luc06_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex25_Luc06_GM | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex25_Luc06_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex26_Luc03b_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/Ex26_Luc03b_GM | O(k2) | O(k2) | |||||||||
| Transformed_CSR_04/Ex26_Luc03b_L | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex26_Luc03b_Z | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/Ex2_Luc02a_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/Ex2_Luc03b_FR | O(k3) | O(k3) | O(k3) | O(k3) | |||||||
| Transformed_CSR_04/Ex2_Luc03b_GM | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/Ex2_Luc03b_L | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| Transformed_CSR_04/Ex2_Luc03b_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex3_12_Luc96a_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex3_12_Luc96a_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex3_3_25_Bor03_GM | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/Ex3_3_25_Bor03_L | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex49_GM04_FR | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/Ex49_GM04_GM | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/Ex49_GM04_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_4_Luc96b_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/Ex4_4_Luc96b_GM | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/Ex4_4_Luc96b_L | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_GM | O(k) | O(k2) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_L | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_15_Bor03_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_56_Bor03_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_56_Bor03_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_77_Bor03_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex4_7_77_Bor03_GM | O(k) | O(k2) | O(k) | O(k2) | O(k) | O(k) | O(k) | ||||
| Transformed_CSR_04/Ex5_DLMMU04_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/Ex5_Zan97_FR | O(k) | O(k2) | O(k2) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex5_Zan97_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex6_9_Luc02c_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex6_9_Luc02c_Z | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex6_GM04_GM | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| Transformed_CSR_04/Ex6_Luc98_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/Ex6_Luc98_GM | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/Ex6_Luc98_L | O(k) | O(1) | O(1) | O(1) | O(1) | ||||||
| Transformed_CSR_04/Ex6_Luc98_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex7_BLR02_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/Ex7_BLR02_Z | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/Ex9_BLR02_GM | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/Ex9_BLR02_L | O(k) | O(k) | O(1) | O(1) | O(k) | O(1) | |||||
| Transformed_CSR_04/Ex9_Luc06_GM | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/ExAppendixB_AEL03_FR | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/ExAppendixB_AEL03_Z | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/ExConc_Zan97_C | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/ExConc_Zan97_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/ExConc_Zan97_GM | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/ExIntrod_GM99_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/ExIntrod_GM99_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/ExIntrod_Zan97_FR | O(k3) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/ExProp7_Luc06_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/ExProp7_Luc06_L | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Transformed_CSR_04/ExProp7_Luc06_Z | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Transformed_CSR_04/ExSec11_1_Luc02a_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/ExSec4_2_DLMMU04_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/ExSec4_2_DLMMU04_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/LISTUTILITIES_nosorts_FR | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/LISTUTILITIES_nosorts_Z | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/MYNAT_nokinds-noand_Z | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/MYNAT_nokinds_FR | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/MYNAT_nokinds_Z | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/MYNAT_nosorts-noand_FR | O(k2) | O(k2) | O(k2) | ||||||||
| Transformed_CSR_04/MYNAT_nosorts_FR | O(k2) | O(k2) | O(k2) | O(k2) | O(k2) | ||||||
| Transformed_CSR_04/PALINDROME_nokinds-noand_Z | O(k2) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/PALINDROME_nokinds_Z | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/PEANO_nokinds-noand_FR | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/PEANO_nokinds-noand_Z | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/PEANO_nokinds_FR | O(k2) | O(k2) | O(k2) | O(k2) | |||||||
| Transformed_CSR_04/PEANO_nokinds_Z | O(k) | O(k) | O(k) | O(k) | |||||||
| Transformed_CSR_04/PEANO_nosorts-noand_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Transformed_CSR_04/PEANO_nosorts_FR | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Various_04/04 | O(1) | O(1) | O(1) | O(1) | |||||||
| Various_04/15 | O(k) | O(k3) | O(k2) | O(k2) | O(k) | O(k) | |||||
| Various_04/23 | O(k) | O(k) | O(k) | O(k) | O(k) | ||||||
| Various_04/24 | O(k2) | O(k) | O(k) | O(k2) | O(k) | ||||||
| Waldmann_06/jwmatchb1 | O(k) | O(k) | O(k) | ||||||||
| Waldmann_06/jwmatchb2 | O(k) | O(k) | O(k) | ||||||||
| Zantema_05/z26 | O(k2) | O(k) | O(k) | O(k2) | O(k) |