(STRATEGY
    INNERMOST)

(VAR
    x10 x7 x3 x2 x1 x6 x5 x4 x82 x90)
(RULES
    rec[x_0][1](f(x10),x7) -> rec[rpm_0][3](x10,f_0(rec[x_0](f(x10))),bot[0]())
    fst_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) ->
      Leaf(snd_cond[1](rec[x_0][1](f(x3),bot[10]()),bot[11]()))
    fst_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5)
                 ,rpm_9(f_0(rec[x_0](f(x4))),x3,x2))
               ,x1) -> Node(fst_cond[1](rec[rpm_0][3](x6
                                                     ,f_0(rec[x_0](f(x7)))
                                                     ,bot[2]())
                                       ,bot[3]())
                           ,fst_cond[1](rec[rpm_0][3](x5
                                                     ,f_0(rec[x_0](f(x7)))
                                                     ,bot[4]())
                                       ,bot[5]()))
    rec[min_0][2](0(),x82) -> 0()
    rec[min_0][2](S(x90),0()) -> 0()
    rec[min_0][2](S(x10),S(x6)) -> S(rec[min_0][2](x10,x6))
    rec[rpm_0][3](Leaf(x3),f_0(rec[x_0](f(x2))),x1) ->
      P(rpm_3(f_0(rec[x_0](f(x2)))),rpm_4(x3))
    rec[rpm_0][3](Node(x4,x3),f_0(rec[x_0](f(x2))),x1) ->
      P(rpm_8(f_0(rec[x_0](f(x2))),x4,x3),rpm_9(f_0(rec[x_0](f(x2))),x4,x3))
    snd_cond[1](P(rpm_3(f_0(rec[x_0](f(x3)))),rpm_4(x2)),x1) -> x2
    snd_cond[1](P(rpm_8(f_0(rec[x_0](f(x7))),x6,x5)
                 ,rpm_9(f_0(rec[x_0](f(x4))),x3,x2))
               ,x1) ->
      rec[min_0][2](snd_cond[1](rec[rpm_0][3](x3,f_0(rec[x_0](f(x4))),bot[6]())
                               ,bot[7]())
                   ,snd_cond[1](rec[rpm_0][3](x2,f_0(rec[x_0](f(x4))),bot[8]())
                               ,bot[9]()))
    main(x3) -> fst_cond[1](rec[x_0][1](f(x3),bot[12]()),bot[13]()))