/home/nowonder/forschung/aprove/TPDB05/TRS/secret2005/aprove1.trs

The program

(VAR f x y xs f g ys)
(RULES
ap(ap(map,f),xs) -> ap(ap(ap(if,ap(isEmpty,xs)),f),xs)
ap(ap(ap(if,true),f),xs) -> null
ap(ap(ap(if,null),f),xs) -> ap(ap(cons,ap(f,ap(last,xs))),ap(ap(if2,f),xs))
ap(ap(if2,f),xs) -> ap(ap(map,f),ap(dropLast,xs))

ap(isEmpty,null) -> true
ap(isEmpty,ap(ap(cons,x),xs)) -> null

ap(last,ap(ap(cons,x),null)) -> x
ap(last,ap(ap(cons,x),ap(ap(cons,y),ys))) -> ap(last,ap(ap(cons,y),ys))

ap(dropLast,ap(ap(cons,x),null)) -> null
ap(dropLast,ap(ap(cons,x),ap(ap(cons,y),ys))) -> ap(ap(cons,x),ap(dropLast,ap(ap(cons,y),ys)))
)

(COMMENT
dropped these rules due to restrictions on secret examples

ap(dropLast,nil) -> nil
ap(ap(ap(if,false),f),xs) -> ap(ap(cons,ap(f,ap(last,xs))),ap(ap(map,f),ap(dropLast,xs)))

and therefore added the second if->if2, and the if2->map rule

moreover, to get the correct nr of functionsymbols,
I identified nil and false to null


the original system is 

ap(ap(map,f),xs) -> ap(ap(ap(if,ap(isEmpty,xs)),f),xs)
ap(ap(ap(if,true),f),xs) -> nil
ap(ap(ap(if,false),f),xs) -> ap(ap(cons,ap(f,ap(last,xs))),ap(ap(map,f),ap(dropLast,xs)))

ap(isEmpty,nil) -> true
ap(isEmpty,ap(ap(cons,x),xs)) -> false

ap(last,ap(ap(cons,x),nil)) -> x
ap(last,ap(ap(cons,x),ap(ap(cons,y),ys))) -> ap(last,ap(ap(cons,y),ys))

ap(dropLast,nil) -> nil
ap(dropLast,ap(ap(cons,x),nil)) -> nil
ap(dropLast,ap(ap(cons,x),ap(ap(cons,y),ys))) -> ap(ap(cons,x),ap(dropLast,ap(ap(cons,y),ys)))

but in this TRS the second if-rule has 11 function-symbols
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend