Question 1  18p

1a  3p

  * 1p by line
  * strict on syntax (since an example was given):
    * -.5p per syntactic mistake per line (up to two)
    * -.5p if some subscripts are wrong
  * strict on content:
    0p if line 2 or 3 is mathematically wrong

1b  3p

  * same as for 1a
  * "exactly the same" when it's not: -.5p

1c  5p

  * -.5p for missing underscores
  * -1p for various mistakes
    * swap h1 and h2
    * get lemma names wrong
    * wrong order of "apply"s
  * -2p at least for wrong proof idea

1d  7p

  * 3p for base case
    * 1p for goal statement
    * 1p for "base"
    * 1p for "step" (0p if "trans")
  * 4p for step case (0p if no induction)
    * 1p for goal statement
    * 1p for recursive call
    * 1p for "step"
    * 1p for rest
    * -1p for too strong IH (with \forall)


Question 2  18p

2a  5p

  * 2p for second line, 3p for third line (1p lhs, 1p or 2p rhs)
    * lhs's contain function name: -.5p
    * lhs's or recursive calls repeat "a": -.5p
    * but if "a" appears in wrong order: -1p
  * accept "list.rec_on" solution if it looks reasonable

2b  6p

  * 2p for base case
  * 4p for induction step
    * 1p for right induction
    * 1p for invocation of IH
  * ignore missing statement of IH in recursive proof, otherwise -.5p

2c  7p

  * 4p for count_append
    * 1p statement
    * 1p for right induction
    * 1p for IH invocation
    * 1p for rest
  * 3p for main lemma
    * 1p for right induction
    * 1p for IH invocation
    * 1p for rest (.5p for base case only)
      * -1p if count_append is not applied
  * ignore missing statement of IH in recursive proof, otherwise -.5p x2


Question 3  25p

3a  4p

  * -.5p for definition without \lambda
  * -1p for \forall instead of \lambda
  * -1p for a comparison where x \in too restricted (e.g. both xs and ys)

3b  6p

  * 2p per hole
  * second hole:
    -1p if brackets are around the whole term
    -.5p if brackets missing (but OK if student states they're unsure)
    -1p if lambda missing
  * third hole:
    1p for property, 1p for justification

3c  5p

  * outer syntactic frame: 1p
    * -.5p for missing {}
  * lhs: 2p
    * -.5p for wrong syntax for function space
  * rhs: 2p
    * "support" instead of comprehension: -1p
  * ignore quotient business (for extensionality?)

3d  6p

  * terms: 3p (1p each)
  * proofs: 3p (1p each)
    * for third hole, "finite A" instead of proof thereof etc.: -.5p

3e  4p

  * term: 2p (text: -.5p)
  * proofs: 2p (1p each)


Question 4  15p

4a  5p

  * 1p per line
    * ignore eta-reduction
    * ignore spurious \sigma arguments
    * -.5p if ite swapped
    * -.5p on each line where recursive call is missing
    * -.5p if unparsable condition
    * -.5p for other oddities

4b  5p

  * rule: 3p
    * 2p for premise(s)
    * 1p for conclusion
    * -.5p if missing negation
    * -.5p for spurious "; q"
    * -1/-1.5p if not in Hoare format but kind of understandable
  * justification: 2p

4c  5p

  * rule(s): 3p
    * 1p for false case
    * 1p for true case
    * 1p for rest
    * -1p if reduced to while without expansion
  * justification: 2p


Question 5  14p

5a  5p

  * first hole: 2p
    * wrong condition in comprehension: -1p
  * second hole: 3p
    * missing "den" call around skip: -.5p
    * missing reflexive: -.5p
    * text as opposed to code: -1p
    * ignore isomorphism

5b  6p

  * 2p per construct
    * give .5p for lhs, 1.5p for rhs
    * -.5p for missing "run"
    * -1p for missing "run p"
    * -1p for (s, s) id syntax
    * -.5p for big o notation instead of recursion

5c  3p

  * -.5p if it is not explained why the measure decreases
  * -.5p if it is not clearly explained why repeat terminates
