Formalizing Jordan Normal Forms in Isabelle/HOL

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).


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.

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)