*************************************
Proof
    { system = (VAR x y
                    z n
                    m u
                    v)
               (STRATEGY INNERMOST)
               (RULES f (true, x, y, z) -> f (gt (x, plus (y, z)), x, s (y), z)
                      f (true, x, y, z) -> f (gt (x, plus (y, z)), x, y, s (z))
                      plus (n, 0) -> n
                      plus (n, s (m)) -> s (plus (n, m))
                      gt (0, v) -> false
                      gt (s (u), 0) -> true
                      gt (s (u), s (v)) -> gt (u, v))
    , property = Termination , truth = Nothing , transform = Ignore_Strategy
    , to = [ Proof
                 { system = (VAR x y
                                 z n
                                 m u
                                 v)
                            (STRATEGY INNERMOST)
                            (RULES f (true, x, y, z) -> f (gt (x, plus (y, z)), x, s (y), z)
                                   f (true, x, y, z) -> f (gt (x, plus (y, z)), x, y, s (z))
                                   plus (n, 0) -> n
                                   plus (n, s (m)) -> s (plus (n, m))
                                   gt (0, v) -> false
                                   gt (s (u), 0) -> true
                                   gt (s (u), s (v)) -> gt (u, v))
                 , property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation
                 , to = [ Proof
                              { system = (VAR x y
                                              z n
                                              m u
                                              v)
                                         (STRATEGY INNERMOST)
                                         (RULES fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, s (y), z)
                                                fP (true, x, y, z) -> gtP (x, plus (y, z))
                                                fP (true, x, y, z) -> plusP (y, z)
                                                fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, y, s (z))
                                                fP (true, x, y, z) -> gtP (x, plus (y, z))
                                                fP (true, x, y, z) -> plusP (y, z)
                                                plusP (n, s (m)) -> plusP (n, m)
                                                gtP (s (u), s (v)) -> gtP (u, v)
                                                f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, s (y), z)
                                                f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, y, s (z))
                                                plus (n, 0) ->= n
                                                plus (n, s (m)) ->= s (plus (n, m))
                                                gt (0, v) ->= false
                                                gt (s (u), 0) ->= true
                                                gt (s (u), s (v)) ->= gt (u, v))
                              , property = Top_Termination , truth = Nothing
                              , transform = Remove
                                                { interpretation = Interpretation
                                                                       gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                       plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                       0 |-> () |-> E^0x1
                                                                       f |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1
                                                                       s |-> (x) |-> E^0x0 * x + E^0x1
                                                                       false |-> () |-> E^0x1
                                                                       fP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (3)
                                                                       gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       true |-> () |-> E^0x1
                                                                       plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                , removes_rules = [ fP (true, x, y, z) -> gtP (x, plus (y, z)) , fP (true, x, y, z) -> plusP (y, z) , fP (true, x, y, z) -> gtP (x, plus (y, z)) , fP (true, x, y, z) -> plusP (y, z) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                                                }
                              , to = [ Proof
                                           { system = (VAR x y
                                                           z n
                                                           m u
                                                           v)
                                                      (STRATEGY INNERMOST)
                                                      (RULES fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, s (y), z)
                                                             fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, y, s (z))
                                                             plusP (n, s (m)) -> plusP (n, m)
                                                             gtP (s (u), s (v)) -> gtP (u, v)
                                                             f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, s (y), z)
                                                             f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, y, s (z))
                                                             plus (n, 0) ->= n
                                                             plus (n, s (m)) ->= s (plus (n, m))
                                                             gt (0, v) ->= false
                                                             gt (s (u), 0) ->= true
                                                             gt (s (u), s (v)) ->= gt (u, v))
                                           , property = Top_Termination , truth = Nothing
                                           , transform = Split
                                                             { interpretation = Interpretation
                                                                                    gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                                    plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                                    0 |-> () |-> E^0x1
                                                                                    f |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1
                                                                                    s |-> (x) |-> E^0x0 * x + E^0x1
                                                                                    false |-> () |-> E^0x1
                                                                                    fP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (3)
                                                                                    gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    true |-> () |-> E^0x1
                                                                                    plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                             , clusters = [ [ plusP (n, s (m)) -> plusP (n, m) ] , [ gtP (s (u), s (v)) -> gtP (u, v) ] , [ fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, s (y), z) , fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, y, s (z)) ] ]
                                                             , comment = size 0 , heights ( 3 , 7 ) , time 
                                                                         split_dimension:  0
                                                             }
                                           , to = [ Proof
                                                        { system = (VAR x y
                                                                        z n
                                                                        m u
                                                                        v)
                                                                   (STRATEGY INNERMOST)
                                                                   (RULES plusP (n, s (m)) -> plusP (n, m)
                                                                          f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, s (y), z)
                                                                          f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, y, s (z))
                                                                          plus (n, 0) ->= n
                                                                          plus (n, s (m)) ->= s (plus (n, m))
                                                                          gt (0, v) ->= false
                                                                          gt (s (u), 0) ->= true
                                                                          gt (s (u), s (v)) ->= gt (u, v))
                                                        , property = Top_Termination
                                                        , truth = Just
                                                                      True
                                                        , transform = Remove
                                                                          { interpretation = Interpretation
                                                                                                 plusP |-> (x , y) |-> (1) * x + (2) * y + (0)
                                                                                                 0 |-> () |-> (0)
                                                                                                 f |-> (p , q , r , s) |-> (0) * p + (0) * q + (0) * r + (0) * s + (0)
                                                                                                 s |-> (x) |-> (1) * x + (1)
                                                                                                 false |-> () |-> (0)
                                                                                                 gt |-> (x , y) |-> (0) * x + (0) * y + (0)
                                                                                                 true |-> () |-> (0)
                                                                                                 plus |-> (x , y) |-> (1) * x + (1) * y + (0)
                                                                          , removes_rules = [ plusP (n, s (m)) -> plusP (n, m) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
                                                                          }
                                                        , to = [ Proof
                                                                     { system = (VAR x y
                                                                                     z n
                                                                                     m u
                                                                                     v)
                                                                                (STRATEGY INNERMOST)
                                                                                (RULES f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, s (y), z)
                                                                                       f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, y, s (z))
                                                                                       plus (n, 0) ->= n
                                                                                       plus (n, s (m)) ->= s (plus (n, m))
                                                                                       gt (0, v) ->= false
                                                                                       gt (s (u), 0) ->= true
                                                                                       gt (s (u), s (v)) ->= gt (u, v))
                                                                     , property = Top_Termination
                                                                     , truth = Just
                                                                                   True
                                                                     , transform = No_Strict_Rules , to = [ ]
                                                                     }
                                                               ]
                                                        }
                                                  , Proof
                                                        { system = (VAR x y
                                                                        z n
                                                                        m u
                                                                        v)
                                                                   (STRATEGY INNERMOST)
                                                                   (RULES gtP (s (u), s (v)) -> gtP (u, v)
                                                                          f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, s (y), z)
                                                                          f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, y, s (z))
                                                                          plus (n, 0) ->= n
                                                                          plus (n, s (m)) ->= s (plus (n, m))
                                                                          gt (0, v) ->= false
                                                                          gt (s (u), 0) ->= true
                                                                          gt (s (u), s (v)) ->= gt (u, v))
                                                        , property = Top_Termination
                                                        , truth = Just
                                                                      True
                                                        , transform = Remove
                                                                          { interpretation = Interpretation
                                                                                                 gtP |-> (x , y) |-> (0) * x + (1) * y + (0)
                                                                                                 0 |-> () |-> (0)
                                                                                                 f |-> (p , q , r , s) |-> (0) * p + (0) * q + (0) * r + (0) * s + (0)
                                                                                                 s |-> (x) |-> (1) * x + (1)
                                                                                                 false |-> () |-> (0)
                                                                                                 gt |-> (x , y) |-> (0) * x + (0) * y + (0)
                                                                                                 true |-> () |-> (0)
                                                                                                 plus |-> (x , y) |-> (4) * x + (1) * y + (0)
                                                                          , removes_rules = [ gtP (s (u), s (v)) -> gtP (u, v) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
                                                                          }
                                                        , to = [ Proof
                                                                     { system = (VAR x y
                                                                                     z n
                                                                                     m u
                                                                                     v)
                                                                                (STRATEGY INNERMOST)
                                                                                (RULES f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, s (y), z)
                                                                                       f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, y, s (z))
                                                                                       plus (n, 0) ->= n
                                                                                       plus (n, s (m)) ->= s (plus (n, m))
                                                                                       gt (0, v) ->= false
                                                                                       gt (s (u), 0) ->= true
                                                                                       gt (s (u), s (v)) ->= gt (u, v))
                                                                     , property = Top_Termination
                                                                     , truth = Just
                                                                                   True
                                                                     , transform = No_Strict_Rules , to = [ ]
                                                                     }
                                                               ]
                                                        }
                                                  , Claim
                                                        { system = (VAR x y
                                                                        z n
                                                                        m u
                                                                        v)
                                                                   (STRATEGY INNERMOST)
                                                                   (RULES fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, s (y), z)
                                                                          fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, y, s (z))
                                                                          f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, s (y), z)
                                                                          f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, y, s (z))
                                                                          plus (n, 0) ->= n
                                                                          plus (n, s (m)) ->= s (plus (n, m))
                                                                          gt (0, v) ->= false
                                                                          gt (s (u), 0) ->= true
                                                                          gt (s (u), s (v)) ->= gt (u, v))
                                                        , property = Top_Termination
                                                        }
                                                  ]
                                           }
                                     ]
                              }
                        ]
                 }
           ]
    }


