*************************************
Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES f (true, x, y) -> f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) -> false
gt (s (u), 0) -> true
gt (s (u), s (v)) -> gt (u, v)
and (x, true) -> x
and (x, false) -> false
plus (n, 0) -> n
plus (n, s (m)) -> s (plus (n, m))
plus (plus (n, m), u) -> plus (n, plus (m, u))
double (0) -> 0
double (s (x)) -> s (s (double (x))))
, property = Termination , truth = Nothing , transform = Ignore_Strategy
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES f (true, x, y) -> f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) -> false
gt (s (u), 0) -> true
gt (s (u), s (v)) -> gt (u, v)
and (x, true) -> x
and (x, false) -> false
plus (n, 0) -> n
plus (n, s (m)) -> s (plus (n, m))
plus (plus (n, m), u) -> plus (n, plus (m, u))
double (0) -> 0
double (s (x)) -> s (s (double (x))))
, property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
fP (true, x, y) -> andP (gt (x, y), gt (y, s (s (0))))
fP (true, x, y) -> gtP (x, y)
fP (true, x, y) -> gtP (y, s (s (0)))
fP (true, x, y) -> plusP (s (0), x)
fP (true, x, y) -> doubleP (y)
gtP (s (u), s (v)) -> gtP (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)
doubleP (s (x)) -> doubleP (x)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination , truth = Nothing
, transform = Remove
{ interpretation = Interpretation
gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
andP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, removes_rules = [ fP (true, x, y) -> gtP (x, y) , fP (true, x, y) -> gtP (y, s (s (0))) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
fP (true, x, y) -> andP (gt (x, y), gt (y, s (s (0))))
fP (true, x, y) -> plusP (s (0), x)
fP (true, x, y) -> doubleP (y)
gtP (s (u), s (v)) -> gtP (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)
doubleP (s (x)) -> doubleP (x)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination , truth = Nothing
, transform = Split
{ interpretation = Interpretation
gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
andP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, clusters = [ [ gtP (s (u), s (v)) -> gtP (u, v) ] , [ fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y)) , fP (true, x, y) -> andP (gt (x, y), gt (y, s (s (0)))) , fP (true, x, y) -> plusP (s (0), x) , fP (true, x, y) -> doubleP (y) , 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) , doubleP (s (x)) -> doubleP (x) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time
split_dimension: 0
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES gtP (s (u), s (v)) -> gtP (u, v)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination
, truth = Just
True
, transform = Remove
{ interpretation = Interpretation
gtP |-> (x , y) |-> (0) * x + (1) * y + (0)
0 |-> () |-> (3)
f |-> (x , y , z) |-> (0) * x + (0) * y + (0) * z + (0)
s |-> (x) |-> (1) * x + (1)
false |-> () |-> (0)
gt |-> (x , y) |-> (0) * x + (0) * y + (0)
double |-> (x) |-> (4) * x + (0)
true |-> () |-> (0)
and |-> (x , y) |-> (2) * x + (0) * y + (0)
plus |-> (x , y) |-> (2) * x + (1) * y + (0)
, removes_rules = [ gtP (s (u), s (v)) -> gtP (u, v) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination
, truth = Just
True
, transform = No_Strict_Rules , to = [ ]
}
]
}
, Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
fP (true, x, y) -> andP (gt (x, y), gt (y, s (s (0))))
fP (true, x, y) -> plusP (s (0), x)
fP (true, x, y) -> doubleP (y)
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)
doubleP (s (x)) -> doubleP (x)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination , truth = Nothing
, transform = Remove
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
andP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, removes_rules = [ fP (true, x, y) -> andP (gt (x, y), gt (y, s (s (0)))) ] , comment = size 0 , heights ( 3 , 7 ) , time 1 sec
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
fP (true, x, y) -> plusP (s (0), x)
fP (true, x, y) -> doubleP (y)
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)
doubleP (s (x)) -> doubleP (x)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination , truth = Nothing
, transform = Remove
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, removes_rules = [ fP (true, x, y) -> plusP (s (0), x) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
fP (true, x, y) -> doubleP (y)
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)
doubleP (s (x)) -> doubleP (x)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination , truth = Nothing
, transform = Split
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, clusters = [ [ 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) ] , [ fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y)) , fP (true, x, y) -> doubleP (y) , doubleP (s (x)) -> doubleP (x) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time
split_dimension: 0
}
, to = [ Proof
{ system = (VAR x y
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)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination
, truth = Just
True
, transform = Remove
{ interpretation = Interpretation
plusP |-> (x , y) |-> (1) * x + (0) * y + (0)
0 |-> () |-> (0)
f |-> (x , y , z) |-> (0) * x + (0) * y + (0) * z + (0)
s |-> (x) |-> (0) * x + (0)
false |-> () |-> (0)
gt |-> (x , y) |-> (0) * x + (0) * y + (0)
double |-> (x) |-> (0) * x + (0)
true |-> () |-> (0)
and |-> (x , y) |-> (4) * x + (0) * y + (0)
plus |-> (x , y) |-> (2) * x + (1) * y + (1)
, removes_rules = [ plusP (plus (n, m), u) -> plusP (n, plus (m, u)) , plusP (plus (n, m), u) -> plusP (m, u) ] , comment = size 1 , heights ( 7 , 15 ) , time 2 secs
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES plusP (n, s (m)) -> plusP (n, m)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination
, truth = Just
True
, transform = Remove
{ interpretation = Interpretation
plusP |-> (x , y) |-> (1) * x + (2) * y + (0)
0 |-> () |-> (0)
f |-> (x , y , z) |-> (0) * x + (0) * y + (0) * z + (0)
s |-> (x) |-> (1) * x + (1)
false |-> () |-> (0)
gt |-> (x , y) |-> (0) * x + (0) * y + (0)
double |-> (x) |-> (4) * x + (7)
true |-> () |-> (0)
and |-> (x , y) |-> (4) * x + (0) * y + (1)
plus |-> (x , y) |-> (1) * x + (1) * y + (0)
, removes_rules = [ plusP (n, s (m)) -> plusP (n, m) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination
, truth = Just
True
, transform = No_Strict_Rules , to = [ ]
}
]
}
]
}
, Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
fP (true, x, y) -> doubleP (y)
doubleP (s (x)) -> doubleP (x)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination , truth = Nothing
, transform = Remove
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (0)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, removes_rules = [ fP (true, x, y) -> doubleP (y) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
doubleP (s (x)) -> doubleP (x)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination , truth = Nothing
, transform = Split
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (0)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, clusters = [ [ doubleP (s (x)) -> doubleP (x) ] , [ fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y)) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time
split_dimension: 0
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES doubleP (s (x)) -> doubleP (x)
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination
, truth = Just
True
, transform = Remove
{ interpretation = Interpretation
doubleP |-> (x) |-> (1) * x + (0)
0 |-> () |-> (1)
f |-> (x , y , z) |-> (0) * x + (0) * y + (0) * z + (0)
s |-> (x) |-> (1) * x + (1)
false |-> () |-> (0)
gt |-> (x , y) |-> (0) * x + (0) * y + (0)
double |-> (x) |-> (2) * x + (7)
true |-> () |-> (0)
and |-> (x , y) |-> (4) * x + (0) * y + (0)
plus |-> (x , y) |-> (2) * x + (1) * y + (0)
, removes_rules = [ doubleP (s (x)) -> doubleP (x) ] , comment = size 1 , heights ( 7 , 15 ) , time 2 secs
}
, to = [ Proof
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination
, truth = Just
True
, transform = No_Strict_Rules , to = [ ]
}
]
}
, Claim
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, property = Top_Termination
}
]
}
]
}
]
}
]
}
]
}
]
}
]
}
]
}
]
}
Proof summary:
value Nothing
for property Termination
for system with 11 strict rules and 0 non-strict rules
follows by transformation
Ignore_Strategy
from
value Nothing
for property Termination
for system with 11 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 11 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
andP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, removes_rules = [ fP (true, x, y) -> gtP (x, y) , fP (true, x, y) -> gtP (y, s (s (0))) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
from
value Nothing
for property Top_Termination
for system with 9 strict rules and 11 non-strict rules
follows by transformation
Split
{ interpretation = Interpretation
gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
andP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, clusters = [ [ gtP (s (u), s (v)) -> gtP (u, v) ] , [ fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y)) , fP (true, x, y) -> andP (gt (x, y), gt (y, s (s (0)))) , fP (true, x, y) -> plusP (s (0), x) , fP (true, x, y) -> doubleP (y) , 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) , doubleP (s (x)) -> doubleP (x) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time
split_dimension: 0
}
from
value Just
True
for property Top_Termination
for system with 1 strict rules and 11 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
gtP |-> (x , y) |-> (0) * x + (1) * y + (0)
0 |-> () |-> (3)
f |-> (x , y , z) |-> (0) * x + (0) * y + (0) * z + (0)
s |-> (x) |-> (1) * x + (1)
false |-> () |-> (0)
gt |-> (x , y) |-> (0) * x + (0) * y + (0)
double |-> (x) |-> (4) * x + (0)
true |-> () |-> (0)
and |-> (x , y) |-> (2) * x + (0) * y + (0)
plus |-> (x , y) |-> (2) * x + (1) * y + (0)
, removes_rules = [ gtP (s (u), s (v)) -> gtP (u, v) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
}
from
value Just
True
for property Top_Termination
for system with 0 strict rules and 11 non-strict rules
follows by transformation
No_Strict_Rules
from
value Nothing
for property Top_Termination
for system with 8 strict rules and 11 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
andP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, removes_rules = [ fP (true, x, y) -> andP (gt (x, y), gt (y, s (s (0)))) ] , comment = size 0 , heights ( 3 , 7 ) , time 1 sec
}
from
value Nothing
for property Top_Termination
for system with 7 strict rules and 11 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, removes_rules = [ fP (true, x, y) -> plusP (s (0), x) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
from
value Nothing
for property Top_Termination
for system with 6 strict rules and 11 non-strict rules
follows by transformation
Split
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (2)
plusP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, clusters = [ [ 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) ] , [ fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y)) , fP (true, x, y) -> doubleP (y) , doubleP (s (x)) -> doubleP (x) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time
split_dimension: 0
}
from
value Just
True
for property Top_Termination
for system with 3 strict rules and 11 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
plusP |-> (x , y) |-> (1) * x + (0) * y + (0)
0 |-> () |-> (0)
f |-> (x , y , z) |-> (0) * x + (0) * y + (0) * z + (0)
s |-> (x) |-> (0) * x + (0)
false |-> () |-> (0)
gt |-> (x , y) |-> (0) * x + (0) * y + (0)
double |-> (x) |-> (0) * x + (0)
true |-> () |-> (0)
and |-> (x , y) |-> (4) * x + (0) * y + (0)
plus |-> (x , y) |-> (2) * x + (1) * y + (1)
, removes_rules = [ plusP (plus (n, m), u) -> plusP (n, plus (m, u)) , plusP (plus (n, m), u) -> plusP (m, u) ] , comment = size 1 , heights ( 7 , 15 ) , time 2 secs
}
from
value Just
True
for property Top_Termination
for system with 1 strict rules and 11 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
plusP |-> (x , y) |-> (1) * x + (2) * y + (0)
0 |-> () |-> (0)
f |-> (x , y , z) |-> (0) * x + (0) * y + (0) * z + (0)
s |-> (x) |-> (1) * x + (1)
false |-> () |-> (0)
gt |-> (x , y) |-> (0) * x + (0) * y + (0)
double |-> (x) |-> (4) * x + (7)
true |-> () |-> (0)
and |-> (x , y) |-> (4) * x + (0) * y + (1)
plus |-> (x , y) |-> (1) * x + (1) * y + (0)
, removes_rules = [ plusP (n, s (m)) -> plusP (n, m) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
}
from
value Just
True
for property Top_Termination
for system with 0 strict rules and 11 non-strict rules
follows by transformation
No_Strict_Rules
from
value Nothing
for property Top_Termination
for system with 3 strict rules and 11 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (0)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, removes_rules = [ fP (true, x, y) -> doubleP (y) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
from
value Nothing
for property Top_Termination
for system with 2 strict rules and 11 non-strict rules
follows by transformation
Split
{ interpretation = Interpretation
doubleP |-> (x) |-> E^1x0 * x + (0)
0 |-> () |-> E^0x1
f |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
false |-> () |-> E^0x1
fP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
double |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
and |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
plus |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
, clusters = [ [ doubleP (s (x)) -> doubleP (x) ] , [ fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y)) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time
split_dimension: 0
}
from
value Just
True
for property Top_Termination
for system with 1 strict rules and 11 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
doubleP |-> (x) |-> (1) * x + (0)
0 |-> () |-> (1)
f |-> (x , y , z) |-> (0) * x + (0) * y + (0) * z + (0)
s |-> (x) |-> (1) * x + (1)
false |-> () |-> (0)
gt |-> (x , y) |-> (0) * x + (0) * y + (0)
double |-> (x) |-> (2) * x + (7)
true |-> () |-> (0)
and |-> (x , y) |-> (4) * x + (0) * y + (0)
plus |-> (x , y) |-> (2) * x + (1) * y + (0)
, removes_rules = [ doubleP (s (x)) -> doubleP (x) ] , comment = size 1 , heights ( 7 , 15 ) , time 2 secs
}
from
value Just
True
for property Top_Termination
for system with 0 strict rules and 11 non-strict rules
follows by transformation
No_Strict_Rules
from
Claim
{ system = (VAR x y
u v
n m)
(STRATEGY INNERMOST)
(RULES fP (true, x, y) -> fP (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
f (true, x, y) ->= f (and (gt (x, y), gt (y, s (s (0)))), plus (s (0), x), double (y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
and (x, true) ->= x
and (x, false) ->= false
plus (n, 0) ->= n
plus (n, s (m)) ->= s (plus (n, m))
plus (plus (n, m), u) ->= plus (n, plus (m, u))
double (0) ->= 0
double (s (x)) ->= s (s (double (x))))
, 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/tmprhkXa-/ex12.trs
started : Thu Feb 22 16:42:52 CET 2007
finished : Thu Feb 22 16:43:50 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