WORST_CASE(Omega(n^1),O(n^1))
proof of input_D6aST1GFvd.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, 23 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), 9 ms]
    (14) typed CpxTrs
    (15) RewriteLemmaProof [LOWER BOUND(ID), 455 ms]
    (16) typed CpxTrs
    (17) RewriteLemmaProof [LOWER BOUND(ID), 149 ms]
    (18) typed CpxTrs
    (19) RewriteLemmaProof [LOWER BOUND(ID), 67 ms]
    (20) typed CpxTrs
    (21) RewriteLemmaProof [LOWER BOUND(ID), 32 ms]
    (22) BEST
        (23) proven lower bound
            (24) LowerBoundPropagationProof [FINISHED, 0 ms]
            (25) BOUNDS(n^1, INF)
        (26) typed CpxTrs
            (27) RewriteLemmaProof [LOWER BOUND(ID), 70 ms]
            (28) typed CpxTrs
            (29) RewriteLemmaProof [LOWER BOUND(ID), 53 ms]
            (30) BOUNDS(1, INF)


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

(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:

   h(f(x), y) -> f(g(x, y))
   g(x, y) -> h(x, y)

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:

   h(f(x), y) -> f(g(x, y))
   g(x, y) -> h(x, y)

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

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by: 
final states : [1, 2]
transitions: 
f0(0) -> 0
h0(0, 0) -> 1
g0(0, 0) -> 2
g1(0, 0) -> 3
f1(3) -> 1
h1(0, 0) -> 2
f1(3) -> 2
h2(0, 0) -> 3
f1(3) -> 3

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

(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:
   h(f(z0), z1) -> f(g(z0, z1))
   g(z0, z1) -> h(z0, z1)
Tuples:
   H(f(z0), z1) -> c(G(z0, z1))
   G(z0, z1) -> c1(H(z0, z1))
S tuples:
   H(f(z0), z1) -> c(G(z0, z1))
   G(z0, z1) -> c1(H(z0, z1))
K tuples:none
Defined Rule Symbols:   h_2, g_2

Defined Pair Symbols:   H_2, G_2

Compound Symbols:   c_1, c1_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:

   H(f(z0), z1) -> c(G(z0, z1))
   G(z0, z1) -> c1(H(z0, z1))

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

   h(f(z0), z1) -> f(g(z0, z1))
   g(z0, z1) -> h(z0, z1)

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:

   H(f(z0), z1) -> c(G(z0, z1))
   G(z0, z1) -> c1(H(z0, z1))

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

   h(f(z0), z1) -> f(g(z0, z1))
   g(z0, z1) -> h(z0, z1)

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

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

(12)
Obligation:
Innermost TRS:
Rules:
H(f(z0), z1) -> c(G(z0, z1))
G(z0, z1) -> c1(H(z0, z1))
h(f(z0), z1) -> f(g(z0, z1))
g(z0, z1) -> h(z0, z1)

Types:
H :: f -> a -> c
f :: f -> f
c :: c1 -> c
G :: f -> a -> c1
c1 :: c -> c1
h :: f -> b -> f
g :: f -> b -> f
hole_c1_2 :: c
hole_f2_2 :: f
hole_a3_2 :: a
hole_c14_2 :: c1
hole_b5_2 :: b
gen_f6_2 :: Nat -> f

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

(13) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
H, G, h, g

They will be analysed ascendingly in the following order:
H = G
h = g

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

(14)
Obligation:
Innermost TRS:
Rules:
H(f(z0), z1) -> c(G(z0, z1))
G(z0, z1) -> c1(H(z0, z1))
h(f(z0), z1) -> f(g(z0, z1))
g(z0, z1) -> h(z0, z1)

Types:
H :: f -> a -> c
f :: f -> f
c :: c1 -> c
G :: f -> a -> c1
c1 :: c -> c1
h :: f -> b -> f
g :: f -> b -> f
hole_c1_2 :: c
hole_f2_2 :: f
hole_a3_2 :: a
hole_c14_2 :: c1
hole_b5_2 :: b
gen_f6_2 :: Nat -> f


Generator Equations:
gen_f6_2(0) <=> hole_f2_2
gen_f6_2(+(x, 1)) <=> f(gen_f6_2(x))


The following defined symbols remain to be analysed:
g, H, G, h

They will be analysed ascendingly in the following order:
H = G
h = g

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
g(gen_f6_2(n8_2), hole_b5_2) -> *7_2, rt in Omega(0)

Induction Base:
g(gen_f6_2(0), hole_b5_2)

Induction Step:
g(gen_f6_2(+(n8_2, 1)), hole_b5_2) ->_R^Omega(0)
h(gen_f6_2(+(n8_2, 1)), hole_b5_2) ->_R^Omega(0)
f(g(gen_f6_2(n8_2), hole_b5_2)) ->_IH
f(*7_2)

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

(16)
Obligation:
Innermost TRS:
Rules:
H(f(z0), z1) -> c(G(z0, z1))
G(z0, z1) -> c1(H(z0, z1))
h(f(z0), z1) -> f(g(z0, z1))
g(z0, z1) -> h(z0, z1)

Types:
H :: f -> a -> c
f :: f -> f
c :: c1 -> c
G :: f -> a -> c1
c1 :: c -> c1
h :: f -> b -> f
g :: f -> b -> f
hole_c1_2 :: c
hole_f2_2 :: f
hole_a3_2 :: a
hole_c14_2 :: c1
hole_b5_2 :: b
gen_f6_2 :: Nat -> f


Lemmas:
g(gen_f6_2(n8_2), hole_b5_2) -> *7_2, rt in Omega(0)


Generator Equations:
gen_f6_2(0) <=> hole_f2_2
gen_f6_2(+(x, 1)) <=> f(gen_f6_2(x))


The following defined symbols remain to be analysed:
h, H, G

They will be analysed ascendingly in the following order:
H = G
h = g

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

(17) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
h(gen_f6_2(+(1, n182_2)), hole_b5_2) -> *7_2, rt in Omega(0)

Induction Base:
h(gen_f6_2(+(1, 0)), hole_b5_2)

Induction Step:
h(gen_f6_2(+(1, +(n182_2, 1))), hole_b5_2) ->_R^Omega(0)
f(g(gen_f6_2(+(1, n182_2)), hole_b5_2)) ->_R^Omega(0)
f(h(gen_f6_2(+(1, n182_2)), hole_b5_2)) ->_IH
f(*7_2)

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

(18)
Obligation:
Innermost TRS:
Rules:
H(f(z0), z1) -> c(G(z0, z1))
G(z0, z1) -> c1(H(z0, z1))
h(f(z0), z1) -> f(g(z0, z1))
g(z0, z1) -> h(z0, z1)

Types:
H :: f -> a -> c
f :: f -> f
c :: c1 -> c
G :: f -> a -> c1
c1 :: c -> c1
h :: f -> b -> f
g :: f -> b -> f
hole_c1_2 :: c
hole_f2_2 :: f
hole_a3_2 :: a
hole_c14_2 :: c1
hole_b5_2 :: b
gen_f6_2 :: Nat -> f


Lemmas:
g(gen_f6_2(n8_2), hole_b5_2) -> *7_2, rt in Omega(0)
h(gen_f6_2(+(1, n182_2)), hole_b5_2) -> *7_2, rt in Omega(0)


Generator Equations:
gen_f6_2(0) <=> hole_f2_2
gen_f6_2(+(x, 1)) <=> f(gen_f6_2(x))


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

They will be analysed ascendingly in the following order:
H = G
h = g

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

(19) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
g(gen_f6_2(n524_2), hole_b5_2) -> *7_2, rt in Omega(0)

Induction Base:
g(gen_f6_2(0), hole_b5_2)

Induction Step:
g(gen_f6_2(+(n524_2, 1)), hole_b5_2) ->_R^Omega(0)
h(gen_f6_2(+(n524_2, 1)), hole_b5_2) ->_R^Omega(0)
f(g(gen_f6_2(n524_2), hole_b5_2)) ->_IH
f(*7_2)

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

(20)
Obligation:
Innermost TRS:
Rules:
H(f(z0), z1) -> c(G(z0, z1))
G(z0, z1) -> c1(H(z0, z1))
h(f(z0), z1) -> f(g(z0, z1))
g(z0, z1) -> h(z0, z1)

Types:
H :: f -> a -> c
f :: f -> f
c :: c1 -> c
G :: f -> a -> c1
c1 :: c -> c1
h :: f -> b -> f
g :: f -> b -> f
hole_c1_2 :: c
hole_f2_2 :: f
hole_a3_2 :: a
hole_c14_2 :: c1
hole_b5_2 :: b
gen_f6_2 :: Nat -> f


Lemmas:
g(gen_f6_2(n524_2), hole_b5_2) -> *7_2, rt in Omega(0)
h(gen_f6_2(+(1, n182_2)), hole_b5_2) -> *7_2, rt in Omega(0)


Generator Equations:
gen_f6_2(0) <=> hole_f2_2
gen_f6_2(+(x, 1)) <=> f(gen_f6_2(x))


The following defined symbols remain to be analysed:
G, H

They will be analysed ascendingly in the following order:
H = G

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
G(gen_f6_2(n1000_2), hole_a3_2) -> *7_2, rt in Omega(n1000_2)

Induction Base:
G(gen_f6_2(0), hole_a3_2)

Induction Step:
G(gen_f6_2(+(n1000_2, 1)), hole_a3_2) ->_R^Omega(1)
c1(H(gen_f6_2(+(n1000_2, 1)), hole_a3_2)) ->_R^Omega(1)
c1(c(G(gen_f6_2(n1000_2), hole_a3_2))) ->_IH
c1(c(*7_2))

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

(22)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
H(f(z0), z1) -> c(G(z0, z1))
G(z0, z1) -> c1(H(z0, z1))
h(f(z0), z1) -> f(g(z0, z1))
g(z0, z1) -> h(z0, z1)

Types:
H :: f -> a -> c
f :: f -> f
c :: c1 -> c
G :: f -> a -> c1
c1 :: c -> c1
h :: f -> b -> f
g :: f -> b -> f
hole_c1_2 :: c
hole_f2_2 :: f
hole_a3_2 :: a
hole_c14_2 :: c1
hole_b5_2 :: b
gen_f6_2 :: Nat -> f


Lemmas:
g(gen_f6_2(n524_2), hole_b5_2) -> *7_2, rt in Omega(0)
h(gen_f6_2(+(1, n182_2)), hole_b5_2) -> *7_2, rt in Omega(0)


Generator Equations:
gen_f6_2(0) <=> hole_f2_2
gen_f6_2(+(x, 1)) <=> f(gen_f6_2(x))


The following defined symbols remain to be analysed:
G, H

They will be analysed ascendingly in the following order:
H = G

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

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

(25)
BOUNDS(n^1, INF)

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

(26)
Obligation:
Innermost TRS:
Rules:
H(f(z0), z1) -> c(G(z0, z1))
G(z0, z1) -> c1(H(z0, z1))
h(f(z0), z1) -> f(g(z0, z1))
g(z0, z1) -> h(z0, z1)

Types:
H :: f -> a -> c
f :: f -> f
c :: c1 -> c
G :: f -> a -> c1
c1 :: c -> c1
h :: f -> b -> f
g :: f -> b -> f
hole_c1_2 :: c
hole_f2_2 :: f
hole_a3_2 :: a
hole_c14_2 :: c1
hole_b5_2 :: b
gen_f6_2 :: Nat -> f


Lemmas:
g(gen_f6_2(n524_2), hole_b5_2) -> *7_2, rt in Omega(0)
h(gen_f6_2(+(1, n182_2)), hole_b5_2) -> *7_2, rt in Omega(0)
G(gen_f6_2(n1000_2), hole_a3_2) -> *7_2, rt in Omega(n1000_2)


Generator Equations:
gen_f6_2(0) <=> hole_f2_2
gen_f6_2(+(x, 1)) <=> f(gen_f6_2(x))


The following defined symbols remain to be analysed:
H

They will be analysed ascendingly in the following order:
H = G

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

(27) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
H(gen_f6_2(+(1, n1481_2)), hole_a3_2) -> *7_2, rt in Omega(n1481_2)

Induction Base:
H(gen_f6_2(+(1, 0)), hole_a3_2)

Induction Step:
H(gen_f6_2(+(1, +(n1481_2, 1))), hole_a3_2) ->_R^Omega(1)
c(G(gen_f6_2(+(1, n1481_2)), hole_a3_2)) ->_R^Omega(1)
c(c1(H(gen_f6_2(+(1, n1481_2)), hole_a3_2))) ->_IH
c(c1(*7_2))

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

(28)
Obligation:
Innermost TRS:
Rules:
H(f(z0), z1) -> c(G(z0, z1))
G(z0, z1) -> c1(H(z0, z1))
h(f(z0), z1) -> f(g(z0, z1))
g(z0, z1) -> h(z0, z1)

Types:
H :: f -> a -> c
f :: f -> f
c :: c1 -> c
G :: f -> a -> c1
c1 :: c -> c1
h :: f -> b -> f
g :: f -> b -> f
hole_c1_2 :: c
hole_f2_2 :: f
hole_a3_2 :: a
hole_c14_2 :: c1
hole_b5_2 :: b
gen_f6_2 :: Nat -> f


Lemmas:
g(gen_f6_2(n524_2), hole_b5_2) -> *7_2, rt in Omega(0)
h(gen_f6_2(+(1, n182_2)), hole_b5_2) -> *7_2, rt in Omega(0)
G(gen_f6_2(n1000_2), hole_a3_2) -> *7_2, rt in Omega(n1000_2)
H(gen_f6_2(+(1, n1481_2)), hole_a3_2) -> *7_2, rt in Omega(n1481_2)


Generator Equations:
gen_f6_2(0) <=> hole_f2_2
gen_f6_2(+(x, 1)) <=> f(gen_f6_2(x))


The following defined symbols remain to be analysed:
G

They will be analysed ascendingly in the following order:
H = G

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

(29) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
G(gen_f6_2(n2125_2), hole_a3_2) -> *7_2, rt in Omega(n2125_2)

Induction Base:
G(gen_f6_2(0), hole_a3_2)

Induction Step:
G(gen_f6_2(+(n2125_2, 1)), hole_a3_2) ->_R^Omega(1)
c1(H(gen_f6_2(+(n2125_2, 1)), hole_a3_2)) ->_R^Omega(1)
c1(c(G(gen_f6_2(n2125_2), hole_a3_2))) ->_IH
c1(c(*7_2))

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

(30)
BOUNDS(1, INF)