MAYBE
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ inc(nil) -> nil,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     inc(app(?xs,?ys)) -> app(inc(?xs),inc(?ys)),
     dec(nil) -> nil,
     dec(cons(0,?xs)) -> cons(0,dec(?xs)),
     dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) -> ?xs,
     inc(dec(?xs)) -> ?xs ]
constructor detection timeout; switch to an approximation.
Constructors: {0,s,nil,cons}
Defined function symbols: {app,dec,inc}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ inc(nil) -> nil,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     dec(nil) -> nil,
     dec(cons(0,?xs)) -> cons(0,dec(?xs)),
     dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)) ]
   [ inc(app(?xs,?ys)) -> app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) -> ?xs,
     inc(dec(?xs)) -> ?xs ]
Trying with:
R:
   [ inc(nil) -> nil,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     dec(nil) -> nil,
     dec(cons(0,?xs)) -> cons(0,dec(?xs)),
     dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)) ]
E:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs,
     inc(dec(?xs)) = ?xs ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat,List}
Signature:
   [ inc : List -> List,
     dec : List -> List,
     app : List,List -> List,
     cons : Nat,List -> List,
     nil : List,
     s : Nat -> Nat,
     0 : Nat ]
Rule Part:
   [ inc(nil) -> nil,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     dec(nil) -> nil,
     dec(cons(0,?xs)) -> cons(0,dec(?xs)),
     dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)) ]
Conjecture Part:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs,
     inc(dec(?xs)) = ?xs ]
Precedence (by weight): {(0,0),(s,3),(app,6),(dec,7),(inc,5),(nil,2),(cons,4)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ inc(nil) -> nil,
     inc(cons(?x,?xs)) -> cons(s(?x),inc(?xs)),
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     dec(nil) -> nil,
     dec(cons(0,?xs)) -> cons(0,dec(?xs)),
     dec(cons(s(?x),?xs)) -> cons(?x,dec(?xs)) ]
Conjectures:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs,
     inc(dec(?xs)) = ?xs ]
STEP 0
ES:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs,
     inc(dec(?xs)) = ?xs ]
HS:
   [ ]
ES0:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs,
     inc(dec(?xs)) = ?xs ]
HS0:
   [ ]
ES1:
   [ inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     dec(inc(?xs)) = ?xs,
     inc(dec(?xs)) = ?xs ]
HS1:
   [ ]
Expand dec(inc(?xs)) = ?xs
   [ dec(nil) = nil,
     dec(cons(s(?x_1),inc(?xs_1))) = cons(?x_1,?xs_1) ]
ES2:
   [ nil = nil,
     cons(?x_1,dec(inc(?xs_1))) = cons(?x_1,?xs_1),
     inc(dec(?xs)) = ?xs,
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS2:
   [ dec(inc(?xs)) -> ?xs ]
STEP 1
ES:
   [ nil = nil,
     cons(?x_1,dec(inc(?xs_1))) = cons(?x_1,?xs_1),
     inc(dec(?xs)) = ?xs,
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS:
   [ dec(inc(?xs)) -> ?xs ]
ES0:
   [ nil = nil,
     cons(?x_1,?xs_1) = cons(?x_1,?xs_1),
     inc(dec(?xs)) = ?xs,
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS0:
   [ dec(inc(?xs)) -> ?xs ]
ES1:
   [ inc(dec(?xs)) = ?xs,
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)) ]
HS1:
   [ dec(inc(?xs)) -> ?xs ]
Expand inc(dec(?xs)) = ?xs
   [ inc(nil) = nil,
     inc(cons(0,dec(?xs_4))) = cons(0,?xs_4),
     inc(cons(?x_5,dec(?xs_5))) = cons(s(?x_5),?xs_5) ]
ES2:
   [ nil = nil,
     cons(s(0),inc(dec(?xs_4))) = cons(0,?xs_4),
     cons(s(?x_5),inc(dec(?xs_5))) = cons(s(?x_5),?xs_5),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)) ]
HS2:
   [ inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
STEP 2
ES:
   [ nil = nil,
     cons(s(0),inc(dec(?xs_4))) = cons(0,?xs_4),
     cons(s(?x_5),inc(dec(?xs_5))) = cons(s(?x_5),?xs_5),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)) ]
HS:
   [ inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES0:
   [ nil = nil,
     cons(s(0),?xs_4) = cons(0,?xs_4),
     cons(s(?x_5),?xs_5) = cons(s(?x_5),?xs_5),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)) ]
