- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] app'(app'(minus,x),0) -> x
[2] app'(app'(minus,app'(s,x)),app'(s,y)) -> app'(app'(minus,x),y)
[3] app'(app'(minus,app'(app'(minus,x),y)),z) ->
 app'(app'(minus,x),app'(app'(plus,y),z))
[4] app'(app'(quot,0),app'(s,y)) -> 0
[5] app'(app'(quot,app'(s,x)),app'(s,y)) ->
 app'(s,app'(app'(quot,app'(app'(minus,x),y)),app'(s,y)))
[6] app'(app'(plus,0),y) -> y
[7] app'(app'(plus,app'(s,x)),y) -> app'(s,app'(app'(plus,x),y))
[8] app'(app'(app,nil),k) -> k
[9] app'(app'(app,l),nil) -> l
[10] app'(app'(app,app'(app'(cons,x),l)),k) ->
 app'(app'(cons,x),app'(app'(app,l),k))
[11] app'(sum,app'(app'(cons,x),nil)) -> app'(app'(cons,x),nil)
[12] app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) ->
 app'(sum,app'(app'(cons,app'(app'(plus,x),y)),l))
[13] app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) ->
 app'(sum,app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k)))))
[14] app'(app'(map,f),nil) -> nil
[15] app'(app'(map,f),app'(app'(cons,x),xs)) ->
 app'(app'(cons,app'(f,x)),app'(app'(map,f),xs))
[16] app'(app'(filter,f),nil) -> nil
[17] app'(app'(filter,f),app'(app'(cons,x),xs)) ->
 app'(app'(app'(app'(filter2,app'(f,x)),f),x),xs)
[18] app'(app'(app'(app'(filter2,true),f),x),xs) ->
 app'(app'(cons,x),app'(app'(filter,f),xs))
[19] app'(app'(app'(app'(filter2,false),f),x),xs) -> app'(app'(filter,f),xs)


Sub problem: 
guided: 

DP termination of:
<Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)>
<Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(minus,x)>
<Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                     app'(app'(plus,y),z))>
<Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),z)>
<Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(plus,y)>
<Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(s,
                                                app'(app'(quot,
                                                      app'(app'(minus,x),y)),
                                                 app'(s,y)))>
<Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                            app'(app'(minus,x),
                                                             y)),app'(s,y))>
<Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(quot,
                                                app'(app'(minus,x),y))>
<Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)>
<Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(minus,x)>
<Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(s,app'(app'(plus,x),y))>
<Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
<Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(plus,x)>
<Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                  app'(app'(app,l),k))>
<Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)>
<Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app,l)>
<Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                             sum,
                                                             app'(app'(
                                                                   cons,
                                                                   app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                              l))>
<Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                             app'(cons,
                                                              app'(app'(plus,x),
                                                               y)),l)>
<Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                             cons,
                                                             app'(app'(plus,x),
                                                              y))>
<Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                             app'(plus,
                                                              x),y)>
<Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(plus,x)>
<Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
<Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
<Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
<Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(cons,
                                                               app'(f,x)),
                                                   app'(app'(map,f),xs))>
<Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(cons,app'(f,x))>
<Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
<Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)>
<Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                  app'(
                                                                   app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                   f),
                                                                  x),
                                                      xs)>
<Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                  app'(
                                                                   filter2,
                                                                   app'(f,x)),
                                                                  f),
                                                      x)>
<Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                  filter2,
                                                                  app'(f,x)),
                                                      f)>
<Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(filter2,
                                                      app'(f,x))>
<Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
<Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(cons,x),
                                                       app'(app'(filter,f),xs))>
<Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(cons,x)>
<Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                   filter,
                                                                   f),
                                                       xs)>
<Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(filter,f)>
<Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                        xs)>
<Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(filter,f)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                           app'(filter,
                                                            f),xs)> 
      --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                  app'(
                                                                   filter,
                                                                   f),
                                                                  xs)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                          app'(filter,
                                                           f),xs)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs))> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(map,f),xs)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs))> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(plus,
                                                                x),y)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               sum,
                                                               app'(app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                l))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               sum,
                                                               app'(app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                l))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               sum,
                                                               app'(app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                l))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               sum,
                                                               app'(app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                l))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               sum,
                                                               app'(app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                l))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                               sum,
                                                               app'(app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                l))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(app,l),k)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k))> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y))> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(plus,y),
                                                       z)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z))> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,false),f),x),xs) , Marked_app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 filter,
                                                                 f),xs)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app'(app'(filter2,true),f),x),xs) , Marked_app'(
                                                                app'(
                                                                 cons,
                                                                 x),
                                                                app'(
                                                                 app'(
                                                                  filter,
                                                                  f),
                                                                 xs))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(filter2,
                                                                app'(f,x)),
                                                               f)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                f),x)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                               app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                x),xs)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(map,
                                                             f),xs)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(f,x)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(map,f),app'(app'(cons,x),xs)) , Marked_app'(
                                                            app'(cons,
                                                             app'(f,x)),
                                                            app'(app'(map,f),
                                                             xs))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k))))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,
           app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    app,
                                                                    l),
                                                                    app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    x),
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    y),
                                                                    k)))))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) , Marked_app'(
                                                                    sum,
                                                                    app'(
                                                                    app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                    l))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(app,l),
                                                           k)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(app,app'(app'(cons,x),l)),k) , Marked_app'(
                                                           app'(cons,
                                                            x),
                                                           app'(app'(app,l),k))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(plus,app'(s,x)),y) , Marked_app'(app'(plus,x),y)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    minus,
                                                                    x),
                                                         y)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(quot,app'(s,x)),app'(s,y)) , Marked_app'(app'(
                                                                    quot,
                                                                    app'(
                                                                    app'(
                                                                    minus,
                                                                    x),
                                                                    y)),
                                                         app'(s,y))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(plus,
                                                               y),z)>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(minus,app'(app'(minus,x),y)),z) , Marked_app'(
                                                              app'(minus,
                                                               x),
                                                              app'(app'(plus,y),
                                                               z))>
  <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(app'(minus,x),y)> 
     --> <Marked_app'(app'(minus,app'(s,x)),app'(s,y)) , Marked_app'(
                                                          app'(minus,
                                                           x),y)>
}
APPLY CRITERIA (Choosing graph)
Trying to solve the following constraints:
{
  app'(app'(app'(app'(filter2,true),f),x),xs) >= app'(app'(cons,x),
                                                  app'(app'(filter,f),xs)) ;
  app'(app'(app'(app'(filter2,false),f),x),xs) >= app'(app'(filter,f),xs) ;
  app'(app'(minus,app'(app'(minus,x),y)),z) >= app'(app'(minus,x),
                                                app'(app'(plus,y),z)) ;
  app'(app'(minus,app'(s,x)),app'(s,y)) >= app'(app'(minus,x),y) ;
  app'(app'(minus,x),0) >= x ;
  app'(app'(plus,app'(s,x)),y) >= app'(s,app'(app'(plus,x),y)) ;
  app'(app'(plus,0),y) >= y ;
  app'(app'(quot,app'(s,x)),app'(s,y)) >= app'(s,
                                           app'(app'(quot,
                                                 app'(app'(minus,x),y)),
                                            app'(s,y))) ;
  app'(app'(quot,0),app'(s,y)) >= 0 ;
  app'(app'(app,app'(app'(cons,x),l)),k) >= app'(app'(cons,x),
                                             app'(app'(app,l),k)) ;
  app'(app'(app,nil),k) >= k ;
  app'(app'(app,l),nil) >= l ;
  app'(app'(map,f),app'(app'(cons,x),xs)) >= app'(app'(cons,app'(f,x)),
                                              app'(app'(map,f),xs)) ;
  app'(app'(map,f),nil) >= nil ;
  app'(app'(filter,f),app'(app'(cons,x),xs)) >= app'(app'(app'(app'(filter2,
                                                                app'(f,x)),
                                                           f),x),xs) ;
  app'(app'(filter,f),nil) >= nil ;
  app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) >= 
