Seite 1 von 1

Hilfe: Praktikum 3

Verfasst: 13. Jan 2007 19:10
von MuldeR
Bin hier gerade etwas am Verzweifeln, weil ich heute und gestern kein Stück weiter gekommen bin :?

Also, das hier is bereits grün:
if{?ø(k), ordered(n + k), true}

Aber das hier scheitert leider:
if{ordered(k), ordered(tl(k)), true}
und zwar offenbar an:
if{?ø(k), ordered(tl(k)), true}

Genau hier sollte doch aber das Lemma greifen, dass bereits grün is!?
Tut es aber nich! (Ja, ich hab es abgeschnitten und nochmal neu verifizieren lassen)
Außerdem: Wenn ich ihn dazu "zwingen" will das Lemme zu benutzen (Use Lemma) dann kommt leider ein Fenster mit (Syntax) Fehlern.

Kann mir jemand auf die Sprünge helfen?
Drehe mich da irgendwie seit 2 Tagen im Kreis...

Verfasst: 14. Jan 2007 00:20
von mantra
Irgendwo woanders im Forum steht, dass tl(k) nicht definiert ist, wenn k leer ist. Also kann die Stelle nicht bewiesen werden. Dein Lemma ist also nicht ganz richtig, schätze ich.

Re: Hilfe: Praktikum 3

Verfasst: 14. Jan 2007 13:51
von Christoph Walther
MuldeR hat geschrieben:Bin hier gerade etwas am Verzweifeln, weil ich heute und gestern kein Stück weiter gekommen bin :?

Also, das hier is bereits grün:
if{?ø(k), ordered(n + k), true}

Aber das hier scheitert leider:
if{ordered(k), ordered(tl(k)), true}
und zwar offenbar an:
if{?ø(k), ordered(tl(k)), true}

Genau hier sollte doch aber das Lemma greifen, dass bereits grün is!?
Tut es aber nich! (Ja, ich hab es abgeschnitten und nochmal neu verifizieren lassen)
Außerdem: Wenn ich ihn dazu "zwingen" will das Lemme zu benutzen (Use Lemma) dann kommt leider ein Fenster mit (Syntax) Fehlern.

Kann mir jemand auf die Sprünge helfen?
Drehe mich da irgendwie seit 2 Tagen im Kreis...
Ihr lemma if{?ø(k), ordered(n + k), true} ist nutzlos, denn 'n+k' besteht nur aus 'n', da k=leere liste vorausgesetzt wird, und jede ein-elementige liste ist geordnet, das ist trivial, denn das steht ja schon in der definition von 'ordered'.

Die aussage if{ordered(k), ordered(tl(k)), true} gilt nicht, denn 'tl(k)' ist undefiniert, falls k=ø. Sie müßten also if{?ø(k), true, if{ordered(k), ordered(tl(k)), true}} schreiben, um den fall 'k=ø' ausszuschließen. Nur ist ein solches lemma auch nutzlos - es formuliert ja nur, was schon ohnehin in der definition von 'ordered' steht.

Verfasst: 14. Jan 2007 21:58
von MuldeR
Danke. Der Fehler in if{ordered(k), ordered(tl(k)), true} ist mir jetzt klar geworden.
Wie ich herausfine, ob ein Lemma "sinnlos" ist oder nicht, leider noch nicht. Die Suche geht weiter...

Verfasst: 15. Jan 2007 10:32
von Christoph Walther
MuldeR hat geschrieben:Wie ich herausfine, ob ein Lemma "sinnlos" ist oder nicht, leider noch nicht. Die Suche geht weiter...
Dann schauen Sie sich am besten doch mal die ausführlichen hinweise dazu auf dem übungsblatt an ...