101.97/46.36
101.97/46.36
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(s(x), x) → f(s(x), round(s(x)))
101.97/46.36
round(0) → 0
101.97/46.36
round(0) → s(0)
101.97/46.36
round(s(0)) → s(0)
101.97/46.36
round(s(s(x))) → s(s(round(x)))
Rewrite Strategy: INNERMOST
101.97/46.36
101.97/46.36
(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match(-raise)-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 4.
The compatible tree automaton used to show the Match(-raise)-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2, 11, 12, 13, 18, 19, 20, 22, 26, 27, 28, 32, 33, 34, 37, 38, 39, 10, 17, 24, 42, 43, 44]
transitions:
f0(0, 0) → 1
s1(0) → 3
s1(0) → 5
round1(5) → 4
f1(3, 4) → 1
s1(0) → 0
s1(6) → 2
round1(0) → 8
s1(8) → 7
s1(7) → 2
round1(0) → 2
s1(0) → 9
round1(0) → 11
f0(9, 0) → 1
f0(0, 9) → 1
f0(10, 0) → 1
f0(0, 10) → 1
f0(9, 9) → 1
f0(9, 10) → 1
f0(10, 9) → 1
f0(10, 10) → 1
f1(9, 4) → 1
s1(9) → 9
s1(10) → 12
s1(11) → 7
f0(12, 0) → 1
f0(0, 12) → 1
f0(12, 12) → 1
f1(12, 4) → 1
f1(3, 13) → 1
f1(12, 13) → 1
s1(12) → 9
s1(13) → 7
s1(9) → 3
s1(9) → 5
s2(14) → 11
s2(14) → 13
round2(9) → 16
s2(16) → 15
s2(15) → 13
round2(9) → 13
round2(12) → 16
round2(12) → 13
round2(10) → 16
round2(10) → 11
round2(9) → 18
round2(12) → 18
round2(10) → 19
f0(9, 12) → 1
f0(12, 9) → 1
f0(12, 10) → 1
f0(10, 12) → 1
f0(17, 0) → 1
f0(17, 9) → 1
f0(17, 10) → 1
f0(17, 12) → 1
f0(0, 17) → 1
f0(9, 17) → 1
f0(10, 17) → 1
f0(12, 17) → 1
f0(17, 17) → 1
f1(9, 13) → 1
f1(3, 18) → 1
f1(9, 18) → 1
f1(12, 18) → 1
s1(17) → 20
s1(18) → 7
s1(19) → 7
s1(17) → 7
round1(12) → 13
round1(17) → 11
s2(17) → 13
s2(18) → 15
s2(19) → 15
round2(17) → 19
f0(20, 0) → 1
f0(20, 9) → 1
f0(20, 10) → 1
f0(20, 12) → 1
f0(0, 20) → 1
f0(9, 20) → 1
f0(10, 20) → 1
f0(12, 20) → 1
f0(20, 20) → 1
f1(20, 4) → 1
f1(20, 13) → 1
s1(20) → 12
round1(20) → 13
round2(20) → 18
s2(17) → 20
s2(18) → 7
s2(19) → 7
s2(17) → 7
round2(17) → 11
round2(20) → 13
s3(21) → 19
s2(14) → 18
s2(15) → 18
s2(17) → 22
s2(18) → 23
s2(19) → 23
f0(20, 17) → 1
f0(17, 20) → 1
f0(22, 0) → 1
f0(22, 9) → 1
f0(22, 10) → 1
f0(22, 12) → 1
f0(22, 17) → 1
f0(22, 20) → 1
f0(0, 22) → 1
f0(9, 22) → 1
f0(10, 22) → 1
f0(12, 22) → 1
f0(17, 22) → 1
f0(20, 22) → 1
f0(24, 0) → 1
f0(24, 9) → 1
f0(24, 10) → 1
f0(24, 12) → 1
f0(24, 17) → 1
f0(24, 20) → 1
f0(0, 24) → 1
f0(9, 24) → 1
f0(10, 24) → 1
f0(12, 24) → 1
f0(17, 24) → 1
f0(20, 24) → 1
f0(22, 22) → 1
f0(22, 24) → 1
f0(24, 22) → 1
f0(24, 24) → 1
f1(20, 18) → 1
f1(22, 4) → 1
f1(22, 13) → 1
f1(22, 18) → 1
f1(3, 22) → 1
f1(9, 22) → 1
f1(12, 22) → 1
f1(20, 22) → 1
f1(22, 22) → 1
s1(23) → 2
s1(24) → 20
s1(20) → 9
s1(24) → 7
round1(9) → 13
round1(22) → 13
s2(23) → 18
s2(24) → 26
s2(24) → 15
round2(22) → 18
s3(24) → 19
f0(25, 0) → 1
f0(25, 9) → 1
f0(25, 10) → 1
f0(25, 12) → 1
f0(25, 17) → 1
f0(25, 20) → 1
f0(0, 25) → 1
f0(9, 25) → 1
f0(10, 25) → 1
f0(12, 25) → 1
f0(17, 25) → 1
f0(20, 25) → 1
f0(26, 0) → 1
f0(26, 9) → 1
f0(26, 10) → 1
f0(26, 12) → 1
f0(26, 17) → 1
f0(26, 20) → 1
f0(0, 26) → 1
f0(9, 26) → 1
f0(10, 26) → 1
f0(12, 26) → 1
f0(17, 26) → 1
f0(20, 26) → 1
f0(25, 25) → 1
f0(25, 26) → 1
f0(26, 25) → 1
f0(26, 26) → 1
f1(25, 4) → 1
f1(25, 13) → 1
f1(25, 18) → 1
f1(26, 4) → 1
f1(26, 13) → 1
f1(26, 18) → 1
f1(3, 26) → 1
f1(9, 26) → 1
f1(12, 26) → 1
f1(20, 26) → 1
f1(25, 26) → 1
f1(26, 26) → 1
s1(25) → 12
round1(25) → 13
s2(26) → 27
round2(25) → 18
f1(3, 27) → 1
f1(9, 27) → 1
f1(12, 27) → 1
f1(20, 27) → 1
s1(27) → 28
s2(27) → 27
s1(28) → 2
s2(23) → 2
s2(24) → 20
s3(24) → 20
s2(24) → 7
s3(24) → 7
round2(22) → 13
s3(24) → 26
s3(24) → 15
s2(26) → 20
s2(26) → 12
round2(25) → 13
s2(27) → 28
s2(22) → 29
s2(22) → 31
round2(31) → 30
f2(29, 30) → 1
s2(22) → 20
s2(22) → 25
s2(22) → 9
s2(26) → 29
s2(26) → 31
s3(21) → 18
s2(26) → 32
s2(22) → 33
f0(22, 25) → 1
f0(22, 26) → 1
f0(25, 22) → 1
f0(26, 22) → 1
f0(24, 25) → 1
f0(24, 26) → 1
f0(25, 24) → 1
f0(26, 24) → 1
f0(32, 0) → 1
f0(32, 9) → 1
f0(32, 10) → 1
f0(32, 12) → 1
f0(32, 17) → 1
f0(32, 20) → 1
f0(32, 22) → 1
f0(32, 24) → 1
f0(32, 25) → 1
f0(32, 26) → 1
f0(0, 32) → 1
f0(9, 32) → 1
f0(10, 32) → 1
f0(12, 32) → 1
f0(17, 32) → 1
f0(20, 32) → 1
f0(22, 32) → 1
f0(24, 32) → 1
f0(25, 32) → 1
f0(26, 32) → 1
f0(33, 0) → 1
f0(33, 9) → 1
f0(33, 10) → 1
f0(33, 12) → 1
f0(33, 17) → 1
f0(33, 20) → 1
f0(33, 22) → 1
f0(33, 24) → 1
f0(33, 25) → 1
f0(33, 26) → 1
f0(0, 33) → 1
f0(9, 33) → 1
f0(10, 33) → 1
f0(12, 33) → 1
f0(17, 33) → 1
f0(20, 33) → 1
f0(22, 33) → 1
f0(24, 33) → 1
f0(25, 33) → 1
f0(26, 33) → 1
f0(32, 32) → 1
f0(32, 33) → 1
f0(33, 32) → 1
f0(33, 33) → 1
f1(22, 26) → 1
f1(22, 27) → 1
f1(25, 22) → 1
f1(26, 22) → 1
f1(26, 27) → 1
f1(32, 4) → 1
f1(32, 13) → 1
f1(32, 18) → 1
f1(32, 22) → 1
f1(32, 26) → 1
f1(32, 27) → 1
f1(3, 32) → 1
f1(9, 32) → 1
f1(12, 32) → 1
f1(20, 32) → 1
f1(22, 32) → 1
f1(25, 32) → 1
f1(26, 32) → 1
f1(25, 27) → 1
f1(33, 4) → 1
f1(33, 13) → 1
f1(33, 18) → 1
f1(33, 22) → 1
f1(33, 26) → 1
f1(33, 27) → 1
f1(32, 32) → 1
f1(33, 32) → 1
s1(22) → 20
s1(26) → 20
s1(33) → 12
s1(27) → 7
s1(22) → 9
s1(33) → 9
s1(26) → 25
round1(33) → 13
s2(32) → 32
s2(32) → 27
s2(27) → 15
s2(26) → 15
s2(32) → 15
round2(33) → 34
round2(33) → 18
s3(24) → 18
f2(32, 30) → 1
f2(33, 30) → 1
f1(3, 34) → 1
f1(9, 34) → 1
f1(12, 34) → 1
f1(20, 34) → 1
f1(22, 34) → 1
f1(25, 34) → 1
f1(26, 34) → 1
s1(34) → 7
s2(34) → 23
f2(29, 34) → 1
s2(32) → 20
s2(27) → 7
s2(26) → 25
s2(32) → 25
round2(33) → 13
s2(34) → 7
s2(32) → 29
s2(32) → 31
round3(24) → 36
s3(36) → 35
s3(35) → 18
round3(24) → 11
round3(24) → 19
round3(26) → 36
round3(26) → 13
round3(26) → 18
round3(32) → 36
round3(32) → 13
round3(32) → 34
round3(32) → 18
s3(35) → 34
round3(24) → 37
round3(26) → 38
round3(32) → 39
f1(32, 34) → 1
f1(33, 34) → 1
f1(3, 38) → 1
f1(9, 38) → 1
f1(12, 38) → 1
f1(20, 38) → 1
f1(22, 38) → 1
f1(25, 38) → 1
f1(26, 38) → 1
f1(32, 38) → 1
f1(33, 38) → 1
f1(3, 39) → 1
f1(9, 39) → 1
f1(12, 39) → 1
f1(20, 39) → 1
f1(22, 39) → 1
f1(25, 39) → 1
f1(26, 39) → 1
f1(32, 39) → 1
f1(33, 39) → 1
s1(32) → 20
s1(37) → 7
s1(38) → 7
s1(39) → 7
s1(32) → 25
round1(26) → 13
round1(32) → 13
s2(37) → 23
s2(38) → 23
s2(39) → 23
s2(37) → 15
s2(34) → 15
s2(38) → 15
s2(39) → 15
round2(26) → 18
round2(32) → 34
round2(32) → 18
s3(37) → 35
s3(38) → 35
s3(39) → 35
f2(32, 34) → 1
f2(33, 34) → 1
f2(29, 39) → 1
f2(32, 39) → 1
f2(33, 39) → 1
round3(32) → 38
s2(37) → 7
s3(37) → 7
s2(38) → 7
s3(38) → 7
s2(39) → 7
s3(39) → 7
round2(26) → 13
round2(32) → 13
s3(37) → 23
s3(38) → 23
s3(39) → 23
s3(37) → 15
s3(38) → 15
s3(39) → 15
04() → 37
04() → 19
04() → 11
04() → 2
04() → 0
04() → 6
04() → 10
04() → 14
04() → 17
04() → 21
04() → 24
04() → 40
s4(40) → 37
s3(21) → 38
s4(40) → 38
s3(35) → 38
s3(35) → 39
s3(37) → 41
s3(38) → 41
s3(39) → 41
04() → 42
f0(42, 0) → 1
f0(42, 9) → 1
f0(42, 10) → 1
f0(42, 12) → 1
f0(42, 17) → 1
f0(42, 20) → 1
f0(42, 22) → 1
f0(42, 24) → 1
f0(42, 25) → 1
f0(42, 26) → 1
f0(42, 32) → 1
f0(42, 33) → 1
f0(0, 42) → 1
f0(9, 42) → 1
f0(10, 42) → 1
f0(12, 42) → 1
f0(17, 42) → 1
f0(20, 42) → 1
f0(22, 42) → 1
f0(24, 42) → 1
f0(25, 42) → 1
f0(26, 42) → 1
f0(32, 42) → 1
f0(33, 42) → 1
f0(42, 42) → 1
s1(41) → 2
s1(42) → 20
s1(42) → 7
round1(42) → 11
s2(41) → 18
s2(42) → 26
s2(42) → 23
s2(42) → 15
round2(42) → 19
s3(41) → 39
s3(42) → 43
s3(42) → 35
round3(42) → 37
s4(42) → 38
f0(43, 0) → 1
f0(43, 9) → 1
f0(43, 10) → 1
f0(43, 12) → 1
f0(43, 17) → 1
f0(43, 20) → 1
f0(43, 22) → 1
f0(43, 24) → 1
f0(43, 25) → 1
f0(43, 26) → 1
f0(43, 32) → 1
f0(43, 33) → 1
f0(0, 43) → 1
f0(9, 43) → 1
f0(10, 43) → 1
f0(12, 43) → 1
f0(17, 43) → 1
f0(20, 43) → 1
f0(22, 43) → 1
f0(24, 43) → 1
f0(25, 43) → 1
f0(26, 43) → 1
f0(32, 43) → 1
f0(33, 43) → 1
f0(43, 43) → 1
f1(43, 4) → 1
f1(43, 13) → 1
f1(43, 18) → 1
f1(43, 22) → 1
f1(43, 26) → 1
f1(43, 27) → 1
f1(43, 32) → 1
f1(43, 34) → 1
f1(43, 38) → 1
f1(43, 39) → 1
f1(3, 43) → 1
f1(9, 43) → 1
f1(12, 43) → 1
f1(20, 43) → 1
f1(22, 43) → 1
f1(25, 43) → 1
f1(26, 43) → 1
f1(32, 43) → 1
f1(33, 43) → 1
f1(43, 43) → 1
s1(43) → 20
round1(43) → 13
s2(43) → 32
round2(43) → 18
s3(43) → 44
round3(43) → 38
f1(3, 44) → 1
f1(9, 44) → 1
f1(12, 44) → 1
f1(20, 44) → 1
f1(22, 44) → 1
f1(25, 44) → 1
f1(26, 44) → 1
f1(32, 44) → 1
f1(33, 44) → 1
s1(44) → 28
s2(44) → 27
s3(44) → 44
f2(29, 44) → 1
f2(32, 44) → 1
f2(33, 44) → 1
s2(41) → 2
s3(41) → 2
s2(42) → 20
s3(42) → 20
s4(42) → 20
s2(42) → 7
s3(42) → 7
s4(42) → 7
round2(42) → 11
round3(42) → 11
s3(41) → 18
s3(42) → 26
s4(42) → 26
s3(42) → 23
s4(42) → 23
s3(42) → 15
s4(42) → 15
round3(42) → 19
s4(42) → 43
s4(42) → 35
s2(43) → 20
s3(43) → 20
round2(43) → 13
round3(43) → 13
s3(43) → 32
round3(43) → 18
s2(44) → 28
s3(44) → 28
s3(44) → 27
101.97/46.36
101.97/46.36
(2) BOUNDS(O(1), O(n^1))
101.97/46.36