</head> <BODY vlink="#990099" link ="#990099", alink="#990099"> <table noborder cellpadding=0 cellspacing=0 width="100%"> <tr bgcolor="#EECCFF"> <td width="50%" align="left"> <font size=-1><i> <a href="http://www.cs.indiana.edu/classes/p415-sjoh/">CSCI P545</a> </i></font> <td width="50%" align="right"> <font size=-1><i> Sat Jan 24 11:14:37 EST 2009 © <a href="http://www.cs.indiana.edu/~sjohnson">[SDJ]</a> </i></font> </table> <H3> Homework Assignment </H3> <h4>Instructions:</h4> <ol> <li> Copy PVS source files <font color="green"><tt><b><a href="K.pvs">K.pvs</a></b></tt></font> and <font color="green"><tt><b><a href="L.pvs">L.pvs</a></b></tt></font> into your working directory. <li> Prove all theorems in both files. <i>Note: in order to do this you will need to introduce some theorems of your own.</i> Not all the results can be proved without additional facts. <li> Turn in <font color="green"><tt><b>.prf</a></b></tt></font> and <font color="green"><tt><b>.status</a></b></tt></font> as usual. </ol> <p> <h4>Notes and Hints:</h4> <i>Coming...</i> </body> </html>