Browsing Interface : Welcome guest : log in
|
Browsing Interface : Welcome guest : log in |
[
Home |
Graph |
LogLearn |
Editor |
]
KB:
Language:
Formal Language:
|
 |
   UniqueList
|
|
|
| appearance as argument number 1 |
|
|
| (subclass UniqueList List) | Merge.kif 3014-3014 | Unique list is a subclass of list |
| (documentation UniqueList EnglishLanguage "A List in which no item appears more than once,i.e. a List for which there are no distinct numbers ?NUMBER1 and ?NUMBER2 such that (ListOrderFn ?LIST ?NUMBER1) and (ListOrderFn ?LIST ?NUMBER2) return the same value.") | Merge.kif 3016-3019 | Unique list is a subclass of list |
| appearance as argument number 2 |
|
|
| (termFormat EnglishLanguage UniqueList "unique list") | english_format.kif 1039-1039 |
| antecedent |
|
|
| (=> (instance ?LIST UniqueList) (forall (?NUMBER1 ?NUMBER2) (=> (equal (ListOrderFn ?LIST ?NUMBER1) (ListOrderFn ?LIST ?NUMBER2)) (equal ?NUMBER1 ?NUMBER2)))) |
Merge.kif 3021-3026 | If X is an instance of unique list, then For all PositiveIntegers Y and Z: if equal W element of X and V element of X, then equal Y and Z |
|