*************************************
Proof
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES diff (x, y) -> cond1 (equal (x, y), x, y)
cond1 (true, x, y) -> 0
cond1 (false, x, y) -> cond2 (gt (x, y), x, y)
cond2 (true, x, y) -> s (diff (x, s (y)))
cond2 (false, x, y) -> s (diff (s (x), y))
gt (0, v) -> false
gt (s (u), 0) -> true
gt (s (u), s (v)) -> gt (u, v)
equal (0, 0) -> true
equal (s (x), 0) -> false
equal (0, s (y)) -> false
equal (s (x), s (y)) -> equal (x, y))
, property = Termination , truth = Nothing , transform = Ignore_Strategy
, to = [ Proof
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES diff (x, y) -> cond1 (equal (x, y), x, y)
cond1 (true, x, y) -> 0
cond1 (false, x, y) -> cond2 (gt (x, y), x, y)
cond2 (true, x, y) -> s (diff (x, s (y)))
cond2 (false, x, y) -> s (diff (s (x), y))
gt (0, v) -> false
gt (s (u), 0) -> true
gt (s (u), s (v)) -> gt (u, v)
equal (0, 0) -> true
equal (s (x), 0) -> false
equal (0, s (y)) -> false
equal (s (x), s (y)) -> equal (x, y))
, property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation
, to = [ Proof
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES diffP (x, y) -> cond1P (equal (x, y), x, y)
diffP (x, y) -> equalP (x, y)
cond1P (false, x, y) -> cond2P (gt (x, y), x, y)
cond1P (false, x, y) -> gtP (x, y)
cond2P (true, x, y) -> diffP (x, s (y))
cond2P (false, x, y) -> diffP (s (x), y)
gtP (s (u), s (v)) -> gtP (u, v)
equalP (s (x), s (y)) -> equalP (x, y)
diff (x, y) ->= cond1 (equal (x, y), x, y)
cond1 (true, x, y) ->= 0
cond1 (false, x, y) ->= cond2 (gt (x, y), x, y)
cond2 (true, x, y) ->= s (diff (x, s (y)))
cond2 (false, x, y) ->= s (diff (s (x), y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
equal (0, 0) ->= true
equal (s (x), 0) ->= false
equal (0, s (y)) ->= false
equal (s (x), s (y)) ->= equal (x, y))
, property = Top_Termination , truth = Nothing
, transform = Remove
{ interpretation = Interpretation
gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
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
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
diff |-> (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
equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
diffP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
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
, removes_rules = [ diffP (x, y) -> equalP (x, y) , cond1P (false, x, y) -> gtP (x, y) ] , comment = size 0 , heights ( 3 , 7 ) , time 1 sec
}
, to = [ Proof
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES diffP (x, y) -> cond1P (equal (x, y), x, y)
cond1P (false, x, y) -> cond2P (gt (x, y), x, y)
cond2P (true, x, y) -> diffP (x, s (y))
cond2P (false, x, y) -> diffP (s (x), y)
gtP (s (u), s (v)) -> gtP (u, v)
equalP (s (x), s (y)) -> equalP (x, y)
diff (x, y) ->= cond1 (equal (x, y), x, y)
cond1 (true, x, y) ->= 0
cond1 (false, x, y) ->= cond2 (gt (x, y), x, y)
cond2 (true, x, y) ->= s (diff (x, s (y)))
cond2 (false, x, y) ->= s (diff (s (x), y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
equal (0, 0) ->= true
equal (s (x), 0) ->= false
equal (0, s (y)) ->= false
equal (s (x), s (y)) ->= equal (x, y))
, property = Top_Termination , truth = Nothing
, transform = Split
{ interpretation = Interpretation
gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
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
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
diff |-> (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
equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
diffP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
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
, clusters = [ [ gtP (s (u), s (v)) -> gtP (u, v) ] , [ equalP (s (x), s (y)) -> equalP (x, y) ] , [ diffP (x, y) -> cond1P (equal (x, y), x, y) , cond1P (false, x, y) -> cond2P (gt (x, y), x, y) , cond2P (true, x, y) -> diffP (x, s (y)) , cond2P (false, x, y) -> diffP (s (x), y) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time 1 sec
split_dimension: 0
}
, to = [ Claim
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES gtP (s (u), s (v)) -> gtP (u, v)
diff (x, y) ->= cond1 (equal (x, y), x, y)
cond1 (true, x, y) ->= 0
cond1 (false, x, y) ->= cond2 (gt (x, y), x, y)
cond2 (true, x, y) ->= s (diff (x, s (y)))
cond2 (false, x, y) ->= s (diff (s (x), y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
equal (0, 0) ->= true
equal (s (x), 0) ->= false
equal (0, s (y)) ->= false
equal (s (x), s (y)) ->= equal (x, y))
, property = Top_Termination
}
, Claim
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES equalP (s (x), s (y)) -> equalP (x, y)
diff (x, y) ->= cond1 (equal (x, y), x, y)
cond1 (true, x, y) ->= 0
cond1 (false, x, y) ->= cond2 (gt (x, y), x, y)
cond2 (true, x, y) ->= s (diff (x, s (y)))
cond2 (false, x, y) ->= s (diff (s (x), y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
equal (0, 0) ->= true
equal (s (x), 0) ->= false
equal (0, s (y)) ->= false
equal (s (x), s (y)) ->= equal (x, y))
, property = Top_Termination
}
, Claim
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES diffP (x, y) -> cond1P (equal (x, y), x, y)
cond1P (false, x, y) -> cond2P (gt (x, y), x, y)
cond2P (true, x, y) -> diffP (x, s (y))
cond2P (false, x, y) -> diffP (s (x), y)
diff (x, y) ->= cond1 (equal (x, y), x, y)
cond1 (true, x, y) ->= 0
cond1 (false, x, y) ->= cond2 (gt (x, y), x, y)
cond2 (true, x, y) ->= s (diff (x, s (y)))
cond2 (false, x, y) ->= s (diff (s (x), y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
equal (0, 0) ->= true
equal (s (x), 0) ->= false
equal (0, s (y)) ->= false
equal (s (x), s (y)) ->= equal (x, y))
, property = Top_Termination
}
]
}
]
}
]
}
]
}
Proof summary:
value Nothing
for property Termination
for system with 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 8 strict rules and 12 non-strict rules
follows by transformation
Remove
{ interpretation = Interpretation
gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
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
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
diff |-> (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
equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
diffP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
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
, removes_rules = [ diffP (x, y) -> equalP (x, y) , cond1P (false, x, y) -> gtP (x, y) ] , comment = size 0 , heights ( 3 , 7 ) , time 1 sec
}
from
value Nothing
for property Top_Termination
for system with 6 strict rules and 12 non-strict rules
follows by transformation
Split
{ interpretation = Interpretation
gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (1)
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
gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
diff |-> (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
equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
diffP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
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
, clusters = [ [ gtP (s (u), s (v)) -> gtP (u, v) ] , [ equalP (s (x), s (y)) -> equalP (x, y) ] , [ diffP (x, y) -> cond1P (equal (x, y), x, y) , cond1P (false, x, y) -> cond2P (gt (x, y), x, y) , cond2P (true, x, y) -> diffP (x, s (y)) , cond2P (false, x, y) -> diffP (s (x), y) ] ]
, comment = size 0 , heights ( 3 , 7 ) , time 1 sec
split_dimension: 0
}
from
Claim
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES gtP (s (u), s (v)) -> gtP (u, v)
diff (x, y) ->= cond1 (equal (x, y), x, y)
cond1 (true, x, y) ->= 0
cond1 (false, x, y) ->= cond2 (gt (x, y), x, y)
cond2 (true, x, y) ->= s (diff (x, s (y)))
cond2 (false, x, y) ->= s (diff (s (x), y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
equal (0, 0) ->= true
equal (s (x), 0) ->= false
equal (0, s (y)) ->= false
equal (s (x), s (y)) ->= equal (x, y))
, property = Top_Termination
}
Claim
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES equalP (s (x), s (y)) -> equalP (x, y)
diff (x, y) ->= cond1 (equal (x, y), x, y)
cond1 (true, x, y) ->= 0
cond1 (false, x, y) ->= cond2 (gt (x, y), x, y)
cond2 (true, x, y) ->= s (diff (x, s (y)))
cond2 (false, x, y) ->= s (diff (s (x), y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
equal (0, 0) ->= true
equal (s (x), 0) ->= false
equal (0, s (y)) ->= false
equal (s (x), s (y)) ->= equal (x, y))
, property = Top_Termination
}
Claim
{ system = (VAR x y
v u)
(STRATEGY INNERMOST)
(RULES diffP (x, y) -> cond1P (equal (x, y), x, y)
cond1P (false, x, y) -> cond2P (gt (x, y), x, y)
cond2P (true, x, y) -> diffP (x, s (y))
cond2P (false, x, y) -> diffP (s (x), y)
diff (x, y) ->= cond1 (equal (x, y), x, y)
cond1 (true, x, y) ->= 0
cond1 (false, x, y) ->= cond2 (gt (x, y), x, y)
cond2 (true, x, y) ->= s (diff (x, s (y)))
cond2 (false, x, y) ->= s (diff (s (x), y))
gt (0, v) ->= false
gt (s (u), 0) ->= true
gt (s (u), s (v)) ->= gt (u, v)
equal (0, 0) ->= true
equal (s (x), 0) ->= false
equal (0, s (y)) ->= false
equal (s (x), s (y)) ->= equal (x, y))
, property = Top_Termination
}
------------------------------------------------------------------
matchbox general information (including details on proof methods):
http://dfa.imn.htwk-leipzig.de/matchbox/
this matchbox implementation uses the SAT solver
SatELite/MiniSat by Niklas Een and Niklas Sörensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
matchbox process information
arguments : --solver=/home/nowonder/forschung/increasing/wst06/matchbox/SatELiteGTI --timeout-command=/home/nowonder/forschung/increasing/wst06/matchbox/timeout --tmpdir=/home/nowonder/forschung/increasing/wst06/matchbox --timeout=60 /tmp/tmpIsYU09/ex14.trs
started : Thu Feb 22 16:44:44 CET 2007
finished : Thu Feb 22 16:45:34 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: 50 secs