HS0:
   [ inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES1:
   [ cons(s(0),?xs_4) = cons(0,?xs_4),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     inc(app(?xs,?ys)) = app(inc(?xs),inc(?ys)) ]
HS1:
   [ inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
Expand app(inc(?xs),inc(?ys)) = inc(app(?xs,?ys))
   [ app(nil,inc(?ys)) = inc(app(nil,?ys)),
     app(cons(s(?x_1),inc(?xs_1)),inc(?ys)) = inc(app(cons(?x_1,?xs_1),?ys)) ]
ES2:
   [ inc(?ys) = inc(app(nil,?ys)),
     cons(s(?x_1),app(inc(?xs_1),inc(?ys))) = inc(app(cons(?x_1,?xs_1),?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS2:
   [ app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
STEP 3
ES:
   [ inc(?ys) = inc(app(nil,?ys)),
     cons(s(?x_1),app(inc(?xs_1),inc(?ys))) = inc(app(cons(?x_1,?xs_1),?ys)),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS:
   [ app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES0:
   [ inc(?ys) = inc(?ys),
     cons(s(?x_1),inc(app(?xs_1,?ys))) = cons(s(?x_1),inc(app(?xs_1,?ys))),
     dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS0:
   [ app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES1:
   [ dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS1:
   [ app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
Expand dec(app(?xs,?ys)) = app(dec(?xs),dec(?ys))
   [ dec(?ys_2) = app(dec(nil),dec(?ys_2)),
     dec(cons(?x_3,app(?xs_3,?ys_3))) = app(dec(cons(?x_3,?xs_3)),dec(?ys_3)) ]
ES2:
   [ dec(?ys_2) = app(dec(nil),dec(?ys_2)),
     dec(cons(?x_3,app(?xs_3,?ys_3))) = app(dec(cons(?x_3,?xs_3)),dec(?ys_3)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS2:
   [ dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
STEP 4
ES:
   [ dec(?ys_2) = app(dec(nil),dec(?ys_2)),
     dec(cons(?x_3,app(?xs_3,?ys_3))) = app(dec(cons(?x_3,?xs_3)),dec(?ys_3)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS:
   [ dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES0:
   [ dec(?ys_2) = dec(?ys_2),
     dec(cons(?x_3,app(?xs_3,?ys_3))) = app(dec(cons(?x_3,?xs_3)),dec(?ys_3)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS0:
   [ dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES1:
   [ dec(cons(?x_3,app(?xs_3,?ys_3))) = app(dec(cons(?x_3,?xs_3)),dec(?ys_3)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS1:
   [ dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
Expand dec(cons(?x_3,app(?xs_3,?ys_3))) = app(dec(cons(?x_3,?xs_3)),dec(?ys_3))
   [ cons(0,dec(app(?xs,?ys))) = app(dec(cons(0,?xs)),dec(?ys)),
     cons(?x_5,dec(app(?xs,?ys))) = app(dec(cons(s(?x_5),?xs)),dec(?ys)) ]
ES2:
   [ cons(0,app(dec(?xs),dec(?ys))) = app(dec(cons(0,?xs)),dec(?ys)),
     cons(?x_5,app(dec(?xs),dec(?ys))) = app(dec(cons(s(?x_5),?xs)),dec(?ys)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS2:
   [ dec(cons(?x_3,app(?xs_3,?ys_3))) -> app(dec(cons(?x_3,?xs_3)),dec(?ys_3)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
STEP 5
ES:
   [ cons(0,app(dec(?xs),dec(?ys))) = app(dec(cons(0,?xs)),dec(?ys)),
     cons(?x_5,app(dec(?xs),dec(?ys))) = app(dec(cons(s(?x_5),?xs)),dec(?ys)),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS:
   [ dec(cons(?x_3,app(?xs_3,?ys_3))) -> app(dec(cons(?x_3,?xs_3)),dec(?ys_3)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES0:
   [ cons(0,app(dec(?xs),dec(?ys))) = cons(0,app(dec(?xs),dec(?ys))),
     cons(?x_5,app(dec(?xs),dec(?ys))) = cons(?x_5,app(dec(?xs),dec(?ys))),
     cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS0:
   [ dec(cons(?x_3,app(?xs_3,?ys_3))) -> app(dec(cons(?x_3,?xs_3)),dec(?ys_3)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
ES1:
   [ cons(s(0),?xs_4) = cons(0,?xs_4) ]
HS1:
   [ dec(cons(?x_3,app(?xs_3,?ys_3))) -> app(dec(cons(?x_3,?xs_3)),dec(?ys_3)),
     dec(app(?xs,?ys)) -> app(dec(?xs),dec(?ys)),
     app(inc(?xs),inc(?ys)) -> inc(app(?xs,?ys)),
     inc(dec(?xs)) -> ?xs,
     dec(inc(?xs)) -> ?xs ]
No equation to expand
Failed to prove conj part consists of inductive theorems of R0.
new/inc3.trs: Failure(unknown)
(1640 msec.)