*************************************
Proof
    { system = (VAR x y
                    u v)
               (STRATEGY INNERMOST)
               (RULES minus (x, y) -> cond (ge (x, s (y)), x, y)
                      cond (false, x, y) -> 0
                      cond (true, x, y) -> s (minus (x, s (y)))
                      ge (u, 0) -> true
                      ge (0, s (v)) -> false
                      ge (s (u), s (v)) -> ge (u, v))
    , property = Termination , truth = Nothing , transform = Ignore_Strategy
    , to = [ Proof
                 { system = (VAR x y
                                 u v)
                            (STRATEGY INNERMOST)
                            (RULES minus (x, y) -> cond (ge (x, s (y)), x, y)
                                   cond (false, x, y) -> 0
                                   cond (true, x, y) -> s (minus (x, s (y)))
                                   ge (u, 0) -> true
                                   ge (0, s (v)) -> false
                                   ge (s (u), s (v)) -> ge (u, v))
                 , property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation
                 , to = [ Proof
                              { system = (VAR x y
                                              u v)
                                         (STRATEGY INNERMOST)
                                         (RULES minusP (x, y) -> condP (ge (x, s (y)), x, y)
                                                minusP (x, y) -> geP (x, s (y))
                                                condP (true, x, y) -> minusP (x, s (y))
                                                geP (s (u), s (v)) -> geP (u, v)
                                                minus (x, y) ->= cond (ge (x, s (y)), x, y)
                                                cond (false, x, y) ->= 0
                                                cond (true, x, y) ->= s (minus (x, s (y)))
                                                ge (u, 0) ->= true
                                                ge (0, s (v)) ->= false
                                                ge (s (u), s (v)) ->= ge (u, v))
                              , property = Top_Termination , truth = Nothing
                              , transform = Remove
                                                { interpretation = Interpretation
                                                                       geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                       minusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
                                                                       condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (1)
                                                                       0 |-> () |-> E^0x1
                                                                       s |-> (x) |-> E^0x0 * x + E^0x1
                                                                       false |-> () |-> E^0x1
                                                                       ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       true |-> () |-> E^0x1
                                                                       minus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                , removes_rules = [ minusP (x, y) -> geP (x, s (y)) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                                                }
                              , to = [ Proof
                                           { system = (VAR x y
                                                           u v)
                                                      (STRATEGY INNERMOST)
                                                      (RULES minusP (x, y) -> condP (ge (x, s (y)), x, y)
                                                             condP (true, x, y) -> minusP (x, s (y))
                                                             geP (s (u), s (v)) -> geP (u, v)
                                                             minus (x, y) ->= cond (ge (x, s (y)), x, y)
                                                             cond (false, x, y) ->= 0
                                                             cond (true, x, y) ->= s (minus (x, s (y)))
                                                             ge (u, 0) ->= true
                                                             ge (0, s (v)) ->= false
                                                             ge (s (u), s (v)) ->= ge (u, v))
                                           , property = Top_Termination , truth = Nothing
                                           , transform = Split
                                                             { interpretation = Interpretation
                                                                                    geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                                    minusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
                                                                                    condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (1)
                                                                                    0 |-> () |-> E^0x1
                                                                                    s |-> (x) |-> E^0x0 * x + E^0x1
                                                                                    false |-> () |-> E^0x1
                                                                                    ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    true |-> () |-> E^0x1
                                                                                    minus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                             , clusters = [ [ geP (s (u), s (v)) -> geP (u, v) ] , [ minusP (x, y) -> condP (ge (x, s (y)), x, y) , condP (true, x, y) -> minusP (x, s (y)) ] ]
                                                             , comment = size 0 , heights ( 3 , 7 ) , time 
                                                                         split_dimension:  0
                                                             }
                                           , to = [ Claim
                                                        { system = (VAR x y
                                                                        u v)
                                                                   (STRATEGY INNERMOST)
                                                                   (RULES geP (s (u), s (v)) -> geP (u, v)
                                                                          minus (x, y) ->= cond (ge (x, s (y)), x, y)
                                                                          cond (false, x, y) ->= 0
                                                                          cond (true, x, y) ->= s (minus (x, s (y)))
                                                                          ge (u, 0) ->= true
                                                                          ge (0, s (v)) ->= false
                                                                          ge (s (u), s (v)) ->= ge (u, v))
                                                        , property = Top_Termination
                                                        }
                                                  , Claim
                                                        { system = (VAR x y
                                                                        u v)
                                                                   (STRATEGY INNERMOST)
                                                                   (RULES minusP (x, y) -> condP (ge (x, s (y)), x, y)
                                                                          condP (true, x, y) -> minusP (x, s (y))
                                                                          minus (x, y) ->= cond (ge (x, s (y)), x, y)
                                                                          cond (false, x, y) ->= 0
                                                                          cond (true, x, y) ->= s (minus (x, s (y)))
                                                                          ge (u, 0) ->= true
                                                                          ge (0, s (v)) ->= false
                                                                          ge (s (u), s (v)) ->= ge (u, v))
                                                        , property = Top_Termination
                                                        }
                                                  ]
                                           }
                                     ]
                              }
                        ]
                 }
           ]
    }


Proof summary:

value Nothing
for property Termination
for system with 6 strict rules and 0 non-strict rules
follows by transformation
    Ignore_Strategy
from
    value Nothing
    for property Termination
    for system with 6 strict rules and 0 non-strict rules
    follows by transformation
        Dependency_Pair_Transformation
    from
        value Nothing
        for property Top_Termination
        for system with 4 strict rules and 6 non-strict rules
        follows by transformation
            Remove
                { interpretation = Interpretation
                                       geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                       minusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
                                       condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (1)
                                       0 |-> () |-> E^0x1
                                       s |-> (x) |-> E^0x0 * x + E^0x1
                                       false |-> () |-> E^0x1
                                       ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       true |-> () |-> E^0x1
                                       minus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                , removes_rules = [ minusP (x, y) -> geP (x, s (y)) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                }
        from
            value Nothing
            for property Top_Termination
            for system with 3 strict rules and 6 non-strict rules
            follows by transformation
                Split
                    { interpretation = Interpretation
                                           geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                           minusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
                                           condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (1)
                                           0 |-> () |-> E^0x1
                                           s |-> (x) |-> E^0x0 * x + E^0x1
                                           false |-> () |-> E^0x1
                                           ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           true |-> () |-> E^0x1
                                           minus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                    , clusters = [ [ geP (s (u), s (v)) -> geP (u, v) ] , [ minusP (x, y) -> condP (ge (x, s (y)), x, y) , condP (true, x, y) -> minusP (x, s (y)) ] ]
                    , comment = size 0 , heights ( 3 , 7 ) , time 
                                split_dimension:  0
                    }
            from
                Claim
                    { system = (VAR x y
                                    u v)
                               (STRATEGY INNERMOST)
                               (RULES geP (s (u), s (v)) -> geP (u, v)
                                      minus (x, y) ->= cond (ge (x, s (y)), x, y)
                                      cond (false, x, y) ->= 0
                                      cond (true, x, y) ->= s (minus (x, s (y)))
                                      ge (u, 0) ->= true
                                      ge (0, s (v)) ->= false
                                      ge (s (u), s (v)) ->= ge (u, v))
                    , property = Top_Termination
                    }
                Claim
                    { system = (VAR x y
                                    u v)
                               (STRATEGY INNERMOST)
                               (RULES minusP (x, y) -> condP (ge (x, s (y)), x, y)
                                      condP (true, x, y) -> minusP (x, s (y))
                                      minus (x, y) ->= cond (ge (x, s (y)), x, y)
                                      cond (false, x, y) ->= 0
                                      cond (true, x, y) ->= s (minus (x, s (y)))
                                      ge (u, 0) ->= true
                                      ge (0, s (v)) ->= false
                                      ge (s (u), s (v)) ->= ge (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/tmpYK6PKp/ex03.trs
started        : Thu Feb 22 16:25:36 CET 2007
finished       : Thu Feb 22 16:26:27 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: 51 secs