:: Manysorted Sets
:: by Andrzej Trybulec
::
:: Received July 7, 1993
:: Copyright (c) 1993 Association of Mizar Users
theorem :: PBOOLE:1
theorem :: PBOOLE:2
:: deftheorem PBOOLE:def 1 :
canceled;
:: deftheorem PBOOLE:def 2 :
canceled;
:: deftheorem Def3 defines ManySortedSet PBOOLE:def 3 :
:: deftheorem Def4 defines in PBOOLE:def 4 :
:: deftheorem Def5 defines c= PBOOLE:def 5 :
theorem Th3: :: PBOOLE:3
definition
let I be
set ;
func [0] I -> ManySortedSet of
I equals :: PBOOLE:def 6
I --> {} ;
coherence
I --> {} is ManySortedSet of I
correctness
;
let X,
Y be
ManySortedSet of
I;
func X \/ Y -> ManySortedSet of
I means :
Def7:
:: PBOOLE:def 7
for
i being
set st
i in I holds
it . i = (X . i) \/ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \/ (Y . i) ) holds
b1 = b2
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \/ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) \/ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) \/ (X . i)
;
func X /\ Y -> ManySortedSet of
I means :
Def8:
:: PBOOLE:def 8
for
i being
set st
i in I holds
it . i = (X . i) /\ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) /\ (Y . i) ) holds
b1 = b2
commutativity
for b1, X, Y being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) /\ (Y . i) ) holds
for i being set st i in I holds
b1 . i = (Y . i) /\ (X . i)
;
idempotence
for X being ManySortedSet of I
for i being set st i in I holds
X . i = (X . i) /\ (X . i)
;
func X \ Y -> ManySortedSet of
I means :
Def9:
:: PBOOLE:def 9
for
i being
set st
i in I holds
it . i = (X . i) \ (Y . i);
existence
ex b1 being ManySortedSet of I st
for i being set st i in I holds
b1 . i = (X . i) \ (Y . i)
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being set st i in I holds
b1 . i = (X . i) \ (Y . i) ) & ( for i being set st i in I holds
b2 . i = (X . i) \ (Y . i) ) holds
b1 = b2
pred X overlaps Y means :
Def10:
:: PBOOLE:def 10
for
i being
set st
i in I holds
X . i meets Y . i;
symmetry
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i meets Y . i ) holds
for i being set st i in I holds
Y . i meets X . i
;
pred X misses Y means :
Def11:
:: PBOOLE:def 11
for
i being
set st
i in I holds
X . i misses Y . i;
symmetry
for X, Y being ManySortedSet of I st ( for i being set st i in I holds
X . i misses Y . i ) holds
for i being set st i in I holds
Y . i misses X . i
;
end;
:: deftheorem defines [0] PBOOLE:def 6 :
:: deftheorem Def7 defines \/ PBOOLE:def 7 :
:: deftheorem Def8 defines /\ PBOOLE:def 8 :
:: deftheorem Def9 defines \ PBOOLE:def 9 :
:: deftheorem Def10 defines overlaps PBOOLE:def 10 :
:: deftheorem Def11 defines misses PBOOLE:def 11 :
:: deftheorem defines \+\ PBOOLE:def 12 :
theorem Th4: :: PBOOLE:4
theorem Th5: :: PBOOLE:5
theorem Th6: :: PBOOLE:6
theorem Th7: :: PBOOLE:7
theorem Th8: :: PBOOLE:8
theorem Th9: :: PBOOLE:9
theorem Th10: :: PBOOLE:10
theorem Th11: :: PBOOLE:11
theorem :: PBOOLE:12
:: deftheorem defines = PBOOLE:def 13 :
theorem :: PBOOLE:13
canceled;
theorem :: PBOOLE:14
canceled;
theorem Th15: :: PBOOLE:15
theorem Th16: :: PBOOLE:16
theorem Th17: :: PBOOLE:17
theorem Th18: :: PBOOLE:18
theorem Th19: :: PBOOLE:19
theorem :: PBOOLE:20
theorem Th21: :: PBOOLE:21
theorem Th22: :: PBOOLE:22
theorem :: PBOOLE:23
theorem Th24: :: PBOOLE:24
theorem Th25: :: PBOOLE:25
theorem :: PBOOLE:26
theorem :: PBOOLE:27
theorem :: PBOOLE:28
theorem :: PBOOLE:29
theorem :: PBOOLE:30
canceled;
theorem :: PBOOLE:31
canceled;
theorem :: PBOOLE:32
canceled;
theorem :: PBOOLE:33
canceled;
theorem Th34: :: PBOOLE:34
theorem Th35: :: PBOOLE:35
theorem Th36: :: PBOOLE:36
theorem Th37: :: PBOOLE:37
theorem Th38: :: PBOOLE:38
theorem Th39: :: PBOOLE:39
theorem :: PBOOLE:40
theorem :: PBOOLE:41
theorem :: PBOOLE:42
theorem :: PBOOLE:43
theorem :: PBOOLE:44
theorem :: PBOOLE:45
theorem :: PBOOLE:46
theorem :: PBOOLE:47
theorem :: PBOOLE:48
theorem Th49: :: PBOOLE:49
theorem Th50: :: PBOOLE:50
theorem :: PBOOLE:51
theorem :: PBOOLE:52
theorem Th53: :: PBOOLE:53
theorem :: PBOOLE:54
theorem :: PBOOLE:55
theorem :: PBOOLE:56
theorem :: PBOOLE:57
theorem Th58: :: PBOOLE:58
theorem Th59: :: PBOOLE:59
theorem Th60: :: PBOOLE:60
theorem :: PBOOLE:61
theorem Th62: :: PBOOLE:62
theorem :: PBOOLE:63
theorem :: PBOOLE:64
theorem Th65: :: PBOOLE:65
theorem Th66: :: PBOOLE:66
theorem :: PBOOLE:67
theorem Th68: :: PBOOLE:68
theorem Th69: :: PBOOLE:69
theorem Th70: :: PBOOLE:70
theorem Th71: :: PBOOLE:71
theorem :: PBOOLE:72
theorem Th73: :: PBOOLE:73
theorem Th74: :: PBOOLE:74
theorem Th75: :: PBOOLE:75
theorem Th76: :: PBOOLE:76
theorem :: PBOOLE:77
theorem Th78: :: PBOOLE:78
theorem Th79: :: PBOOLE:79
theorem :: PBOOLE:80
theorem Th81: :: PBOOLE:81
theorem :: PBOOLE:82
theorem Th83: :: PBOOLE:83
theorem Th84: :: PBOOLE:84
theorem :: PBOOLE:85
theorem :: PBOOLE:86
theorem :: PBOOLE:87
theorem :: PBOOLE:88
theorem :: PBOOLE:89
theorem :: PBOOLE:90
canceled;
theorem :: PBOOLE:91
theorem :: PBOOLE:92
theorem :: PBOOLE:93
canceled;
theorem :: PBOOLE:94
theorem Th95: :: PBOOLE:95
theorem :: PBOOLE:96
theorem :: PBOOLE:97
theorem Th98: :: PBOOLE:98
theorem :: PBOOLE:99
theorem Th100: :: PBOOLE:100
theorem Th101: :: PBOOLE:101
theorem Th102: :: PBOOLE:102
theorem Th103: :: PBOOLE:103
theorem :: PBOOLE:104
theorem :: PBOOLE:105
theorem :: PBOOLE:106
theorem :: PBOOLE:107
canceled;
theorem Th108: :: PBOOLE:108
theorem Th109: :: PBOOLE:109
theorem Th110: :: PBOOLE:110
theorem :: PBOOLE:111
theorem :: PBOOLE:112
theorem :: PBOOLE:113
theorem :: PBOOLE:114
theorem :: PBOOLE:115
theorem Th116: :: PBOOLE:116
theorem :: PBOOLE:117
canceled;
theorem Th118: :: PBOOLE:118
theorem :: PBOOLE:119
theorem :: PBOOLE:120
theorem Th121: :: PBOOLE:121
theorem :: PBOOLE:122
theorem :: PBOOLE:123
theorem :: PBOOLE:124
theorem :: PBOOLE:125
canceled;
theorem Th126: :: PBOOLE:126
theorem :: PBOOLE:127
theorem :: PBOOLE:128
theorem :: PBOOLE:129
:: deftheorem Def14 defines [= PBOOLE:def 14 :
theorem :: PBOOLE:130
theorem :: PBOOLE:131
canceled;
theorem :: PBOOLE:132
theorem :: PBOOLE:133
theorem :: PBOOLE:134
theorem :: PBOOLE:135
theorem Th136: :: PBOOLE:136
theorem :: PBOOLE:137
theorem :: PBOOLE:138
theorem Th139: :: PBOOLE:139
theorem :: PBOOLE:140
:: deftheorem Def15 defines empty-yielding PBOOLE:def 15 :
:: deftheorem Def16 defines non-empty PBOOLE:def 16 :
theorem :: PBOOLE:141
theorem :: PBOOLE:142
theorem Th143: :: PBOOLE:143
theorem Th144: :: PBOOLE:144
theorem :: PBOOLE:145
theorem :: PBOOLE:146
theorem Th147: :: PBOOLE:147
theorem :: PBOOLE:148
theorem Th149: :: PBOOLE:149
theorem :: PBOOLE:150
theorem :: PBOOLE:151
:: deftheorem defines Element PBOOLE:def 17 :
:: deftheorem Def18 defines ManySortedFunction PBOOLE:def 18 :
:: deftheorem Def19 defines # PBOOLE:def 19 :
:: deftheorem Def20 defines *--> PBOOLE:def 20 :
theorem Th152: :: PBOOLE:152
theorem :: PBOOLE:153
:: deftheorem defines [| PBOOLE:def 21 :
:: deftheorem defines MSFuncs PBOOLE:def 22 :
:: deftheorem Def23 defines ManySortedSubset PBOOLE:def 23 :
:: deftheorem Def24 defines ** PBOOLE:def 24 :
:: deftheorem defines .:.: PBOOLE:def 25 :
theorem :: PBOOLE:154