MAYBE

Problem:
 app(app(eq(),0()),0()) -> true()
 app(app(eq(),0()),app(s(),x)) -> false()
 app(app(eq(),app(s(),x)),0()) -> false()
 app(app(eq(),app(s(),x)),app(s(),y)) -> app(app(eq(),x),y)
 app(app(or(),true()),y) -> true()
 app(app(or(),false()),y) -> y
 app(app(union(),empty()),h) -> h
 app(app(union(),app(app(app(edge(),x),y),i)),h) -> app(app(app(edge(),x),y),app(app(union(),i),h))
 app(app(app(app(reach(),x),y),empty()),h) -> false()
 app(app(app(app(reach(),x),y),app(app(app(edge(),u),v),i)),h) ->
 app(app(app(app(app(if_reach_1(),app(app(eq(),x),u)),x),y),app(app(app(edge(),u),v),i)),h)
 app(app(app(app(app(if_reach_1(),true()),x),y),app(app(app(edge(),u),v),i)),h) ->
 app(app(app(app(app(if_reach_2(),app(app(eq(),y),v)),x),y),app(app(app(edge(),u),v),i)),h)
 app(app(app(app(app(if_reach_1(),false()),x),y),app(app(app(edge(),u),v),i)),h) ->
 app(app(app(app(reach(),x),y),i),app(app(app(edge(),u),v),h))
 app(app(app(app(app(if_reach_2(),true()),x),y),app(app(app(edge(),u),v),i)),h) -> true()
 app(app(app(app(app(if_reach_2(),false()),x),y),app(app(app(edge(),u),v),i)),h) ->
 app(app(or(),app(app(app(app(reach(),x),y),i),h)),app(app(app(app(reach(),v),y),
                                                           app(app(union(),i),h)),
                                                       empty()))
 app(app(map(),f),nil()) -> nil()
 app(app(map(),f),app(app(cons(),x),xs)) -> app(app(cons(),app(f,x)),app(app(map(),f),xs))
 app(app(filter(),f),nil()) -> nil()
 app(app(filter(),f),app(app(cons(),x),xs)) -> app(app(app(app(filter2(),app(f,x)),f),x),xs)
 app(app(app(app(filter2(),true()),f),x),xs) -> app(app(cons(),x),app(app(filter(),f),xs))
 app(app(app(app(filter2(),false()),f),x),xs) -> app(app(filter(),f),xs)

Proof:
 Open