************************************* Proof { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES sort (l) -> st (0, l) st (n, l) -> cond1 (member (n, l), n, l) cond1 (true, n, l) -> cons (n, st (s (n), l)) cond1 (false, n, l) -> cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) -> nil cond2 (false, n, l) -> st (s (n), l) member (n, nil) -> false member (n, cons (m, l)) -> or (equal (n, m), member (n, l)) or (x, true) -> true or (x, false) -> x equal (0, 0) -> true equal (s (x), 0) -> false equal (0, s (y)) -> false equal (s (x), s (y)) -> equal (x, y) gt (0, v) -> false gt (s (u), 0) -> true gt (s (u), s (v)) -> gt (u, v) max (nil) -> 0 max (cons (u, l)) -> if (gt (u, max (l)), u, max (l)) if (true, u, v) -> u if (false, u, v) -> v) , property = Termination , truth = Nothing , transform = Ignore_Strategy , to = [ Proof { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES sort (l) -> st (0, l) st (n, l) -> cond1 (member (n, l), n, l) cond1 (true, n, l) -> cons (n, st (s (n), l)) cond1 (false, n, l) -> cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) -> nil cond2 (false, n, l) -> st (s (n), l) member (n, nil) -> false member (n, cons (m, l)) -> or (equal (n, m), member (n, l)) or (x, true) -> true or (x, false) -> x equal (0, 0) -> true equal (s (x), 0) -> false equal (0, s (y)) -> false equal (s (x), s (y)) -> equal (x, y) gt (0, v) -> false gt (s (u), 0) -> true gt (s (u), s (v)) -> gt (u, v) max (nil) -> 0 max (cons (u, l)) -> if (gt (u, max (l)), u, max (l)) if (true, u, v) -> u if (false, u, v) -> v) , property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation , to = [ Proof { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES sortP (l) -> stP (0, l) stP (n, l) -> cond1P (member (n, l), n, l) stP (n, l) -> memberP (n, l) cond1P (true, n, l) -> stP (s (n), l) cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) cond1P (false, n, l) -> gtP (n, max (l)) cond1P (false, n, l) -> maxP (l) cond2P (false, n, l) -> stP (s (n), l) memberP (n, cons (m, l)) -> orP (equal (n, m), member (n, l)) memberP (n, cons (m, l)) -> equalP (n, m) memberP (n, cons (m, l)) -> memberP (n, l) equalP (s (x), s (y)) -> equalP (x, y) gtP (s (u), s (v)) -> gtP (u, v) maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l)) maxP (cons (u, l)) -> gtP (u, max (l)) maxP (cons (u, l)) -> maxP (l) maxP (cons (u, l)) -> maxP (l) sort (l) ->= st (0, l) st (n, l) ->= cond1 (member (n, l), n, l) cond1 (true, n, l) ->= cons (n, st (s (n), l)) cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) ->= nil cond2 (false, n, l) ->= st (s (n), l) member (n, nil) ->= false member (n, cons (m, l)) ->= or (equal (n, m), member (n, l)) or (x, true) ->= true or (x, false) ->= x equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y) gt (0, v) ->= false gt (s (u), 0) ->= true gt (s (u), s (v)) ->= gt (u, v) max (nil) ->= 0 max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l)) if (true, u, v) ->= u if (false, u, v) ->= v) , property = Top_Termination , truth = Nothing , transform = Remove { interpretation = Interpretation ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) orP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) sort |-> (x) |-> E^0x0 * x + E^0x1 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 sortP |-> (x) |-> E^1x0 * x + (2) cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) true |-> () |-> E^0x1 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 nil |-> () |-> E^0x1 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 maxP |-> (x) |-> E^1x0 * x + (2) member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 max |-> (x) |-> E^0x0 * x + E^0x1 , removes_rules = [ memberP (n, cons (m, l)) -> orP (equal (n, m), member (n, l)) ] , comment = size 0 , heights ( 3 , 7 ) , time } , to = [ Proof { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES sortP (l) -> stP (0, l) stP (n, l) -> cond1P (member (n, l), n, l) stP (n, l) -> memberP (n, l) cond1P (true, n, l) -> stP (s (n), l) cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) cond1P (false, n, l) -> gtP (n, max (l)) cond1P (false, n, l) -> maxP (l) cond2P (false, n, l) -> stP (s (n), l) memberP (n, cons (m, l)) -> equalP (n, m) memberP (n, cons (m, l)) -> memberP (n, l) equalP (s (x), s (y)) -> equalP (x, y) gtP (s (u), s (v)) -> gtP (u, v) maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l)) maxP (cons (u, l)) -> gtP (u, max (l)) maxP (cons (u, l)) -> maxP (l) maxP (cons (u, l)) -> maxP (l) sort (l) ->= st (0, l) st (n, l) ->= cond1 (member (n, l), n, l) cond1 (true, n, l) ->= cons (n, st (s (n), l)) cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) ->= nil cond2 (false, n, l) ->= st (s (n), l) member (n, nil) ->= false member (n, cons (m, l)) ->= or (equal (n, m), member (n, l)) or (x, true) ->= true or (x, false) ->= x equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y) gt (0, v) ->= false gt (s (u), 0) ->= true gt (s (u), s (v)) ->= gt (u, v) max (nil) ->= 0 max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l)) if (true, u, v) ->= u if (false, u, v) ->= v) , property = Top_Termination , truth = Nothing , transform = Remove { interpretation = Interpretation ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) sort |-> (x) |-> E^0x0 * x + E^0x1 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 sortP |-> (x) |-> E^1x0 * x + (2) cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) true |-> () |-> E^0x1 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 nil |-> () |-> E^0x1 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 maxP |-> (x) |-> E^1x0 * x + (0) member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 max |-> (x) |-> E^0x0 * x + E^0x1 , removes_rules = [ sortP (l) -> stP (0, l) ] , comment = size 0 , heights ( 3 , 7 ) , time } , to = [ Proof { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES stP (n, l) -> cond1P (member (n, l), n, l) stP (n, l) -> memberP (n, l) cond1P (true, n, l) -> stP (s (n), l) cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) cond1P (false, n, l) -> gtP (n, max (l)) cond1P (false, n, l) -> maxP (l) cond2P (false, n, l) -> stP (s (n), l) memberP (n, cons (m, l)) -> equalP (n, m) memberP (n, cons (m, l)) -> memberP (n, l) equalP (s (x), s (y)) -> equalP (x, y) gtP (s (u), s (v)) -> gtP (u, v) maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l)) maxP (cons (u, l)) -> gtP (u, max (l)) maxP (cons (u, l)) -> maxP (l) maxP (cons (u, l)) -> maxP (l) sort (l) ->= st (0, l) st (n, l) ->= cond1 (member (n, l), n, l) cond1 (true, n, l) ->= cons (n, st (s (n), l)) cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) ->= nil cond2 (false, n, l) ->= st (s (n), l) member (n, nil) ->= false member (n, cons (m, l)) ->= or (equal (n, m), member (n, l)) or (x, true) ->= true or (x, false) ->= x equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y) gt (0, v) ->= false gt (s (u), 0) ->= true gt (s (u), s (v)) ->= gt (u, v) max (nil) ->= 0 max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l)) if (true, u, v) ->= u if (false, u, v) ->= v) , property = Top_Termination , truth = Nothing , transform = Remove { interpretation = Interpretation ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) sort |-> (x) |-> E^0x0 * x + E^0x1 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) true |-> () |-> E^0x1 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 nil |-> () |-> E^0x1 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 maxP |-> (x) |-> E^1x0 * x + (2) member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 max |-> (x) |-> E^0x0 * x + E^0x1 , removes_rules = [ memberP (n, cons (m, l)) -> equalP (n, m) , maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l)) ] , comment = size 0 , heights ( 3 , 7 ) , time } , to = [ Proof { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES stP (n, l) -> cond1P (member (n, l), n, l) stP (n, l) -> memberP (n, l) cond1P (true, n, l) -> stP (s (n), l) cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) cond1P (false, n, l) -> gtP (n, max (l)) cond1P (false, n, l) -> maxP (l) cond2P (false, n, l) -> stP (s (n), l) memberP (n, cons (m, l)) -> memberP (n, l) equalP (s (x), s (y)) -> equalP (x, y) gtP (s (u), s (v)) -> gtP (u, v) maxP (cons (u, l)) -> gtP (u, max (l)) maxP (cons (u, l)) -> maxP (l) maxP (cons (u, l)) -> maxP (l) sort (l) ->= st (0, l) st (n, l) ->= cond1 (member (n, l), n, l) cond1 (true, n, l) ->= cons (n, st (s (n), l)) cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) ->= nil cond2 (false, n, l) ->= st (s (n), l) member (n, nil) ->= false member (n, cons (m, l)) ->= or (equal (n, m), member (n, l)) or (x, true) ->= true or (x, false) ->= x equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y) gt (0, v) ->= false gt (s (u), 0) ->= true gt (s (u), s (v)) ->= gt (u, v) max (nil) ->= 0 max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l)) if (true, u, v) ->= u if (false, u, v) ->= v) , property = Top_Termination , truth = Nothing , transform = Split { interpretation = Interpretation ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) sort |-> (x) |-> E^0x0 * x + E^0x1 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) true |-> () |-> E^0x1 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 nil |-> () |-> E^0x1 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 maxP |-> (x) |-> E^1x0 * x + (2) member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 max |-> (x) |-> E^0x0 * x + E^0x1 , clusters = [ [ equalP (s (x), s (y)) -> equalP (x, y) ] , [ stP (n, l) -> cond1P (member (n, l), n, l) , stP (n, l) -> memberP (n, l) , cond1P (true, n, l) -> stP (s (n), l) , cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) , cond1P (false, n, l) -> gtP (n, max (l)) , cond1P (false, n, l) -> maxP (l) , cond2P (false, n, l) -> stP (s (n), l) , memberP (n, cons (m, l)) -> memberP (n, l) , gtP (s (u), s (v)) -> gtP (u, v) , maxP (cons (u, l)) -> gtP (u, max (l)) , maxP (cons (u, l)) -> maxP (l) , maxP (cons (u, l)) -> maxP (l) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } , to = [ Claim { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES equalP (s (x), s (y)) -> equalP (x, y) sort (l) ->= st (0, l) st (n, l) ->= cond1 (member (n, l), n, l) cond1 (true, n, l) ->= cons (n, st (s (n), l)) cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) ->= nil cond2 (false, n, l) ->= st (s (n), l) member (n, nil) ->= false member (n, cons (m, l)) ->= or (equal (n, m), member (n, l)) or (x, true) ->= true or (x, false) ->= x equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y) gt (0, v) ->= false gt (s (u), 0) ->= true gt (s (u), s (v)) ->= gt (u, v) max (nil) ->= 0 max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l)) if (true, u, v) ->= u if (false, u, v) ->= v) , property = Top_Termination } , Claim { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES stP (n, l) -> cond1P (member (n, l), n, l) stP (n, l) -> memberP (n, l) cond1P (true, n, l) -> stP (s (n), l) cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) cond1P (false, n, l) -> gtP (n, max (l)) cond1P (false, n, l) -> maxP (l) cond2P (false, n, l) -> stP (s (n), l) memberP (n, cons (m, l)) -> memberP (n, l) gtP (s (u), s (v)) -> gtP (u, v) maxP (cons (u, l)) -> gtP (u, max (l)) maxP (cons (u, l)) -> maxP (l) maxP (cons (u, l)) -> maxP (l) sort (l) ->= st (0, l) st (n, l) ->= cond1 (member (n, l), n, l) cond1 (true, n, l) ->= cons (n, st (s (n), l)) cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) ->= nil cond2 (false, n, l) ->= st (s (n), l) member (n, nil) ->= false member (n, cons (m, l)) ->= or (equal (n, m), member (n, l)) or (x, true) ->= true or (x, false) ->= x equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y) gt (0, v) ->= false gt (s (u), 0) ->= true gt (s (u), s (v)) ->= gt (u, v) max (nil) ->= 0 max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l)) if (true, u, v) ->= u if (false, u, v) ->= v) , property = Top_Termination } ] } ] } ] } ] } ] } ] } Proof summary: value Nothing for property Termination for system with 21 strict rules and 0 non-strict rules follows by transformation Ignore_Strategy from value Nothing for property Termination for system with 21 strict rules and 0 non-strict rules follows by transformation Dependency_Pair_Transformation from value Nothing for property Top_Termination for system with 17 strict rules and 21 non-strict rules follows by transformation Remove { interpretation = Interpretation ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) orP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) sort |-> (x) |-> E^0x0 * x + E^0x1 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 sortP |-> (x) |-> E^1x0 * x + (2) cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) true |-> () |-> E^0x1 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 nil |-> () |-> E^0x1 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 maxP |-> (x) |-> E^1x0 * x + (2) member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 max |-> (x) |-> E^0x0 * x + E^0x1 , removes_rules = [ memberP (n, cons (m, l)) -> orP (equal (n, m), member (n, l)) ] , comment = size 0 , heights ( 3 , 7 ) , time } from value Nothing for property Top_Termination for system with 16 strict rules and 21 non-strict rules follows by transformation Remove { interpretation = Interpretation ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) sort |-> (x) |-> E^0x0 * x + E^0x1 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 sortP |-> (x) |-> E^1x0 * x + (2) cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) true |-> () |-> E^0x1 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 nil |-> () |-> E^0x1 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 maxP |-> (x) |-> E^1x0 * x + (0) member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 max |-> (x) |-> E^0x0 * x + E^0x1 , removes_rules = [ sortP (l) -> stP (0, l) ] , comment = size 0 , heights ( 3 , 7 ) , time } from value Nothing for property Top_Termination for system with 15 strict rules and 21 non-strict rules follows by transformation Remove { interpretation = Interpretation ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) sort |-> (x) |-> E^0x0 * x + E^0x1 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) true |-> () |-> E^0x1 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 nil |-> () |-> E^0x1 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 maxP |-> (x) |-> E^1x0 * x + (2) member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 max |-> (x) |-> E^0x0 * x + E^0x1 , removes_rules = [ memberP (n, cons (m, l)) -> equalP (n, m) , maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l)) ] , comment = size 0 , heights ( 3 , 7 ) , time } from value Nothing for property Top_Termination for system with 13 strict rules and 21 non-strict rules follows by transformation Split { interpretation = Interpretation ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0) gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) sort |-> (x) |-> E^0x0 * x + E^0x1 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) true |-> () |-> E^0x1 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2) equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 nil |-> () |-> E^0x1 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 maxP |-> (x) |-> E^1x0 * x + (2) member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2) cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1 max |-> (x) |-> E^0x0 * x + E^0x1 , clusters = [ [ equalP (s (x), s (y)) -> equalP (x, y) ] , [ stP (n, l) -> cond1P (member (n, l), n, l) , stP (n, l) -> memberP (n, l) , cond1P (true, n, l) -> stP (s (n), l) , cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) , cond1P (false, n, l) -> gtP (n, max (l)) , cond1P (false, n, l) -> maxP (l) , cond2P (false, n, l) -> stP (s (n), l) , memberP (n, cons (m, l)) -> memberP (n, l) , gtP (s (u), s (v)) -> gtP (u, v) , maxP (cons (u, l)) -> gtP (u, max (l)) , maxP (cons (u, l)) -> maxP (l) , maxP (cons (u, l)) -> maxP (l) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } from Claim { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES equalP (s (x), s (y)) -> equalP (x, y) sort (l) ->= st (0, l) st (n, l) ->= cond1 (member (n, l), n, l) cond1 (true, n, l) ->= cons (n, st (s (n), l)) cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) ->= nil cond2 (false, n, l) ->= st (s (n), l) member (n, nil) ->= false member (n, cons (m, l)) ->= or (equal (n, m), member (n, l)) or (x, true) ->= true or (x, false) ->= x equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y) gt (0, v) ->= false gt (s (u), 0) ->= true gt (s (u), s (v)) ->= gt (u, v) max (nil) ->= 0 max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l)) if (true, u, v) ->= u if (false, u, v) ->= v) , property = Top_Termination } Claim { system = (VAR l n m x y v u) (STRATEGY INNERMOST) (RULES stP (n, l) -> cond1P (member (n, l), n, l) stP (n, l) -> memberP (n, l) cond1P (true, n, l) -> stP (s (n), l) cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) cond1P (false, n, l) -> gtP (n, max (l)) cond1P (false, n, l) -> maxP (l) cond2P (false, n, l) -> stP (s (n), l) memberP (n, cons (m, l)) -> memberP (n, l) gtP (s (u), s (v)) -> gtP (u, v) maxP (cons (u, l)) -> gtP (u, max (l)) maxP (cons (u, l)) -> maxP (l) maxP (cons (u, l)) -> maxP (l) sort (l) ->= st (0, l) st (n, l) ->= cond1 (member (n, l), n, l) cond1 (true, n, l) ->= cons (n, st (s (n), l)) cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l) cond2 (true, n, l) ->= nil cond2 (false, n, l) ->= st (s (n), l) member (n, nil) ->= false member (n, cons (m, l)) ->= or (equal (n, m), member (n, l)) or (x, true) ->= true or (x, false) ->= x equal (0, 0) ->= true equal (s (x), 0) ->= false equal (0, s (y)) ->= false equal (s (x), s (y)) ->= equal (x, y) gt (0, v) ->= false gt (s (u), 0) ->= true gt (s (u), s (v)) ->= gt (u, v) max (nil) ->= 0 max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l)) if (true, u, v) ->= u if (false, u, v) ->= 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/tmpOwPakZ/ex15.trs started : Thu Feb 22 16:50:44 CET 2007 finished : Thu Feb 22 16:51:36 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: 52 secs