Termination Proof

by AProVE (version ba869e7b28377cd372aedcb96abeb62c4ad6aaa5 rene 20130719 unpublished dirty )

Input

The rewrite relation of the following TRS is considered.

iS_cps(no_a(x)) no_a(iS_cps(x))
iS_cps(no_cp(x)) no_cp(iS_cps(x))
iS_cps(no_lbeta(x)) no_lbeta(iS_cps(x))
iS_cps(no_a(no_cp(x))) no_a(x)
iS_cps(no_cp(no_cp(x))) no_cp(x)
iS_cps(no_lbeta(no_cp(x))) no_lbeta(x)
iS_cps(no_a(x)) no_a(x)
iS_cps(no_cp(x)) no_cp(x)
iS_cps(no_lbeta(x)) no_lbeta(x)
iS_cpd(no_a(x)) no_a(iS_cpd(x))
iS_cpd(no_cp(x)) no_cp(iS_cpd(x))
iS_cpd(no_lbeta(x)) no_lbeta(iS_cpd(x))
iS_cpd(no_cp(x)) no_cp(iS_cpd(iS_cpd(x)))
iS_cpd(no_a(x)) no_a(x)
iS_cpd(no_cp(x)) no_cp(x)
iS_cpd(no_lbeta(x)) no_lbeta(x)
iS_cpd(no_lbeta(x)) no_lbeta(iS_cps(x))
iS_cps(Answer) Answer
iS_cpd(Answer) Answer
The evaluation strategy is innermost.

Proof

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[iS_cps(x1)] = 1 · x1
[no_a(x1)] = 1 · x1
[no_cp(x1)] = 1 · x1 + 1
[no_lbeta(x1)] = 1 · x1
[iS_cpd(x1)] = 1 · x1
[Answer] = 0
the rules
iS_cps(no_a(x)) no_a(iS_cps(x))
iS_cps(no_cp(x)) no_cp(iS_cps(x))
iS_cps(no_lbeta(x)) no_lbeta(iS_cps(x))
iS_cps(no_a(x)) no_a(x)
iS_cps(no_cp(x)) no_cp(x)
iS_cps(no_lbeta(x)) no_lbeta(x)
iS_cpd(no_a(x)) no_a(iS_cpd(x))
iS_cpd(no_cp(x)) no_cp(iS_cpd(x))
iS_cpd(no_lbeta(x)) no_lbeta(iS_cpd(x))
iS_cpd(no_cp(x)) no_cp(iS_cpd(iS_cpd(x)))
iS_cpd(no_a(x)) no_a(x)
iS_cpd(no_cp(x)) no_cp(x)
iS_cpd(no_lbeta(x)) no_lbeta(x)
iS_cpd(no_lbeta(x)) no_lbeta(iS_cps(x))
iS_cps(Answer) Answer
iS_cpd(Answer) Answer
remain.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
iS_cps#(no_a(x)) iS_cps#(x)
iS_cps#(no_cp(x)) iS_cps#(x)
iS_cps#(no_lbeta(x)) iS_cps#(x)
iS_cpd#(no_a(x)) iS_cpd#(x)
iS_cpd#(no_cp(x)) iS_cpd#(x)
iS_cpd#(no_lbeta(x)) iS_cpd#(x)
iS_cpd#(no_cp(x)) iS_cpd#(iS_cpd(x))
iS_cpd#(no_lbeta(x)) iS_cps#(x)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.