(0) Obligation:

Clauses:

t :- ','(=(X, f(0, f(1, f(0, X)))), g(X)).
g(f(X, f(X, X1))) :- !.
g(f(X2, X)) :- g(X).

Query: t()

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:none

Compound Symbols:none

(3) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(4) BOUNDS(O(1), O(1))

(5) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:none
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:none

Defined Pair Symbols:none

Compound Symbols:none