Op eigenschap zoeken

Deze pagina biedt een eenvoudige bladerinteractie voor het vinden van entiteiten met een eigenschap met een bepaalde waarde. Andere beschikbare zoekinteracties zijn de zoekpagina voor pagina-eigenschappen en de querybouwer.

Lijst van resultaten

• Beweren en bewijzen/2011-12/feedback/ATB-deel2-her  + (Het informele gedeelte van het werkstuk is …
  Het informele gedeelte van het werkstuk is in orde; het enige wat ontbrak was het bewijs. Maar helaas sluit ook het nu ingeleverde bewijs niet. Het eerste gat, waarin je correct een all_e wilt toepassen (uit forall t:T, TH t /\ ... -> SR (t+3000) concludeer je correct TH (t0-3000) /\ ... -> SR t0) kun je dichten met zoiets als replace t0 with (t0-3000+3000). Het tweede gat is een echt gat. Je moet niet alleen schrijven: „[I]k zie hier dat H[T]ehardRijden overeenkomt met de [conclusie]”, maar dat moet je met de bewijsregels die Coq aanbiedt '''bewijzen.''' Als je een paar stappen neemt, zie je namelijk dat HTeHardRijden HS t0 > MS t0 bevat, maar dat de conclusie HS (t0-3000) > MS (t0-3000) eist. Waarschijnlijk moet je hier de specificaties van de onderdelen aanpassen zodat de zaak kloppend wordt. Bij het derde gat moet je eenvoudigweg de formule in delen opsplitsen (met con_i) en elk deel apart bewijzen. Om de formule in de juiste vorm te krijgen, moet je eerst exi_e (exists q:T, t0+3000 gebruiken, en dat kun je eenvoudig bewijzen uit aanname HRemmer.
  erst <tt>exi_e (exists q:T, t0+3000<q /\ SS q /\ ...)</tt> gebruiken, en dat kun je eenvoudig bewijzen uit aanname HRemmer.)
• Beweren en bewijzen/2011-12/feedback/airco-deel2  + (Het ingeleverde bewijs werkt niet. Ongevee …
  Het ingeleverde bewijs werkt niet. Ongeveer 40 regels voor het einde hangt hij met een syntax-error. En in de specificatie van het geheel staat hier opeens Lucht_binnen (t+6) terwijl het in de tekst hierboven nog gewoon t is. Dat past dan natuurlijk helemaal niet meer bij de natuurlijke taal. Wat wel goed is, is dat jullie een hulpstelling maken en die met apply gebruiken. Maar zorg dan svp wel voor wat tekst waardoor duidelijk wordt wat het doel is van die hulpstelling.
  ordt wat het doel is van die hulpstelling.)
• Beweren en bewijzen/2012-13/feedback/Dubbele schuifdeur-deel2-her  + (Het is al op 20 juni gelukt; daarover had ik al een opmerking gemaakt in mijn vorige beoordeling. Dank je wel voor de tussenkopjes.)
• Beweren en bewijzen/2013-14/feedback/homecinemaset-deel2  + (Het is simpelweg niet af. Verder kennen jullie de constructie 'unfold onderdeel in aanname' blijkbaar niet, want dan zou het bewijs er leesbaarder uit hebben gezien omdat je alleen de spec die je echt nodig hebt open klapt.)
• Beweren en bewijzen/2013-14/feedback/boormachine-deel2  + (Hier gelukkig wel een correctheidsstelling en een bewijs dat gebruik maakt van onder meer exi_e, exi_i, interval, lin_solve, replace.)
• Beweren en bewijzen/2012-13/feedback/Stoplicht-deel2-her  + (Ik bedenk achteraf dat je een deel van de …
  Ik bedenk achteraf dat je een deel van de herhalingen in een Lemma had kunnen stoppen, dat je één keer bewijst en dan meerdere keren met „apply .” aanroept, maar dat ik jullie niet eerder hierop heb gewezen kan ik jullie niet kwalijk nemen. In sommige delen is het ook alleen ''bijna'' een herhaling.
  is het ook alleen ''bijna'' een herhaling.)
• Beweren en bewijzen/2011-12/feedback/elektrische tandenborstel-deel2  + (Ik ben niet blij met de keuze om Coq de ge …
  Ik ben niet blij met de keuze om Coq de gebonden variabelen te hernoemen. Ik zie liever zinvollere namen als 'startmoment' of zo. Gelukkig hielp de naamgeving van de aannames vaak wel wat, al waren ze soms ook wat cryptisch. Goed gebruik gemaakt van de verschillende regels: interval, exi_e, neg_i en neg_e'. Hebben jullie nog geprobeerd om het zonder neg_e' te kunnen doen?
  beerd om het zonder neg_e' te kunnen doen?)
• Beweren en bewijzen/2013-14/feedback/kentekenslagboom-deel2  + (Ik was even onzeker of je bewijs wel af is omdat er geen <tt>Qed.</tt> aan het einde stond. Het is af.)
• Beweren en bewijzen/2011-12/feedback/cylinderslot-deel2  + (In het Coq-script worden opeens allerlei s …
  In het Coq-script worden opeens allerlei specifieke invullingen als profiel1 en profiel2 gegeven terwijl daar in het werkstuk zelf helemaal niets over gezegd is. Profiel1 gebruiken jullie nog wel in de definitie van profielSlot en in de definitie van sleutelPast. (Dat laatste is raar. Waarom staat daar niet de globale profielSlot? Als je nu met een ander slot gaat werken moet je op meerdere plekken iets gaan veranderen.) Maar de dingen als g1 en g2 zie ik nergens meer terugkomen. Het commentaar in het bewijs helpt wel om te zien waar we precies mee bezig zijn. In het bewijs doen jullie een unfold op SleutelPinnen, terwijl je iets bewijst met SluitPinnen. Technisch gaat dat goed omdat bij assumption Coq wel gaat zoeken of er een aanname is die past. Maar het staat wel slordig. Om dit te voorkomen zou je je bewijs niet met assumption, maar met exact moeten maken. Vervolgens openen jullie voor de volgende tak SluitPinnen terwijl jullie juist SleutelPinnen gebruiken. Verder maken jullie hier predikaten profielMatch, sleutelPast en juisteSleutelpinHoogte aan die eigenlijk helemaal geen predikaten zijn, maar hulpdefinities.
  geen predikaten zijn, maar hulpdefinities.)
• Beweren en bewijzen/2013-14/feedback/vaatwasmachine-deel2  + (In het bewijsscript staat veel commentaar. …
  In het bewijsscript staat veel commentaar. Dat is op zich goed. Maar er staat ook nog dat jullie alle ∧-tekens zijn vervangen door →'s, maar dat klopt geloof ik niet meer. Positief is dat er lemma's worden gebruikt. Wel jammer dat jullie de parameters daarbij eigenlijk misbruiken. Coq vertaalt die nu voor jullie naar ∀'s, maar dat hadden jullie eigenlijk zelf moeten doen.
  igenlijk zelf moeten doen.)
• Beweren en bewijzen/2011-12/feedback/cilinderslot-deel2-her  + (Jammer dat die specificatie "de andere kant op" niet gelukt is te bewijzen. Was dat wel gelukt, was het cijfer echt hoger geweest.)
• Beweren en bewijzen/2012-13/feedback/Koelkast-deel2  + (Jammer dat er zo ruim wordt ingesprongen d …
  Jammer dat er zo ruim wordt ingesprongen dat de formules niet meer in de linkerkolom passen. Het is erg onoverzichtelijk om unfold op alle onderdelen te gebruiken in plaats van alleen op het onderdeel waar het van belang is. Ook is de specificatie van het geheel hier weer anders weergegeven dan in het werkstuk zelf, maar nog steeds niet volgens de structuur van de formule. In het Coq-script wordt gewoon een conjunctie gesuggereerd, maar dat is het volgens mij niet. Gebruikte regels: neg_i, imp_e, imp_i, con_i, con_e1, con_e2, interval, lin_solve. Hiervan is alleen die neg_i een beetje bijzonder.
  is alleen die neg_i een beetje bijzonder.)
• Beweren en bewijzen/2012-13/feedback/Eukaryoot-deel2  + (Jullie beginnen heel raar met een exi_e op …
  Jullie beginnen heel raar met een exi_e op wat je moet bewijzen, terwijl die regel eigenlijk alleen zin heeft op exists uit de aannames. Na een stap of tien waarbij jullie ook nog eens een assumption over het hoofd zien zijn jullie weer terug bij af. En vervolgens doen jullie weer zo iets raars met een imp_e gevolgd door een imp_i. Een legale truc om iets met intervallen te kunnen bewijzen, maar op een 'normaal' moment in het bewijs zeer ongebruikelijk. En ook overbodig want asl jullie dit niet doen en gewoon verder gaan met 'fold GolgiApparaat' kunnen jullie het hele bewijs afmaken en hoeven jullie alleen aan het eind nog een paar lin_solve's toe te voegen.
  nd nog een paar lin_solve's toe te voegen.)
• Beweren en bewijzen/2013-14/feedback/tandenborstel-deel2  + (Jullie gebruiken commentaar en originele stappen om de stelling te bewijzen.)
• Beweren en bewijzen/2013-14/feedback/walkietalkie-deel2  + (Jullie gebruiken een andere spec van het g …
  Jullie gebruiken een andere spec van het geheel dan voorheen. Nu staat er opeens: (exists d:T, jack_uit w g (d+125)). Omdat er verder geen eisen aan die d zijn gesteld qua interval (zoals wel in de andere gevallen) is dit een beetje onzinnig. Oh wacht, dit staat tussen commentaartekens. Dus jullie hebben zelf ook bedacht dat het niet zo zinnig is. En kennen jullie de 'unfold onderdeel in aanname' niet? Het is veel overzichtelijker als je alleen het belangrijke onderdeel openklapt.
  lleen het belangrijke onderdeel openklapt.)
• Beweren en bewijzen/2013-14/feedback/achtbaan-deel2  + (Jullie gebruiken hier andere haakjes bij S …
  Jullie gebruiken hier andere haakjes bij Station. Blijkbaar hadden jullie het probleem zelf ook al gezien, maar het niet consequent verbeterd. Positief is dat jullie wat commentaar gebruiken tussen de stappen, maar helaas niet consequent. Zo wordt er wel gezegd wanneer het bewijs van de eerste eigenschap begint, maar bijvoorbeeld niet waar het bewijs van de laatste eigenschap begint. Negatief is daarentegen dat jullie ogenschijnlijk nietszeggende variabelen als t1 en zo gebruiken.
  eggende variabelen als t1 en zo gebruiken.)
• Beweren en bewijzen/2011-12/feedback/ov-oplader-deel2  + (Jullie hebben ervoor gekozen om de verzame …
  Jullie hebben ervoor gekozen om de verzameling berichten abstract te houden met als enige kennis dat mChipkaartOpgeladen en mChipkaartIngevoerd variabelen van dat type zijn. Die kunnen dus nog wel het zelfde zijn. En er kunnen ook nog veel meer berichten zijn. Maar in jullie bewijs maakt het niet uit. Het positieve aan het bewijs is dat jullie zowel exi_e-regels als lin_solve-, replace- en interval-regels gebruiken. Jullie specificatie van het geheel wijkt dus genoeg af van de onderdelen om echt te kunnen laten zien dat er werk verzet moet worden.
  laten zien dat er werk verzet moet worden.)
• Beweren en bewijzen/2012-13/feedback/Magnetron-deel1-her  + (Jullie hebben in elk geval een Coq scipt toegevoegd, maar dat past helemaal niet bij jullie werkstuk. En in het bijzonder zitten er syntaxfouten in! Persoonlijk vond ik de specs in het werkstuk zelf beter dan deze...)
• Beweren en bewijzen/2013-14/feedback/kopieerapparaat-deel2  + (Jullie kennen het commando 'unfold onderde …
  Jullie kennen het commando 'unfold onderdeel in aanname' niet? Daarmee zorg je dat alleen het op dat moment belangrijke onderdeel is opengeklapt, wat nogal helpt bij de overzichtelijkheid. Wel prettig daarentegen is dat jullie commentara gebruiken om aan te geven waar jullie mee bezig zijn.
  m aan te geven waar jullie mee bezig zijn.)
• Beweren en bewijzen/2011-12/feedback/Rekenmachine-deel2  + (Jullie leggen zelf uit waarom dit een prima proeve van bekwaamheid is.)
• Beweren en bewijzen/2011-12/feedback/airco-deel2-her  + (Jullie maken dezelfde fout als bij de vori …
  Jullie maken dezelfde fout als bij de vorige versie: er staat hier opeens een heel ander onderdeel dan bij de onderdeelspecificaties! Het onderdeel Bedieningspaneel is ineens een stuk ingewikkelder geworden. In het bijzonder mist hier uitleg in natuurlijke taal bij. Waarom is dit deel erbij gekomen? Welk onderdeel heeft deze eigenschap nodig?
  elk onderdeel heeft deze eigenschap nodig?)
• Beweren en bewijzen/2011-12/feedback/Automatische lamp-deel2  + (Maar behoorlijk simpel. Jullie hebben welgeteld een keer een replace nodig, die vervolgens vrij eenvoudig te bewijzen is.)
• Beweren en bewijzen/2013-14/feedback/koffiezetapparaat-deel2  + (Mooi gebruik van een lemma. Netjes commentaar tussen de bewijsstappen.)
• Beweren en bewijzen/2013-14/feedback/thuisalarmsysteem-deel2  + (Naast de gebruikelijke regels worden ook dis_e, exi_e, exi_i, interval, lin_solve en replace gebruikt.)
• Beweren en bewijzen/2013-14/feedback/snoepautomaat-deel2  + (Niet fout, maar wel af te raden is dat jullie voor de onbesproken variabelen met t2 dezelfde naam gebruiken als de bijbehorende gebonden variabele. Dit maakt het onoverzichtelijk)
• Beweren en bewijzen/2013-14/feedback/elektrischegitaar-deel2  + (Om te beginnen: gebruik zinnige namen voor …
  Om te beginnen: gebruik zinnige namen voor de variabelen. Als t1 het moment van aanslaan voorstelt kun je het beter 'taan' noemen dan 't_a1'. Verder maken jullie een rare opmerking over dat je 'geen all_i (t_a3 +1/100)' kunnen doen. Maar als jullie de regels goed snappen, dan weten jullie waarom je alleen maar een (onbesproken) variabele mag invullen bij een all_i en dus geen term als (t_a3+1/100).
  n all_i en dus geen term als (t_a3+1/100).)

• Beweren en bewijzen/2011-12/feedback/ATB-deel2  + (Ontbreekt geheel.)

• Beweren en bewijzen/2013-14/feedback/boormachine-deel1  + (Op zich is het bewijs goed, maar het is een veel te simpel bewijs. Of beter gezegd: je stelling is veel te simpel. Daar moet echt wat aan verbeteren voordat je een voldoende kunt krijgen.)
• Beweren en bewijzen/2011-12/feedback/loopband-deel2  + (Op zich ziet het bewijs er prima uit. Veel …
  Op zich ziet het bewijs er prima uit. Veel noeste arbeid. Netjes uitgelegd hoe die iff_e en iff_i regels werken. Alleen wel jammer dat de inhoud van Resetten blijkbaar niet van belang is. Als je die vervangt door 't is ongelijk aan t', kan precies hetzelfde script gebruikt worden. Dus blijkbaar is het niet van belang of er achter Resetten iets zinnigs of onzinnigs zit.
  er Resetten iets zinnigs of onzinnigs zit.)
• Beweren en bewijzen/2011-12/feedback/kassa-deel2  + (Prettig dat er met commentaar is aangegeve …
  Prettig dat er met commentaar is aangegeven welke goal er bewezen moet worden. (Als stond er wel ergens een 0 in plaats van VTB (a + 7100 + 1000).) Zoals gezegd is het jammer dat jullie jullie bewijskwaliteiten niet helemaal tonen. Jullie hebben op een gegeven moment een ∃ in de aanname, maar omdat de intervallen precies overeenkomen, hoeven jullie die niet eens met de exi_e regel uit te werken om vervolgens te laten zien dat er echt zo'n moment is.
  ten zien dat er echt zo'n moment is.)
• Beweren en bewijzen/2012-13/feedback/Scheerapparaat-deel2  + (Prettig dat er wat commentaar tussen staat waardoor beter te volgen is wat er op dat moment bewezen wordt. Gebruikte regels: exi_e, exi_i, dis_i1, replace, lin_solve, interval.)
• Beweren en bewijzen/2011-12/feedback/waterkoker-deel2-her  + (Qed ontbreekt, maar dat is natuurlijk niet echt essentieel.)
• Beweren en bewijzen/2012-13/feedback/Bankkluis-deel2-her  + (Technisch gesproken goed, maar jullie hebb …
  Technisch gesproken goed, maar jullie hebben waarschijnlijk ook wel gemerkt dat jullie alleen de simpele regels imp_e, imp_i, all_e, all_i en zo nodig hebben gehad. Overigens is het wel handig om zinnige namen te geven. Nu gebruiken jullie t5 voor het moment waarop de code wordt ingetoets en t3 (een later moment) voor het moment waarop de sleutel wordt ingestoken. Dat is verre van logisch en verwarrend. Als jullie zinnige namen als 'tcode' of 'tsleutel' (of 'tc' en 'ts' als jullie die andere namen te lang vinden) zouden gebruiken, is het veel makkelijker te zien wat het allemaal voorstelt.
  lijker te zien wat het allemaal voorstelt.)
• Beweren en bewijzen/2013-14/feedback/vaatwasmachine-deel1  + (Tja, er hoefde nog niets te worden gedaan, …
  Tja, er hoefde nog niets te worden gedaan, maar tauto proberen is wel erg optimistisch voor iets in predikaatlogica. Anders gezegd, als tauto het bewijs wel kon afronden, weet je eigenlijk zeker dat het niet spannend genoeg is omdat je dan slechts propositielogica gebruikt.
  je dan slechts propositielogica gebruikt.)
• Beweren en bewijzen/2011-12/feedback/grijpautomaat-deel2-her  + (Tja, het bewijs is alleen maar rondgekrege …
  Tja, het bewijs is alleen maar rondgekregen doordat er gebruik gemaakt wordt van twee keer een hypothesis, waarbij elk van die aannames zeer discutabel zijn. Zeg maar gewoon fout. Ze hebben namelijk de vorm van de standaardfout dat ∀ gecombineerd wordt met ∧ tekens.
  ecombineerd wordt met ∧ tekens.)
• Beweren en bewijzen/2012-13/feedback/Magnetron-deel2-her  + (Toen ik het had over het toepassen van Lem …
  Toen ik het had over het toepassen van Lemma's doelde ik op de manier zoals je bij 'reverse' hebt gedaan. Het was niet de bedoeling om een nieuwe tactiek aan te maken. Het eindresultaat is echter mooi; helaas weet ik niet welke bron je gebruikt hebt om deze tactiek zo te definiëren. Verder zou ik ook graag uitleg hebben gekregen over hoe die tactiek nu werkt. Misschien zit er wel iets illegaals in deze tactiek? (Is niet zo, maar ik had het wel leuk gevonden als jij dat had opgemerkt.) Het voordeel van zo'n lemma is dat je dat lemma eerst moet bewijzen. Maar hoe bewijs je dat deze tactiek alleen maar eerlijke stappen gebruikt?
  lleen maar eerlijke stappen gebruikt?)
• Beweren en bewijzen/2012-13/feedback/Alarmsysteem-deel2-her  + (Twee onmogelijk te bewijzen takken: *Zoals …
  Twee onmogelijk te bewijzen takken: *Zoals ik al drie keer heb aangegeven, zul je geen relatie tussen a en b (a=b+30 of b=a+30) kunnen bewijzen omdat je beide variabelen als onbesproken hebt geïntroduceerd. *Als de negatie van een existentiële uitspraak in de aannames staat, kun je normaliter niet bewijzen dat deze existentiële uitspraak waar is. De exi_e-regel is niet te bewijzen. Verdere onhandigheden: * Je splitst een formule met con_i op en voegt direct daarna met con_e1 het zojuist afgesplitste deel toe. Als resultaat moet je dat twee keer bewijzen i.p.v. één keer. * Als gevolg van die onmogelijke existentiële uitspraak (hierboven) voer je een neg_e-regel uit. Die regel moet je eigenlijk alleen uitvoeren als je al ziet dat er een tegenspraak in de '''aannames''' zit. Dat de conclusie de aannames tegenspreekt is misschien een hint, maar dan moet je op zoek naar de tegenspraak in de aannames.
  p zoek naar de tegenspraak in de aannames.)
• Beweren en bewijzen/2013-14/feedback/elektrischegitaar-deel2-her  + (Verantwoord gebruik van hypothesis. Wel gebruik gemaakt van replace, lin_solve, interval en apply, maar niet van exi_e of dis_e.)
• Beweren en bewijzen/2011-12/feedback/frituurpan-deel2  + (Waarom hebben jullie gekozen voor Z_scope? Op zich is het bewijs natuurlijk wel goed, maar er zit geen enkele moeilijke stap in. Geen replace, lin_solve, interval...)
• Beweren en bewijzen/2013-14/feedback/buizenpost-deel2  + (Waarom unfold op alle onderdelen? Kennen j …
  Waarom unfold op alle onderdelen? Kennen jullie de 'unfold onderdeel in aanname' niet? Daarmee zijn bewijzen veel overzichtelijker omdat je alleen de noodzakelijke onderdelen openklapt. En die interval in het begin is ook nergens voor nodig. Dat commando heb je pas nodig als je iets over de afzonderlijke grenzen moet bewijzen. Verder staan er twee Hypotheses in het bewijs die nergens worden uitgelegd. (En op de slides stond dat dat moest!) Erger is dat de tweede Hypothesis een beetje onzinnig is: x <=y is niet echt gelijk aan x+a <= y+a, maar x+a <= y+a is een gevolg van x<=y. Hadden jullie dit met een → geschreven, was het simpelweg bewijsbaar geweest met all_i, imp_i en lin_solve. En dan had je kunnen laten zien dat je een lemma kunt toepassen.En je had lin_solve gebruikt. Nog een slak om zout op te leggen: antisymmetrie is een wiskundig begrip dat niet veel te maken heeft met wat jullie antisymmetrie noemen. Positief is dan weer wel dat jullie een dis_e nodig hebben. En op zich is het bewijs in orde. Er staat zelfs netjes in commentaar aangegeven waar de tweede tak begint.
  aangegeven waar de tweede tak begint.)
• Beweren en bewijzen/2011-12/feedback/fiets-deel2  + (Wel weer goed dat jullie de gebruikte iff_e regels uitleggen.)
• Beweren en bewijzen/2011-12/feedback/frisdrankautomaat-deel2  + (Zoals verwacht een tamelijk simpel bewijs. Er zit geloof ik een keer een replace in om de zes seconden tijdsverschil in een stuk van vijf en van een te hakken, maar dat is ook zo ongeveer het moeilijkste wat er in zit.)
• Beweren en bewijzen/2011-12/feedback/Verwarmingssysteem-deel2-her  + (alle stappen zijn formeel correct, alleen …
  alle stappen zijn formeel correct, alleen gebruik je op één punt de inconsistente aanname, namelijk bij con_e2 (v = (v - 12)). Omdat je kunt bewijzen dat v gelijk is aan v-12, kun je hier de moeilijkheden van het bewijs omzeilen. Ik zie uit de rest van het bewijs dat je wel serieus bezig bent.
  ijs omzeilen. Ik zie uit de rest van het bewijs dat je wel serieus bezig bent.)
• Beweren en bewijzen/2013-14/feedback/geautomatiseerd-subwayrestaurant-deel2  + (duidelijk gestructureerd met lemma’s en commentaren.)
• Beweren en bewijzen/2013-14/feedback/Schiphol Bagage Sorteersysteem-deel2  + (eenvoudig, maar voldoende afwisselend, en met hier en daar een behulpzaam commentaar.)
• Beweren en bewijzen/2012-13/feedback/Flessenautomaat-deel2  + (het was wel fijn geweest als er meer aanda …
  het was wel fijn geweest als er meer aandacht was geschonken aan de layout van de formules in het Coq-script. Ze zijn vaak breder dan de linkerkolom en toch niet verdeeld over meerdere regels. Positief is dat jullie lemma's definiëren en gebruiken. Echter, bij die lemma's gebeurt ook iets raars. Er staat een forall o:O in de formule terwijl er helemaal niets met o gedaan wordt. De enige reden dat dit gedaan wordt is denk ik omdat de specificatie van in dit geval Sensor niet volgens de systematische methode is gedaan, waardoor er een forall o:O over de hele conjunctie staat terwijl die alleen voor de eerste twee eigenschappen van belang is. Dit heeft tot gevolg dat jullie op een gegeven moment de eigenschap 'O' moeten bewijzen. Dat kan dan toevallig via assumption, maar wat betekent het dat jullie 'O' moeten bewijzen? Gebruikte regels: dis_e, dis_i1, dis_i2, apply, imp_e, imp_i, con_i, con_e1, con_e2, replace, lin_solve, interval, all_e, all_i.
  e, lin_solve, interval, all_e, all_i.)
• Beweren en bewijzen/2011-12/feedback/Brandsysteem-deel2  + (omslachtig (maar niet incorrect) door herhaalde en overbodige invoering van dezelfde aanname.)
• Beweren en bewijzen/2012-13/feedback/Kruimeldief-deel2  + (onaf. Je legt de vinger precies bij het ontbrekende punt. Je zou namelijk aan de specificatie van het Stof_Reservoir zoiets moeten toevoegen als: Als de stofzak niet geleegd wordt, dan wordt de teller niet gereset.)
• Beweren en bewijzen/2012-13/feedback/Stoplicht-deel2  + (onaf. Onvoldoende. In de laatste tak moet …
  onaf. Onvoldoende. In de laatste tak moet je iets bewijzen o.a. op basis van aanname H32b. Dat bewijs verloopt vrijwel precies zoals het bewijs op basis van aanname H32a. Coq is niet alleen magie. Ik verzoek je te proberen om te begrijpen wat je moet bewijzen: Er bestaat een tijdstip w in (v-20, v-8) waarop knop2 is ingedrukt, en je moet bewijzen dat één van de lichten voor auto’s op tijdstip v rood staat. Dat is echt bijna de situatie van aanname H32a (het enige verschil is dat daar knop1 was ingedrukt). Dan bedenk je eerst via welke onderdelen het bewijs verloopt en merk je dat H20 helemaal niet gebruikt wordt, dus dat dis_e overbodig is.
  ebruikt wordt, dus dat dis_e overbodig is.)
• Beweren en bewijzen/2012-13/feedback/verwarmingsysteem-deel2  + (onnodig ingewikkeld: „isI s0 /\ ingT s0 > kamerT s0” bewijs je door con_i. en daarna con_e1 (ingT s0 > kamerT s0). te doen, dus heen en terug naar dezelfde formule?)
• Beweren en bewijzen/2012-13/feedback/Halon-Systeem-deel2-her  + (ontbreekt geheel)
• Beweren en bewijzen/2013-14/feedback/Schiphol Bagage Sorteersysteem-deel1  + (tauto werkt alleen bij bewijzen in propositielogica, niet in predicaatlogica.)