dritte Praxisaufgabe

Nathan Wasser
Kernelcompilierer
Kernelcompilierer
Beiträge: 430
Registriert: 16. Okt 2009 09:48

dritte Praxisaufgabe

Beitrag von Nathan Wasser »

Die dritte Praxisaufgabe ist auf der Webseite verfügbar.

b_b
Erstie
Erstie
Beiträge: 15
Registriert: 7. Nov 2009 21:20

Re: dritte Praxisaufgabe

Beitrag von b_b »

Hallo,

im Ordner "Substitutions" - "Applications to Variables, Terms andTermlists" - "Application Properties" ist ein Lemma doppelt vorhanden:


lemma v ⊀ l → ((v∙t)::σ ⊫ l) = (σ ⊫ l) <= ∀ v, t : term, σ : list[pair[variable.symbol, term]], l : list[term]
if{?var(v), if{v ≺ l, true, ((vsym(v) ∙ t) :: σ ⊫ l) = (σ ⊫ l)}, true}

lemma v⊀k → ((v∙t)::σ ⊫ k) = (σ ⊫ k) <= ∀ k : list[term], v : variable.symbol, t : term, σ : list[pair[variable.symbol, term]]
if{¬ var(v) ≺ k, ((v ∙ t) :: σ ⊫ k) = (σ ⊫ k), true}



Die beiden Lemmata sagen ja dasselbe aus, sie sind nur etwas anders definiert. Soll das so sein? Wundert mich gerade etwas.

Antworten

Zurück zu „Archiv“