************************************* Proof { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES div (x, s (y)) -> d (x, s (y), 0) d (x, s (y), z) -> cond (ge (x, z), x, y, z) cond (true, x, y, z) -> s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) -> 0 ge (u, 0) -> true ge (0, s (v)) -> false ge (s (u), s (v)) -> ge (u, v) plus (n, 0) -> n plus (n, s (m)) -> s (plus (n, m)) plus (plus (n, m), u) -> plus (n, plus (m, u))) , property = Termination , truth = Nothing , transform = Ignore_Strategy , to = [ Proof { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES div (x, s (y)) -> d (x, s (y), 0) d (x, s (y), z) -> cond (ge (x, z), x, y, z) cond (true, x, y, z) -> s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) -> 0 ge (u, 0) -> true ge (0, s (v)) -> false ge (s (u), s (v)) -> ge (u, v) plus (n, 0) -> n plus (n, s (m)) -> s (plus (n, m)) plus (plus (n, m), u) -> plus (n, plus (m, u))) , property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation , to = [ Proof { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES divP (x, s (y)) -> dP (x, s (y), 0) dP (x, s (y), z) -> condP (ge (x, z), x, y, z) dP (x, s (y), z) -> geP (x, z) condP (true, x, y, z) -> dP (x, s (y), plus (s (y), z)) condP (true, x, y, z) -> plusP (s (y), z) geP (s (u), s (v)) -> geP (u, v) plusP (n, s (m)) -> plusP (n, m) plusP (plus (n, m), u) -> plusP (n, plus (m, u)) plusP (plus (n, m), u) -> plusP (m, u) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , property = Top_Termination , truth = Nothing , transform = Remove { interpretation = Interpretation geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) condP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (0) 0 |-> () |-> E^0x1 d |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 dP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 true |-> () |-> E^0x1 divP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) div |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1 , removes_rules = [ divP (x, s (y)) -> dP (x, s (y), 0) ] , comment = size 0 , heights ( 3 , 7 ) , time 1 sec } , to = [ Proof { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES dP (x, s (y), z) -> condP (ge (x, z), x, y, z) dP (x, s (y), z) -> geP (x, z) condP (true, x, y, z) -> dP (x, s (y), plus (s (y), z)) condP (true, x, y, z) -> plusP (s (y), z) geP (s (u), s (v)) -> geP (u, v) plusP (n, s (m)) -> plusP (n, m) plusP (plus (n, m), u) -> plusP (n, plus (m, u)) plusP (plus (n, m), u) -> plusP (m, u) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , property = Top_Termination , truth = Nothing , transform = Remove { interpretation = Interpretation geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) condP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (2) 0 |-> () |-> E^0x1 d |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 dP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 true |-> () |-> E^0x1 div |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1 , removes_rules = [ dP (x, s (y), z) -> geP (x, z) , condP (true, x, y, z) -> plusP (s (y), z) ] , comment = size 0 , heights ( 3 , 7 ) , time } , to = [ Proof { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES dP (x, s (y), z) -> condP (ge (x, z), x, y, z) condP (true, x, y, z) -> dP (x, s (y), plus (s (y), z)) geP (s (u), s (v)) -> geP (u, v) plusP (n, s (m)) -> plusP (n, m) plusP (plus (n, m), u) -> plusP (n, plus (m, u)) plusP (plus (n, m), u) -> plusP (m, u) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , property = Top_Termination , truth = Nothing , transform = Split { interpretation = Interpretation geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) condP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (2) 0 |-> () |-> E^0x1 d |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 dP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 true |-> () |-> E^0x1 div |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1 , clusters = [ [ geP (s (u), s (v)) -> geP (u, v) ] , [ plusP (n, s (m)) -> plusP (n, m) , plusP (plus (n, m), u) -> plusP (n, plus (m, u)) , plusP (plus (n, m), u) -> plusP (m, u) ] , [ dP (x, s (y), z) -> condP (ge (x, z), x, y, z) , condP (true, x, y, z) -> dP (x, s (y), plus (s (y), z)) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } , to = [ Claim { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES geP (s (u), s (v)) -> geP (u, v) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , property = Top_Termination } , Claim { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES plusP (n, s (m)) -> plusP (n, m) plusP (plus (n, m), u) -> plusP (n, plus (m, u)) plusP (plus (n, m), u) -> plusP (m, u) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , property = Top_Termination } , Claim { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES dP (x, s (y), z) -> condP (ge (x, z), x, y, z) condP (true, x, y, z) -> dP (x, s (y), plus (s (y), z)) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , property = Top_Termination } ] } ] } ] } ] } ] } Proof summary: value Nothing for property Termination for system with 10 strict rules and 0 non-strict rules follows by transformation Ignore_Strategy from value Nothing for property Termination for system with 10 strict rules and 0 non-strict rules follows by transformation Dependency_Pair_Transformation from value Nothing for property Top_Termination for system with 9 strict rules and 10 non-strict rules follows by transformation Remove { interpretation = Interpretation geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) condP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (0) 0 |-> () |-> E^0x1 d |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 dP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 true |-> () |-> E^0x1 divP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) div |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1 , removes_rules = [ divP (x, s (y)) -> dP (x, s (y), 0) ] , comment = size 0 , heights ( 3 , 7 ) , time 1 sec } from value Nothing for property Top_Termination for system with 8 strict rules and 10 non-strict rules follows by transformation Remove { interpretation = Interpretation geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) condP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (2) 0 |-> () |-> E^0x1 d |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 dP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 true |-> () |-> E^0x1 div |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1 , removes_rules = [ dP (x, s (y), z) -> geP (x, z) , condP (true, x, y, z) -> plusP (s (y), z) ] , comment = size 0 , heights ( 3 , 7 ) , time } from value Nothing for property Top_Termination for system with 6 strict rules and 10 non-strict rules follows by transformation Split { interpretation = Interpretation geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) condP |-> (p , q , r , s) |-> E^1x0 * p + E^1x0 * q + E^1x0 * r + E^1x0 * s + (2) 0 |-> () |-> E^0x1 d |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 dP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 true |-> () |-> E^0x1 div |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond |-> (p , q , r , s) |-> E^0x0 * p + E^0x0 * q + E^0x0 * r + E^0x0 * s + E^0x1 , clusters = [ [ geP (s (u), s (v)) -> geP (u, v) ] , [ plusP (n, s (m)) -> plusP (n, m) , plusP (plus (n, m), u) -> plusP (n, plus (m, u)) , plusP (plus (n, m), u) -> plusP (m, u) ] , [ dP (x, s (y), z) -> condP (ge (x, z), x, y, z) , condP (true, x, y, z) -> dP (x, s (y), plus (s (y), z)) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } from Claim { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES geP (s (u), s (v)) -> geP (u, v) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , property = Top_Termination } Claim { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES plusP (n, s (m)) -> plusP (n, m) plusP (plus (n, m), u) -> plusP (n, plus (m, u)) plusP (plus (n, m), u) -> plusP (m, u) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , property = Top_Termination } Claim { system = (VAR x y z u v n m) (STRATEGY INNERMOST) (RULES dP (x, s (y), z) -> condP (ge (x, z), x, y, z) condP (true, x, y, z) -> dP (x, s (y), plus (s (y), z)) div (x, s (y)) ->= d (x, s (y), 0) d (x, s (y), z) ->= cond (ge (x, z), x, y, z) cond (true, x, y, z) ->= s (d (x, s (y), plus (s (y), z))) cond (false, x, y, z) ->= 0 ge (u, 0) ->= true ge (0, s (v)) ->= false ge (s (u), s (v)) ->= ge (u, v) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m)) plus (plus (n, m), u) ->= plus (n, plus (m, u))) , 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/tmpxLiSZI/ex13.trs started : Thu Feb 22 16:43:50 CET 2007 finished : Thu Feb 22 16:44:44 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: 54 secs