************************************* Proof { system = (VAR x y v u) (STRATEGY INNERMOST) (RULES minus (x, x) -> 0 minus (x, y) -> cond (equal (min (x, y), y), x, y) cond (true, x, y) -> s (minus (x, s (y))) min (0, v) -> 0 min (u, 0) -> 0 min (s (u), s (v)) -> s (min (u, v)) equal (0, 0) -> true equal (s (x), 0) -> false equal (0, s (y)) -> false equal (s (x), s (y)) -> equal (x, y)) , property = Termination , truth = Nothing , transform = Ignore_Strategy , to = [ Proof { system = (VAR x y v u) (STRATEGY INNERMOST) (RULES minus (x, x) -> 0 minus (x, y) -> cond (equal (min (x, y), y), x, y) cond (true, x, y) -> s (minus (x, s (y))) min (0, v) -> 0 min (u, 0) -> 0 min (s (u), s (v)) -> s (min (u, v)) equal (0, 0) -> true equal (s (x), 0) -> false equal (0, s (y)) -> false equal (s (x), s (y)) -> equal (x, y)) , property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation , to = [ Proof { system = (VAR x y v u) (STRATEGY INNERMOST) (RULES minusP (x, y) -> condP (equal (min (x, y), y), x, y) minusP (x, y) -> equalP (min (x, y), y) minusP (x, y) -> minP (x, y) condP (true, x, y) -> minusP (x, s (y)) minP (s (u), s (v)) -> minP (u, v) equalP (s (x), s (y)) -> equalP (x, y) minus (x, x) ->= 0 minus (x, y) ->= cond (equal (min (x, y), y), x, y) cond (true, x, y) ->= s (minus (x, s (y))) min (0, v) ->= 0 min (u, 0) ->= 0 min (s (u), s (v)) ->= s (min (u, v)) equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y)) , property = Top_Termination , truth = Nothing , transform = Remove { interpretation = Interpretation equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) minusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (3) condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (3) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 true |-> () |-> E^0x1 minP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 minus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 min |-> (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) -> equalP (min (x, y), y) , minusP (x, y) -> minP (x, y) ] , comment = size 0 , heights ( 3 , 7 ) , time } , to = [ Proof { system = (VAR x y v u) (STRATEGY INNERMOST) (RULES minusP (x, y) -> condP (equal (min (x, y), y), x, y) condP (true, x, y) -> minusP (x, s (y)) minP (s (u), s (v)) -> minP (u, v) equalP (s (x), s (y)) -> equalP (x, y) minus (x, x) ->= 0 minus (x, y) ->= cond (equal (min (x, y), y), x, y) cond (true, x, y) ->= s (minus (x, s (y))) min (0, v) ->= 0 min (u, 0) ->= 0 min (s (u), s (v)) ->= s (min (u, v)) equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y)) , property = Top_Termination , truth = Nothing , transform = Split { interpretation = Interpretation equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) minusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (3) condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (3) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 true |-> () |-> E^0x1 minP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 minus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 min |-> (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 = [ [ minP (s (u), s (v)) -> minP (u, v) ] , [ equalP (s (x), s (y)) -> equalP (x, y) ] , [ minusP (x, y) -> condP (equal (min (x, y), 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 v u) (STRATEGY INNERMOST) (RULES minP (s (u), s (v)) -> minP (u, v) minus (x, x) ->= 0 minus (x, y) ->= cond (equal (min (x, y), y), x, y) cond (true, x, y) ->= s (minus (x, s (y))) min (0, v) ->= 0 min (u, 0) ->= 0 min (s (u), s (v)) ->= s (min (u, v)) equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y)) , property = Top_Termination } , Claim { system = (VAR x y v u) (STRATEGY INNERMOST) (RULES equalP (s (x), s (y)) -> equalP (x, y) minus (x, x) ->= 0 minus (x, y) ->= cond (equal (min (x, y), y), x, y) cond (true, x, y) ->= s (minus (x, s (y))) min (0, v) ->= 0 min (u, 0) ->= 0 min (s (u), s (v)) ->= s (min (u, v)) equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y)) , property = Top_Termination } , Claim { system = (VAR x y v u) (STRATEGY INNERMOST) (RULES minusP (x, y) -> condP (equal (min (x, y), y), x, y) condP (true, x, y) -> minusP (x, s (y)) minus (x, x) ->= 0 minus (x, y) ->= cond (equal (min (x, y), y), x, y) cond (true, x, y) ->= s (minus (x, s (y))) min (0, v) ->= 0 min (u, 0) ->= 0 min (s (u), s (v)) ->= s (min (u, v)) equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y)) , 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 6 strict rules and 10 non-strict rules follows by transformation Remove { interpretation = Interpretation equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) minusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (3) condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (3) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 true |-> () |-> E^0x1 minP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 minus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 min |-> (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) -> equalP (min (x, y), y) , minusP (x, y) -> minP (x, y) ] , comment = size 0 , heights ( 3 , 7 ) , time } from value Nothing for property Top_Termination for system with 4 strict rules and 10 non-strict rules follows by transformation Split { interpretation = Interpretation equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) minusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (3) condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (3) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 true |-> () |-> E^0x1 minP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 minus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 min |-> (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 = [ [ minP (s (u), s (v)) -> minP (u, v) ] , [ equalP (s (x), s (y)) -> equalP (x, y) ] , [ minusP (x, y) -> condP (equal (min (x, y), 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 v u) (STRATEGY INNERMOST) (RULES minP (s (u), s (v)) -> minP (u, v) minus (x, x) ->= 0 minus (x, y) ->= cond (equal (min (x, y), y), x, y) cond (true, x, y) ->= s (minus (x, s (y))) min (0, v) ->= 0 min (u, 0) ->= 0 min (s (u), s (v)) ->= s (min (u, v)) equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y)) , property = Top_Termination } Claim { system = (VAR x y v u) (STRATEGY INNERMOST) (RULES equalP (s (x), s (y)) -> equalP (x, y) minus (x, x) ->= 0 minus (x, y) ->= cond (equal (min (x, y), y), x, y) cond (true, x, y) ->= s (minus (x, s (y))) min (0, v) ->= 0 min (u, 0) ->= 0 min (s (u), s (v)) ->= s (min (u, v)) equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y)) , property = Top_Termination } Claim { system = (VAR x y v u) (STRATEGY INNERMOST) (RULES minusP (x, y) -> condP (equal (min (x, y), y), x, y) condP (true, x, y) -> minusP (x, s (y)) minus (x, x) ->= 0 minus (x, y) ->= cond (equal (min (x, y), y), x, y) cond (true, x, y) ->= s (minus (x, s (y))) min (0, v) ->= 0 min (u, 0) ->= 0 min (s (u), s (v)) ->= s (min (u, v)) equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y)) , 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/tmpqjZZtU/ex05.trs started : Thu Feb 22 16:27:19 CET 2007 finished : Thu Feb 22 16:28:17 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: 58 secs