Volume 2, 1990

University of Bialystok

Copyright (c) 1990 Association of Mizar Users

### The abstract of the Mizar article:

### Many-Argument Relations

**by****Edmund Woronowicz**- Received June 1, 1990
- MML identifier: MARGREL1

- [ Mizar article, MML identifier index ]

environ vocabulary FUNCOP_1, FUNCT_2, RELAT_1, FINSEQ_1, BOOLE, QC_LANG1, ZF_LANG, MARGREL1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, NAT_1, FINSEQ_1, RELAT_1, FUNCOP_1, FRAENKEL; constructors FINSEQ_1, FUNCOP_1, FRAENKEL, MEMBERED, XBOOLE_0; clusters RELSET_1, FUNCOP_1, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; begin reserve x,z for set; reserve k for Nat; reserve D for non empty set; definition let B,A be non empty set, b be Element of B; redefine func A --> b -> Element of Funcs(A,B); end; definition let IT be set; attr IT is relation-like means :: MARGREL1:def 1 (for x being set st x in IT holds x is FinSequence) & for a,b being FinSequence st a in IT & b in IT holds len a = len b; end; definition cluster relation-like set; end; definition mode relation is relation-like set; end; reserve X for set; reserve p,r for relation; reserve a,a1,a2,b for FinSequence; canceled 6; theorem :: MARGREL1:7 X c= p implies X is relation-like; theorem :: MARGREL1:8 {a} is relation-like; scheme rel_exist{A() -> set, P[FinSequence]}: ex r st for a holds a in r iff a in A() & P[a] provided for a,b st P[a] & P[b] holds len a = len b; definition let p,r; redefine pred p = r means :: MARGREL1:def 2 for a holds a in p iff a in r; end; definition cluster {} -> relation-like; end; theorem :: MARGREL1:9 for p st for a holds not a in p holds p = {}; definition let p; assume p <> {}; canceled; func the_arity_of p -> Nat means :: MARGREL1:def 4 for a st a in p holds it = len a; end; definition let k; mode relation_length of k -> relation means :: MARGREL1:def 5 for a st a in it holds len a = k; end; definition let X be set; mode relation of X -> relation means :: MARGREL1:def 6 for a st a in it holds rng a c= X; end; canceled 10; theorem :: MARGREL1:20 {} is relation of X; theorem :: MARGREL1:21 {} is relation_length of k; definition let X, k; mode relation of X,k -> relation means :: MARGREL1:def 7 it is relation of X & it is relation_length of k; end; definition let D; func relations_on D -> set means :: MARGREL1:def 8 for X holds X in it iff X c= D* & for a,b being FinSequence of D st a in X & b in X holds len a = len b; end; definition let D; cluster relations_on D -> non empty; end; definition let D be non empty set; mode relation of D is Element of relations_on D; end; reserve a,b for FinSequence of D; reserve p,r for Element of relations_on D; canceled 4; theorem :: MARGREL1:26 X c= r implies X is Element of relations_on D; theorem :: MARGREL1:27 {a} is Element of relations_on D; theorem :: MARGREL1:28 for x,y being Element of D holds {<*x,y*>} is Element of relations_on D; definition let D,p,r; redefine pred p = r means :: MARGREL1:def 9 for a holds a in p iff a in r; end; scheme rel_D_exist{D() -> non empty set, P[FinSequence of D()]}: ex r being Element of relations_on D() st for a being FinSequence of D() holds a in r iff P[a] provided for a,b being FinSequence of D() st P[a] & P[b] holds len a = len b; definition let D; func empty_rel(D) -> Element of relations_on D means :: MARGREL1:def 10 not a in it; end; canceled 3; theorem :: MARGREL1:32 empty_rel(D) = {}; definition let D,p; assume p <> empty_rel(D); func the_arity_of p -> Nat means :: MARGREL1:def 11 a in p implies it = len a; end; scheme rel_D_exist2{D() -> non empty set, k() -> Nat, P[FinSequence of D()]}: ex r being Element of relations_on D() st for a being FinSequence of D() st len a = k() holds a in r iff P[a]; definition func BOOLEAN -> set equals :: MARGREL1:def 12 {0,1}; end; definition cluster BOOLEAN -> non empty; end; definition func FALSE -> Element of BOOLEAN equals :: MARGREL1:def 13 0; func TRUE -> Element of BOOLEAN equals :: MARGREL1:def 14 1; end; canceled 3; theorem :: MARGREL1:36 FALSE = 0 & TRUE = 1; theorem :: MARGREL1:37 BOOLEAN = {FALSE,TRUE}; theorem :: MARGREL1:38 FALSE <> TRUE; definition let x be set; attr x is boolean means :: MARGREL1:def 15 x in BOOLEAN; end; definition cluster boolean set; cluster -> boolean Element of BOOLEAN; end; reserve u,v,w for boolean set; theorem :: MARGREL1:39 v = FALSE or v = TRUE; definition let v be boolean set; func 'not' v equals :: MARGREL1:def 16 TRUE if v = FALSE, FALSE if v = TRUE; let w be boolean set; func v '&' w equals :: MARGREL1:def 17 TRUE if v = TRUE & w =TRUE otherwise FALSE; commutativity; end; definition let v be boolean set; cluster 'not' v -> boolean; let w be boolean set; cluster v '&' w -> boolean; end; definition let v be Element of BOOLEAN; redefine func 'not' v -> Element of BOOLEAN; let w be Element of BOOLEAN; func v '&' w -> Element of BOOLEAN; end; theorem :: MARGREL1:40 'not' 'not' v = v; theorem :: MARGREL1:41 (v = FALSE iff 'not' v = TRUE) & (v = TRUE iff 'not' v = FALSE); canceled; theorem :: MARGREL1:43 v <> TRUE iff v = FALSE; canceled; theorem :: MARGREL1:45 (v '&' w = TRUE iff v = TRUE & w = TRUE) & (v '&' w = FALSE iff v = FALSE or w = FALSE); theorem :: MARGREL1:46 v '&' 'not' v = FALSE; theorem :: MARGREL1:47 'not'(v '&''not' v) = TRUE; canceled; theorem :: MARGREL1:49 FALSE '&' v = FALSE; theorem :: MARGREL1:50 TRUE '&' v = v; theorem :: MARGREL1:51 v '&' v = FALSE implies v = FALSE; theorem :: MARGREL1:52 v '&' (w '&' u) = (v '&' w) '&' u; definition let X; func ALL(X) equals :: MARGREL1:def 18 TRUE if not FALSE in X otherwise FALSE; end; definition let X; cluster ALL X -> boolean; end; definition let X; redefine func ALL X -> Element of BOOLEAN; end; theorem :: MARGREL1:53 (not FALSE in X iff ALL(X) = TRUE) & (FALSE in X iff ALL(X) = FALSE);

Back to top