Hilfe: Praktikum 3

[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...

[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.

[Christoph Walther]

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.

[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...

[Christoph Walther]

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 ...