WORST_CASE(Omega(n^1),O(n^1))
proof of input_0xtxxYaRQQ.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1).

(0) CpxTRS
(1) RelTrsToTrsProof [UPPER BOUND(ID), 0 ms]
(2) CpxTRS
    (3) CpxTrsMatchBoundsTAProof [FINISHED, 20 ms]
    (4) BOUNDS(1, n^1)
(5) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CdtProblem
    (7) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CpxRelTRS
    (9) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CpxRelTRS
    (11) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
    (12) typed CpxTrs
    (13) OrderProof [LOWER BOUND(ID), 8 ms]
    (14) typed CpxTrs
    (15) RewriteLemmaProof [LOWER BOUND(ID), 280 ms]
    (16) BEST
        (17) proven lower bound
            (18) LowerBoundPropagationProof [FINISHED, 0 ms]
            (19) BOUNDS(n^1, INF)
        (20) typed CpxTrs
            (21) RewriteLemmaProof [LOWER BOUND(ID), 744 ms]
            (22) typed CpxTrs


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, n^1).


The TRS R consists of the following rules:

   f(nil) -> nil
   f(.(nil, y)) -> .(nil, f(y))
   f(.(.(x, y), z)) -> f(.(x, .(y, z)))
   g(nil) -> nil
   g(.(x, nil)) -> .(g(x), nil)
   g(.(x, .(y, z))) -> g(.(.(x, y), z))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) RelTrsToTrsProof (UPPER BOUND(ID))
transformed relative TRS to TRS
----------------------------------------

(2)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   f(nil) -> nil
   f(.(nil, y)) -> .(nil, f(y))
   f(.(.(x, y), z)) -> f(.(x, .(y, z)))
   g(nil) -> nil
   g(.(x, nil)) -> .(g(x), nil)
   g(.(x, .(y, z))) -> g(.(.(x, y), z))

S is empty.
Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsMatchBoundsTAProof (FINISHED)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1. 

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: 
final states : [1, 2]
transitions: 
nil0() -> 0
.0(0, 0) -> 0
f0(0) -> 1
g0(0) -> 2
nil1() -> 1
nil1() -> 3
f1(0) -> 4
.1(3, 4) -> 1
.1(0, 0) -> 6
.1(0, 6) -> 5
f1(5) -> 1
nil1() -> 2
g1(0) -> 7
nil1() -> 8
.1(7, 8) -> 2
.1(0, 0) -> 10
.1(10, 0) -> 9
g1(9) -> 2
nil1() -> 4
.1(3, 4) -> 4
f1(6) -> 4
f1(5) -> 4
.1(0, 6) -> 6
nil1() -> 7
.1(7, 8) -> 7
g1(10) -> 7
g1(9) -> 7
.1(10, 0) -> 10

----------------------------------------

(4)
BOUNDS(1, n^1)

----------------------------------------

(5) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   f(nil) -> nil
   f(.(nil, z0)) -> .(nil, f(z0))
   f(.(.(z0, z1), z2)) -> f(.(z0, .(z1, z2)))
   g(nil) -> nil
   g(.(z0, nil)) -> .(g(z0), nil)
   g(.(z0, .(z1, z2))) -> g(.(.(z0, z1), z2))
Tuples:
   F(nil) -> c
   F(.(nil, z0)) -> c1(F(z0))
   F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
   G(nil) -> c3
   G(.(z0, nil)) -> c4(G(z0))
   G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))
S tuples:
   F(nil) -> c
   F(.(nil, z0)) -> c1(F(z0))
   F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
   G(nil) -> c3
   G(.(z0, nil)) -> c4(G(z0))
   G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))
K tuples:none
Defined Rule Symbols:   f_1, g_1

Defined Pair Symbols:   F_1, G_1

Compound Symbols:   c, c1_1, c2_1, c3, c4_1, c5_1


----------------------------------------

(7) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(8)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   F(nil) -> c
   F(.(nil, z0)) -> c1(F(z0))
   F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
   G(nil) -> c3
   G(.(z0, nil)) -> c4(G(z0))
   G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))