app'(sum,app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k))))) ;
  app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) >= app'(sum,
                                                        app'(app'(cons,
                                                              app'(app'(plus,x),
                                                               y)),l)) ;
  app'(sum,app'(app'(cons,x),nil)) >= app'(app'(cons,x),nil) ;
  Marked_app'(app'(app'(app'(filter2,true),f),x),xs) >= Marked_app'(app'(
                                                                    cons,
                                                                    x),
                                                         app'(app'(filter,f),
                                                          xs)) ;
  Marked_app'(app'(app'(app'(filter2,true),f),x),xs) >= Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs) ;
  Marked_app'(app'(app'(app'(filter2,false),f),x),xs) >= Marked_app'(
                                                          app'(filter,
                                                           f),xs) ;
  Marked_app'(app'(minus,app'(app'(minus,x),y)),z) >= Marked_app'(app'(minus,x),
                                                       app'(app'(plus,y),z)) ;
  Marked_app'(app'(minus,app'(app'(minus,x),y)),z) >= Marked_app'(app'(plus,y),
                                                       z) ;
  Marked_app'(app'(minus,app'(s,x)),app'(s,y)) >= Marked_app'(app'(minus,x),y) ;
  Marked_app'(app'(plus,app'(s,x)),y) >= Marked_app'(app'(plus,x),y) ;
  Marked_app'(app'(quot,app'(s,x)),app'(s,y)) >= Marked_app'(app'(minus,x),y) ;
  Marked_app'(app'(quot,app'(s,x)),app'(s,y)) >= Marked_app'(app'(quot,
                                                              app'(app'(
                                                                    minus,
                                                                    x),
                                                               y)),app'(s,y)) ;
  Marked_app'(app'(app,app'(app'(cons,x),l)),k) >= Marked_app'(app'(app,l),k) ;
  Marked_app'(app'(app,app'(app'(cons,x),l)),k) >= Marked_app'(app'(cons,x),
                                                    app'(app'(app,l),k)) ;
  Marked_app'(app'(map,f),app'(app'(cons,x),xs)) >= Marked_app'(app'(
                                                                 cons,
                                                                 app'(f,x)),
                                                     app'(app'(map,f),xs)) ;
  Marked_app'(app'(map,f),app'(app'(cons,x),xs)) >= Marked_app'(app'(map,f),xs) ;
  Marked_app'(app'(map,f),app'(app'(cons,x),xs)) >= Marked_app'(f,x) ;
  Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) >= Marked_app'(app'(
                                                                    app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                    x),
                                                        xs) ;
  Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) >= Marked_app'(app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                        x) ;
  Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) >= Marked_app'(app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                        f) ;
  Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) >= Marked_app'(f,x) ;
  Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) >= 
Marked_app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k)))) ;
  Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) >= 
