:: Enumerated Sets :: by Andrzej Trybulec :: :: Received January 8, 1989 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies TARSKI, XBOOLE_0; notations TARSKI, XBOOLE_0; constructors TARSKI, XBOOLE_0; begin reserve x,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,y for object, X,Z for set; definition let x1,x2,x3 be object; func { x1,x2,x3 } -> set means :: ENUMSET1:def 1 x in it iff x=x1 or x=x2 or x=x3; end; definition let x1,x2,x3,x4 be object; func { x1,x2,x3,x4 } -> set means :: ENUMSET1:def 2 x in it iff x=x1 or x=x2 or x=x3 or x=x4; end; definition let x1,x2,x3,x4,x5 be object; func { x1,x2,x3,x4,x5 } -> set means :: ENUMSET1:def 3 x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5; end; definition let x1,x2,x3,x4,x5,x6 be object; func { x1,x2,x3,x4,x5,x6 } -> set means :: ENUMSET1:def 4 x in it iff x=x1 or x=x2 or x =x3 or x=x4 or x=x5 or x=x6; end; definition let x1,x2,x3,x4,x5,x6,x7 be object; func { x1,x2,x3,x4,x5,x6,x7 } -> set means :: ENUMSET1:def 5 x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7; end; definition let x1,x2,x3,x4,x5,x6,x7,x8 be object; func { x1,x2,x3,x4,x5,x6,x7,x8 } -> set means :: ENUMSET1:def 6 x in it iff x=x1 or x= x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8; end; definition let x1,x2,x3,x4,x5,x6,x7,x8,x9 be object; func { x1,x2,x3,x4,x5,x6,x7,x8,x9 } -> set means :: ENUMSET1:def 7 x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 or x=x9; end; definition let x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 be object; func { x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 } -> set means :: ENUMSET1:def 8 x in it iff x=x1 or x=x2 or x=x3 or x=x4 or x=x5 or x=x6 or x=x7 or x=x8 or x=x9 or x=x10; end; theorem :: ENUMSET1:1 { x1,x2 } = { x1 } \/ { x2 }; theorem :: ENUMSET1:2 { x1,x2,x3 } = { x1 } \/ { x2,x3 }; theorem :: ENUMSET1:3 { x1,x2,x3 } = { x1,x2 } \/ { x3 }; theorem :: ENUMSET1:4 { x1,x2,x3,x4 } = { x1 } \/ { x2,x3,x4 }; theorem :: ENUMSET1:5 { x1,x2,x3,x4 } = { x1,x2 } \/ { x3,x4 }; theorem :: ENUMSET1:6 { x1,x2,x3,x4 } = { x1,x2,x3 } \/ { x4 }; theorem :: ENUMSET1:7 { x1,x2,x3,x4,x5 } = { x1 } \/ { x2,x3,x4,x5 }; theorem :: ENUMSET1:8 { x1,x2,x3,x4,x5 } = { x1,x2 } \/ { x3,x4,x5 }; theorem :: ENUMSET1:9 { x1,x2,x3,x4,x5 } = { x1,x2,x3 } \/ { x4,x5 }; theorem :: ENUMSET1:10 { x1,x2,x3,x4,x5 } = { x1,x2,x3,x4 } \/ { x5 }; theorem :: ENUMSET1:11 { x1,x2,x3,x4,x5,x6 } = { x1 } \/ { x2,x3,x4,x5,x6 }; theorem :: ENUMSET1:12 { x1,x2,x3,x4,x5,x6 } = { x1,x2 } \/ { x3,x4,x5,x6 }; theorem :: ENUMSET1:13 { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3 } \/ { x4,x5,x6 }; theorem :: ENUMSET1:14 { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4 } \/ { x5,x6 }; theorem :: ENUMSET1:15 { x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5 } \/ { x6 }; theorem :: ENUMSET1:16 { x1,x2,x3,x4,x5,x6,x7 } = { x1 } \/ { x2,x3,x4,x5,x6,x7 }; theorem :: ENUMSET1:17 { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2 } \/ { x3,x4,x5,x6,x7 }; theorem :: ENUMSET1:18 { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3 } \/ { x4,x5,x6,x7 }; theorem :: ENUMSET1:19 { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4 } \/ { x5,x6,x7 }; theorem :: ENUMSET1:20 { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5 } \/ { x6,x7 }; theorem :: ENUMSET1:21 { x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5,x6 } \/ { x7 }; theorem :: ENUMSET1:22 { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1 } \/ { x2,x3,x4,x5,x6,x7,x8 }; theorem :: ENUMSET1:23 { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2 } \/ { x3,x4,x5,x6,x7,x8 }; theorem :: ENUMSET1:24 { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3 } \/ { x4,x5,x6,x7,x8 }; theorem :: ENUMSET1:25 { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8 }; theorem :: ENUMSET1:26 { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5 } \/ { x6,x7,x8 }; theorem :: ENUMSET1:27 { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5,x6 } \/ { x7,x8 }; theorem :: ENUMSET1:28 { x1,x2,x3,x4,x5,x6,x7,x8 } = { x1,x2,x3,x4,x5,x6,x7 } \/ { x8 }; theorem :: ENUMSET1:29 { x1,x1 } = { x1 }; theorem :: ENUMSET1:30 { x1,x1,x2 } = { x1,x2 }; theorem :: ENUMSET1:31 { x1,x1,x2,x3 } = { x1,x2,x3 }; theorem :: ENUMSET1:32 { x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }; theorem :: ENUMSET1:33 { x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 }; theorem :: ENUMSET1:34 { x1,x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5,x6 }; theorem :: ENUMSET1:35 { x1,x1,x2,x3,x4,x5,x6,x7 } = { x1,x2,x3,x4,x5,x6,x7 }; theorem :: ENUMSET1:36 { x1,x1,x1 } = { x1 }; theorem :: ENUMSET1:37 { x1,x1,x1,x2 } = { x1,x2 }; theorem :: ENUMSET1:38 { x1,x1,x1,x2,x3 } = { x1,x2,x3 }; theorem :: ENUMSET1:39 { x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }; theorem :: ENUMSET1:40 { x1,x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 }; theorem :: ENUMSET1:41 { x1,x1,x1,x2,x3,x4,x5,x6 } = { x1,x2,x3,x4,x5,x6 }; theorem :: ENUMSET1:42 { x1,x1,x1,x1 } = { x1 }; theorem :: ENUMSET1:43 { x1,x1,x1,x1,x2 } = { x1,x2 }; theorem :: ENUMSET1:44 { x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 }; theorem :: ENUMSET1:45 { x1,x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }; theorem :: ENUMSET1:46 { x1,x1,x1,x1,x2,x3,x4,x5 } = { x1,x2,x3,x4,x5 }; theorem :: ENUMSET1:47 { x1,x1,x1,x1,x1 } = { x1 }; theorem :: ENUMSET1:48 { x1,x1,x1,x1,x1,x2 } = { x1,x2 }; theorem :: ENUMSET1:49 { x1,x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 }; theorem :: ENUMSET1:50 { x1,x1,x1,x1,x1,x2,x3,x4 } = { x1,x2,x3,x4 }; theorem :: ENUMSET1:51 { x1,x1,x1,x1,x1,x1 } = { x1 }; theorem :: ENUMSET1:52 { x1,x1,x1,x1,x1,x1,x2 } = { x1,x2 }; theorem :: ENUMSET1:53 { x1,x1,x1,x1,x1,x1,x2,x3 } = { x1,x2,x3 }; theorem :: ENUMSET1:54 { x1,x1,x1,x1,x1,x1,x1 } = { x1 }; theorem :: ENUMSET1:55 { x1,x1,x1,x1,x1,x1,x1,x2 } = { x1,x2 }; theorem :: ENUMSET1:56 { x1,x1,x1,x1,x1,x1,x1,x1 } = { x1 }; theorem :: ENUMSET1:57 { x1,x2,x3 } = { x1,x3,x2 }; theorem :: ENUMSET1:58 { x1,x2,x3 } = { x2,x1,x3 }; theorem :: ENUMSET1:59 { x1,x2,x3 } = { x2,x3,x1 }; theorem :: ENUMSET1:60 { x1,x2,x3 } = { x3,x2,x1 }; theorem :: ENUMSET1:61 { x1,x2,x3,x4 } = { x1,x2,x4,x3 }; theorem :: ENUMSET1:62 { x1,x2,x3,x4 } = { x1,x3,x2,x4 }; theorem :: ENUMSET1:63 { x1,x2,x3,x4 } = { x1,x3,x4,x2 }; theorem :: ENUMSET1:64 { x1,x2,x3,x4 } = { x1,x4,x3,x2 }; theorem :: ENUMSET1:65 { x1,x2,x3,x4 } = { x2,x1,x3,x4 }; theorem :: ENUMSET1:66 { x1,x2,x3,x4 } = { x2,x1,x4,x3 }; theorem :: ENUMSET1:67 { x1,x2,x3,x4 } = { x2,x3,x1,x4 }; theorem :: ENUMSET1:68 { x1,x2,x3,x4 } = { x2,x3,x4,x1 }; theorem :: ENUMSET1:69 { x1,x2,x3,x4 } = { x2,x4,x1,x3 }; theorem :: ENUMSET1:70 { x1,x2,x3,x4 } = { x2,x4,x3,x1 }; theorem :: ENUMSET1:71 { x1,x2,x3,x4 } = { x3,x2,x1,x4 }; theorem :: ENUMSET1:72 { x1,x2,x3,x4 } = { x3,x2,x4,x1 }; theorem :: ENUMSET1:73 { x1,x2,x3,x4 } = { x3,x4,x1,x2 }; theorem :: ENUMSET1:74 { x1,x2,x3,x4 } = { x3,x4,x2,x1 }; theorem :: ENUMSET1:75 { x1,x2,x3,x4 } = { x4,x2,x3,x1 }; theorem :: ENUMSET1:76 { x1,x2,x3,x4 } = { x4,x3,x2,x1 }; theorem :: ENUMSET1:77 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1 } \/ { x2,x3,x4,x5,x6,x7,x8,x9 }; theorem :: ENUMSET1:78 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2 } \/ { x3,x4,x5,x6,x7,x8,x9 }; theorem :: ENUMSET1:79 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3 } \/ { x4,x5,x6,x7,x8,x9 }; theorem :: ENUMSET1:80 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4 } \/ { x5,x6,x7,x8,x9 }; theorem :: ENUMSET1:81 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5 } \/ { x6,x7,x8,x9 }; theorem :: ENUMSET1:82 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6 } \/ { x7,x8,x9 }; theorem :: ENUMSET1:83 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6,x7 } \/ { x8,x9 }; theorem :: ENUMSET1:84 { x1,x2,x3,x4,x5,x6,x7,x8,x9 } = { x1,x2,x3,x4,x5,x6,x7,x8 } \/ { x9 }; theorem :: ENUMSET1:85 { x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 } = { x1,x2,x3,x4,x5,x6,x7,x8,x9 } \/ { x10 }; begin :: Addenda theorem :: ENUMSET1:86 :: from AMI_7, 2006.03.15, A.T. for x, y, z being set st x <> y & x <> z holds {x, y, z} \ {x} = {y, z }; :: from SCMBSORT, 2007.07.26, A.T. theorem :: ENUMSET1:87 for x1,x2,x3 being set holds {x2,x1} \/ {x3,x1} = {x1,x2,x3};