Term Rewriting System R:
[X]
active(c) -> mark(f(g(c)))
active(f(g(X))) -> mark(g(X))
proper(c) -> ok(c)
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))

Termination of R to be shown.



   TRS
Dependency Pair Analysis



R contains the following Dependency Pairs:

ACTIVE(c) -> F(g(c))
ACTIVE(c) -> G(c)
PROPER(f(X)) -> F(proper(X))
PROPER(f(X)) -> PROPER(X)
PROPER(g(X)) -> G(proper(X))
PROPER(g(X)) -> PROPER(X)
F(ok(X)) -> F(X)
G(ok(X)) -> G(X)
TOP(mark(X)) -> TOP(proper(X))
TOP(mark(X)) -> PROPER(X)
TOP(ok(X)) -> TOP(active(X))
TOP(ok(X)) -> ACTIVE(X)

Furthermore, R contains four SCCs.


   TRS
DPs
       →DP Problem 1
Modular Removal of Rules
       →DP Problem 2
MRR
       →DP Problem 3
MRR
       →DP Problem 4
MRR


Dependency Pair:

F(ok(X)) -> F(X)


Rules:


active(c) -> mark(f(g(c)))
active(f(g(X))) -> mark(g(X))
proper(c) -> ok(c)
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(ok(x1))=  x1  
  POL(F(x1))=  x1  

We have the following set D of usable symbols: {F}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

F(ok(X)) -> F(X)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.



   TRS
DPs
       →DP Problem 1
MRR
       →DP Problem 2
Modular Removal of Rules
       →DP Problem 3
MRR
       →DP Problem 4
MRR


Dependency Pair:

G(ok(X)) -> G(X)


Rules:


active(c) -> mark(f(g(c)))
active(f(g(X))) -> mark(g(X))
proper(c) -> ok(c)
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(G(x1))=  x1  
  POL(ok(x1))=  x1  

We have the following set D of usable symbols: {G}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

G(ok(X)) -> G(X)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.



   TRS
DPs
       →DP Problem 1
MRR
       →DP Problem 2
MRR
       →DP Problem 3
Modular Removal of Rules
       →DP Problem 4
MRR


Dependency Pairs:

PROPER(g(X)) -> PROPER(X)
PROPER(f(X)) -> PROPER(X)


Rules:


active(c) -> mark(f(g(c)))
active(f(g(X))) -> mark(g(X))
proper(c) -> ok(c)
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))





We have the following set of usable rules: none
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(g(x1))=  x1  
  POL(PROPER(x1))=  x1  
  POL(f(x1))=  x1  

We have the following set D of usable symbols: {PROPER}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

PROPER(g(X)) -> PROPER(X)
PROPER(f(X)) -> PROPER(X)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.



   TRS
DPs
       →DP Problem 1
MRR
       →DP Problem 2
MRR
       →DP Problem 3
MRR
       →DP Problem 4
Modular Removal of Rules


Dependency Pairs:

TOP(ok(X)) -> TOP(active(X))
TOP(mark(X)) -> TOP(proper(X))


Rules:


active(c) -> mark(f(g(c)))
active(f(g(X))) -> mark(g(X))
proper(c) -> ok(c)
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
top(mark(X)) -> top(proper(X))
top(ok(X)) -> top(active(X))





We have the following set of usable rules:

active(c) -> mark(f(g(c)))
active(f(g(X))) -> mark(g(X))
proper(c) -> ok(c)
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(active(x1))=  x1  
  POL(proper(x1))=  x1  
  POL(c)=  0  
  POL(g(x1))=  x1  
  POL(mark(x1))=  x1  
  POL(TOP(x1))=  x1  
  POL(ok(x1))=  x1  
  POL(f(x1))=  x1  

We have the following set D of usable symbols: {active, proper, c, g, mark, TOP, ok, f}
No Dependency Pairs can be deleted.
2 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   TRS
DPs
       →DP Problem 1
MRR
       →DP Problem 2
MRR
       →DP Problem 3
MRR
       →DP Problem 4
MRR
           →DP Problem 5
RFC Match Bounds


Dependency Pairs:

TOP(ok(X)) -> TOP(active(X))
TOP(mark(X)) -> TOP(proper(X))


Rules:


active(c) -> mark(f(g(c)))
active(f(g(X))) -> mark(g(X))
f(ok(X)) -> ok(f(X))
g(ok(X)) -> ok(g(X))
proper(c) -> ok(c)
proper(f(X)) -> f(proper(X))
proper(g(X)) -> g(proper(X))





Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 5.
The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 131, 132, 133

Node 99 is start node and node 100 is final node.

Those nodes are connect through the following edges:



Termination of R successfully shown.
Duration:
0:04 minutes