Marked_app'(sum,
 app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k))))) ;
  Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) >= 
Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),k))) ;
  Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) >= Marked_app'(
                                                               app'(plus,
                                                                x),y) ;
  Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) >= Marked_app'(
                                                               app'(cons,
                                                                app'(
                                                                 app'(
                                                                  plus,
                                                                  x),
                                                                 y)),
                                                               l) ;
  Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) >= Marked_app'(
                                                               sum,
                                                               app'(app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                                l)) ;
 }
 + Disjunctions:{ 
{
  Marked_app'(app'(app'(app'(filter2,true),f),x),xs) > Marked_app'(app'(cons,x),
                                                        app'(app'(filter,f),xs)) ;
 }
{
  Marked_app'(app'(app'(app'(filter2,true),f),x),xs) > Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                        xs) ;
 }
{
  Marked_app'(app'(app'(app'(filter2,false),f),x),xs) > Marked_app'(app'(
                                                                    filter,
                                                                    f),
                                                         xs) ;
 }
{
  Marked_app'(app'(minus,app'(app'(minus,x),y)),z) > Marked_app'(app'(minus,x),
                                                      app'(app'(plus,y),z)) ;
 }
{
  Marked_app'(app'(minus,app'(app'(minus,x),y)),z) > Marked_app'(app'(plus,y),
                                                      z) ;
 }
{
  Marked_app'(app'(minus,app'(s,x)),app'(s,y)) > Marked_app'(app'(minus,x),y) ;
 }
{
  Marked_app'(app'(plus,app'(s,x)),y) > Marked_app'(app'(plus,x),y) ;
 }
{
  Marked_app'(app'(quot,app'(s,x)),app'(s,y)) > Marked_app'(app'(minus,x),y) ;
 }
{
  Marked_app'(app'(quot,app'(s,x)),app'(s,y)) > Marked_app'(app'(quot,
                                                             app'(app'(minus,x),
                                                              y)),app'(s,y)) ;
 }
{
  Marked_app'(app'(app,app'(app'(cons,x),l)),k) > Marked_app'(app'(app,l),k) ;
 }
{
  Marked_app'(app'(app,app'(app'(cons,x),l)),k) > Marked_app'(app'(cons,x),
                                                   app'(app'(app,l),k)) ;
 }
{
  Marked_app'(app'(map,f),app'(app'(cons,x),xs)) > Marked_app'(app'(cons,
                                                                app'(f,x)),
                                                    app'(app'(map,f),xs)) ;
 }
{
  Marked_app'(app'(map,f),app'(app'(cons,x),xs)) > Marked_app'(app'(map,f),xs) ;
 }
{
  Marked_app'(app'(map,f),app'(app'(cons,x),xs)) > Marked_app'(f,x) ;
 }
{
  Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) > Marked_app'(app'(
                                                                   app'(
                                                                    app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                    f),
                                                                   x),
                                                       xs) ;
 }
{
  Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) > Marked_app'(app'(
                                                                   app'(
                                                                    filter2,
                                                                    app'(f,x)),
                                                                   f),
                                                       x) ;
 }
{
  Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) > Marked_app'(app'(
                                                                   filter2,
                                                                   app'(f,x)),
                                                       f) ;
 }
{
  Marked_app'(app'(filter,f),app'(app'(cons,x),xs)) > Marked_app'(f,x) ;
 }
{
  Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) > 
Marked_app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k)))) ;
 }
{
  Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) > 
Marked_app'(sum,
 app'(app'(app,l),app'(sum,app'(app'(cons,x),app'(app'(cons,y),k))))) ;
 }
{
  Marked_app'(sum,app'(app'(app,l),app'(app'(cons,x),app'(app'(cons,y),k)))) > 
Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),k))) ;
 }
{
  Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) > Marked_app'(
                                                              app'(plus,
                                                               x),y) ;
 }
{
  Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) > Marked_app'(
                                                              app'(cons,
                                                               app'(app'(
                                                                    plus,
                                                                    x),
                                                                y)),l) ;
 }
{
  Marked_app'(sum,app'(app'(cons,x),app'(app'(cons,y),l))) > Marked_app'(
                                                              sum,
                                                              app'(app'(
                                                                    cons,
                                                                    app'(
                                                                    app'(
                                                                    plus,
                                                                    x),
                                                                    y)),
                                                               l)) ;
 }
 } 
=== TIMER virtual : 10.000000 ===
Entering poly_solver
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 10.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
Entering rpo_solver
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 25.000000 ===
Search parameters: AFS type: 2 ; time limit: 25.. 
=== STOPING TIMER virtual ===
=== TIMER virtual : 15.000000 ===
Entering poly_solver
Starting Sat solver initialization
=== STOPING TIMER virtual ===
Time out for these parameters.
=== TIMER virtual : 50.000000 ===
trying sub matrices of size: 1
Matrix interpretation constraints generated.
Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. 
Termination constraints generated.
Starting Sat solver initialization
Calling Sat solver...
=== STOPING TIMER virtual ===
=== TIMER real : 50.000000 ===
=== STOPING TIMER real ===
Sat solver returned
=== STOPING TIMER real ===
=== STOPING TIMER virtual ===
No solution found for these parameters.
No solution found for these constraints.
APPLY CRITERIA (ID_CRIT)
NOT SOLVED
No proof found
Cime worked for 97.575631 seconds (real time)
Cime Exit Status: 0