MAYBE
Time: 0.239084
TRS:
 {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
       if(mark X1, X2, X3) -> mark if(X1, X2, X3),
   if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                  f mark X -> mark f X,
                    f ok X -> ok f X,
     active if(X1, X2, X3) -> if(X1, active X2, X3),
     active if(X1, X2, X3) -> if(active X1, X2, X3),
   active if(true(), X, Y) -> mark X,
  active if(false(), X, Y) -> mark Y,
                active f X -> mark if(X, c(), f true()),
                active f X -> f active X,
     proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                proper c() -> ok c(),
                proper f X -> f proper X,
             proper true() -> ok true(),
            proper false() -> ok false(),
                top mark X -> top proper X,
                  top ok X -> top active X}
 DP:
  DP:
   {    if#(X1, mark X2, 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),
                   f# mark X -> f# X,
                     f# ok X -> f# X,
      active# if(X1, X2, X3) -> if#(X1, active X2, X3),
      active# if(X1, X2, X3) -> if#(active X1, X2, X3),
      active# if(X1, X2, X3) -> active# X1,
      active# if(X1, X2, X3) -> active# X2,
                 active# f X -> if#(X, c(), f true()),
                 active# f X -> f# true(),
                 active# f X -> f# active X,
                 active# f X -> active# X,
      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,
                 proper# f X -> f# proper X,
                 proper# f X -> proper# X,
                 top# mark X -> proper# X,
                 top# mark X -> top# proper X,
                   top# ok X -> active# X,
                   top# ok X -> top# active X}
  TRS:
  {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
        if(mark X1, X2, X3) -> mark if(X1, X2, X3),
    if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                   f mark X -> mark f X,
                     f ok X -> ok f X,
      active if(X1, X2, X3) -> if(X1, active X2, X3),
      active if(X1, X2, X3) -> if(active X1, X2, X3),
    active if(true(), X, Y) -> mark X,
   active if(false(), X, Y) -> mark Y,
                 active f X -> mark if(X, c(), f true()),
                 active f X -> f active X,
      proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                 proper c() -> ok c(),
                 proper f X -> f proper X,
              proper true() -> ok true(),
             proper false() -> ok false(),
                 top mark X -> top proper X,
                   top ok X -> top active X}
  UR:
   {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
         if(mark X1, X2, X3) -> mark if(X1, X2, X3),
     if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                    f mark X -> mark f X,
                      f ok X -> ok f X,
       active if(X1, X2, X3) -> if(X1, active X2, X3),
       active if(X1, X2, X3) -> if(active X1, X2, X3),
     active if(true(), X, Y) -> mark X,
    active if(false(), X, Y) -> mark Y,
                  active f X -> mark if(X, c(), f true()),
                  active f X -> f active X,
       proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                  proper c() -> ok c(),
                  proper f X -> f proper X,
               proper true() -> ok true(),
              proper false() -> ok false()}
   EDG:
    {(active# f X -> if#(X, c(), f true()), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (active# f X -> if#(X, c(), f true()), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# f X -> if#(X, c(), f true()), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (proper# f X -> f# proper X, f# ok X -> f# X)
     (proper# f X -> f# proper X, f# mark X -> f# 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)
     (proper# if(X1, X2, X3) -> proper# X3, proper# f X -> proper# X)
     (proper# if(X1, X2, X3) -> proper# X3, proper# f X -> f# proper X)
     (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))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (if#(X1, mark X2, X3) -> if#(X1, X2, X3), if#(X1, mark 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))
     (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#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> active# X1, active# f X -> active# X)
     (active# if(X1, X2, X3) -> active# X1, active# f X -> f# active X)
     (active# if(X1, X2, X3) -> active# X1, active# f X -> f# true())
     (active# if(X1, X2, X3) -> active# X1, active# f X -> if#(X, c(), f true()))
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> active# X2)
     (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))
     (active# if(X1, X2, X3) -> active# X1, active# if(X1, X2, X3) -> if#(X1, active X2, X3))
     (f# mark X -> f# X, f# ok X -> f# X)
     (f# mark X -> f# X, f# mark X -> f# X)
     (active# f X -> active# X, active# f X -> active# X)
     (active# f X -> active# X, active# f X -> f# active X)
     (active# f X -> active# X, active# f X -> f# true())
     (active# f X -> active# X, active# f X -> if#(X, c(), f true()))
     (active# f X -> active# X, active# if(X1, X2, X3) -> active# X2)
     (active# f X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (active# f X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# f X -> active# X, active# if(X1, X2, X3) -> if#(X1, active X2, X3))
     (top# mark X -> proper# X, proper# f X -> proper# X)
     (top# mark X -> proper# X, proper# f X -> f# proper 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))
     (active# if(X1, X2, X3) -> active# X2, active# f X -> active# X)
     (active# if(X1, X2, X3) -> active# X2, active# f X -> f# active X)
     (active# if(X1, X2, X3) -> active# X2, active# f X -> f# true())
     (active# if(X1, X2, X3) -> active# X2, active# f X -> if#(X, c(), f true()))
     (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> active# X2)
     (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> active# X1)
     (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (active# if(X1, X2, X3) -> active# X2, active# if(X1, X2, X3) -> if#(X1, active X2, X3))
     (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# if(X1, X2, X3) -> proper# X2, proper# f X -> f# proper X)
     (proper# if(X1, X2, X3) -> proper# X2, proper# f X -> proper# X)
     (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(X1, active X2, X3))
     (top# ok X -> active# X, active# if(X1, X2, X3) -> if#(active X1, X2, X3))
     (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X1)
     (top# ok X -> active# X, active# if(X1, X2, X3) -> active# X2)
     (top# ok X -> active# X, active# f X -> if#(X, c(), f true()))
     (top# ok X -> active# X, active# f X -> f# true())
     (top# ok X -> active# X, active# f X -> f# active X)
     (top# ok X -> active# X, active# f X -> active# X)
     (proper# f X -> proper# X, proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3))
     (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X1)
     (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X2)
     (proper# f X -> proper# X, proper# if(X1, X2, X3) -> proper# X3)
     (proper# f X -> proper# X, proper# f X -> f# proper X)
     (proper# f X -> proper# X, proper# f X -> proper# X)
     (f# ok X -> f# X, f# mark X -> f# X)
     (f# ok X -> f# X, f# ok X -> f# X)
     (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# if(X1, X2, X3) -> proper# X1, proper# f X -> f# proper X)
     (proper# if(X1, X2, X3) -> proper# X1, proper# f X -> proper# X)
     (active# if(X1, X2, X3) -> if#(active X1, X2, X3), if#(X1, mark X2, 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))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (if#(mark X1, X2, X3) -> if#(X1, X2, X3), if#(mark X1, X2, 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))
     (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(mark X1, X2, X3) -> if#(X1, X2, X3))
     (active# if(X1, X2, X3) -> if#(X1, active X2, X3), if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3))
     (proper# if(X1, X2, X3) -> if#(proper X1, proper X2, proper X3), if#(X1, mark X2, X3) -> if#(X1, X2, X3))
     (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))
     (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# f X -> f# active X, f# mark X -> f# X)
     (active# f X -> f# active X, f# ok X -> f# X)
     (active# f X -> f# true(), f# mark X -> f# X)
     (active# f X -> f# true(), f# ok X -> f# X)}
    STATUS:
     arrows: 0.809074
     SCCS (5):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {active# if(X1, X2, X3) -> active# X1,
        active# if(X1, X2, X3) -> active# X2,
                   active# f X -> active# X}
      Scc:
       {proper# if(X1, X2, X3) -> proper# X1,
        proper# if(X1, X2, X3) -> proper# X2,
        proper# if(X1, X2, X3) -> proper# X3,
                   proper# f X -> proper# X}
      Scc:
       {    if#(X1, mark X2, 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)}
      Scc:
       {f# mark X -> f# X,
          f# ok X -> f# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                        f mark X -> mark f X,
                          f ok X -> ok f X,
           active if(X1, X2, X3) -> if(X1, active X2, X3),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true()),
                      active f X -> f active X,
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      proper c() -> ok c(),
                      proper f X -> f proper X,
                   proper true() -> ok true(),
                  proper false() -> ok false(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       Fail
      
      SCC (3):
       Strict:
        {active# if(X1, X2, X3) -> active# X1,
         active# if(X1, X2, X3) -> active# X2,
                    active# f X -> active# X}
       Weak:
       {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                        f mark X -> mark f X,
                          f ok X -> ok f X,
           active if(X1, X2, X3) -> if(X1, active X2, X3),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true()),
                      active f X -> f active X,
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      proper c() -> ok c(),
                      proper f X -> f proper X,
                   proper true() -> ok true(),
                  proper false() -> ok false(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2) = x0 + x1 + x2,
         
         [mark](x0) = 0,
         
         [f](x0) = x0 + 1,
         
         [active](x0) = 0,
         
         [proper](x0) = 0,
         
         [ok](x0) = 0,
         
         [top](x0) = 0,
         
         [c] = 1,
         
         [true] = 0,
         
         [false] = 0,
         
         [active#](x0) = x0
        Strict:
         active# f X -> active# X
         1 + 1X >= 0 + 1X
         active# if(X1, X2, X3) -> active# X2
         0 + 1X1 + 1X2 + 1X3 >= 0 + 1X2
         active# if(X1, X2, X3) -> active# X1
         0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1
        Weak:
         top ok X -> top active X
         0 + 0X >= 0 + 0X
         top mark X -> top proper X
         0 + 0X >= 0 + 0X
         proper false() -> ok false()
         0 >= 0
         proper true() -> ok true()
         0 >= 0
         proper f X -> f proper X
         0 + 0X >= 1 + 0X
         proper c() -> ok c()
         0 >= 0
         proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
         0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
         active f X -> f active X
         0 + 0X >= 1 + 0X
         active f X -> mark if(X, c(), f true())
         0 + 0X >= 0 + 0X
         active if(false(), X, Y) -> mark Y
         0 + 0X + 0Y >= 0 + 0Y
         active if(true(), X, Y) -> mark X
         0 + 0X + 0Y >= 0 + 0X
         active if(X1, X2, X3) -> if(active X1, X2, X3)
         0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 1X2 + 1X3
         active if(X1, X2, X3) -> if(X1, active X2, X3)
         0 + 0X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 1X3
         f ok X -> ok f X
         1 + 0X >= 0 + 0X
         f mark X -> mark f X
         1 + 0X >= 0 + 0X
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
         0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
         if(mark X1, X2, X3) -> mark if(X1, X2, X3)
         0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3
         if(X1, mark X2, X3) -> mark if(X1, X2, X3)
         0 + 1X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3
       SCCS (1):
        Scc:
         {active# if(X1, X2, X3) -> active# X1,
          active# if(X1, X2, X3) -> active# X2}
        
        SCC (2):
         Strict:
          {active# if(X1, X2, X3) -> active# X1,
           active# if(X1, X2, X3) -> active# X2}
         Weak:
         {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
               if(mark X1, X2, X3) -> mark if(X1, X2, X3),
           if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
             active if(X1, X2, X3) -> if(X1, active X2, X3),
             active if(X1, X2, X3) -> if(active X1, X2, X3),
           active if(true(), X, Y) -> mark X,
          active if(false(), X, Y) -> mark Y,
                        active f X -> mark if(X, c(), f true()),
                        active f X -> f active X,
             proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                        proper c() -> ok c(),
                        proper f X -> f proper X,
                     proper true() -> ok true(),
                    proper false() -> ok false(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [if](x0, x1, x2) = x0 + x1 + 1,
           
           [mark](x0) = x0 + 1,
           
           [f](x0) = x0 + 1,
           
           [active](x0) = 0,
           
           [proper](x0) = x0 + 1,
           
           [ok](x0) = 0,
           
           [top](x0) = 0,
           
           [c] = 1,
           
           [true] = 1,
           
           [false] = 1,
           
           [active#](x0) = x0 + 1
          Strict:
           active# if(X1, X2, X3) -> active# X2
           2 + 1X1 + 1X2 + 0X3 >= 1 + 1X2
           active# if(X1, X2, X3) -> active# X1
           2 + 1X1 + 1X2 + 0X3 >= 1 + 1X1
          Weak:
           top ok X -> top active X
           0 + 0X >= 0 + 0X
           top mark X -> top proper X
           0 + 0X >= 0 + 0X
           proper false() -> ok false()
           2 >= 0
           proper true() -> ok true()
           2 >= 0
           proper f X -> f proper X
           2 + 1X >= 2 + 1X
           proper c() -> ok c()
           2 >= 0
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
           2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3
           active f X -> f active X
           0 + 0X >= 1 + 0X
           active f X -> mark if(X, c(), f true())
           0 + 0X >= 3 + 1X
           active if(false(), X, Y) -> mark Y
           0 + 0X + 0Y >= 1 + 1Y
           active if(true(), X, Y) -> mark X
           0 + 0X + 0Y >= 1 + 1X
           active if(X1, X2, X3) -> if(active X1, X2, X3)
           0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3
           active if(X1, X2, X3) -> if(X1, active X2, X3)
           0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3
           f ok X -> ok f X
           1 + 0X >= 0 + 0X
           f mark X -> mark f X
           2 + 1X >= 2 + 1X
           if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
           1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
           if(mark X1, X2, X3) -> mark if(X1, X2, X3)
           2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
           if(X1, mark X2, X3) -> mark if(X1, X2, X3)
           2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
         Qed
     
     
     
     SCC (4):
      Strict:
       {proper# if(X1, X2, X3) -> proper# X1,
        proper# if(X1, X2, X3) -> proper# X2,
        proper# if(X1, X2, X3) -> proper# X3,
                   proper# f X -> proper# X}
      Weak:
      {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
            if(mark X1, X2, X3) -> mark if(X1, X2, X3),
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                       f mark X -> mark f X,
                         f ok X -> ok f X,
          active if(X1, X2, X3) -> if(X1, active X2, X3),
          active if(X1, X2, X3) -> if(active X1, X2, X3),
        active if(true(), X, Y) -> mark X,
       active if(false(), X, Y) -> mark Y,
                     active f X -> mark if(X, c(), f true()),
                     active f X -> f active X,
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                     proper c() -> ok c(),
                     proper f X -> f proper X,
                  proper true() -> ok true(),
                 proper false() -> ok false(),
                     top mark X -> top proper X,
                       top ok X -> top active X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [if](x0, x1, x2) = x0 + x1 + x2,
        
        [mark](x0) = 0,
        
        [f](x0) = x0 + 1,
        
        [active](x0) = 0,
        
        [proper](x0) = 0,
        
        [ok](x0) = 0,
        
        [top](x0) = 0,
        
        [c] = 1,
        
        [true] = 0,
        
        [false] = 0,
        
        [proper#](x0) = x0
       Strict:
        proper# f X -> proper# X
        1 + 1X >= 0 + 1X
        proper# if(X1, X2, X3) -> proper# X3
        0 + 1X1 + 1X2 + 1X3 >= 0 + 1X3
        proper# if(X1, X2, X3) -> proper# X2
        0 + 1X1 + 1X2 + 1X3 >= 0 + 1X2
        proper# if(X1, X2, X3) -> proper# X1
        0 + 1X1 + 1X2 + 1X3 >= 0 + 1X1
       Weak:
        top ok X -> top active X
        0 + 0X >= 0 + 0X
        top mark X -> top proper X
        0 + 0X >= 0 + 0X
        proper false() -> ok false()
        0 >= 0
        proper true() -> ok true()
        0 >= 0
        proper f X -> f proper X
        0 + 0X >= 1 + 0X
        proper c() -> ok c()
        0 >= 0
        proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
        0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
        active f X -> f active X
        0 + 0X >= 1 + 0X
        active f X -> mark if(X, c(), f true())
        0 + 0X >= 0 + 0X
        active if(false(), X, Y) -> mark Y
        0 + 0X + 0Y >= 0 + 0Y
        active if(true(), X, Y) -> mark X
        0 + 0X + 0Y >= 0 + 0X
        active if(X1, X2, X3) -> if(active X1, X2, X3)
        0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 1X2 + 1X3
        active if(X1, X2, X3) -> if(X1, active X2, X3)
        0 + 0X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 1X3
        f ok X -> ok f X
        1 + 0X >= 0 + 0X
        f mark X -> mark f X
        1 + 0X >= 0 + 0X
        if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
        0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
        if(mark X1, X2, X3) -> mark if(X1, X2, X3)
        0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3
        if(X1, mark X2, X3) -> mark if(X1, X2, X3)
        0 + 1X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 0X3
      SCCS (1):
       Scc:
        {proper# if(X1, X2, X3) -> proper# X1,
         proper# if(X1, X2, X3) -> proper# X2,
         proper# if(X1, X2, X3) -> proper# X3}
       
       SCC (3):
        Strict:
         {proper# if(X1, X2, X3) -> proper# X1,
          proper# if(X1, X2, X3) -> proper# X2,
          proper# if(X1, X2, X3) -> proper# X3}
        Weak:
        {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
              if(mark X1, X2, X3) -> mark if(X1, X2, X3),
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                         f mark X -> mark f X,
                           f ok X -> ok f X,
            active if(X1, X2, X3) -> if(X1, active X2, X3),
            active if(X1, X2, X3) -> if(active X1, X2, X3),
          active if(true(), X, Y) -> mark X,
         active if(false(), X, Y) -> mark Y,
                       active f X -> mark if(X, c(), f true()),
                       active f X -> f active X,
            proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                       proper c() -> ok c(),
                       proper f X -> f proper X,
                    proper true() -> ok true(),
                   proper false() -> ok false(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
        POLY:
         Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
         Interpretation:
          [if](x0, x1, x2) = x0 + x1 + x2 + 1,
          
          [mark](x0) = x0,
          
          [f](x0) = 0,
          
          [active](x0) = x0 + 1,
          
          [proper](x0) = 0,
          
          [ok](x0) = x0 + 1,
          
          [top](x0) = 0,
          
          [c] = 0,
          
          [true] = 0,
          
          [false] = 0,
          
          [proper#](x0) = x0 + 1
         Strict:
          proper# if(X1, X2, X3) -> proper# X3
          2 + 1X1 + 1X2 + 1X3 >= 1 + 1X3
          proper# if(X1, X2, X3) -> proper# X2
          2 + 1X1 + 1X2 + 1X3 >= 1 + 1X2
          proper# if(X1, X2, X3) -> proper# X1
          2 + 1X1 + 1X2 + 1X3 >= 1 + 1X1
         Weak:
          top ok X -> top active X
          0 + 0X >= 0 + 0X
          top mark X -> top proper X
          0 + 0X >= 0 + 0X
          proper false() -> ok false()
          0 >= 1
          proper true() -> ok true()
          0 >= 1
          proper f X -> f proper X
          0 + 0X >= 0 + 0X
          proper c() -> ok c()
          0 >= 1
          proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
          0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3
          active f X -> f active X
          1 + 0X >= 0 + 0X
          active f X -> mark if(X, c(), f true())
          1 + 0X >= 1 + 1X
          active if(false(), X, Y) -> mark Y
          2 + 1X + 1Y >= 0 + 1Y
          active if(true(), X, Y) -> mark X
          2 + 1X + 1Y >= 0 + 1X
          active if(X1, X2, X3) -> if(active X1, X2, X3)
          2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3
          active if(X1, X2, X3) -> if(X1, active X2, X3)
          2 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3
          f ok X -> ok f X
          0 + 0X >= 1 + 0X
          f mark X -> mark f X
          0 + 0X >= 0 + 0X
          if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
          4 + 1X1 + 1X2 + 1X3 >= 2 + 1X1 + 1X2 + 1X3
          if(mark X1, X2, X3) -> mark if(X1, X2, X3)
          1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3
          if(X1, mark X2, X3) -> mark if(X1, X2, X3)
          1 + 1X1 + 1X2 + 1X3 >= 1 + 1X1 + 1X2 + 1X3
        Qed
    
    
    
    
    SCC (3):
     Strict:
      {    if#(X1, mark X2, 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)}
     Weak:
     {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
           if(mark X1, X2, X3) -> mark if(X1, X2, X3),
       if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      f mark X -> mark f X,
                        f ok X -> ok f X,
         active if(X1, X2, X3) -> if(X1, active X2, X3),
         active if(X1, X2, X3) -> if(active X1, X2, X3),
       active if(true(), X, Y) -> mark X,
      active if(false(), X, Y) -> mark Y,
                    active f X -> mark if(X, c(), f true()),
                    active f X -> f active X,
         proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper c() -> ok c(),
                    proper f X -> f proper X,
                 proper true() -> ok true(),
                proper false() -> ok false(),
                    top mark X -> top proper X,
                      top ok X -> top active X}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = x0 + x1 + 1,
       
       [mark](x0) = x0 + 1,
       
       [f](x0) = x0 + 1,
       
       [active](x0) = x0 + 1,
       
       [proper](x0) = x0 + 1,
       
       [ok](x0) = x0 + 1,
       
       [top](x0) = 0,
       
       [c] = 1,
       
       [true] = 0,
       
       [false] = 0,
       
       [if#](x0, x1, x2) = x0
      Strict:
       if#(ok X1, ok X2, ok X3) -> if#(X1, X2, X3)
       1 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3
       if#(mark X1, X2, X3) -> if#(X1, X2, X3)
       0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3
       if#(X1, mark X2, X3) -> if#(X1, X2, X3)
       0 + 0X1 + 0X2 + 1X3 >= 0 + 0X1 + 0X2 + 1X3
      Weak:
       top ok X -> top active X
       0 + 0X >= 0 + 0X
       top mark X -> top proper X
       0 + 0X >= 0 + 0X
       proper false() -> ok false()
       1 >= 1
       proper true() -> ok true()
       1 >= 1
       proper f X -> f proper X
       2 + 1X >= 2 + 1X
       proper c() -> ok c()
       2 >= 2
       proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
       2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3
       active f X -> f active X
       2 + 1X >= 2 + 1X
       active f X -> mark if(X, c(), f true())
       2 + 1X >= 3 + 1X
       active if(false(), X, Y) -> mark Y
       2 + 1X + 0Y >= 1 + 1Y
       active if(true(), X, Y) -> mark X
       2 + 1X + 0Y >= 1 + 1X
       active if(X1, X2, X3) -> if(active X1, X2, X3)
       2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
       active if(X1, X2, X3) -> if(X1, active X2, X3)
       2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
       f ok X -> ok f X
       2 + 1X >= 2 + 1X
       f mark X -> mark f X
       2 + 1X >= 2 + 1X
       if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
       3 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
       if(mark X1, X2, X3) -> mark if(X1, X2, X3)
       2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
       if(X1, mark X2, X3) -> mark if(X1, X2, X3)
       2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
     SCCS (1):
      Scc:
       {if#(X1, mark X2, X3) -> if#(X1, X2, X3),
        if#(mark X1, X2, X3) -> if#(X1, X2, X3)}
      
      SCC (2):
       Strict:
        {if#(X1, mark X2, X3) -> if#(X1, X2, X3),
         if#(mark X1, X2, X3) -> if#(X1, X2, X3)}
       Weak:
       {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
             if(mark X1, X2, X3) -> mark if(X1, X2, X3),
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                        f mark X -> mark f X,
                          f ok X -> ok f X,
           active if(X1, X2, X3) -> if(X1, active X2, X3),
           active if(X1, X2, X3) -> if(active X1, X2, X3),
         active if(true(), X, Y) -> mark X,
        active if(false(), X, Y) -> mark Y,
                      active f X -> mark if(X, c(), f true()),
                      active f X -> f active X,
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                      proper c() -> ok c(),
                      proper f X -> f proper X,
                   proper true() -> ok true(),
                  proper false() -> ok false(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [if](x0, x1, x2) = x0 + x1 + 1,
         
         [mark](x0) = x0 + 1,
         
         [f](x0) = x0 + 1,
         
         [active](x0) = x0 + 1,
         
         [proper](x0) = x0 + 1,
         
         [ok](x0) = 0,
         
         [top](x0) = 0,
         
         [c] = 1,
         
         [true] = 0,
         
         [false] = 1,
         
         [if#](x0, x1, x2) = x0
        Strict:
         if#(mark X1, X2, X3) -> if#(X1, X2, X3)
         1 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3
         if#(X1, mark X2, X3) -> if#(X1, X2, X3)
         0 + 1X1 + 0X2 + 0X3 >= 0 + 1X1 + 0X2 + 0X3
        Weak:
         top ok X -> top active X
         0 + 0X >= 0 + 0X
         top mark X -> top proper X
         0 + 0X >= 0 + 0X
         proper false() -> ok false()
         2 >= 0
         proper true() -> ok true()
         1 >= 0
         proper f X -> f proper X
         2 + 1X >= 2 + 1X
         proper c() -> ok c()
         2 >= 0
         proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
         2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3
         active f X -> f active X
         2 + 1X >= 2 + 1X
         active f X -> mark if(X, c(), f true())
         2 + 1X >= 3 + 1X
         active if(false(), X, Y) -> mark Y
         3 + 1X + 0Y >= 1 + 1Y
         active if(true(), X, Y) -> mark X
         2 + 1X + 0Y >= 1 + 1X
         active if(X1, X2, X3) -> if(active X1, X2, X3)
         2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
         active if(X1, X2, X3) -> if(X1, active X2, X3)
         2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
         f ok X -> ok f X
         1 + 0X >= 0 + 0X
         f mark X -> mark f X
         2 + 1X >= 2 + 1X
         if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
         1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
         if(mark X1, X2, X3) -> mark if(X1, X2, X3)
         2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
         if(X1, mark X2, X3) -> mark if(X1, X2, X3)
         2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
       SCCS (1):
        Scc:
         {if#(X1, mark X2, X3) -> if#(X1, X2, X3)}
        
        SCC (1):
         Strict:
          {if#(X1, mark X2, X3) -> if#(X1, X2, X3)}
         Weak:
         {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
               if(mark X1, X2, X3) -> mark if(X1, X2, X3),
           if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                          f mark X -> mark f X,
                            f ok X -> ok f X,
             active if(X1, X2, X3) -> if(X1, active X2, X3),
             active if(X1, X2, X3) -> if(active X1, X2, X3),
           active if(true(), X, Y) -> mark X,
          active if(false(), X, Y) -> mark Y,
                        active f X -> mark if(X, c(), f true()),
                        active f X -> f active X,
             proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                        proper c() -> ok c(),
                        proper f X -> f proper X,
                     proper true() -> ok true(),
                    proper false() -> ok false(),
                        top mark X -> top proper X,
                          top ok X -> top active X}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [if](x0, x1, x2) = x0 + x1 + 1,
           
           [mark](x0) = x0 + 1,
           
           [f](x0) = x0 + 1,
           
           [active](x0) = 0,
           
           [proper](x0) = x0 + 1,
           
           [ok](x0) = 0,
           
           [top](x0) = x0 + 1,
           
           [c] = 1,
           
           [true] = 1,
           
           [false] = 1,
           
           [if#](x0, x1, x2) = x0
          Strict:
           if#(X1, mark X2, X3) -> if#(X1, X2, X3)
           1 + 0X1 + 1X2 + 0X3 >= 0 + 0X1 + 1X2 + 0X3
          Weak:
           top ok X -> top active X
           1 + 0X >= 1 + 0X
           top mark X -> top proper X
           2 + 1X >= 2 + 1X
           proper false() -> ok false()
           2 >= 0
           proper true() -> ok true()
           2 >= 0
           proper f X -> f proper X
           2 + 1X >= 2 + 1X
           proper c() -> ok c()
           2 >= 0
           proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
           2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3
           active f X -> f active X
           0 + 0X >= 1 + 0X
           active f X -> mark if(X, c(), f true())
           0 + 0X >= 3 + 1X
           active if(false(), X, Y) -> mark Y
           0 + 0X + 0Y >= 1 + 1Y
           active if(true(), X, Y) -> mark X
           0 + 0X + 0Y >= 1 + 1X
           active if(X1, X2, X3) -> if(active X1, X2, X3)
           0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3
           active if(X1, X2, X3) -> if(X1, active X2, X3)
           0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3
           f ok X -> ok f X
           1 + 0X >= 0 + 0X
           f mark X -> mark f X
           2 + 1X >= 2 + 1X
           if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
           1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
           if(mark X1, X2, X3) -> mark if(X1, X2, X3)
           2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
           if(X1, mark X2, X3) -> mark if(X1, X2, X3)
           2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
         Qed
  
  SCC (2):
   Strict:
    {f# mark X -> f# X,
       f# ok X -> f# X}
   Weak:
   {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
         if(mark X1, X2, X3) -> mark if(X1, X2, X3),
     if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                    f mark X -> mark f X,
                      f ok X -> ok f X,
       active if(X1, X2, X3) -> if(X1, active X2, X3),
       active if(X1, X2, X3) -> if(active X1, X2, X3),
     active if(true(), X, Y) -> mark X,
    active if(false(), X, Y) -> mark Y,
                  active f X -> mark if(X, c(), f true()),
                  active f X -> f active X,
       proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                  proper c() -> ok c(),
                  proper f X -> f proper X,
               proper true() -> ok true(),
              proper false() -> ok false(),
                  top mark X -> top proper X,
                    top ok X -> top active X}
   POLY:
    Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
    Interpretation:
     [if](x0, x1, x2) = 0,
     
     [mark](x0) = x0,
     
     [f](x0) = 0,
     
     [active](x0) = 0,
     
     [proper](x0) = 0,
     
     [ok](x0) = x0 + 1,
     
     [top](x0) = x0,
     
     [c] = 1,
     
     [true] = 1,
     
     [false] = 1,
     
     [f#](x0) = x0
    Strict:
     f# ok X -> f# X
     1 + 1X >= 0 + 1X
     f# mark X -> f# X
     0 + 1X >= 0 + 1X
    Weak:
     top ok X -> top active X
     1 + 1X >= 0 + 0X
     top mark X -> top proper X
     0 + 1X >= 0 + 0X
     proper false() -> ok false()
     0 >= 2
     proper true() -> ok true()
     0 >= 2
     proper f X -> f proper X
     0 + 0X >= 0 + 0X
     proper c() -> ok c()
     0 >= 2
     proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
     0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
     active f X -> f active X
     0 + 0X >= 0 + 0X
     active f X -> mark if(X, c(), f true())
     0 + 0X >= 0 + 0X
     active if(false(), X, Y) -> mark Y
     0 + 0X + 0Y >= 0 + 1Y
     active if(true(), X, Y) -> mark X
     0 + 0X + 0Y >= 0 + 1X
     active if(X1, X2, X3) -> if(active X1, X2, X3)
     0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
     active if(X1, X2, X3) -> if(X1, active X2, X3)
     0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
     f ok X -> ok f X
     0 + 0X >= 1 + 0X
     f mark X -> mark f X
     0 + 0X >= 0 + 0X
     if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
     0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 0X2 + 0X3
     if(mark X1, X2, X3) -> mark if(X1, X2, X3)
     0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
     if(X1, mark X2, X3) -> mark if(X1, X2, X3)
     0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
   SCCS (1):
    Scc:
     {f# mark X -> f# X}
    
    SCC (1):
     Strict:
      {f# mark X -> f# X}
     Weak:
     {     if(X1, mark X2, X3) -> mark if(X1, X2, X3),
           if(mark X1, X2, X3) -> mark if(X1, X2, X3),
       if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3),
                      f mark X -> mark f X,
                        f ok X -> ok f X,
         active if(X1, X2, X3) -> if(X1, active X2, X3),
         active if(X1, X2, X3) -> if(active X1, X2, X3),
       active if(true(), X, Y) -> mark X,
      active if(false(), X, Y) -> mark Y,
                    active f X -> mark if(X, c(), f true()),
                    active f X -> f active X,
         proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3),
                    proper c() -> ok c(),
                    proper f X -> f proper X,
                 proper true() -> ok true(),
                proper false() -> ok false(),
                    top mark X -> top proper X,
                      top ok X -> top active X}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [if](x0, x1, x2) = x0 + x1 + 1,
       
       [mark](x0) = x0 + 1,
       
       [f](x0) = x0 + 1,
       
       [active](x0) = 0,
       
       [proper](x0) = x0 + 1,
       
       [ok](x0) = 0,
       
       [top](x0) = x0 + 1,
       
       [c] = 1,
       
       [true] = 1,
       
       [false] = 1,
       
       [f#](x0) = x0
      Strict:
       f# mark X -> f# X
       1 + 1X >= 0 + 1X
      Weak:
       top ok X -> top active X
       1 + 0X >= 1 + 0X
       top mark X -> top proper X
       2 + 1X >= 2 + 1X
       proper false() -> ok false()
       2 >= 0
       proper true() -> ok true()
       2 >= 0
       proper f X -> f proper X
       2 + 1X >= 2 + 1X
       proper c() -> ok c()
       2 >= 0
       proper if(X1, X2, X3) -> if(proper X1, proper X2, proper X3)
       2 + 1X1 + 1X2 + 0X3 >= 3 + 1X1 + 1X2 + 0X3
       active f X -> f active X
       0 + 0X >= 1 + 0X
       active f X -> mark if(X, c(), f true())
       0 + 0X >= 3 + 1X
       active if(false(), X, Y) -> mark Y
       0 + 0X + 0Y >= 1 + 1Y
       active if(true(), X, Y) -> mark X
       0 + 0X + 0Y >= 1 + 1X
       active if(X1, X2, X3) -> if(active X1, X2, X3)
       0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3
       active if(X1, X2, X3) -> if(X1, active X2, X3)
       0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 0X2 + 0X3
       f ok X -> ok f X
       1 + 0X >= 0 + 0X
       f mark X -> mark f X
       2 + 1X >= 2 + 1X
       if(ok X1, ok X2, ok X3) -> ok if(X1, X2, X3)
       1 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3
       if(mark X1, X2, X3) -> mark if(X1, X2, X3)
       2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
       if(X1, mark X2, X3) -> mark if(X1, X2, X3)
       2 + 1X1 + 1X2 + 0X3 >= 2 + 1X1 + 1X2 + 0X3
     Qed