NO
Rewrite Rules:
   [ null(nil) -> true,
     null(cons(?x,?xs)) -> false,
     tl(nil) -> nil,
     tl(cons(?x,?xs)) -> ?xs,
     len(?xs) -> if(null(?xs),0,s(len(tl(?xs)))),
     if(true,?x,?y) -> ?x,
     if(false,?x,?y) -> ?y,
     app(nil,?ys) -> ?ys,
     app(cons(?x,?xs),?ys) -> cons(?x,app(?xs,?ys)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     len(app(?xs,?ys)) -> +(len(?xs),len(?ys)) ]
Apply Direct Methods...
Inner CPs:
   [ len(?ys_5) = +(len(nil),len(?ys_5)),
     len(cons(?x_6,app(?xs_6,?ys_6))) = +(len(cons(?x_6,?xs_6)),len(?ys_6)) ]
Outer CPs:
   [ if(null(app(?xs_9,?ys_9)),0,s(len(tl(app(?xs_9,?ys_9))))) = +(len(?xs_9),len(?ys_9)) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Left-Linear, not Right-Linear
unknown Development Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ +(len(?xs_9),len(?ys_9)) = if(null(app(?xs_9,?ys_9)),0,s(len(tl(app(?xs_9,?ys_9))))),
     +(len(nil),len(?ys)) = len(?ys),
     +(len(cons(?x,?xs)),len(?ys)) = len(cons(?x,app(?xs,?ys))),
     if(null(?ys),0,s(len(tl(?ys)))) = +(len(nil),len(?ys)),
     if(null(cons(?x_8,app(?xs_8,?ys))),0,s(len(tl(cons(?x_8,app(?xs_8,?ys)))))) = +(len(cons(?x_8,?xs_8)),len(?ys)),
     if(null(app(?xs,?ys)),0,s(len(tl(app(?xs,?ys))))) = +(len(?xs),len(?ys)),
     len(?ys) = +(len(nil),len(?ys)),
     len(cons(?x_8,app(?xs_8,?ys))) = +(len(cons(?x_8,?xs_8)),len(?ys)) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <len(?ys_5), +(len(nil),len(?ys_5))> by Rules <7, 11> preceded by [(len,1)]
 joinable by a reduction of rules <[], [([(+,1)],4),([(+,1),(if,1)],0),([(+,1)],5),([],9)]>
Critical Pair <len(cons(?x_6,app(?xs_6,?ys_6))), +(len(cons(?x_6,?xs_6)),len(?ys_6))> by Rules <8, 11> preceded by [(len,1)]
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,3),(s,1)],11),([(if,1)],1),([],6)], [([(+,1)],4),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1),(if,1)],1),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,3),(s,1)],11),([(if,1)],1),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,3),(s,1)],11),([(if,1)],1),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([(+,1),(s,1),(len,1)],3),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,3),(s,1)],11),([(if,1)],1),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([],10),([(s,1),(+,1),(len,1)],3)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,1)],1),([(if,3),(s,1)],11),([],6)], [([(+,1)],4),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1),(if,1)],1),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,1)],1),([(if,3),(s,1)],11),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,1)],1),([(if,3),(s,1)],11),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([(+,1),(s,1),(len,1)],3),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,1)],1),([(if,3),(s,1)],11),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([],10),([(s,1),(+,1),(len,1)],3)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,1)],1),([],6),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1),(if,1)],1),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,1)],1),([],6),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,1)],1),([],6),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([(+,1),(s,1),(len,1)],3),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,3),(s,1),(len,1)],3),([(if,1)],1),([],6),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([],10),([(s,1),(+,1),(len,1)],3)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([(if,3),(s,1),(len,1)],3),([(if,3),(s,1)],11),([],6)], [([(+,1)],4),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1),(if,1)],1),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([(if,3),(s,1),(len,1)],3),([(if,3),(s,1)],11),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([(if,3),(s,1),(len,1)],3),([(if,3),(s,1)],11),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([(+,1),(s,1),(len,1)],3),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([(if,3),(s,1),(len,1)],3),([(if,3),(s,1)],11),([],6)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([],10),([(s,1),(+,1),(len,1)],3)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([(if,3),(s,1),(len,1)],3),([],6),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1),(if,1)],1),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([(if,3),(s,1),(len,1)],3),([],6),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([(if,3),(s,1),(len,1)],3),([],6),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([(+,1),(s,1),(len,1)],3),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([(if,3),(s,1),(len,1)],3),([],6),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([],10),([(s,1),(+,1),(len,1)],3)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([],6),([(s,1),(len,1)],3),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1),(if,1)],1),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([],6),([(s,1),(len,1)],3),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1),(if,3),(s,1),(len,1)],3),([(+,1)],6),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([],6),([(s,1),(len,1)],3),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([(+,1),(s,1),(len,1)],3),([],10)]>
 joinable by a reduction of rules <[([],4),([(if,1)],1),([],6),([(s,1),(len,1)],3),([(s,1)],11)], [([(+,1)],4),([(+,1),(if,1)],1),([(+,1)],6),([],10),([(s,1),(+,1),(len,1)],3)]>
