(STRATEGY
    INNERMOST)

(VAR
    x12 x13 x14 x11 x24 x2 x1 x4 x3 x8 x16 x28)
(RULES
    cond_eval_e_1(Triple(x12,x13,x14)) -> x12
    eval_e_6#1(x11,0()) -> ite_b#2(True()
                                  ,cond_eval_e_1(div_mod#2(eval#1(x11),0())))
    eval_e_6#1(x11,S(x24)) -> ite_b#2(False()
                                     ,cond_eval_e_1(div_mod#2(eval#1(x11)
                                                             ,S(x24))))
    eval_e_6#1(x11,S(0())) -> ite_b#2(True()
                                     ,cond_eval_e_1(div_mod#2(eval#1(x11)
                                                             ,S(0()))))
    eval#1(Eadd(x2,x1)) -> plus#2(eval#1(x2),eval#1(x1))
    eval#1(Emult(x2,x1)) -> mult#2(eval#1(x2),eval#1(x1))
    eval#1(Ediv(x2,x1)) -> eval_e_6#1(x2,eval#1(x1))
    eval#1(Econst(x1)) -> x1
    mult#2(0(),x2) -> 0()
    mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2))
    cond_div_mod_n_m_2(Triple(x4,x3,x2),x1) -> Triple(plus#2(S(0()),x4),x3,x1)
    cond_div_mod_n_m(Pair(0(),x2),x1) -> Triple(0(),x1,x2)
    cond_div_mod_n_m(Pair(S(x3),x2),x1) -> cond_div_mod_n_m_2(div_mod#2(S(x3)
                                                                       ,x2)
                                                             ,x2)
    div_mod#2(x8,x4) -> cond_div_mod_n_m(Pair(minus'#2(x8,x4),x4),x8)
    plus#2(x16,0()) -> x16
    plus#2(x4,S(x2)) -> S(plus#2(x4,x2))
    minus'#2(0(),x24) -> 0()
    minus'#2(S(x28),0()) -> S(x28)
    minus'#2(S(x4),S(x2)) -> minus'#2(x4,x2)
    main(x28) -> eval#1(x28))