Proof summary:

value Nothing
for property Termination
for system with 7 strict rules and 0 non-strict rules
follows by transformation
    Ignore_Strategy
from
    value Nothing
    for property Termination
    for system with 7 strict rules and 0 non-strict rules
    follows by transformation
        Dependency_Pair_Transformation
    from
        value Nothing
        for property Top_Termination
        for system with 8 strict rules and 7 non-strict rules
        follows by transformation
            Remove
                { interpretation = Interpretation
                                       gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                       plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                       0 |-> () |-> E^0x1
                                       f |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1
                                       s |-> (x) |-> E^0x0 * x + E^0x1
                                       false |-> () |-> E^0x1
                                       fP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (3)
                                       gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       true |-> () |-> E^0x1
                                       plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                , removes_rules = [ fP (true, x, y, z) -> gtP (x, plus (y, z)) , fP (true, x, y, z) -> plusP (y, z) , fP (true, x, y, z) -> gtP (x, plus (y, z)) , fP (true, x, y, z) -> plusP (y, z) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                }
        from
            value Nothing
            for property Top_Termination
            for system with 4 strict rules and 7 non-strict rules
            follows by transformation
                Split
                    { interpretation = Interpretation
                                           gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                           plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                           0 |-> () |-> E^0x1
                                           f |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1
                                           s |-> (x) |-> E^0x0 * x + E^0x1
                                           false |-> () |-> E^0x1
                                           fP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (3)
                                           gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           true |-> () |-> E^0x1
                                           plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                    , clusters = [ [ plusP (n, s (m)) -> plusP (n, m) ] , [ gtP (s (u), s (v)) -> gtP (u, v) ] , [ fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, s (y), z) , fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, y, s (z)) ] ]
                    , comment = size 0 , heights ( 3 , 7 ) , time 
                                split_dimension:  0
                    }
            from
                value Just
                          True
                for property Top_Termination
                for system with 1 strict rules and 7 non-strict rules
                follows by transformation
                    Remove
                        { interpretation = Interpretation
                                               plusP |-> (x , y) |-> (1) * x + (2) * y + (0)
                                               0 |-> () |-> (0)
                                               f |-> (p , q , r , s) |-> (0) * p + (0) * q + (0) * r + (0) * s + (0)
                                               s |-> (x) |-> (1) * x + (1)
                                               false |-> () |-> (0)
                                               gt |-> (x , y) |-> (0) * x + (0) * y + (0)
                                               true |-> () |-> (0)
                                               plus |-> (x , y) |-> (1) * x + (1) * y + (0)
                        , removes_rules = [ plusP (n, s (m)) -> plusP (n, m) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
                        }
                from
                    value Just
                              True
                    for property Top_Termination
                    for system with 0 strict rules and 7 non-strict rules
                    follows by transformation
                        No_Strict_Rules
                    from
                value Just
                          True
                for property Top_Termination
                for system with 1 strict rules and 7 non-strict rules
                follows by transformation
                    Remove
                        { interpretation = Interpretation
                                               gtP |-> (x , y) |-> (0) * x + (1) * y + (0)
                                               0 |-> () |-> (0)
                                               f |-> (p , q , r , s) |-> (0) * p + (0) * q + (0) * r + (0) * s + (0)
                                               s |-> (x) |-> (1) * x + (1)
                                               false |-> () |-> (0)
                                               gt |-> (x , y) |-> (0) * x + (0) * y + (0)
                                               true |-> () |-> (0)
                                               plus |-> (x , y) |-> (4) * x + (1) * y + (0)
                        , removes_rules = [ gtP (s (u), s (v)) -> gtP (u, v) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
                        }
                from
                    value Just
                              True
                    for property Top_Termination
                    for system with 0 strict rules and 7 non-strict rules
                    follows by transformation
                        No_Strict_Rules
                    from
                Claim
                    { system = (VAR x y
                                    z n
                                    m u
                                    v)
                               (STRATEGY INNERMOST)
                               (RULES fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, s (y), z)
                                      fP (true, x, y, z) -> fP (gt (x, plus (y, z)), x, y, s (z))
                                      f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, s (y), z)
                                      f (true, x, y, z) ->= f (gt (x, plus (y, z)), x, y, s (z))
                                      plus (n, 0) ->= n
                                      plus (n, s (m)) ->= s (plus (n, m))
                                      gt (0, v) ->= false
                                      gt (s (u), 0) ->= true
                                      gt (s (u), s (v)) ->= gt (u, v))
                    , property = Top_Termination
                    }
------------------------------------------------------------------
matchbox general information (including details on proof methods):
http://dfa.imn.htwk-leipzig.de/matchbox/

this matchbox implementation uses the SAT solver
SatELite/MiniSat by Niklas Een and Niklas Sörensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

matchbox process information
arguments      : --solver=/home/nowonder/forschung/increasing/wst06/matchbox/SatELiteGTI --timeout-command=/home/nowonder/forschung/increasing/wst06/matchbox/timeout --tmpdir=/home/nowonder/forschung/increasing/wst06/matchbox --timeout=60 /tmp/tmp6Tjvxx/ex06.trs
started        : Thu Feb 22 16:37:25 CET 2007
finished       : Thu Feb 22 16:38:29 CET 2007
run system     : Linux aprove 2.6.14-gentoo-r5 #1 SMP Sun Dec 25 15:42:02 CET 2005 x86_64
release date   : Thu Jun 8 23:18:07 CEST 2006
build date     : Thu Jun 8 23:18:07 CEST 2006
build system   : Linux dfa 2.6.8-2-k7 #1 Tue Aug 16 14:00:15 UTC 2005 i686 GNU/Linux

used clock time: 64 secs