0 QTRS
↳1 QTRSToCSRProof (⇔)
↳2 CSR
↳3 PoloCSRProof (⇔)
↳4 CSR
↳5 PoloCSRProof (⇔)
↳6 CSR
↳7 RisEmptyProof (⇔)
↳8 TRUE
active(zeros) → mark(cons(0, zeros))
active(tail(cons(X, XS))) → mark(XS)
active(cons(X1, X2)) → cons(active(X1), X2)
active(tail(X)) → tail(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
tail(mark(X)) → mark(tail(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(tail(X)) → tail(proper(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
tail(ok(X)) → ok(tail(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
active(zeros) → mark(cons(0, zeros))
active(tail(cons(X, XS))) → mark(XS)
active(cons(X1, X2)) → cons(active(X1), X2)
active(tail(X)) → tail(active(X))
cons(mark(X1), X2) → mark(cons(X1, X2))
tail(mark(X)) → mark(tail(X))
proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))
proper(0) → ok(0)
proper(tail(X)) → tail(proper(X))
cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
tail(ok(X)) → ok(tail(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
zeros: empty set
cons: {1}
0: empty set
tail: {1}
The QTRS contained all rules created by the complete Giesl-Middeldorp transformation. Therefore, the inverse transformation is complete (and sound).
zeros → cons(0, zeros)
tail(cons(X, XS)) → XS
zeros: empty set
cons: {1}
0: empty set
tail: {1}
Used ordering:
tail(cons(X, XS)) → XS
POL(0) = 0
POL(cons(x1, x2)) = 2·x1 + 2·x2
POL(tail(x1)) = 1 + x1
POL(zeros) = 0
zeros → cons(0, zeros)
zeros: empty set
cons: {1}
0: empty set
Used ordering:
zeros → cons(0, zeros)
POL(0) = 0
POL(cons(x1, x2)) = 1 + 2·x1
POL(zeros) = 2