WORST_CASE(?,O(1))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, 1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 475 ms]
(2) CpxRelTRS
(3) NarrowingOnBasicTermsTerminatesProof [FINISHED, 11 ms]
(4) BOUNDS(1, 1)


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

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


The TRS R consists of the following rules:

   F(0, 1, z0) -> c(F(h(z0), h(z0), z0), H(z0))
   F(0, 1, z0) -> c1(F(h(z0), h(z0), z0), H(z0))
   H(0) -> c2
   H(g(z0, z1)) -> c3

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

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

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

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

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


The TRS R consists of the following rules:

   F(0, 1, z0) -> c(F(h(z0), h(z0), z0), H(z0))
   F(0, 1, z0) -> c1(F(h(z0), h(z0), z0), H(z0))
   H(0) -> c2
   H(g(z0, z1)) -> c3

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

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

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

(3) NarrowingOnBasicTermsTerminatesProof (FINISHED)
Constant runtime complexity proven by termination of constructor-based narrowing.

The maximal most general narrowing sequences give rise to the following rewrite sequences:

h(0) ->^* 0

f(0, 1, g(x0, x1)) ->^* f(x1, x1, g(x0, x1))

f(0, 1, 0) ->^* f(0, 0, 0)

f(0, 1, g(x0, x1)) ->^* f(x1, x1, g(x0, x1))

f(0, 1, 0) ->^* f(0, 0, 0)

H(g(x0, x1)) ->^* c3

H(0) ->^* c2

F(0, 1, g(x0, x1)) ->^* c1(F(x1, x1, g(x0, x1)), c3)

F(0, 1, g(x0, x1)) ->^* c1(F(x1, x1, g(x0, x1)), c3)

F(0, 1, 0) ->^* c1(F(0, 0, 0), c2)

F(0, 1, 0) ->^* c1(F(0, 0, 0), c2)

F(0, 1, g(x0, x1)) ->^* c1(F(x1, x1, g(x0, x1)), c3)

F(0, 1, g(x0, x1)) ->^* c1(F(x1, x1, g(x0, x1)), c3)

F(0, 1, 0) ->^* c1(F(0, 0, 0), c2)

F(0, 1, 0) ->^* c1(F(0, 0, 0), c2)

F(0, 1, g(x0, x1)) ->^* c1(F(x1, x1, g(x0, x1)), c3)

F(0, 1, g(x0, x1)) ->^* c1(F(x1, x1, g(x0, x1)), c3)

F(0, 1, 0) ->^* c1(F(0, 0, 0), c2)

F(0, 1, 0) ->^* c1(F(0, 0, 0), c2)

F(0, 1, g(x0, x1)) ->^* c(F(x1, x1, g(x0, x1)), c3)

F(0, 1, g(x0, x1)) ->^* c(F(x1, x1, g(x0, x1)), c3)

F(0, 1, 0) ->^* c(F(0, 0, 0), c2)

F(0, 1, 0) ->^* c(F(0, 0, 0), c2)

F(0, 1, g(x0, x1)) ->^* c(F(x1, x1, g(x0, x1)), c3)

F(0, 1, g(x0, x1)) ->^* c(F(x1, x1, g(x0, x1)), c3)

F(0, 1, 0) ->^* c(F(0, 0, 0), c2)

F(0, 1, 0) ->^* c(F(0, 0, 0), c2)

F(0, 1, g(x0, x1)) ->^* c(F(x1, x1, g(x0, x1)), c3)

F(0, 1, g(x0, x1)) ->^* c(F(x1, x1, g(x0, x1)), c3)

F(0, 1, 0) ->^* c(F(0, 0, 0), c2)

F(0, 1, 0) ->^* c(F(0, 0, 0), c2)




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

(4)
BOUNDS(1, 1)