Critical Pair <+(len(?xs_9),len(?ys_9)), if(null(app(?xs_9,?ys_9)),0,s(len(tl(app(?xs_9,?ys_9)))))> by Rules <11, 4> preceded by []
unknown Diagram Decreasing
   [ null(nil) -> true,
     null(cons(?x,?xs)) -> false,
     tl(nil) -> nil,
     tl(cons(?x_1,?xs_1)) -> ?xs_1,
     len(?xs_2) -> if(null(?xs_2),0,s(len(tl(?xs_2)))),
     if(true,?x_3,?y_3) -> ?x_3,
     if(false,?x_4,?y_4) -> ?y_4,
     app(nil,?ys_5) -> ?ys_5,
     app(cons(?x_6,?xs_6),?ys_6) -> cons(?x_6,app(?xs_6,?ys_6)),
     +(0,?y_7) -> ?y_7,
     +(s(?x_8),?y_8) -> s(+(?x_8,?y_8)),
     len(app(?xs_9,?ys_9)) -> +(len(?xs_9),len(?ys_9)) ]
Sort Assignment:
 + : 44*44=>44
 0 : =>44
 s : 44=>44
 if : 25*44*44=>44
 tl : 47=>47
 app : 47*47=>47
 len : 47=>44
 nil : =>47
 cons : 37*47=>47
 null : 47=>25
 true : =>25
 false : =>25
non-linear variables: {?xs_2}
non-linear types: {47}
types leq non-linear types: {47}
rules applicable to terms of non-linear types:
   [ tl(nil) -> nil,
     tl(cons(?x_1,?xs_1)) -> ?xs_1,
     app(nil,?ys_5) -> ?ys_5,
     app(cons(?x_6,?xs_6),?ys_6) -> cons(?x_6,app(?xs_6,?ys_6)) ]
Rnl:
0: {}
1: {}
2: {}
3: {}
4: {2,3,7,8}
5: {}
6: {}
7: {}
8: {}
9: {}
10: {}
11: {}
terms of non-linear types are innermost terminating
Critical Pair <len(?ys_5), +(len(nil),len(?ys_5))> by Rules <7, 11>
no joinable sequence for some critical pairs
unknown Quasi-Linear & Linearized-Decreasing
   [ null(nil) -> true,
     null(cons(?x,?xs)) -> false,
     tl(nil) -> nil,
     tl(cons(?x_1,?xs_1)) -> ?xs_1,
     len(?xs_2) -> if(null(?xs_2),0,s(len(tl(?xs_2)))),
     if(true,?x_3,?y_3) -> ?x_3,
     if(false,?x_4,?y_4) -> ?y_4,
     app(nil,?ys_5) -> ?ys_5,
     app(cons(?x_6,?xs_6),?ys_6) -> cons(?x_6,app(?xs_6,?ys_6)),
     +(0,?y_7) -> ?y_7,
     +(s(?x_8),?y_8) -> s(+(?x_8,?y_8)),
     len(app(?xs_9,?ys_9)) -> +(len(?xs_9),len(?ys_9)) ]
Sort Assignment:
 + : 44*44=>44
 0 : =>44
 s : 44=>44
 if : 25*44*44=>44
 tl : 47=>47
 app : 47*47=>47
 len : 47=>44
 nil : =>47
 cons : 37*47=>47
 null : 47=>25
 true : =>25
 false : =>25
non-linear variables: {?xs_2}
non-linear types: {47}
types leq non-linear types: {47}
rules applicable to terms of non-linear types:
   [ tl(nil) -> nil,
     tl(cons(?x_1,?xs_1)) -> ?xs_1,
     app(nil,?ys_5) -> ?ys_5,
     app(cons(?x_6,?xs_6),?ys_6) -> cons(?x_6,app(?xs_6,?ys_6)) ]
terms of non-linear types are terminating
Check Joinablility of CP from NLR:
done.
Critical Pair <len(?ys_5), +(len(nil),len(?ys_5))> by Rules <7, 11>
no joinable sequence for some critical pairs
unknown Strongly Quasi-Linear & Hierarchically Decreasing
check Non-Confluence...
obtain 16 rules by 3 steps unfolding
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
   [ null(nil) -> true,
     null(cons(?x:Nat,?xs:List)) -> false,
     tl(nil) -> nil,
     tl(cons(?x:Nat,?xs:List)) -> ?xs:List,
     len(?xs:List) -> if(null(?xs:List),0,s(len(tl(?xs:List)))),
     if(true,?x:Nat,?y:Nat) -> ?x:Nat,
     if(false,?x:Nat,?y:Nat) -> ?y:Nat,
     app(nil,?ys:List) -> ?ys:List,
     app(cons(?x:Nat,?xs:List),?ys:List) -> cons(?x:Nat,app(?xs:List,?ys:List)),
     +(0,?y:Nat) -> ?y:Nat,
     +(s(?x:Nat),?y:Nat) -> s(+(?x:Nat,?y:Nat)),
     len(app(?xs:List,?ys:List)) -> +(len(?xs:List),len(?ys:List)) ]
 (success)
Witness for Non-Confluence: <if(null(app(c_1,c_2)),0,s(len(tl(app(c_1,c_2))))) <- len(app(c_1,c_2)) -> +(if(null(c_1),0,s(len(tl(c_1)))),len(c_2))>
Direct Methods: not CR

Final result: not CR
new/len-app.trs: Success(not CR)
(62 msec.)