The (relative) TRS S consists of the following rules:

   f(nil) -> nil
   f(.(nil, z0)) -> .(nil, f(z0))
   f(.(.(z0, z1), z2)) -> f(.(z0, .(z1, z2)))
   g(nil) -> nil
   g(.(z0, nil)) -> .(g(z0), nil)
   g(.(z0, .(z1, z2))) -> g(.(.(z0, z1), z2))

Rewrite Strategy: INNERMOST
----------------------------------------

(9) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

(10)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).


The TRS R consists of the following rules:

   F(nil) -> c
   F(.(nil, z0)) -> c1(F(z0))
   F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
   G(nil) -> c3
   G(.(z0, nil)) -> c4(G(z0))
   G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))

The (relative) TRS S consists of the following rules:

   f(nil) -> nil
   f(.(nil, z0)) -> .(nil, f(z0))
   f(.(.(z0, z1), z2)) -> f(.(z0, .(z1, z2)))
   g(nil) -> nil
   g(.(z0, nil)) -> .(g(z0), nil)
   g(.(z0, .(z1, z2))) -> g(.(.(z0, z1), z2))

Rewrite Strategy: INNERMOST
----------------------------------------

(11) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(12)
Obligation:
Innermost TRS:
Rules:
F(nil) -> c
F(.(nil, z0)) -> c1(F(z0))
F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
G(nil) -> c3
G(.(z0, nil)) -> c4(G(z0))
G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))
f(nil) -> nil
f(.(nil, z0)) -> .(nil, f(z0))
f(.(.(z0, z1), z2)) -> f(.(z0, .(z1, z2)))
g(nil) -> nil
g(.(z0, nil)) -> .(g(z0), nil)
g(.(z0, .(z1, z2))) -> g(.(.(z0, z1), z2))

Types:
F :: nil:. -> c:c1:c2
nil :: nil:.
c :: c:c1:c2
. :: nil:. -> nil:. -> nil:.
c1 :: c:c1:c2 -> c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
G :: nil:. -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5 -> c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
f :: nil:. -> nil:.
g :: nil:. -> nil:.
hole_c:c1:c21_6 :: c:c1:c2
hole_nil:.2_6 :: nil:.
hole_c3:c4:c53_6 :: c3:c4:c5
gen_c:c1:c24_6 :: Nat -> c:c1:c2
gen_nil:.5_6 :: Nat -> nil:.
gen_c3:c4:c56_6 :: Nat -> c3:c4:c5

----------------------------------------

(13) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
F, G, f, g
----------------------------------------

(14)
Obligation:
Innermost TRS:
Rules:
F(nil) -> c
F(.(nil, z0)) -> c1(F(z0))
F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
G(nil) -> c3
G(.(z0, nil)) -> c4(G(z0))
G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))
f(nil) -> nil
f(.(nil, z0)) -> .(nil, f(z0))
f(.(.(z0, z1), z2)) -> f(.(z0, .(z1, z2)))
g(nil) -> nil
g(.(z0, nil)) -> .(g(z0), nil)
g(.(z0, .(z1, z2))) -> g(.(.(z0, z1), z2))

Types:
F :: nil:. -> c:c1:c2
nil :: nil:.
c :: c:c1:c2
. :: nil:. -> nil:. -> nil:.
c1 :: c:c1:c2 -> c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
G :: nil:. -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5 -> c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
f :: nil:. -> nil:.
g :: nil:. -> nil:.
hole_c:c1:c21_6 :: c:c1:c2
hole_nil:.2_6 :: nil:.
hole_c3:c4:c53_6 :: c3:c4:c5
gen_c:c1:c24_6 :: Nat -> c:c1:c2
gen_nil:.5_6 :: Nat -> nil:.
gen_c3:c4:c56_6 :: Nat -> c3:c4:c5


