Added another lemma to a test file

1 files changed, 6 insertions, 0 deletions

diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy
index ab45f536..725d68f6 100644
--- a/Test/dafny4/NipkowKlein-chapter3.dfy
+++ b/Test/dafny4/NipkowKlein-chapter3.dfy
@@ -131,6 +131,12 @@ lemma AsimpCorrect(a: aexp, s: state)
   forall a' | a' < a { AsimpCorrect(a', s); }

 }

 

+// The following lemma is not in the Nipkow and Klein book, but it's a fun one to prove.

+lemma ASimplInvolutive(a: aexp)

+  ensures asimp(asimp(a)) == asimp(a)

+{

+}

+

 // ----- boolean expressions -----

 

 datatype bexp = Bc(v: bool) | Not(bexp) | And(bexp, bexp) | Less(aexp, aexp)