From b4f23f8247f42c29a20df2a3d8adadf360f75af6 Mon Sep 17 00:00:00 2001
From: Tobias Eidelpes <tobias@eidelpes.info>
Date: Thu, 3 Jun 2021 10:37:14 +0200
Subject: [PATCH] Prove syntactic char -> semantic char

---
 Project2.fst | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Project2.fst b/Project2.fst
index 64d315b..4b2ba76 100644
--- a/Project2.fst
+++ b/Project2.fst
@@ -176,9 +176,9 @@ let rec nsteps n te cs =
 
 val gas: plaincallstack -> Tot nat
 let gas cs =
-    match cs with
-        | (((gas, _, _, _), _, _)::_) -> gas
-        | _ -> 0
+  match cs with
+    | (((gas, _, _, _), _, _)::_) -> gas
+    | _ -> 0
 
 val getDecArgList: (cs: callstack {wellformed cs}) -> Tot (list nat)
 let getDecArgList (cs: callstack {wellformed cs}) =
@@ -223,7 +223,7 @@ val nsteps_stop: (n: nat) -> (te:tenv) -> (cs: callstack{wellformed cs}) ->
 Lemma (requires (isFinal cs))
       (ensures (nsteps n te cs == cs))
 let rec nsteps_stop n te cs =
- admit ()
+  if n = 0 then () else nsteps_stop (n-1) te (step_simp te cs)
 
 (* Prove that if a call stack does not change within one step then it must be final. Formulate first the Lemma and then prove it *)
 (* val progress: *)