Generator Equations:
gen_c:c1:c24_6(0) <=> c
gen_c:c1:c24_6(+(x, 1)) <=> c1(gen_c:c1:c24_6(x))
gen_nil:.5_6(0) <=> nil
gen_nil:.5_6(+(x, 1)) <=> .(nil, gen_nil:.5_6(x))
gen_c3:c4:c56_6(0) <=> c3
gen_c3:c4:c56_6(+(x, 1)) <=> c4(gen_c3:c4:c56_6(x))


The following defined symbols remain to be analysed:
F, G, f, g
----------------------------------------

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
F(gen_nil:.5_6(n8_6)) -> gen_c:c1:c24_6(n8_6), rt in Omega(1 + n8_6)

Induction Base:
F(gen_nil:.5_6(0)) ->_R^Omega(1)
c

Induction Step:
F(gen_nil:.5_6(+(n8_6, 1))) ->_R^Omega(1)
c1(F(gen_nil:.5_6(n8_6))) ->_IH
c1(gen_c:c1:c24_6(c9_6))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(16)
Complex Obligation (BEST)

----------------------------------------

(17)
Obligation:
Proved the lower bound n^1 for the following obligation:

Innermost TRS:
Rules:
F(nil) -> c
F(.(nil, z0)) -> c1(F(z0))
F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
G(nil) -> c3
G(.(z0, nil)) -> c4(G(z0))
G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))
f(nil) -> nil
f(.(nil, z0)) -> .(nil, f(z0))
f(.(.(z0, z1), z2)) -> f(.(z0, .(z1, z2)))
g(nil) -> nil
g(.(z0, nil)) -> .(g(z0), nil)
g(.(z0, .(z1, z2))) -> g(.(.(z0, z1), z2))

Types:
F :: nil:. -> c:c1:c2
nil :: nil:.
c :: c:c1:c2
. :: nil:. -> nil:. -> nil:.
c1 :: c:c1:c2 -> c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
G :: nil:. -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5 -> c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
f :: nil:. -> nil:.
g :: nil:. -> nil:.
hole_c:c1:c21_6 :: c:c1:c2
hole_nil:.2_6 :: nil:.
hole_c3:c4:c53_6 :: c3:c4:c5
gen_c:c1:c24_6 :: Nat -> c:c1:c2
gen_nil:.5_6 :: Nat -> nil:.
gen_c3:c4:c56_6 :: Nat -> c3:c4:c5


Generator Equations:
gen_c:c1:c24_6(0) <=> c
gen_c:c1:c24_6(+(x, 1)) <=> c1(gen_c:c1:c24_6(x))
gen_nil:.5_6(0) <=> nil
gen_nil:.5_6(+(x, 1)) <=> .(nil, gen_nil:.5_6(x))
gen_c3:c4:c56_6(0) <=> c3
gen_c3:c4:c56_6(+(x, 1)) <=> c4(gen_c3:c4:c56_6(x))


The following defined symbols remain to be analysed:
F, G, f, g
----------------------------------------

(18) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(19)
BOUNDS(n^1, INF)

----------------------------------------

(20)
Obligation:
Innermost TRS:
Rules:
F(nil) -> c
F(.(nil, z0)) -> c1(F(z0))
F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
G(nil) -> c3
G(.(z0, nil)) -> c4(G(z0))
G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))
f(nil) -> nil
f(.(nil, z0)) -> .(nil, f(z0))
f(.(.(z0, z1), z2)) -> f(.(z0, .(z1, z2)))
g(nil) -> nil
g(.(z0, nil)) -> .(g(z0), nil)
g(.(z0, .(z1, z2))) -> g(.(.(z0, z1), z2))

Types:
F :: nil:. -> c:c1:c2
nil :: nil:.
c :: c:c1:c2
. :: nil:. -> nil:. -> nil:.
c1 :: c:c1:c2 -> c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
G :: nil:. -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5 -> c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
f :: nil:. -> nil:.
g :: nil:. -> nil:.
hole_c:c1:c21_6 :: c:c1:c2
hole_nil:.2_6 :: nil:.
hole_c3:c4:c53_6 :: c3:c4:c5
gen_c:c1:c24_6 :: Nat -> c:c1:c2
gen_nil:.5_6 :: Nat -> nil:.
gen_c3:c4:c56_6 :: Nat -> c3:c4:c5


