"Je ne comprends pas les Anglais

MACHINE
vaincusVainqueurs
/*Je ne comprends pas les Anglais ! Tandis qu'en France nous donnons à nos rues des noms de victoires : Wagram, Austerlitz… là-bas, on leur colle des noms de défaites : Trafalgar Square, Waterloo Palace… (Alponse Allais)"
SETS
PAYS; LIEU; DATE
VARIABLES
aBattuA
DEFINITIONS
victoires(pp) == ran({ (xx|->yy)|->zz) | (xx|->yy)|->zz) : dom(aBattuA) & (xx =pp)});
defaites(pp) == ran({ (xx|->yy)|->zz) | (xx|->yy)|->zz) : dom(aBattuA) & (yy =pp)})

INVARIANT
aBattuA : (PAYS * PAYS) * DATE +-> LIEU
/* le pays x a battu le pays y à la date d au lieu l */
INITIALISATION
aBattuA :={}
END

/* Alphonse Allais avait bien compris qu'une date n'est pas plus une date de naissance qu'une date de décès, que 3 rue Ml Joffre est l'adresse postale du département informatique de l'IUT de Nantes mais aussi l'adresse du lieu où vous avez glissé sur une peau de banane, que Nantes n'est pas plus une ville de décès qu'une ville de naissance, etc. */
/* Alors ne spécifiez pas ainsi :
SETS
DATE_De_NAISSANCE; DATE_De_DECES
ou encore
PISTE_OCCUPEE; PISTE_Non_OCCUPEE