MAYBE
Time: 0.043473
TRS:
 {    active minus(0(), Y) -> mark 0(),
    active minus(s X, s Y) -> mark minus(X, Y),
                active s X -> s active X,
        active geq(X, 0()) -> mark true(),
      active geq(0(), s Y) -> mark false(),
      active geq(s X, s Y) -> mark geq(X, Y),
        active div(X1, X2) -> div(active X1, X2),
      active div(0(), s Y) -> mark 0(),
      active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
     active if(X1, X2, X3) -> if(active X1, X2, X3),
   active if(true(), X, Y) -> mark X,
  active if(false(), X, Y) -> mark Y,
       minus(ok X1, ok X2) -> ok minus(X1, X2),
                  s mark X -> mark s X,
                    s ok X -> ok s X,
         geq(ok X1, ok X2) -> ok geq(X1, X2),
          div(mark X1, X2) -> mark div(X1, X2),
         div(ok X1, ok X2) -> ok div(X1, X2),
       if(mark X1, X2, X3) -> mark if(X1, X2, X3),
   if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                proper 0() -> ok 0(),
      proper minus(X1, X2) -> minus(proper X1, proper X2),
                proper s X -> s proper X,
             proper true() -> ok true(),
        proper geq(X1, X2) -> geq(proper X1, proper X2),
            proper false() -> ok false(),
        proper div(X1, X2) -> div(proper X1, proper X2),
     proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                top mark X -> top proper X,
                  top ok X -> top active X}
 DP:
  DP:
   { active# minus(s X, s Y) -> minus#(X, Y),
                 active# s X -> active# X,
                 active# s X -> s# active X,
       active# geq(s X, s Y) -> geq#(X, Y),
         active# div(X1, X2) -> active# X1,
         active# div(X1, X2) -> div#(active X1, X2),
       active# div(s X, s Y) -> minus#(X, Y),
       active# div(s X, s Y) -> s# div(minus(X, Y), s Y),
       active# div(s X, s Y) -> geq#(X, Y),
       active# div(s X, s Y) -> div#(minus(X, Y), s Y),
       active# div(s X, s Y) -> if#(geq(X, Y), s div(minus(X, Y), s Y), 0()),
      active# if(X1, X2, X3) -> active# X1,
      active# if(X1, X2, X3) -> if#(active X1, X2, X3),
        minus#(ok X1, ok X2) -> minus#(X1, X2),
                   s# mark X -> s# X,
                     s# ok X -> s# X,
          geq#(ok X1, ok X2) -> geq#(X1, X2),
           div#(mark X1, X2) -> div#(X1, X2),
          div#(ok X1, ok X2) -> div#(X1, X2),
        if#(mark X1, X2, X3) -> if#(X1, X2, X3),
    if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3),
       proper# minus(X1, X2) -> minus#(proper X1, proper X2),
       proper# minus(X1, X2) -> proper# X1,
       proper# minus(X1, X2) -> proper# X2,
                 proper# s X -> s# proper X,
                 proper# s X -> proper# X,
         proper# geq(X1, X2) -> geq#(proper X1, proper X2),
         proper# geq(X1, X2) -> proper# X1,
         proper# geq(X1, X2) -> proper# X2,
         proper# div(X1, X2) -> div#(proper X1, proper X2),
         proper# div(X1, X2) -> proper# X1,
         proper# div(X1, X2) -> proper# X2,
      proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3),
      proper# if(X1, X2, X3) -> proper# X1,
      proper# if(X1, X2, X3) -> proper# X2,
      proper# if(X1, X2, X3) -> proper# X3,
                 top# mark X -> proper# X,
                 top# mark X -> top# proper X,
                   top# ok X -> active# X,
                   top# ok X -> top# active X}
  TRS:
  {    active minus(0(), Y) -> mark 0(),
     active minus(s X, s Y) -> mark minus(X, Y),
                 active s X -> s active X,
         active geq(X, 0()) -> mark true(),
       active geq(0(), s Y) -> mark false(),
       active geq(s X, s Y) -> mark geq(X, Y),
         active div(X1, X2) -> div(active X1, X2),
       active div(0(), s Y) -> mark 0(),
       active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
      active if(X1, X2, X3) -> if(active X1, X2, X3),
    active if(true(), X, Y) -> mark X,
   active if(false(), X, Y) -> mark Y,
        minus(ok X1, ok X2) -> ok minus(X1, X2),
                   s mark X -> mark s X,
                     s ok X -> ok s X,
          geq(ok X1, ok X2) -> ok geq(X1, X2),
           div(mark X1, X2) -> mark div(X1, X2),
          div(ok X1, ok X2) -> ok div(X1, X2),
        if(mark X1, X2, X3) -> mark if(X1, X2, X3),
    if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                 proper 0() -> ok 0(),
       proper minus(X1, X2) -> minus(proper X1, proper X2),
                 proper s X -> s proper X,
              proper true() -> ok true(),
         proper geq(X1, X2) -> geq(proper X1, proper X2),
             proper false() -> ok false(),
         proper div(X1, X2) -> div(proper X1, proper X2),
      proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                 top mark X -> top proper X,
                   top ok X -> top active X}
  UR:
   {    active minus(0(), Y) -> mark 0(),
      active minus(s X, s Y) -> mark minus(X, Y),
                  active s X -> s active X,
          active geq(X, 0()) -> mark true(),
        active geq(0(), s Y) -> mark false(),
        active geq(s X, s Y) -> mark geq(X, Y),
          active div(X1, X2) -> div(active X1, X2),
        active div(0(), s Y) -> mark 0(),
        active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
       active if(X1, X2, X3) -> if(active X1, X2, X3),
     active if(true(), X, Y) -> mark X,
    active if(false(), X, Y) -> mark Y,
         minus(ok X1, ok X2) -> ok minus(X1, X2),
                    s mark X -> mark s X,
                      s ok X -> ok s X,
           geq(ok X1, ok X2) -> ok geq(X1, X2),
            div(mark X1, X2) -> mark div(X1, X2),
           div(ok X1, ok X2) -> ok div(X1, X2),
         if(mark X1, X2, X3) -> mark if(X1, X2, X3),
     if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                  proper 0() -> ok 0(),
        proper minus(X1, X2) -> minus(proper X1, proper X2),
                  proper s X -> s proper X,
               proper true() -> ok true(),
          proper geq(X1, X2) -> geq(proper X1, proper X2),
              proper false() -> ok false(),
          proper div(X1, X2) -> div(proper X1, proper X2),
       proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {
     (proper# s X -> s# proper X, s# ok X -> s# X)
     (proper# s X -> s# proper X, s# mark X -> s# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (active# div(X1, X2) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# div(X1, X2) -> active# X1, active# if(X1, X2, X3) -> active# X1)
     (active# div(X1, X2) -> active# X1, active# div(s X, s Y) -> if#(geq(X, Y), s div(minus(X, Y), s Y), 0()))
     (active# div(X1, X2) -> active# X1, active# div(s X, s Y) -> div#(minus(X, Y), s Y))
     (active# div(X1, X2) -> active# X1, active# div(s X, s Y) -> geq#(X, Y))
     (active# div(X1, X2) -> active# X1, active# div(s X, s Y) -> s# div(minus(X, Y), s Y))
     (active# div(X1, X2) -> active# X1, active# div(s X, s Y) -> minus#(X, Y))
     (active# div(X1, X2) -> active# X1, active# div(X1, X2) -> div#(active X1, X2))
     (active# div(X1, X2) -> active# X1, active# div(X1, X2) -> active# X1)
     (active# div(X1, X2) -> active# X1, active# geq(s X, s Y) -> geq#(X, Y))
     (active# div(X1, X2) -> active# X1, active# s X -> s# active X)
     (active# div(X1, X2) -> active# X1, active# s X -> active# X)
     (active# div(X1, X2) -> active# X1, active# minus(s X, s Y) -> minus#(X, Y))
     (proper# minus(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
     (proper# minus(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
     (proper# minus(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
     (proper# minus(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# minus(X1, X2) -> proper# X1, proper# div(X1, X2) -> proper# X2)
     (proper# minus(X1, X2) -> proper# X1, proper# div(X1, X2) -> proper# X1)
     (proper# minus(X1, X2) -> proper# X1, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# minus(X1, X2) -> proper# X1, proper# geq(X1, X2) -> proper# X2)
     (proper# minus(X1, X2) -> proper# X1, proper# geq(X1, X2) -> proper# X1)
     (proper# minus(X1, X2) -> proper# X1, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# minus(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# minus(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# minus(X1, X2) -> proper# X1, proper# minus(X1, X2) -> proper# X2)
     (proper# minus(X1, X2) -> proper# X1, proper# minus(X1, X2) -> proper# X1)
     (proper# minus(X1, X2) -> proper# X1, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# div(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
     (proper# div(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
     (proper# div(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
     (proper# div(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# div(X1, X2) -> proper# X1, proper# div(X1, X2) -> proper# X2)
     (proper# div(X1, X2) -> proper# X1, proper# div(X1, X2) -> proper# X1)
     (proper# div(X1, X2) -> proper# X1, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# div(X1, X2) -> proper# X1, proper# geq(X1, X2) -> proper# X2)
     (proper# div(X1, X2) -> proper# X1, proper# geq(X1, X2) -> proper# X1)
     (proper# div(X1, X2) -> proper# X1, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# div(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# div(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# div(X1, X2) -> proper# X1, proper# minus(X1, X2) -> proper# X2)
     (proper# div(X1, X2) -> proper# X1, proper# minus(X1, X2) -> proper# X1)
     (proper# div(X1, X2) -> proper# X1, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X3)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X3, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# if(X1, X2, X3) -> proper# X3, proper# div(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X3, proper# div(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X3, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X3, proper# geq(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X3, proper# geq(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X3, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# s X -> s# proper X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# minus(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X3, proper# minus(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X3, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (active# geq(s X, s Y) -> geq#(X, Y), geq#(ok X1, ok X2) -> geq#(X1, X2))
     (active# div(s X, s Y) -> geq#(X, Y), geq#(ok X1, ok X2) -> geq#(X1, X2))
     (active# div(s X, s Y) -> div#(minus(X, Y), s Y), div#(ok X1, ok X2) -> div#(X1, X2))
     (proper# geq(X1, X2) -> geq#(proper X1, proper X2), geq#(ok X1, ok X2) -> geq#(X1, X2))
     (active# div(X1, X2) -> div#(active X1, X2), div#(ok X1, ok X2) -> div#(X1, X2))
     (active# div(X1, X2) -> div#(active X1, X2), div#(mark X1, X2) -> div#(X1, X2))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# s X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# s X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (active# s X -> active# X, active# div(s X, s Y) -> if#(geq(X, Y), s div(minus(X, Y), s Y), 0()))
     (active# s X -> active# X, active# div(s X, s Y) -> div#(minus(X, Y), s Y))
     (active# s X -> active# X, active# div(s X, s Y) -> geq#(X, Y))
     (active# s X -> active# X, active# div(s X, s Y) -> s# div(minus(X, Y), s Y))
     (active# s X -> active# X, active# div(s X, s Y) -> minus#(X, Y))
     (active# s X -> active# X, active# div(X1, X2) -> div#(active X1, X2))
     (active# s X -> active# X, active# div(X1, X2) -> active# X1)
     (active# s X -> active# X, active# geq(s X, s Y) -> geq#(X, Y))
     (active# s X -> active# X, active# s X -> s# active X)
     (active# s X -> active# X, active# s X -> active# X)
     (active# s X -> active# X, active# minus(s X, s Y) -> minus#(X, Y))
     (s# ok X -> s# X, s# ok X -> s# X)
     (s# ok X -> s# X, s# mark X -> s# X)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (top# mark X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (top# mark X -> proper# X, proper# div(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# div(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# geq(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# geq(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# s X -> proper# X)
     (top# mark X -> proper# X, proper# s X -> s# proper X)
     (top# mark X -> proper# X, proper# minus(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# minus(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# minus(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
     (proper# minus(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
     (proper# minus(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
     (proper# minus(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# minus(X1, X2) -> proper# X2, proper# div(X1, X2) -> proper# X2)
     (proper# minus(X1, X2) -> proper# X2, proper# div(X1, X2) -> proper# X1)
     (proper# minus(X1, X2) -> proper# X2, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# minus(X1, X2) -> proper# X2, proper# geq(X1, X2) -> proper# X2)
     (proper# minus(X1, X2) -> proper# X2, proper# geq(X1, X2) -> proper# X1)
     (proper# minus(X1, X2) -> proper# X2, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# minus(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# minus(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# minus(X1, X2) -> proper# X2, proper# minus(X1, X2) -> proper# X2)
     (proper# minus(X1, X2) -> proper# X2, proper# minus(X1, X2) -> proper# X1)
     (proper# minus(X1, X2) -> proper# X2, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# div(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
     (proper# div(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
     (proper# div(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
     (proper# div(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# div(X1, X2) -> proper# X2, proper# div(X1, X2) -> proper# X2)
     (proper# div(X1, X2) -> proper# X2, proper# div(X1, X2) -> proper# X1)
     (proper# div(X1, X2) -> proper# X2, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# div(X1, X2) -> proper# X2, proper# geq(X1, X2) -> proper# X2)
     (proper# div(X1, X2) -> proper# X2, proper# geq(X1, X2) -> proper# X1)
     (proper# div(X1, X2) -> proper# X2, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# div(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# div(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# div(X1, X2) -> proper# X2, proper# minus(X1, X2) -> proper# X2)
     (proper# div(X1, X2) -> proper# X2, proper# minus(X1, X2) -> proper# X1)
     (proper# div(X1, X2) -> proper# X2, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (minus#(ok X1, ok X2) -> minus#(X1, X2), minus#(ok X1, ok X2) -> minus#(X1, X2))
     (div#(mark X1, X2) -> div#(X1, X2), div#(ok X1, ok X2) -> div#(X1, X2))
     (div#(mark X1, X2) -> div#(X1, X2), div#(mark X1, X2) -> div#(X1, X2))
     (active# div(s X, s Y) -> s# div(minus(X, Y), s Y), s# ok X -> s# X)
     (div#(ok X1, ok X2) -> div#(X1, X2), div#(mark X1, X2) -> div#(X1, X2))
     (div#(ok X1, ok X2) -> div#(X1, X2), div#(ok X1, ok X2) -> div#(X1, X2))
     (geq#(ok X1, ok X2) -> geq#(X1, X2), geq#(ok X1, ok X2) -> geq#(X1, X2))
     (proper# if(X1, X2, X3) -> proper# X2, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X2, proper# minus(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X2, proper# minus(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> s# proper X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# s X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X2, proper# geq(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X2, proper# geq(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X2, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X2, proper# div(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X2, proper# div(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
     (proper# geq(X1, X2) -> proper# X2, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# geq(X1, X2) -> proper# X2, proper# minus(X1, X2) -> proper# X1)
     (proper# geq(X1, X2) -> proper# X2, proper# minus(X1, X2) -> proper# X2)
     (proper# geq(X1, X2) -> proper# X2, proper# s X -> s# proper X)
     (proper# geq(X1, X2) -> proper# X2, proper# s X -> proper# X)
     (proper# geq(X1, X2) -> proper# X2, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# geq(X1, X2) -> proper# X2, proper# geq(X1, X2) -> proper# X1)
     (proper# geq(X1, X2) -> proper# X2, proper# geq(X1, X2) -> proper# X2)
     (proper# geq(X1, X2) -> proper# X2, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# geq(X1, X2) -> proper# X2, proper# div(X1, X2) -> proper# X1)
     (proper# geq(X1, X2) -> proper# X2, proper# div(X1, X2) -> proper# X2)
     (proper# geq(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# geq(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X1)
     (proper# geq(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X2)
     (proper# geq(X1, X2) -> proper# X2, proper# if(X1, X2, X3) -> proper# X3)
     (top# ok X -> active# X, active# minus(s X, s Y) -> minus#(X, Y))
     (top# ok X -> active# X, active# s X -> active# X)
     (top# ok X -> active# X, active# s X -> s# active X)
     (top# ok X -> active# X, active# geq(s X, s Y) -> geq#(X, Y))
     (top# ok X -> active# X, active# div(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# div(X1, X2) -> div#(active X1, X2))
     (top# ok X -> active# X, active# div(s X, s Y) -> minus#(X, Y))
     (top# ok X -> active# X, active# div(s X, s Y) -> s# div(minus(X, Y), s Y))
     (top# ok X -> active# X, active# div(s X, s Y) -> geq#(X, Y))
     (top# ok X -> active# X, active# div(s X, s Y) -> div#(minus(X, Y), s Y))
     (top# ok X -> active# X, active# div(s X, s Y) -> if#(geq(X, Y), s div(minus(X, Y), s Y), 0()))
     (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (proper# s X -> proper# X, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# minus(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# minus(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# s X -> s# proper X)
     (proper# s X -> proper# X, proper# s X -> proper# X)
     (proper# s X -> proper# X, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# geq(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# geq(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# s X -> proper# X, proper# div(X1, X2) -> proper# X1)
     (proper# s X -> proper# X, proper# div(X1, X2) -> proper# X2)
     (proper# s X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (proper# s X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (s# mark X -> s# X, s# mark X -> s# X)
     (s# mark X -> s# X, s# ok X -> s# X)
     (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (proper# div(X1, X2) -> div#(proper X1, proper X2), div#(mark X1, X2) -> div#(X1, X2))
     (proper# div(X1, X2) -> div#(proper X1, proper X2), div#(ok X1, ok X2) -> div#(X1, X2))
     (proper# minus(X1, X2) -> minus#(proper X1, proper X2), minus#(ok X1, ok X2) -> minus#(X1, X2))
     (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (active# div(s X, s Y) -> minus#(X, Y), minus#(ok X1, ok X2) -> minus#(X1, X2))
     (active# minus(s X, s Y) -> minus#(X, Y), minus#(ok X1, ok X2) -> minus#(X1, X2))
     (proper# if(X1, X2, X3) -> proper# X1, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X1, proper# minus(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X1, proper# minus(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X1, proper# s X -> s# proper X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# s X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X1, proper# geq(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X1, proper# geq(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X1, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# if(X1, X2, X3) -> proper# X1, proper# div(X1, X2) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X1, proper# div(X1, X2) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
     (proper# if(X1, X2, X3) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
     (proper# geq(X1, X2) -> proper# X1, proper# minus(X1, X2) -> minus#(proper X1, proper X2))
     (proper# geq(X1, X2) -> proper# X1, proper# minus(X1, X2) -> proper# X1)
     (proper# geq(X1, X2) -> proper# X1, proper# minus(X1, X2) -> proper# X2)
     (proper# geq(X1, X2) -> proper# X1, proper# s X -> s# proper X)
     (proper# geq(X1, X2) -> proper# X1, proper# s X -> proper# X)
     (proper# geq(X1, X2) -> proper# X1, proper# geq(X1, X2) -> geq#(proper X1, proper X2))
     (proper# geq(X1, X2) -> proper# X1, proper# geq(X1, X2) -> proper# X1)
     (proper# geq(X1, X2) -> proper# X1, proper# geq(X1, X2) -> proper# X2)
     (proper# geq(X1, X2) -> proper# X1, proper# div(X1, X2) -> div#(proper X1, proper X2))
     (proper# geq(X1, X2) -> proper# X1, proper# div(X1, X2) -> proper# X1)
     (proper# geq(X1, X2) -> proper# X1, proper# div(X1, X2) -> proper# X2)
     (proper# geq(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# geq(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X1)
     (proper# geq(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X2)
     (proper# geq(X1, X2) -> proper# X1, proper# if(X1, X2, X3) -> proper# X3)
     (active# if(X1, X2, X3) -> active# X1, active# minus(s X, s Y) -> minus#(X, Y))
     (active# if(X1, X2, X3) -> active# X1, active# s X -> active# X)
     (active# if(X1, X2, X3) -> active# X1, active# s X -> s# active X)
     (active# if(X1, X2, X3) -> active# X1, active# geq(s X, s Y) -> geq#(X, Y))
     (active# if(X1, X2, X3) -> active# X1, active# div(X1, X2) -> active# X1)
     (active# if(X1, X2, X3) -> active# X1, active# div(X1, X2) -> div#(active X1, X2))
     (active# if(X1, X2, X3) -> active# X1, active# div(s X, s Y) -> minus#(X, Y))
     (active# if(X1, X2, X3) -> active# X1, active# div(s X, s Y) -> s# div(minus(X, Y), s Y))
     (active# if(X1, X2, X3) -> active# X1, active# div(s X, s Y) -> geq#(X, Y))
     (active# if(X1, X2, X3) -> active# X1, active# div(s X, s Y) -> div#(minus(X, Y), s Y))
     (active# if(X1, X2, X3) -> active# X1, active# div(s X, s Y) -> if#(geq(X, Y), s div(minus(X, Y), s Y), 0()))
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X1)
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (active# s X -> s# active X, s# mark X -> s# X)
     (active# s X -> s# active X, s# ok X -> s# X)
    }
    STATUS:
     arrows: 0.838125
     SCCS (8):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {           active# s X -> active# X,
           active# div(X1, X2) -> active# X1,
        active# if(X1, X2, X3) -> active# X1}
      Scc:
       { proper# minus(X1, X2) -> proper# X1,
         proper# minus(X1, X2) -> proper# X2,
                   proper# s X -> proper# X,
           proper# geq(X1, X2) -> proper# X1,
           proper# geq(X1, X2) -> proper# X2,
           proper# div(X1, X2) -> proper# X1,
           proper# div(X1, X2) -> proper# X2,
        proper# if(X1, X2, X3) -> proper# X1,
        proper# if(X1, X2, X3) -> proper# X2,
        proper# if(X1, X2, X3) -> proper# X3}
      Scc:
       {    if#(mark X1, X2, X3) -> if#(X1, X2, X3),
        if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)}
      Scc:
       { div#(mark X1, X2) -> div#(X1, X2),
        div#(ok X1, ok X2) -> div#(X1, X2)}
      Scc:
       {geq#(ok X1, ok X2) -> geq#(X1, X2)}
      Scc:
       {minus#(ok X1, ok X2) -> minus#(X1, X2)}
      Scc:
       {s# mark X -> s# X,
          s# ok X -> s# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {    active minus(0(), Y) -> mark 0(),
          active minus(s X, s Y) -> mark minus(X, Y),
                      active s X -> s active X,
              active geq(X, 0()) -> mark true(),
            active geq(0(), s Y) -> mark false(),
            active geq(s X, s Y) -> mark geq(X, Y),
              active div(X1, X2) -> div(active X1, X2),
            active div(0(), s Y) -> mark 0(),
            active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
             minus(ok X1, ok X2) -> ok minus(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               geq(ok X1, ok X2) -> ok geq(X1, X2),
                div(mark X1, X2) -> mark div(X1, X2),
               div(ok X1, ok X2) -> ok div(X1, X2),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      proper 0() -> ok 0(),
            proper minus(X1, X2) -> minus(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper true() -> ok true(),
              proper geq(X1, X2) -> geq(proper X1, proper X2),
                  proper false() -> ok false(),
              proper div(X1, X2) -> div(proper X1, proper X2),
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (3):
       Strict:
        {           active# s X -> active# X,
            active# div(X1, X2) -> active# X1,
         active# if(X1, X2, X3) -> active# X1}
       Weak:
       {    active minus(0(), Y) -> mark 0(),
          active minus(s X, s Y) -> mark minus(X, Y),
                      active s X -> s active X,
              active geq(X, 0()) -> mark true(),
            active geq(0(), s Y) -> mark false(),
            active geq(s X, s Y) -> mark geq(X, Y),
              active div(X1, X2) -> div(active X1, X2),
            active div(0(), s Y) -> mark 0(),
            active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
             minus(ok X1, ok X2) -> ok minus(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               geq(ok X1, ok X2) -> ok geq(X1, X2),
                div(mark X1, X2) -> mark div(X1, X2),
               div(ok X1, ok X2) -> ok div(X1, X2),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      proper 0() -> ok 0(),
            proper minus(X1, X2) -> minus(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper true() -> ok true(),
              proper geq(X1, X2) -> geq(proper X1, proper X2),
                  proper false() -> ok false(),
              proper div(X1, X2) -> div(proper X1, proper X2),
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      
      
      
      
      
      
      
      
      SCC (10):
       Strict:
        { proper# minus(X1, X2) -> proper# X1,
          proper# minus(X1, X2) -> proper# X2,
                    proper# s X -> proper# X,
            proper# geq(X1, X2) -> proper# X1,
            proper# geq(X1, X2) -> proper# X2,
            proper# div(X1, X2) -> proper# X1,
            proper# div(X1, X2) -> proper# X2,
         proper# if(X1, X2, X3) -> proper# X1,
         proper# if(X1, X2, X3) -> proper# X2,
         proper# if(X1, X2, X3) -> proper# X3}
       Weak:
       {    active minus(0(), Y) -> mark 0(),
          active minus(s X, s Y) -> mark minus(X, Y),
                      active s X -> s active X,
              active geq(X, 0()) -> mark true(),
            active geq(0(), s Y) -> mark false(),
            active geq(s X, s Y) -> mark geq(X, Y),
              active div(X1, X2) -> div(active X1, X2),
            active div(0(), s Y) -> mark 0(),
            active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
             minus(ok X1, ok X2) -> ok minus(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               geq(ok X1, ok X2) -> ok geq(X1, X2),
                div(mark X1, X2) -> mark div(X1, X2),
               div(ok X1, ok X2) -> ok div(X1, X2),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      proper 0() -> ok 0(),
            proper minus(X1, X2) -> minus(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper true() -> ok true(),
              proper geq(X1, X2) -> geq(proper X1, proper X2),
                  proper false() -> ok false(),
              proper div(X1, X2) -> div(proper X1, proper X2),
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        {    if#(mark X1, X2, X3) -> if#(X1, X2, X3),
         if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)}
       Weak:
       {    active minus(0(), Y) -> mark 0(),
          active minus(s X, s Y) -> mark minus(X, Y),
                      active s X -> s active X,
              active geq(X, 0()) -> mark true(),
            active geq(0(), s Y) -> mark false(),
            active geq(s X, s Y) -> mark geq(X, Y),
              active div(X1, X2) -> div(active X1, X2),
            active div(0(), s Y) -> mark 0(),
            active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
             minus(ok X1, ok X2) -> ok minus(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               geq(ok X1, ok X2) -> ok geq(X1, X2),
                div(mark X1, X2) -> mark div(X1, X2),
               div(ok X1, ok X2) -> ok div(X1, X2),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      proper 0() -> ok 0(),
            proper minus(X1, X2) -> minus(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper true() -> ok true(),
              proper geq(X1, X2) -> geq(proper X1, proper X2),
                  proper false() -> ok false(),
              proper div(X1, X2) -> div(proper X1, proper X2),
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (2):
       Strict:
        { div#(mark X1, X2) -> div#(X1, X2),
         div#(ok X1, ok X2) -> div#(X1, X2)}
       Weak:
       {    active minus(0(), Y) -> mark 0(),
          active minus(s X, s Y) -> mark minus(X, Y),
                      active s X -> s active X,
              active geq(X, 0()) -> mark true(),
            active geq(0(), s Y) -> mark false(),
            active geq(s X, s Y) -> mark geq(X, Y),
              active div(X1, X2) -> div(active X1, X2),
            active div(0(), s Y) -> mark 0(),
            active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
             minus(ok X1, ok X2) -> ok minus(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               geq(ok X1, ok X2) -> ok geq(X1, X2),
                div(mark X1, X2) -> mark div(X1, X2),
               div(ok X1, ok X2) -> ok div(X1, X2),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      proper 0() -> ok 0(),
            proper minus(X1, X2) -> minus(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper true() -> ok true(),
              proper geq(X1, X2) -> geq(proper X1, proper X2),
                  proper false() -> ok false(),
              proper div(X1, X2) -> div(proper X1, proper X2),
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {geq#(ok X1, ok X2) -> geq#(X1, X2)}
       Weak:
       {    active minus(0(), Y) -> mark 0(),
          active minus(s X, s Y) -> mark minus(X, Y),
                      active s X -> s active X,
              active geq(X, 0()) -> mark true(),
            active geq(0(), s Y) -> mark false(),
            active geq(s X, s Y) -> mark geq(X, Y),
              active div(X1, X2) -> div(active X1, X2),
            active div(0(), s Y) -> mark 0(),
            active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
             minus(ok X1, ok X2) -> ok minus(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               geq(ok X1, ok X2) -> ok geq(X1, X2),
                div(mark X1, X2) -> mark div(X1, X2),
               div(ok X1, ok X2) -> ok div(X1, X2),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      proper 0() -> ok 0(),
            proper minus(X1, X2) -> minus(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper true() -> ok true(),
              proper geq(X1, X2) -> geq(proper X1, proper X2),
                  proper false() -> ok false(),
              proper div(X1, X2) -> div(proper X1, proper X2),
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      SCC (1):
       Strict:
        {minus#(ok X1, ok X2) -> minus#(X1, X2)}
       Weak:
       {    active minus(0(), Y) -> mark 0(),
          active minus(s X, s Y) -> mark minus(X, Y),
                      active s X -> s active X,
              active geq(X, 0()) -> mark true(),
            active geq(0(), s Y) -> mark false(),
            active geq(s X, s Y) -> mark geq(X, Y),
              active div(X1, X2) -> div(active X1, X2),
            active div(0(), s Y) -> mark 0(),
            active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
             minus(ok X1, ok X2) -> ok minus(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               geq(ok X1, ok X2) -> ok geq(X1, X2),
                div(mark X1, X2) -> mark div(X1, X2),
               div(ok X1, ok X2) -> ok div(X1, X2),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      proper 0() -> ok 0(),
            proper minus(X1, X2) -> minus(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper true() -> ok true(),
              proper geq(X1, X2) -> geq(proper X1, proper X2),
                  proper false() -> ok false(),
              proper div(X1, X2) -> div(proper X1, proper X2),
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open
      
      
      SCC (2):
       Strict:
        {s# mark X -> s# X,
           s# ok X -> s# X}
       Weak:
       {    active minus(0(), Y) -> mark 0(),
          active minus(s X, s Y) -> mark minus(X, Y),
                      active s X -> s active X,
              active geq(X, 0()) -> mark true(),
            active geq(0(), s Y) -> mark false(),
            active geq(s X, s Y) -> mark geq(X, Y),
              active div(X1, X2) -> div(active X1, X2),
            active div(0(), s Y) -> mark 0(),
            active div(s X, s Y) -> mark if(geq(X, Y), s div(minus(X, Y), s Y), 0()),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
             minus(ok X1, ok X2) -> ok minus(X1, X2),
                        s mark X -> mark s X,
                          s ok X -> ok s X,
               geq(ok X1, ok X2) -> ok geq(X1, X2),
                div(mark X1, X2) -> mark div(X1, X2),
               div(ok X1, ok X2) -> ok div(X1, X2),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      proper 0() -> ok 0(),
            proper minus(X1, X2) -> minus(proper X1, proper X2),
                      proper s X -> s proper X,
                   proper true() -> ok true(),
              proper geq(X1, X2) -> geq(proper X1, proper X2),
                  proper false() -> ok false(),
              proper div(X1, X2) -> div(proper X1, proper X2),
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Open