Lemmas:
F(gen_nil:.5_6(n8_6)) -> gen_c:c1:c24_6(n8_6), rt in Omega(1 + n8_6)


Generator Equations:
gen_c:c1:c24_6(0) <=> c
gen_c:c1:c24_6(+(x, 1)) <=> c1(gen_c:c1:c24_6(x))
gen_nil:.5_6(0) <=> nil
gen_nil:.5_6(+(x, 1)) <=> .(nil, gen_nil:.5_6(x))
gen_c3:c4:c56_6(0) <=> c3
gen_c3:c4:c56_6(+(x, 1)) <=> c4(gen_c3:c4:c56_6(x))


The following defined symbols remain to be analysed:
G, f, g
----------------------------------------

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
f(gen_nil:.5_6(n5779_6)) -> gen_nil:.5_6(n5779_6), rt in Omega(0)

Induction Base:
f(gen_nil:.5_6(0)) ->_R^Omega(0)
nil

Induction Step:
f(gen_nil:.5_6(+(n5779_6, 1))) ->_R^Omega(0)
.(nil, f(gen_nil:.5_6(n5779_6))) ->_IH
.(nil, gen_nil:.5_6(c5780_6))

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
F(nil) -> c
F(.(nil, z0)) -> c1(F(z0))
F(.(.(z0, z1), z2)) -> c2(F(.(z0, .(z1, z2))))
G(nil) -> c3
G(.(z0, nil)) -> c4(G(z0))
G(.(z0, .(z1, z2))) -> c5(G(.(.(z0, z1), z2)))
f(nil) -> nil
f(.(nil, z0)) -> .(nil, f(z0))
f(.(.(z0, z1), z2)) -> f(.(z0, .(z1, z2)))
g(nil) -> nil
g(.(z0, nil)) -> .(g(z0), nil)
g(.(z0, .(z1, z2))) -> g(.(.(z0, z1), z2))

Types:
F :: nil:. -> c:c1:c2
nil :: nil:.
c :: c:c1:c2
. :: nil:. -> nil:. -> nil:.
c1 :: c:c1:c2 -> c:c1:c2
c2 :: c:c1:c2 -> c:c1:c2
G :: nil:. -> c3:c4:c5
c3 :: c3:c4:c5
c4 :: c3:c4:c5 -> c3:c4:c5
c5 :: c3:c4:c5 -> c3:c4:c5
f :: nil:. -> nil:.
g :: nil:. -> nil:.
hole_c:c1:c21_6 :: c:c1:c2
hole_nil:.2_6 :: nil:.
hole_c3:c4:c53_6 :: c3:c4:c5
gen_c:c1:c24_6 :: Nat -> c:c1:c2
gen_nil:.5_6 :: Nat -> nil:.
gen_c3:c4:c56_6 :: Nat -> c3:c4:c5


Lemmas:
F(gen_nil:.5_6(n8_6)) -> gen_c:c1:c24_6(n8_6), rt in Omega(1 + n8_6)
f(gen_nil:.5_6(n5779_6)) -> gen_nil:.5_6(n5779_6), rt in Omega(0)


Generator Equations:
gen_c:c1:c24_6(0) <=> c
gen_c:c1:c24_6(+(x, 1)) <=> c1(gen_c:c1:c24_6(x))
gen_nil:.5_6(0) <=> nil
gen_nil:.5_6(+(x, 1)) <=> .(nil, gen_nil:.5_6(x))
gen_c3:c4:c56_6(0) <=> c3
gen_c3:c4:c56_6(+(x, 1)) <=> c4(gen_c3:c4:c56_6(x))


The following defined symbols remain to be analysed:
g