Problem:
 ap(f(),x) -> x
 ap(ap(ap(g(),x),y),ap(s(),z)) -> ap(ap(ap(g(),x),y),ap(ap(x,y),0()))

Proof:
 Uncurry Processor:
  f1(x) -> x
  g3(x,y,s1(z)) -> g3(x,y,ap(ap(x,y),0()))
  ap(f(),x5) -> f1(x5)
  ap(g2(x4,x3),x5) -> g3(x4,x3,x5)
  ap(g1(x4),x5) -> g2(x4,x5)
  ap(g(),x5) -> g1(x5)
  ap(s(),x5) -> s1(x5)
  Unfolding Processor:
   loop length: 4
   terms:
    g3(f(),s(),s1(z))
    g3(f(),s(),ap(ap(f(),s()),0()))
    g3(f(),s(),ap(f1(s()),0()))
    g3(f(),s(),ap(s(),0()))
   context: []
   substitution:
    z -> 0()
   Qed