[isabelle] Linear Arithmetic



Hello,

my project Columbo is slowly making progress. I currently wonder about 
decidability of the halting problem for simple while programs, resp. 
Rice's theorem. The following while program does clearly halt for all 
integer values in i,s,ug,og and it's function can be expressed by a 
denotation:

http://cococo.de/products/windows/Columbo/sample1.html

What would Isabelle deduct from the code or it's denotation?

Greetings,
Jens





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.