MAYBE

Problem:
 plus(x,y) -> ifPlus(isZero(x),x,inc(y))
 ifPlus(true(),x,y) -> p(y)
 ifPlus(false(),x,y) -> plus(p(x),y)
 times(x,y) -> timesIter(0(),x,y,0())
 timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
 ifTimes(true(),i,x,y,z) -> z
 ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
 isZero(0()) -> true()
 isZero(s(0())) -> false()
 isZero(s(s(x))) -> isZero(s(x))
 inc(0()) -> s(0())
 inc(s(x)) -> s(inc(x))
 inc(x) -> s(x)
 p(0()) -> 0()
 p(s(x)) -> x
 p(s(s(x))) -> s(p(s(x)))
 ge(x,0()) -> true()
 ge(0(),s(y)) -> false()
 ge(s(x),s(y)) -> ge(x,y)
 f0(0(),y,x) -> f1(x,y,x)
 f1(x,y,z) -> f2(x,y,z)
 f2(x,1(),z) -> f0(x,z,z)
 f0(x,y,z) -> d()
 f1(x,y,z) -> c()

Proof:
 DP Processor:
  DPs:
   plus#(x,y) -> inc#(y)
   plus#(x,y) -> isZero#(x)
   plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
   ifPlus#(true(),x,y) -> p#(y)
   ifPlus#(false(),x,y) -> p#(x)
   ifPlus#(false(),x,y) -> plus#(p(x),y)
   times#(x,y) -> timesIter#(0(),x,y,0())
   timesIter#(i,x,y,z) -> ge#(i,x)
   timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
   ifTimes#(false(),i,x,y,z) -> plus#(z,y)
   ifTimes#(false(),i,x,y,z) -> inc#(i)
   ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
   isZero#(s(s(x))) -> isZero#(s(x))
   inc#(s(x)) -> inc#(x)
   p#(s(s(x))) -> p#(s(x))
   ge#(s(x),s(y)) -> ge#(x,y)
   f0#(0(),y,x) -> f1#(x,y,x)
   f1#(x,y,z) -> f2#(x,y,z)
   f2#(x,1(),z) -> f0#(x,z,z)
  TRS:
   plus(x,y) -> ifPlus(isZero(x),x,inc(y))
   ifPlus(true(),x,y) -> p(y)
   ifPlus(false(),x,y) -> plus(p(x),y)
   times(x,y) -> timesIter(0(),x,y,0())
   timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
   ifTimes(true(),i,x,y,z) -> z
   ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
   isZero(0()) -> true()
   isZero(s(0())) -> false()
   isZero(s(s(x))) -> isZero(s(x))
   inc(0()) -> s(0())
   inc(s(x)) -> s(inc(x))
   inc(x) -> s(x)
   p(0()) -> 0()
   p(s(x)) -> x
   p(s(s(x))) -> s(p(s(x)))
   ge(x,0()) -> true()
   ge(0(),s(y)) -> false()
   ge(s(x),s(y)) -> ge(x,y)
   f0(0(),y,x) -> f1(x,y,x)
   f1(x,y,z) -> f2(x,y,z)
   f2(x,1(),z) -> f0(x,z,z)
   f0(x,y,z) -> d()
   f1(x,y,z) -> c()
  EDG Processor:
   DPs:
    plus#(x,y) -> inc#(y)
    plus#(x,y) -> isZero#(x)
    plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
    ifPlus#(true(),x,y) -> p#(y)
    ifPlus#(false(),x,y) -> p#(x)
    ifPlus#(false(),x,y) -> plus#(p(x),y)
    times#(x,y) -> timesIter#(0(),x,y,0())
    timesIter#(i,x,y,z) -> ge#(i,x)
    timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
    ifTimes#(false(),i,x,y,z) -> plus#(z,y)
    ifTimes#(false(),i,x,y,z) -> inc#(i)
    ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
    isZero#(s(s(x))) -> isZero#(s(x))
    inc#(s(x)) -> inc#(x)
    p#(s(s(x))) -> p#(s(x))
    ge#(s(x),s(y)) -> ge#(x,y)
    f0#(0(),y,x) -> f1#(x,y,x)
    f1#(x,y,z) -> f2#(x,y,z)
    f2#(x,1(),z) -> f0#(x,z,z)
   TRS:
    plus(x,y) -> ifPlus(isZero(x),x,inc(y))
    ifPlus(true(),x,y) -> p(y)
    ifPlus(false(),x,y) -> plus(p(x),y)
    times(x,y) -> timesIter(0(),x,y,0())
    timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
    ifTimes(true(),i,x,y,z) -> z
    ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
    isZero(0()) -> true()
    isZero(s(0())) -> false()
    isZero(s(s(x))) -> isZero(s(x))
    inc(0()) -> s(0())
    inc(s(x)) -> s(inc(x))
    inc(x) -> s(x)
    p(0()) -> 0()
    p(s(x)) -> x
    p(s(s(x))) -> s(p(s(x)))
    ge(x,0()) -> true()
    ge(0(),s(y)) -> false()
    ge(s(x),s(y)) -> ge(x,y)
    f0(0(),y,x) -> f1(x,y,x)
    f1(x,y,z) -> f2(x,y,z)
    f2(x,1(),z) -> f0(x,z,z)
    f0(x,y,z) -> d()
    f1(x,y,z) -> c()
   graph:
    f2#(x,1(),z) -> f0#(x,z,z) -> f0#(0(),y,x) -> f1#(x,y,x)
    f1#(x,y,z) -> f2#(x,y,z) -> f2#(x,1(),z) -> f0#(x,z,z)
    f0#(0(),y,x) -> f1#(x,y,x) ->
    f1#(x,y,z) -> f2#(x,y,z)
    ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y)) ->
    timesIter#(i,x,y,z) -> ge#(i,x)
    ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y)) ->
    timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
    ifTimes#(false(),i,x,y,z) -> inc#(i) ->
    inc#(s(x)) -> inc#(x)
    ifTimes#(false(),i,x,y,z) -> plus#(z,y) ->
    plus#(x,y) -> inc#(y)
    ifTimes#(false(),i,x,y,z) -> plus#(z,y) ->
    plus#(x,y) -> isZero#(x)
    ifTimes#(false(),i,x,y,z) -> plus#(z,y) ->
    plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
    ge#(s(x),s(y)) -> ge#(x,y) ->
    ge#(s(x),s(y)) -> ge#(x,y)
    timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z) ->
    ifTimes#(false(),i,x,y,z) -> plus#(z,y)
    timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z) ->
    ifTimes#(false(),i,x,y,z) -> inc#(i)
    timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z) ->
    ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
    timesIter#(i,x,y,z) -> ge#(i,x) ->
    ge#(s(x),s(y)) -> ge#(x,y)
    times#(x,y) -> timesIter#(0(),x,y,0()) ->
    timesIter#(i,x,y,z) -> ge#(i,x)
    times#(x,y) -> timesIter#(0(),x,y,0()) ->
    timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
    p#(s(s(x))) -> p#(s(x)) -> p#(s(s(x))) -> p#(s(x))
    ifPlus#(false(),x,y) -> p#(x) -> p#(s(s(x))) -> p#(s(x))
    ifPlus#(false(),x,y) -> plus#(p(x),y) ->
    plus#(x,y) -> inc#(y)
    ifPlus#(false(),x,y) -> plus#(p(x),y) ->
    plus#(x,y) -> isZero#(x)
    ifPlus#(false(),x,y) -> plus#(p(x),y) ->
    plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
    ifPlus#(true(),x,y) -> p#(y) -> p#(s(s(x))) -> p#(s(x))
    isZero#(s(s(x))) -> isZero#(s(x)) -> isZero#(s(s(x))) -> isZero#(s(x))
    inc#(s(x)) -> inc#(x) -> inc#(s(x)) -> inc#(x)
    plus#(x,y) -> ifPlus#(isZero(x),x,inc(y)) ->
    ifPlus#(true(),x,y) -> p#(y)
    plus#(x,y) -> ifPlus#(isZero(x),x,inc(y)) ->
    ifPlus#(false(),x,y) -> p#(x)
    plus#(x,y) -> ifPlus#(isZero(x),x,inc(y)) ->
    ifPlus#(false(),x,y) -> plus#(p(x),y)
    plus#(x,y) -> isZero#(x) -> isZero#(s(s(x))) -> isZero#(s(x))
    plus#(x,y) -> inc#(y) -> inc#(s(x)) -> inc#(x)
   SCC Processor:
    #sccs: 7
    #rules: 11
    #arcs: 29/361
    DPs:
     ifTimes#(false(),i,x,y,z) -> timesIter#(inc(i),x,y,plus(z,y))
     timesIter#(i,x,y,z) -> ifTimes#(ge(i,x),i,x,y,z)
    TRS:
     plus(x,y) -> ifPlus(isZero(x),x,inc(y))
     ifPlus(true(),x,y) -> p(y)
     ifPlus(false(),x,y) -> plus(p(x),y)
     times(x,y) -> timesIter(0(),x,y,0())
     timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
     ifTimes(true(),i,x,y,z) -> z
     ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
     isZero(0()) -> true()
     isZero(s(0())) -> false()
     isZero(s(s(x))) -> isZero(s(x))
     inc(0()) -> s(0())
     inc(s(x)) -> s(inc(x))
     inc(x) -> s(x)
     p(0()) -> 0()
     p(s(x)) -> x
     p(s(s(x))) -> s(p(s(x)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     f0(0(),y,x) -> f1(x,y,x)
     f1(x,y,z) -> f2(x,y,z)
     f2(x,1(),z) -> f0(x,z,z)
     f0(x,y,z) -> d()
     f1(x,y,z) -> c()
    Open
    
    DPs:
     ge#(s(x),s(y)) -> ge#(x,y)
    TRS:
     plus(x,y) -> ifPlus(isZero(x),x,inc(y))
     ifPlus(true(),x,y) -> p(y)
     ifPlus(false(),x,y) -> plus(p(x),y)
     times(x,y) -> timesIter(0(),x,y,0())
     timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
     ifTimes(true(),i,x,y,z) -> z
     ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
     isZero(0()) -> true()
     isZero(s(0())) -> false()
     isZero(s(s(x))) -> isZero(s(x))
     inc(0()) -> s(0())
     inc(s(x)) -> s(inc(x))
     inc(x) -> s(x)
     p(0()) -> 0()
     p(s(x)) -> x
     p(s(s(x))) -> s(p(s(x)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     f0(0(),y,x) -> f1(x,y,x)
     f1(x,y,z) -> f2(x,y,z)
     f2(x,1(),z) -> f0(x,z,z)
     f0(x,y,z) -> d()
     f1(x,y,z) -> c()
    Subterm Criterion Processor:
     simple projection:
      pi(ge#) = 1
     problem:
      DPs:
       
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
     Qed
    
    DPs:
     plus#(x,y) -> ifPlus#(isZero(x),x,inc(y))
     ifPlus#(false(),x,y) -> plus#(p(x),y)
    TRS:
     plus(x,y) -> ifPlus(isZero(x),x,inc(y))
     ifPlus(true(),x,y) -> p(y)
     ifPlus(false(),x,y) -> plus(p(x),y)
     times(x,y) -> timesIter(0(),x,y,0())
     timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
     ifTimes(true(),i,x,y,z) -> z
     ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
     isZero(0()) -> true()
     isZero(s(0())) -> false()
     isZero(s(s(x))) -> isZero(s(x))
     inc(0()) -> s(0())
     inc(s(x)) -> s(inc(x))
     inc(x) -> s(x)
     p(0()) -> 0()
     p(s(x)) -> x
     p(s(s(x))) -> s(p(s(x)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     f0(0(),y,x) -> f1(x,y,x)
     f1(x,y,z) -> f2(x,y,z)
     f2(x,1(),z) -> f0(x,z,z)
     f0(x,y,z) -> d()
     f1(x,y,z) -> c()
    Open
    
    DPs:
     p#(s(s(x))) -> p#(s(x))
    TRS:
     plus(x,y) -> ifPlus(isZero(x),x,inc(y))
     ifPlus(true(),x,y) -> p(y)
     ifPlus(false(),x,y) -> plus(p(x),y)
     times(x,y) -> timesIter(0(),x,y,0())
     timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
     ifTimes(true(),i,x,y,z) -> z
     ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
     isZero(0()) -> true()
     isZero(s(0())) -> false()
     isZero(s(s(x))) -> isZero(s(x))
     inc(0()) -> s(0())
     inc(s(x)) -> s(inc(x))
     inc(x) -> s(x)
     p(0()) -> 0()
     p(s(x)) -> x
     p(s(s(x))) -> s(p(s(x)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     f0(0(),y,x) -> f1(x,y,x)
     f1(x,y,z) -> f2(x,y,z)
     f2(x,1(),z) -> f0(x,z,z)
     f0(x,y,z) -> d()
     f1(x,y,z) -> c()
    Subterm Criterion Processor:
     simple projection:
      pi(p#) = 0
     problem:
      DPs:
       
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
     Qed
    
    DPs:
     isZero#(s(s(x))) -> isZero#(s(x))
    TRS:
     plus(x,y) -> ifPlus(isZero(x),x,inc(y))
     ifPlus(true(),x,y) -> p(y)
     ifPlus(false(),x,y) -> plus(p(x),y)
     times(x,y) -> timesIter(0(),x,y,0())
     timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
     ifTimes(true(),i,x,y,z) -> z
     ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
     isZero(0()) -> true()
     isZero(s(0())) -> false()
     isZero(s(s(x))) -> isZero(s(x))
     inc(0()) -> s(0())
     inc(s(x)) -> s(inc(x))
     inc(x) -> s(x)
     p(0()) -> 0()
     p(s(x)) -> x
     p(s(s(x))) -> s(p(s(x)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     f0(0(),y,x) -> f1(x,y,x)
     f1(x,y,z) -> f2(x,y,z)
     f2(x,1(),z) -> f0(x,z,z)
     f0(x,y,z) -> d()
     f1(x,y,z) -> c()
    Subterm Criterion Processor:
     simple projection:
      pi(isZero#) = 0
     problem:
      DPs:
       
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
     Qed
    
    DPs:
     inc#(s(x)) -> inc#(x)
    TRS:
     plus(x,y) -> ifPlus(isZero(x),x,inc(y))
     ifPlus(true(),x,y) -> p(y)
     ifPlus(false(),x,y) -> plus(p(x),y)
     times(x,y) -> timesIter(0(),x,y,0())
     timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
     ifTimes(true(),i,x,y,z) -> z
     ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
     isZero(0()) -> true()
     isZero(s(0())) -> false()
     isZero(s(s(x))) -> isZero(s(x))
     inc(0()) -> s(0())
     inc(s(x)) -> s(inc(x))
     inc(x) -> s(x)
     p(0()) -> 0()
     p(s(x)) -> x
     p(s(s(x))) -> s(p(s(x)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     f0(0(),y,x) -> f1(x,y,x)
     f1(x,y,z) -> f2(x,y,z)
     f2(x,1(),z) -> f0(x,z,z)
     f0(x,y,z) -> d()
     f1(x,y,z) -> c()
    Subterm Criterion Processor:
     simple projection:
      pi(inc#) = 0
     problem:
      DPs:
       
      TRS:
       plus(x,y) -> ifPlus(isZero(x),x,inc(y))
       ifPlus(true(),x,y) -> p(y)
       ifPlus(false(),x,y) -> plus(p(x),y)
       times(x,y) -> timesIter(0(),x,y,0())
       timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
       ifTimes(true(),i,x,y,z) -> z
       ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
       isZero(0()) -> true()
       isZero(s(0())) -> false()
       isZero(s(s(x))) -> isZero(s(x))
       inc(0()) -> s(0())
       inc(s(x)) -> s(inc(x))
       inc(x) -> s(x)
       p(0()) -> 0()
       p(s(x)) -> x
       p(s(s(x))) -> s(p(s(x)))
       ge(x,0()) -> true()
       ge(0(),s(y)) -> false()
       ge(s(x),s(y)) -> ge(x,y)
       f0(0(),y,x) -> f1(x,y,x)
       f1(x,y,z) -> f2(x,y,z)
       f2(x,1(),z) -> f0(x,z,z)
       f0(x,y,z) -> d()
       f1(x,y,z) -> c()
     Qed
    
    DPs:
     f2#(x,1(),z) -> f0#(x,z,z)
     f0#(0(),y,x) -> f1#(x,y,x)
     f1#(x,y,z) -> f2#(x,y,z)
    TRS:
     plus(x,y) -> ifPlus(isZero(x),x,inc(y))
     ifPlus(true(),x,y) -> p(y)
     ifPlus(false(),x,y) -> plus(p(x),y)
     times(x,y) -> timesIter(0(),x,y,0())
     timesIter(i,x,y,z) -> ifTimes(ge(i,x),i,x,y,z)
     ifTimes(true(),i,x,y,z) -> z
     ifTimes(false(),i,x,y,z) -> timesIter(inc(i),x,y,plus(z,y))
     isZero(0()) -> true()
     isZero(s(0())) -> false()
     isZero(s(s(x))) -> isZero(s(x))
     inc(0()) -> s(0())
     inc(s(x)) -> s(inc(x))
     inc(x) -> s(x)
     p(0()) -> 0()
     p(s(x)) -> x
     p(s(s(x))) -> s(p(s(x)))
     ge(x,0()) -> true()
     ge(0(),s(y)) -> false()
     ge(s(x),s(y)) -> ge(x,y)
     f0(0(),y,x) -> f1(x,y,x)
     f1(x,y,z) -> f2(x,y,z)
     f2(x,1(),z) -> f0(x,z,z)
     f0(x,y,z) -> d()
     f1(x,y,z) -> c()
    Open