Porządki dobrze ufundowane
Zadanie ma na celu dowiedzenie pewnych własności rozszerzenia
leksykograficznego danej relacji. Ewentualną kontynuacją byłoby
zdefiniowanie rozszerzenia multizbiorowego i dowiedzenie dla niego
podobnych własności.
Używane będzie pojęcie "`pięknej relacji'', zdefiniowane
następująco:
Relacja ltA Î A× A jest piękna, jeśli z
każdego nieskończonego ciągu {ai}i Î N można wybrać
pare indeksów i<j t.że (ltA ai aj) lub ai=aj.
Alternatywna (równoważna) własność definiująca piękność relacji to:
z każdego nieskończonego ciągu {ai}i Î N można
wybrać podciąg {aij}j Î N t.że dla każdego j
zachodzi (ltA aij aij+1) lub aij=aij+1.
Państwa zadaniem będzie:
-
obejrzenie i zrozumienie definicji rozszerzenia
leksykograficznego danej relacji ltA na zbiorze A
na listy elementów z A (Definicja Ltl jest w pliku
theories/Relations/Relation_Operators.v i używa leA jako
nazwy rozszerzanej relacji. Jednak nazwa ltA wydaje się
sensowniejsza.1)
- zdefiniowanie Ltlen -- ograniczenia Ltl do
list o równej długości
- dowiedzenie, że jeśli ltA jest dobrze ufundowane
(definicja well_founded w pliku theories/Init/Wf.v), to
Ltlen też jest dobrze ufundowane
- zdefiniowanie pojęcia ``bycia ostrym porządkiem'' (chodzi o
zdefiniowanie własności, które ostry porządek musi spełniać --
w stylu definicji z pliku
theories/Relations/Relation_Definitions.v)
- dowiedzenie, że jeśli ltA jest ostrym porządkiem, to
Ltl i Ltlen też są ostrymi porządkami
- zdefiniowanie pięknej relacji
- dowiedzenie, że każde rozszerzenie (w sensie zawierania relacji)
pięknej relacji jest piękną relacją
- dowiedzenie, że rozszerzenie leksykograficzne z ograniczoną
długością Ltlen pięknej relacji jest piękną relacją
- (*)dowiedzenie, że każda piękna relacja jest dobrze ufundowana
Jacek Chrząszcz, 11 kwietnia 2002 ostatnia zmiana: May 23, 2002
- 1
- le -- ``less or equal'', lt -- ``less than''
-- rozszerzanie leksykograficzne relacji ``nieostrej'' nie wydaje
się być sensowne
This document was translated from LATEX by
HEVEA.