1. Eval (DynamicAssignment Env){
      Say DynamicAssignment= id := expr1 during expr2
      val = Eval (expr1, Env);
      Env1 = UpdateEnv(Env, id, val); // Updates the nearest matching "id".
      Eval (expr2 Env1);
   }

2. 

language: e::= c | lambda x. e | e1 e2 

e1 -> e1'
--------
e1 e2 -> e1' e2


\lambda x. e  e2 -> e[x / e2]

Rest of the rules remain the same.

3. 
Two statements are axiomatically equivalent if

{P} S1 {Q} <=> {P} S2 {Q}

We have the following rule:
   {P} do c while (b) {P AND !b} <=> {P} c {P},  {P AND b} c {P}
    
 
Now, given the above preconditions, we have to prove that
   {P} c; if (b) c; while (b) c {P AND !b}
   <=> 
   {P} c {P}; {P} if (b) c {P} ; {P} while (b) c {P AND !b}
   (Using conditional, and sequencing rules, and the premise of the
   do-while loop given in rhs)
   Which is true!

4. Given {P'} c {Q'}, we can write {P} c {Q} provided, P => P' and Q' => Q.

The strongest such P is false, because false => Any P1. and the weakest Q
is true as any P2 => true.

5.
Lemma 1 (Type Preservation)  If |- e : t, and e -> e', then |- e' : t. 
Lemma 2 (Progress)           If |- e : t, then e is not stuck.

[Details of both the lemmas with reasonable details should be written. ]

[Note: We don't need the useless assumption lemma, substitution lemma, typable
value lemma, or the closedness preservation lemma -- We don't have lambda's as part
of our language.]

Theorem  A well-typed expression cannot go wrong.
Proof    Let e be a well-typed expression, that is, suppose we have |- e : t.
         Suppose e can go wrong, that is, suppose
             e ->* e_n, and e_n is stuck.
         By Lemma 1 (and induction), we have that |- e_n : t,
         and by Lemma 2 we then have that e_n is not stuck, a contradiction.

6. The loop terminates if G = \phi or failure = true.
Given any G, in each iteration one element from G (making it smaller). The
only point where we increase the size of G is in Rule b[iii]. 
There are two subcases -
	- The types are finite - in such a case, after finite number of
	iterations, b[iii] cannot be invoked.
	- The types are infinite (recursive types) - Rule b[vii] ensures
	that failure is set to true.

	In either case the loop will terminate.