From c37c909f880365a5c52883e8e47a4bdd95742a2a Mon Sep 17 00:00:00 2001 From: Alice Date: Mon, 13 Nov 2023 13:11:23 +0000 Subject: [PATCH] vault backup: 2023-11-13 13:11:23 --- 4a1s/MFES/PL - Aula 8.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/4a1s/MFES/PL - Aula 8.md b/4a1s/MFES/PL - Aula 8.md index 8711652..1c5f949 100644 --- a/4a1s/MFES/PL - Aula 8.md +++ b/4a1s/MFES/PL - Aula 8.md @@ -1,4 +1,4 @@ -https://why3.lri.fr/try/?name=test.mlw&lang=whyml&code=AN7HpJ4Recall1the4officeyassignment%2F4puzzle2from3Fichaz17r3whereBHz44people1areydistributed%2F0byz35officesl2such2that7vH7s2each4person0is6assignedza4singleVHm2Nuno1and3Pedro0do1not3share0anlHl0If1Ana1hasoo2just1for5herselfV2then0so2doesdHg5Officesyaccomodate%2F0at2most1twouIHHuBuMg0if5running2Why32withXyappropriate%2F1SMT4solverlBH0inuByfollowing%2F1you2will0be2able0to5inspect5counterASA6examplesBH2when6adequate7tBNHHz1s3Modele5problemuI6definingVVypredicate%2FBKuQ5writingza1set0of4axiomsfH0In3orderV5expressc3thirdyrequirement%2F3above7r4defineBHfc7h3alonesyexpressing%2Ful5someoneuMg2onlyBH6occupierXSuVWHEz2s2ShowikTuGuPyinconsistent%2Fu0u3hBKu12goalhHEz3s2Find1outuhfunyproperties%2F4followuDpb7vL7suP3MariaPuKR1One7ruT1sheukukLfu7u7u7u8iTDccuOusuLuMu9lbbXmuSaBL5equally2haveusiiidBMDHz4s5Finallyfyformulate%2Fg3provezau85statingVBLuUuU1onef1mayvG3emptyd1For2thisc3first3writeduvBHuwdVfvAg7nzieAzesuzu%2FvO4anyone7ItBHDz5n5Producefyalternative%2Fyformalization%2F3usingV5insteadvEVVpBLr3logic6functionU3givesvB4uniqueRXXBHuIuIY4Repeat1allk6previous3stepsuXvWVlDN7JoBNNNN4moduleuQNF2typec7yu7781Twos3ThreeHnanu%2Fou%2FsvBsvANHveyhasOffice%2F7nk7orerNH3axiom0A1B7v4forallzprAlV4existszopAjphmoHj0A2BmjorAj7r0o10o2BphhJhln7O3qqm7MzoUqFHfzBBiBfnoqhhiVngqUlgLo7RzqDHVurUbfAZUZbWAoAaap0p1plpJjbikiapkpbngpNFXzCgdPlrWHnzDBnBbk0p20p3ApZRdqXXJakoZqjqqqjqdLnam7XuqqnqsrpNMBvHysanity%2Btest%2Fg3falseuAA3checkuzvk3model3makes3senseAvpHHi0g1BiBZvvvrYv3qHm0g2mPvyrQQ7nhv1nOqvxq7oeBLvvvxAhAhhkvyoiqcqBNDvxvQdzoiif7yazpAoAvxdvQjenijHH3lemmayatMostOneEmpty%2FBjBiXcqBegdoarnXLpbqNN1endBNNNNv2NvnyOffices%2BFn%2FBNDvqhmv878vosvoHnSnv9ov9sv%2Bsv%2BNHvZhOkRUBpNHvqB7NNtHHHv8v4lzpmAkkdlNHkBsNNHv4BsNNHjQjzojAgjjBHHv8v8BojNNQBNv2NNNN + ```c module Offices