Kozen, Dexter2007-04-232007-04-231996-01http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR96-1563https://hdl.handle.net/1813/7220We give an equational proof, using Kleene algebra with tests and commutativity conditions, of the following classical result: every while program can be simulated by a while program with at most one while loop. The proof illustrates the use of Kleene algebra with extra conditions in program equivalence proofs. We also show, using a construction of Cohen, that the universal Horn theory of *-continuous Kleene algebras is not finitely axiomatizable.216235 bytes181869 bytesapplication/pdfapplication/postscripten-UScomputer sciencetechnical reporttechnical report