*************************************
Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtail (n, l) -> cond (ge (n, length (l)), n, l)
cond (true, n, l) -> l
cond (false, n, l) -> tail (nthtail (s (n), l))
tail (nil) -> nil
tail (cons (x, l)) -> l
length (nil) -> 0
length (cons (x, l)) -> s (length (l))
ge (u, 0) -> true
ge (0, s (v)) -> false
ge (s (u), s (v)) -> ge (u, v))
, property = Termination , truth = Nothing , transform = Ignore_Strategy
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtail (n, l) -> cond (ge (n, length (l)), n, l)
cond (true, n, l) -> l
cond (false, n, l) -> tail (nthtail (s (n), l))
tail (nil) -> nil
tail (cons (x, l)) -> l
length (nil) -> 0
length (cons (x, l)) -> s (length (l))
ge (u, 0) -> true
ge (0, s (v)) -> false
ge (s (u), s (v)) -> ge (u, v))
, property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtailP (n, l) -> condP (ge (n, length (l)), n, l)
nthtailP (n, l) -> geP (n, length (l))
nthtailP (n, l) -> lengthP (l)
condP (false, n, l) -> tailP (nthtail (s (n), l))
condP (false, n, l) -> nthtailP (s (n), l)
lengthP (cons (x, l)) -> lengthP (l)
geP (s (u), s (v)) -> geP (u, v)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination , truth = Nothing
, transform = Remove
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
lengthP |-> (x) |-> E^1x0 * x + (1)
tailP |-> (x) |-> E^1x0 * x + (2)
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, removes_rules = [ nthtailP (n, l) -> lengthP (l) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtailP (n, l) -> condP (ge (n, length (l)), n, l)
nthtailP (n, l) -> geP (n, length (l))
condP (false, n, l) -> tailP (nthtail (s (n), l))
condP (false, n, l) -> nthtailP (s (n), l)
lengthP (cons (x, l)) -> lengthP (l)
geP (s (u), s (v)) -> geP (u, v)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination , truth = Nothing
, transform = Split
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
lengthP |-> (x) |-> E^1x0 * x + (1)
tailP |-> (x) |-> E^1x0 * x + (2)
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, clusters = [ [ lengthP (cons (x, l)) -> lengthP (l) ] , [ nthtailP (n, l) -> condP (ge (n, length (l)), n, l) , nthtailP (n, l) -> geP (n, length (l)) , condP (false, n, l) -> tailP (nthtail (s (n), l)) , condP (false, n, l) -> nthtailP (s (n), l) , geP (s (u), s (v)) -> geP (u, v) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time
split_dimension: 0
}
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES lengthP (cons (x, l)) -> lengthP (l)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination
, truth = Just
True
, transform = Remove
{ interpretation = Interpretation
nthtail |-> (x , y) |-> (0) * x + (4) * y + (0)
0 |-> () |-> (0)
s |-> (x) |-> (0) * x + (0)
false |-> () |-> (0)
ge |-> (x , y) |-> (0) * x + (0) * y + (0)
tail |-> (x) |-> (1) * x + (0)
true |-> () |-> (0)
lengthP |-> (x) |-> (1) * x + (1)
nil |-> () |-> (0)
cons |-> (x , y) |-> (0) * x + (1) * y + (1)
length |-> (x) |-> (0) * x + (0)
cond |-> (x , y , z) |-> (0) * x + (0) * y + (4) * z + (0)
, removes_rules = [ lengthP (cons (x, l)) -> lengthP (l) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
}
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination
, truth = Just
True
, transform = No_Strict_Rules , to = [ ]
}
]
}
, Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtailP (n, l) -> condP (ge (n, length (l)), n, l)
nthtailP (n, l) -> geP (n, length (l))
condP (false, n, l) -> tailP (nthtail (s (n), l))
condP (false, n, l) -> nthtailP (s (n), l)
geP (s (u), s (v)) -> geP (u, v)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination , truth = Nothing
, transform = Remove
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
tailP |-> (x) |-> E^1x0 * x + (1)
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, removes_rules = [ condP (false, n, l) -> tailP (nthtail (s (n), l)) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtailP (n, l) -> condP (ge (n, length (l)), n, l)
nthtailP (n, l) -> geP (n, length (l))
condP (false, n, l) -> nthtailP (s (n), l)
geP (s (u), s (v)) -> geP (u, v)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination , truth = Nothing
, transform = Remove
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (1)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, removes_rules = [ nthtailP (n, l) -> geP (n, length (l)) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtailP (n, l) -> condP (ge (n, length (l)), n, l)
condP (false, n, l) -> nthtailP (s (n), l)
geP (s (u), s (v)) -> geP (u, v)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination , truth = Nothing
, transform = Split
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (1)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, clusters = [ [ geP (s (u), s (v)) -> geP (u, v) ] , [ nthtailP (n, l) -> condP (ge (n, length (l)), n, l) , condP (false, n, l) -> nthtailP (s (n), l) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time
split_dimension: 0
}
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES geP (s (u), s (v)) -> geP (u, v)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination
, truth = Just
True
, transform = Remove
{ interpretation = Interpretation
geP |-> (x , y) |-> (1) * x + (0) * y + (1)
nthtail |-> (x , y) |-> (0) * x + (1) * y + (0)
0 |-> () |-> (0)
s |-> (x) |-> (1) * x + (1)
false |-> () |-> (0)
ge |-> (x , y) |-> (0) * x + (0) * y + (0)
tail |-> (x) |-> (1) * x + (0)
true |-> () |-> (0)
nil |-> () |-> (0)
cons |-> (x , y) |-> (0) * x + (1) * y + (1)
length |-> (x) |-> (1) * x + (0)
cond |-> (x , y , z) |-> (0) * x + (0) * y + (1) * z + (0)
, removes_rules = [ geP (s (u), s (v)) -> geP (u, v) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
}
, to = [ Proof
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, property = Top_Termination
, truth = Just
True
, transform = No_Strict_Rules , to = [ ]
}
]
}
, Claim
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtailP (n, l) -> condP (ge (n, length (l)), n, l)
condP (false, n, l) -> nthtailP (s (n), l)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, v))
, 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 7 strict rules and 10 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
lengthP |-> (x) |-> E^1x0 * x + (1)
tailP |-> (x) |-> E^1x0 * x + (2)
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, removes_rules = [ nthtailP (n, l) -> lengthP (l) ] , 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 + (2)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
lengthP |-> (x) |-> E^1x0 * x + (1)
tailP |-> (x) |-> E^1x0 * x + (2)
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, clusters = [ [ lengthP (cons (x, l)) -> lengthP (l) ] , [ nthtailP (n, l) -> condP (ge (n, length (l)), n, l) , nthtailP (n, l) -> geP (n, length (l)) , condP (false, n, l) -> tailP (nthtail (s (n), l)) , condP (false, n, l) -> nthtailP (s (n), l) , geP (s (u), s (v)) -> geP (u, v) ] ]
, 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 10 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
nthtail |-> (x , y) |-> (0) * x + (4) * y + (0)
0 |-> () |-> (0)
s |-> (x) |-> (0) * x + (0)
false |-> () |-> (0)
ge |-> (x , y) |-> (0) * x + (0) * y + (0)
tail |-> (x) |-> (1) * x + (0)
true |-> () |-> (0)
lengthP |-> (x) |-> (1) * x + (1)
nil |-> () |-> (0)
cons |-> (x , y) |-> (0) * x + (1) * y + (1)
length |-> (x) |-> (0) * x + (0)
cond |-> (x , y , z) |-> (0) * x + (0) * y + (4) * z + (0)
, removes_rules = [ lengthP (cons (x, l)) -> lengthP (l) ] , comment = size 1 , heights ( 7 , 15 ) , time 1 sec
}
from
value Just
True
for property Top_Termination
for system with 0 strict rules and 10 non-strict rules
follows by transformation
No_Strict_Rules
from
value Nothing
for property Top_Termination
for system with 5 strict rules and 10 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
tailP |-> (x) |-> E^1x0 * x + (1)
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, removes_rules = [ condP (false, n, l) -> tailP (nthtail (s (n), l)) ] , 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
Remove
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (1)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, removes_rules = [ nthtailP (n, l) -> geP (n, length (l)) ] , comment = size 0 , heights ( 3 , 7 ) , time
}
from
value Nothing
for property Top_Termination
for system with 3 strict rules and 10 non-strict rules
follows by transformation
Split
{ interpretation = Interpretation
geP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
nthtail |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
condP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (1)
0 |-> () |-> E^0x1
s |-> (x) |-> E^0x0 * x + E^0x1
nthtailP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
false |-> () |-> E^0x1
ge |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
tail |-> (x) |-> E^0x0 * x + E^0x1
true |-> () |-> E^0x1
nil |-> () |-> E^0x1
cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
length |-> (x) |-> E^0x0 * x + E^0x1
cond |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
, clusters = [ [ geP (s (u), s (v)) -> geP (u, v) ] , [ nthtailP (n, l) -> condP (ge (n, length (l)), n, l) , condP (false, n, l) -> nthtailP (s (n), l) ] ]
, 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 10 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
geP |-> (x , y) |-> (1) * x + (0) * y + (1)
nthtail |-> (x , y) |-> (0) * x + (1) * y + (0)
0 |-> () |-> (0)
s |-> (x) |-> (1) * x + (1)
false |-> () |-> (0)
ge |-> (x , y) |-> (0) * x + (0) * y + (0)
tail |-> (x) |-> (1) * x + (0)
true |-> () |-> (0)
nil |-> () |-> (0)
cons |-> (x , y) |-> (0) * x + (1) * y + (1)
length |-> (x) |-> (1) * x + (0)
cond |-> (x , y , z) |-> (0) * x + (0) * y + (1) * z + (0)
, removes_rules = [ geP (s (u), s (v)) -> geP (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 10 non-strict rules
follows by transformation
No_Strict_Rules
from
Claim
{ system = (VAR l n
l x
u v)
(STRATEGY INNERMOST)
(RULES nthtailP (n, l) -> condP (ge (n, length (l)), n, l)
condP (false, n, l) -> nthtailP (s (n), l)
nthtail (n, l) ->= cond (ge (n, length (l)), n, l)
cond (true, n, l) ->= l
cond (false, n, l) ->= tail (nthtail (s (n), l))
tail (nil) ->= nil
tail (cons (x, l)) ->= l
length (nil) ->= 0
length (cons (x, l)) ->= s (length (l))
ge (u, 0) ->= true
ge (0, s (v)) ->= false
ge (s (u), s (v)) ->= ge (u, 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/tmpjXWGyY/ex17.trs
started : Thu Feb 22 16:53:04 CET 2007
finished : Thu Feb 22 16:53:59 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: 55 secs