Question 1  18p

1a  6p

  * 2p per rule
  * 1p if m result is wrong but rest is OK
  * -2p overall if the initial state has an m but it's threaded through
    properly

1b  6p

  * 2p if skip is missing; 1p if looping but right; otherwise 0p
  * 2p for print rule
  * 2p for seq rules
  * 1p if m result is wrong but rest is OK

1c  6p

  * 2p per program
  * 1p if right answer but no or wrong justification


Question 2  21p

2a  4p

  * 1p for general syntax
  * 1p per equation

2b  6p

  * 2p base case
  * 2p each induction step
    * -1p each if IH invocation is not clear

2c  4p

  * 1p for general syntax
  * 1p per equation


2d  7p

  * 2p base case
  * 2p each induction step
    * -1p if IH invocation is not clear
  * 1p for mentioning the recursive discharging of the hypotheses


Question 3  16p

3a  4p

  * 2p sound (1p answer + 1p reason)
  * 2p complete (1p answer + 1p reason)

3b  4p

  * 2p right answer
  * 2p justification

3c  8p

  * 4p each proof


Question 4  20p

4a  3p

  * 1p lhs
  * 1p hyps
  * 1p concl

4b  5p

  * -1p missing IH/goal stmts

4c  3p

  * 1p syntax + 1p for each side of //

4d  4p

  * two terms + two proofs, each 1p

4e  5p


Question 5  15p

5a  4p

  * 1p per rule
  * 1p for general syntax (0p if math = Lean)

5b  7p

  * 1p iff_intro
  * 2p easy direction (rc.base)
  * 4p hard direction
    * 1p rule induction
    * 1p each case: base (assumption), refl (refl_r), symm (symm_r + IH)

5c  4p

  * 2p instantiate 2b
  * 2p discharge the two hypotheses using rsc.refl and rsc.symm
