************************************* Proof { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES log (x, s (s (y))) -> cond (le (x, s (s (y))), x, y) cond (true, x, y) -> s (0) cond (false, x, y) -> double (log (x, square (s (s (y))))) le (0, v) -> true le (s (u), 0) -> false le (s (u), s (v)) -> le (u, v) double (0) -> 0 double (s (x)) -> s (s (double (x))) square (0) -> 0 square (s (x)) -> s (plus (square (x), double (x))) plus (n, 0) -> n plus (n, s (m)) -> s (plus (n, m))) , property = Termination , truth = Nothing , transform = Ignore_Strategy , to = [ Proof { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES log (x, s (s (y))) -> cond (le (x, s (s (y))), x, y) cond (true, x, y) -> s (0) cond (false, x, y) -> double (log (x, square (s (s (y))))) le (0, v) -> true le (s (u), 0) -> false le (s (u), s (v)) -> le (u, v) double (0) -> 0 double (s (x)) -> s (s (double (x))) square (0) -> 0 square (s (x)) -> s (plus (square (x), double (x))) plus (n, 0) -> n plus (n, s (m)) -> s (plus (n, m))) , property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation , to = [ Proof { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES logP (x, s (s (y))) -> condP (le (x, s (s (y))), x, y) logP (x, s (s (y))) -> leP (x, s (s (y))) condP (false, x, y) -> doubleP (log (x, square (s (s (y))))) condP (false, x, y) -> logP (x, square (s (s (y)))) condP (false, x, y) -> squareP (s (s (y))) leP (s (u), s (v)) -> leP (u, v) doubleP (s (x)) -> doubleP (x) squareP (s (x)) -> plusP (square (x), double (x)) squareP (s (x)) -> squareP (x) squareP (s (x)) -> doubleP (x) plusP (n, s (m)) -> plusP (n, m) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination , truth = Nothing , transform = Remove { interpretation = Interpretation squareP |-> (x) |-> E^1x0 * x + (0) leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) 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 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 logP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ logP (x, s (s (y))) -> leP (x, s (s (y))) , condP (false, x, y) -> doubleP (log (x, square (s (s (y))))) , condP (false, x, y) -> squareP (s (s (y))) ] , comment = size 0 , heights ( 3 , 7 ) , time } , to = [ Proof { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES logP (x, s (s (y))) -> condP (le (x, s (s (y))), x, y) condP (false, x, y) -> logP (x, square (s (s (y)))) leP (s (u), s (v)) -> leP (u, v) doubleP (s (x)) -> doubleP (x) squareP (s (x)) -> plusP (square (x), double (x)) squareP (s (x)) -> squareP (x) squareP (s (x)) -> doubleP (x) plusP (n, s (m)) -> plusP (n, m) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination , truth = Nothing , transform = Split { interpretation = Interpretation squareP |-> (x) |-> E^1x0 * x + (0) leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) 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 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 logP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ [ leP (s (u), s (v)) -> leP (u, v) , doubleP (s (x)) -> doubleP (x) , squareP (s (x)) -> plusP (square (x), double (x)) , squareP (s (x)) -> squareP (x) , squareP (s (x)) -> doubleP (x) , plusP (n, s (m)) -> plusP (n, m) ] , [ logP (x, s (s (y))) -> condP (le (x, s (s (y))), x, y) , condP (false, x, y) -> logP (x, square (s (s (y)))) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } , to = [ Proof { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES leP (s (u), s (v)) -> leP (u, v) doubleP (s (x)) -> doubleP (x) squareP (s (x)) -> plusP (square (x), double (x)) squareP (s (x)) -> squareP (x) squareP (s (x)) -> doubleP (x) plusP (n, s (m)) -> plusP (n, m) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination , truth = Nothing , transform = Remove { interpretation = Interpretation squareP |-> (x) |-> E^1x0 * x + (2) leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ squareP (s (x)) -> plusP (square (x), double (x)) , squareP (s (x)) -> doubleP (x) ] , comment = size 0 , heights ( 3 , 7 ) , time } , to = [ Proof { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES leP (s (u), s (v)) -> leP (u, v) doubleP (s (x)) -> doubleP (x) squareP (s (x)) -> squareP (x) plusP (n, s (m)) -> plusP (n, m) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination , truth = Nothing , transform = Split { interpretation = Interpretation squareP |-> (x) |-> E^1x0 * x + (2) leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ [ leP (s (u), s (v)) -> leP (u, v) , doubleP (s (x)) -> doubleP (x) ] , [ plusP (n, s (m)) -> plusP (n, m) ] , [ squareP (s (x)) -> squareP (x) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } , to = [ Proof { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES leP (s (u), s (v)) -> leP (u, v) doubleP (s (x)) -> doubleP (x) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination , truth = Nothing , transform = Split { interpretation = Interpretation leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (2) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ [ leP (s (u), s (v)) -> leP (u, v) ] , [ doubleP (s (x)) -> doubleP (x) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } , to = [ Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES leP (s (u), s (v)) -> leP (u, v) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } , Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES doubleP (s (x)) -> doubleP (x) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } ] } , Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES plusP (n, s (m)) -> plusP (n, m) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } , Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES squareP (s (x)) -> squareP (x) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } ] } ] } , Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES logP (x, s (s (y))) -> condP (le (x, s (s (y))), x, y) condP (false, x, y) -> logP (x, square (s (s (y)))) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } ] } ] } ] } ] } Proof summary: value Nothing for property Termination for system with 12 strict rules and 0 non-strict rules follows by transformation Ignore_Strategy from value Nothing for property Termination for system with 12 strict rules and 0 non-strict rules follows by transformation Dependency_Pair_Transformation from value Nothing for property Top_Termination for system with 11 strict rules and 12 non-strict rules follows by transformation Remove { interpretation = Interpretation squareP |-> (x) |-> E^1x0 * x + (0) leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) 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 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 logP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ logP (x, s (s (y))) -> leP (x, s (s (y))) , condP (false, x, y) -> doubleP (log (x, square (s (s (y))))) , condP (false, x, y) -> squareP (s (s (y))) ] , comment = size 0 , heights ( 3 , 7 ) , time } from value Nothing for property Top_Termination for system with 8 strict rules and 12 non-strict rules follows by transformation Split { interpretation = Interpretation squareP |-> (x) |-> E^1x0 * x + (0) leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) 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 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 logP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ [ leP (s (u), s (v)) -> leP (u, v) , doubleP (s (x)) -> doubleP (x) , squareP (s (x)) -> plusP (square (x), double (x)) , squareP (s (x)) -> squareP (x) , squareP (s (x)) -> doubleP (x) , plusP (n, s (m)) -> plusP (n, m) ] , [ logP (x, s (s (y))) -> condP (le (x, s (s (y))), x, y) , condP (false, x, y) -> logP (x, square (s (s (y)))) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } from value Nothing for property Top_Termination for system with 6 strict rules and 12 non-strict rules follows by transformation Remove { interpretation = Interpretation squareP |-> (x) |-> E^1x0 * x + (2) leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ squareP (s (x)) -> plusP (square (x), double (x)) , squareP (s (x)) -> doubleP (x) ] , comment = size 0 , heights ( 3 , 7 ) , time } from value Nothing for property Top_Termination for system with 4 strict rules and 12 non-strict rules follows by transformation Split { interpretation = Interpretation squareP |-> (x) |-> E^1x0 * x + (2) leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (0) plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ [ leP (s (u), s (v)) -> leP (u, v) , doubleP (s (x)) -> doubleP (x) ] , [ plusP (n, s (m)) -> plusP (n, m) ] , [ squareP (s (x)) -> squareP (x) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } from value Nothing for property Top_Termination for system with 2 strict rules and 12 non-strict rules follows by transformation Split { interpretation = Interpretation leP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0) doubleP |-> (x) |-> E^1x0 * x + (2) 0 |-> () |-> E^0x1 s |-> (x) |-> E^0x0 * x + E^0x1 false |-> () |-> E^0x1 square |-> (x) |-> E^0x0 * x + E^0x1 le |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 double |-> (x) |-> E^0x0 * x + E^0x1 true |-> () |-> E^0x1 log |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1 plus |-> (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 = [ [ leP (s (u), s (v)) -> leP (u, v) ] , [ doubleP (s (x)) -> doubleP (x) ] ] , comment = size 0 , heights ( 3 , 7 ) , time split_dimension: 0 } from Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES leP (s (u), s (v)) -> leP (u, v) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES doubleP (s (x)) -> doubleP (x) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES plusP (n, s (m)) -> plusP (n, m) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES squareP (s (x)) -> squareP (x) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , property = Top_Termination } Claim { system = (VAR l x y v u n m) (STRATEGY INNERMOST) (RULES logP (x, s (s (y))) -> condP (le (x, s (s (y))), x, y) condP (false, x, y) -> logP (x, square (s (s (y)))) log (x, s (s (y))) ->= cond (le (x, s (s (y))), x, y) cond (true, x, y) ->= s (0) cond (false, x, y) ->= double (log (x, square (s (s (y))))) le (0, v) ->= true le (s (u), 0) ->= false le (s (u), s (v)) ->= le (u, v) double (0) ->= 0 double (s (x)) ->= s (s (double (x))) square (0) ->= 0 square (s (x)) ->= s (plus (square (x), double (x))) plus (n, 0) ->= n plus (n, s (m)) ->= s (plus (n, m))) , 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/tmpqXca0t/ex18.trs started : Thu Feb 22 16:52:32 CET 2007 finished : Thu Feb 22 16:53:23 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