Question 9

A structure combining information from songs and plays can be defined using the following definition:

SongsAndPlaysList == seq SongDetails 

We assume the existence of the following abbreviation:

SongDetails ==  Id × SongName × Artist × AlbumTitle ×  Length × Time × Time × N 

Here, the details of each song consists of: an identifier; a song name; an artist; an album title; the song length; the date it was added; the last time it was played; and the number of times it has been played.

(a) A valid element of SongsAndPlaysList will: ensure that there are no duplicate identifiers and ensure that any 'last played' time is later than

any 'date added' time. Define such a ValidSongsAndPlaysList structure. (b) Define a specific ValidSongsAndPlaysList, songs_and_plays, the values of which are defined by the values of songs and plays of Question 6.

(c) Show how the set comprehensions of Question 7 might be recast as set comprehensions on the sequence of part (b).

(d) Show how the recursive function of Question 8 might be recast as a function that takes a sequence of type seq SongDetails as input.

Question 10

You have been informed that the following statements are true:

• "If the team wins all of its league matches, then the team will win the league."

• "The team wins the cup if, and only if, the team wins all of its cup matches."

Assume that: AC represents "wins all cup matches"; AL represents "wins all league matches"; WC represents "wins the cup"; and WL represents "wins the league".

By using the above, prove each of the following via a proof tree.

(a) AC  Ù AL  => WC Ù WL  ( where AND = Ù)

(b) AC V AL => WC V WL (where V = or)

Each step in your tree should be labelled and justified by a basic introduction or elimination rule from our system.