MAYBE 275.32/69.75 MAYBE 275.32/69.76 275.32/69.76 Problem: 275.32/69.76 active(incr(nil())) -> mark(nil()) 275.32/69.76 active(incr(cons(X,L))) -> mark(cons(s(X),incr(L))) 275.32/69.76 active(adx(nil())) -> mark(nil()) 275.32/69.76 active(adx(cons(X,L))) -> mark(incr(cons(X,adx(L)))) 275.32/69.76 active(nats()) -> mark(adx(zeros())) 275.32/69.76 active(zeros()) -> mark(cons(0(),zeros())) 275.32/69.76 active(head(cons(X,L))) -> mark(X) 275.32/69.76 active(tail(cons(X,L))) -> mark(L) 275.32/69.76 active(incr(X)) -> incr(active(X)) 275.32/69.76 active(cons(X1,X2)) -> cons(active(X1),X2) 275.32/69.76 active(s(X)) -> s(active(X)) 275.32/69.76 active(adx(X)) -> adx(active(X)) 275.32/69.76 active(head(X)) -> head(active(X)) 275.32/69.76 active(tail(X)) -> tail(active(X)) 275.32/69.76 incr(mark(X)) -> mark(incr(X)) 275.32/69.76 cons(mark(X1),X2) -> mark(cons(X1,X2)) 275.32/69.76 s(mark(X)) -> mark(s(X)) 275.32/69.76 adx(mark(X)) -> mark(adx(X)) 275.32/69.76 head(mark(X)) -> mark(head(X)) 275.32/69.76 tail(mark(X)) -> mark(tail(X)) 275.32/69.76 proper(incr(X)) -> incr(proper(X)) 275.32/69.76 proper(nil()) -> ok(nil()) 275.32/69.76 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) 275.32/69.76 proper(s(X)) -> s(proper(X)) 275.32/69.76 proper(adx(X)) -> adx(proper(X)) 275.32/69.76 proper(nats()) -> ok(nats()) 275.32/69.76 proper(zeros()) -> ok(zeros()) 275.32/69.76 proper(0()) -> ok(0()) 275.32/69.76 proper(head(X)) -> head(proper(X)) 275.32/69.76 proper(tail(X)) -> tail(proper(X)) 275.32/69.76 incr(ok(X)) -> ok(incr(X)) 275.32/69.76 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) 275.32/69.76 s(ok(X)) -> ok(s(X)) 275.32/69.76 adx(ok(X)) -> ok(adx(X)) 275.32/69.76 head(ok(X)) -> ok(head(X)) 275.32/69.76 tail(ok(X)) -> ok(tail(X)) 275.32/69.76 top(mark(X)) -> top(proper(X)) 275.32/69.76 top(ok(X)) -> top(active(X)) 275.32/69.76 275.32/69.76 Proof: 275.32/69.76 Open 275.32/69.76 EOF