### The Mizar article:

### Many-Argument Relations

**by****Edmund Woronowicz**

- Received June 1, 1990
Copyright (c) 1990 Association of Mizar Users

- MML identifier: MARGREL1
- [ 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; definitions TARSKI; theorems TARSKI, ZFMISC_1, FINSEQ_1, FUNCT_2, FUNCOP_1, XBOOLE_0, XBOOLE_1; schemes XBOOLE_0; 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); coherence proof A1: {b} c= B by ZFMISC_1:37; set f = A --> b; dom f = A & rng f = {b} by FUNCOP_1:14,19; hence thesis by A1,FUNCT_2:def 2; end; end; definition let IT be set; attr IT is relation-like means :Def1: (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; existence proof take {}; thus (for x being set st x in {} holds x is FinSequence) & for a,b being FinSequence st a in {} & b in {} holds len a = len b; end; 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 X c= p implies X is relation-like proof assume A1: x in X implies x in p; thus (for x st x in X holds x is FinSequence) proof let x; assume x in X; then x in p by A1; hence thesis by Def1; end; thus for a,b st a in X & b in X holds len a = len b proof let a,b; assume a in X & b in X; then a in p & b in p by A1; hence thesis by Def1; end; end; theorem {a} is relation-like proof thus for z st z in {a} holds z is FinSequence by TARSKI:def 1; thus for a1,a2 st a1 in {a} & a2 in {a} holds len a1 = len a2 proof let a1,a2; assume a1 in {a} & a2 in {a}; then a1 = a & a2 = a by TARSKI:def 1; hence thesis; end; end; scheme rel_exist{A() -> set, P[FinSequence]}: ex r st for a holds a in r iff a in A() & P[a] provided A1: for a,b st P[a] & P[b] holds len a = len b proof defpred _P[set] means ex a st P[a] & $1 = a; consider X such that A2: x in X iff x in A() & _P[x] from Separation; A3: for x being set st x in X holds x is FinSequence proof let x be set; assume x in X; then ex a st P[a] & x = a by A2; hence x is FinSequence; end; for a,b st a in X & b in X holds len a = len b proof let a,b; assume that A4: a in X and A5: b in X; A6: ex c being FinSequence st P[c] & a = c by A2,A4; ex d being FinSequence st P[d] & b = d by A2,A5; hence thesis by A1,A6; end; then reconsider r = X as relation by A3,Def1; for a holds a in r iff a in A() & P[a] proof let a; now assume A7: a in r; then ex c being FinSequence st P[c] & a = c by A2; hence a in A() & P[a] by A2,A7; end; hence thesis by A2; end; hence thesis; end; definition let p,r; redefine pred p = r means for a holds a in p iff a in r; compatibility proof thus p = r implies (for a holds a in p iff a in r); thus (for a holds a in p iff a in r) implies p = r proof assume A1: for a holds a in p iff a in r; now let x; A2: now assume A3: x in p; then x is FinSequence by Def1; hence x in r by A1,A3; end; now assume A4: x in r; then x is FinSequence by Def1; hence x in p by A1,A4; end; hence x in p iff x in r by A2; end; hence thesis by TARSKI:2; end; end; end; definition cluster {} -> relation-like; coherence proof thus (for x being set st x in {} holds x is FinSequence) & for a,b being FinSequence st a in {} & b in {} holds len a = len b; end; end; theorem Th9: for p st for a holds not a in p holds p = {} proof let p such that A1: for a holds not a in p; assume p <> {}; then consider x being set such that A2: x in p by XBOOLE_0:def 1; x is FinSequence by A2,Def1; hence contradiction by A1,A2; end; definition let p; assume A1: p <> {}; canceled; func the_arity_of p -> Nat means for a st a in p holds it = len a; existence proof consider c being FinSequence such that A2: c in p by A1,Th9; for a st a in p holds len c = len a by A2,Def1; hence thesis; end; uniqueness proof let n1,n2 be Nat; assume that A3: for a st a in p holds n1 = len a and A4: for a st a in p holds n2 = len a; consider a such that A5: a in p by A1,Th9; len a = n1 & len a = n2 by A3,A4,A5; hence thesis; end; end; definition let k; mode relation_length of k -> relation means for a st a in it holds len a = k; existence proof take {}; thus thesis; end; end; definition let X be set; mode relation of X -> relation means for a st a in it holds rng a c= X; existence proof take {}; thus thesis; end; end; canceled 10; theorem Th20: {} is relation of X proof thus a in {} implies rng a c= X; end; theorem Th21: {} is relation_length of k proof thus a in {} implies len a = k; end; definition let X, k; mode relation of X,k -> relation means it is relation of X & it is relation_length of k; existence proof take {}; thus thesis by Th20,Th21; end; end; definition let D; func relations_on D -> set means :Def8: 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; existence proof defpred P[set] means ex Y being set st Y = $1 & Y c= D* & for a,b being FinSequence of D st a in Y & b in Y holds len a = len b; consider A being set such that A1: for x holds x in A iff x in bool(D*) & P[x] from Separation; take A; for X being set holds X in A iff X c= D* & for a,b being FinSequence of D st a in X & b in X holds len a = len b proof let X be set; thus X in A implies X c= D* & for a,b being FinSequence of D st a in X & b in X holds len a = len b proof assume X in A; then ex Y being set st Y = X & Y c= D* & for a,b being FinSequence of D st a in Y & b in Y holds len a=len b by A1; hence thesis; end; thus X c= D* & (for a,b being FinSequence of D st a in X & b in X holds len a = len b) implies X in A by A1; end; hence thesis; end; uniqueness proof let A1,A2 be set; assume that A2: for X being set holds X in A1 iff X c= D* & for a,b being FinSequence of D st a in X & b in X holds len a=len b and A3: for X being set holds X in A2 iff X c= D* & for a,b being FinSequence of D st a in X & b in X holds len a=len b; for x being set holds x in A1 iff x in A2 proof let x; thus x in A1 implies x in A2 proof assume x in A1; then x c= D* & for a,b being FinSequence of D st a in x & b in x holds len a=len b by A2; hence thesis by A3; end; thus x in A2 implies x in A1 proof assume x in A2; then x c= D* & for a,b being FinSequence of D st a in x & b in x holds len a=len b by A3; hence thesis by A2; end; end; hence thesis by TARSKI:2; end; end; definition let D; cluster relations_on D -> non empty; coherence proof defpred P[set] means ex Y being set st Y = $1 & Y c= D* & for a,b being FinSequence of D st a in Y & b in Y holds len a = len b; consider XX being set such that A1: for x holds x in XX iff x in bool(D*) & P[x] from Separation; A2: {} c= D* by XBOOLE_1:2; for a,b being FinSequence of D st a in {} & b in {} holds len a = len b; then reconsider A = XX as non empty set by A1,A2; for X being set holds X in A iff X c= D* & for a,b being FinSequence of D st a in X & b in X holds len a = len b proof let X be set; thus X in A implies X c= D* & for a,b being FinSequence of D st a in X & b in X holds len a = len b proof assume X in A; then ex Y being set st Y = X & Y c= D* & for a,b being FinSequence of D st a in Y & b in Y holds len a=len b by A1; hence thesis; end; thus X c= D* & (for a,b being FinSequence of D st a in X & b in X holds len a = len b) implies X in A by A1; end; hence thesis by Def8; end; 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 X c= r implies X is Element of relations_on D proof assume A1: X c= r; X in relations_on D proof r c= D* by Def8; then A2: X c= D* by A1,XBOOLE_1:1; for a,b st a in X & b in X holds len a = len b by A1,Def8; hence thesis by A2,Def8; end; hence thesis; end; theorem {a} is Element of relations_on D proof {a} in relations_on D proof a in D* by FINSEQ_1:def 11; then A1: {a} c= D* by ZFMISC_1:37; for a1,a2 being FinSequence of D st a1 in {a} & a2 in {a} holds len a1 = len a2 proof let a1,a2 be FinSequence of D; assume a1 in {a} & a2 in {a}; then a1 = a & a2 = a by TARSKI:def 1; hence thesis; end; hence thesis by A1,Def8; end; hence thesis; end; theorem for x,y being Element of D holds {<*x,y*>} is Element of relations_on D proof let x,y be Element of D; {<*x,y*>} in relations_on D proof <*x*>^<*y*> is FinSequence of D; then <*x,y*> is FinSequence of D by FINSEQ_1:def 9; then <*x,y*> in D* by FINSEQ_1:def 11; then A1: {<*x,y*>} c= D* by ZFMISC_1:37; for a1,a2 being FinSequence of D st a1 in {<*x,y*>} & a2 in {<*x,y*>} holds len a1 = len a2 proof let a1,a2 be FinSequence of D; assume a1 in {<*x,y*>} & a2 in {<*x,y*>}; then a1 = <*x,y*> & a2 = <*x,y*> by TARSKI:def 1; hence thesis; end; hence thesis by A1,Def8; end; hence thesis; end; definition let D,p,r; redefine pred p = r means :Def9: for a holds a in p iff a in r; compatibility proof thus p = r implies (for a holds a in p iff a in r); thus (for a holds a in p iff a in r) implies p = r proof assume A1: for a holds a in p iff a in r; now let x; A2: now A3: p is Subset of D* by Def8; assume A4: x in p; then x is FinSequence of D by A3,FINSEQ_1:def 11; hence x in r by A1,A4; end; now A5: r is Subset of D* by Def8; assume A6: x in r; then x is FinSequence of D by A5,FINSEQ_1:def 11; hence x in p by A1,A6; end; hence x in p iff x in r by A2; end; hence thesis by TARSKI:2; end; end; 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 A1: for a,b being FinSequence of D() st P[a] & P[b] holds len a = len b proof defpred _P[set] means ex a being FinSequence of D() st P[a] & $1 = a; consider X being set such that A2: x in X iff x in D()* & _P[x] from Separation; A3: X c= D()* proof for x holds x in X implies x in D()* by A2; hence thesis by TARSKI:def 3; end; for a,b being FinSequence of D() st a in X & b in X holds len a = len b proof let a,b be FinSequence of D(); assume that A4: a in X and A5: b in X; A6: ex c being FinSequence of D() st P[c] & a = c by A2,A4; ex d being FinSequence of D() st P[d] & b = d by A2,A5; hence thesis by A1,A6; end; then reconsider r = X as Element of relations_on D() by A3,Def8; for a being FinSequence of D() holds a in r iff P[a] proof let a be FinSequence of D(); A7: now assume a in r; then ex c being FinSequence of D() st P[c] & a = c by A2; hence P[a]; end; now assume A8: P[a]; a in D()* by FINSEQ_1:def 11; hence a in r by A2,A8; end; hence thesis by A7; end; hence thesis; end; definition let D; func empty_rel(D) -> Element of relations_on D means :Def10: not a in it; existence proof defpred P[FinSequence of D] means $1 in {} & contradiction; A1: P[a] & P[b] implies len a = len b; consider r such that A2: for a holds a in r iff P[a] from rel_D_exist(A1); take r; thus thesis by A2; end; uniqueness proof let r1,r2 be Element of relations_on D; assume that A3: not a in r1 and A4: not a in r2; for a holds ( a in r1 iff a in r2) by A3,A4; hence r1 = r2 by Def9; end; end; canceled 3; theorem empty_rel(D) = {} proof assume A1: not thesis; consider x being Element of empty_rel(D); empty_rel(D) is Subset of D* by Def8; then x in D* by A1,TARSKI:def 3; then reconsider a = x as FinSequence of D by FINSEQ_1:def 11; a in empty_rel(D) by A1; hence contradiction by Def10; end; definition let D,p; assume A1: p <> empty_rel(D); func the_arity_of p -> Nat means a in p implies it = len a; existence proof consider c being FinSequence of D such that A2: c in p by A1,Def10; a in p implies len c = len a by A2,Def8; hence thesis; end; uniqueness proof let n1,n2 be Nat; assume that A3: a in p implies n1 = len a and A4: a in p implies n2 = len a; consider a such that A5: a in p by A1,Def10; len a = n1 & len a = n2 by A3,A4,A5; hence thesis; end; 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] proof defpred _P[set] means ex a being FinSequence of D() st len a = k() & P[a] & $1 = a; consider X being set such that A1: x in X iff x in D()* & _P[x] from Separation; A2: X c= D()* proof for x holds x in X implies x in D()* by A1; hence thesis by TARSKI:def 3; end; for a,b being FinSequence of D() st a in X & b in X holds len a = len b proof let a,b be FinSequence of D(); assume that A3: a in X and A4: b in X; A5: ex c being FinSequence of D() st len c = k() & P[c] & a = c by A1,A3; ex d being FinSequence of D() st len d = k() & P[d] & b = d by A1,A4; hence len a = len b by A5; end; then reconsider r = X as Element of relations_on D() by A2,Def8; for a being FinSequence of D() st len a = k() holds a in r iff P[a] proof let a be FinSequence of D() such that A6: len a = k(); A7: now assume a in r; then ex c being FinSequence of D() st len c = k() & P[c] & a = c by A1; hence P[a]; end; now assume A8: P[a]; a in D()* by FINSEQ_1:def 11; hence a in r by A1,A6,A8; end; hence thesis by A7; end; hence thesis; end; definition func BOOLEAN -> set equals :Def12: {0,1}; coherence; end; definition cluster BOOLEAN -> non empty; coherence by Def12; end; definition func FALSE -> Element of BOOLEAN equals :Def13: 0; coherence by Def12,TARSKI:def 2; func TRUE -> Element of BOOLEAN equals :Def14: 1; coherence by Def12,TARSKI:def 2; end; canceled 3; theorem FALSE = 0 & TRUE = 1 by Def13,Def14; theorem BOOLEAN = {FALSE,TRUE} by Def12,Def13,Def14; theorem FALSE <> TRUE by Def13,Def14; definition let x be set; attr x is boolean means :Def15: x in BOOLEAN; end; definition cluster boolean set; existence proof take FALSE; thus thesis by Def15; end; cluster -> boolean Element of BOOLEAN; coherence by Def15; end; reserve u,v,w for boolean set; theorem Th39: v = FALSE or v = TRUE proof v in BOOLEAN by Def15; hence thesis by Def12,Def13,Def14,TARSKI:def 2; end; definition let v be boolean set; func 'not' v equals :Def16: TRUE if v = FALSE, FALSE if v = TRUE; correctness; let w be boolean set; func v '&' w equals :Def17: TRUE if v = TRUE & w =TRUE otherwise FALSE; correctness; commutativity; end; definition let v be boolean set; cluster 'not' v -> boolean; coherence proof v in BOOLEAN by Def15; then v = FALSE or v = TRUE by Def12,Def13,Def14,TARSKI:def 2; hence thesis by Def16; end; let w be boolean set; cluster v '&' w -> boolean; correctness proof v = TRUE & w = TRUE or not(v = TRUE & w = TRUE); hence thesis by Def17; end; end; definition let v be Element of BOOLEAN; redefine func 'not' v -> Element of BOOLEAN; correctness by Def15; let w be Element of BOOLEAN; func v '&' w -> Element of BOOLEAN; correctness by Def15; end; theorem Th40: 'not' 'not' v = v proof A1: now assume v = TRUE; then 'not' v = FALSE by Def16; hence 'not' 'not' v = TRUE by Def16; end; now assume v = FALSE; then 'not' v = TRUE by Def16; hence 'not' 'not' v = FALSE by Def16; end; hence thesis by A1,Th39; end; theorem Th41: (v = FALSE iff 'not' v = TRUE) & (v = TRUE iff 'not' v = FALSE) proof thus v = FALSE implies 'not' v = TRUE by Def16; thus 'not' v = TRUE implies v = FALSE proof assume 'not' v = TRUE; then 'not' 'not' v = FALSE by Def16; hence thesis by Th40; end; thus v = TRUE implies 'not' v = FALSE by Def16; thus 'not' v = FALSE implies v = TRUE proof assume 'not' v = FALSE; then 'not' 'not' v = TRUE by Def16; hence thesis by Th40; end; end; canceled; theorem v <> TRUE iff v = FALSE by Def13,Def14,Th39; canceled; theorem Th45: (v '&' w = TRUE iff v = TRUE & w = TRUE) & (v '&' w = FALSE iff v = FALSE or w = FALSE) proof thus v '&' w = TRUE implies v = TRUE & w = TRUE by Def13,Def14,Def17; thus v = TRUE & w = TRUE implies v '&' w = TRUE by Def17; thus v '&' w = FALSE implies v = FALSE or w = FALSE proof assume v '&' w = FALSE; then not (v = TRUE & w = TRUE) by Def13,Def14,Def17; hence thesis by Th39; end; assume v = FALSE or w = FALSE; hence thesis by Def13,Def14,Def17; end; theorem Th46: v '&' 'not' v = FALSE proof A1: now assume v = TRUE; then 'not' v = FALSE by Th41; hence v '&''not' v = FALSE by Th45; end; v = FALSE implies v '&''not' v = FALSE by Th45; hence thesis by A1,Th39; end; theorem 'not'(v '&''not' v) = TRUE proof v '&''not' v = FALSE by Th46; hence thesis by Th41; end; canceled; theorem FALSE '&' v = FALSE by Th45; theorem TRUE '&' v = v proof A1: v = TRUE implies thesis by Th45; v = FALSE implies thesis by Th45; hence thesis by A1,Th39; end; theorem v '&' v = FALSE implies v = FALSE by Th45; theorem v '&' (w '&' u) = (v '&' w) '&' u proof A1: now assume A2: v = TRUE; A3: now assume w = TRUE; A4: u = TRUE implies thesis by A2; now assume A5: u = FALSE; then w '&' u = FALSE by Th45; then v '&' (w '&' u) = FALSE by Th45; hence thesis by A5,Th45; end; hence thesis by A4,Th39; end; now assume A6: w = FALSE; A7: now assume u = TRUE; w '&' u = FALSE by A6,Th45; then A8: v '&' (w '&' u) = FALSE by Th45; v '&' w = FALSE by A6,Th45; hence thesis by A8,Th45; end; now assume A9: u = FALSE; then w '&' u = FALSE by Th45; then v '&' (w '&' u) = FALSE by Th45; hence thesis by A9,Th45; end; hence thesis by A7,Th39; end; hence thesis by A3,Th39; end; now assume A10: v = FALSE; then A11: v '&' (w '&' u) = FALSE by Th45; v '&' w = FALSE by A10,Th45; hence thesis by A11,Th45; end; hence thesis by A1,Th39; end; definition let X; func ALL(X) equals :Def18: TRUE if not FALSE in X otherwise FALSE; correctness; end; definition let X; cluster ALL X -> boolean; correctness proof FALSE in X or not FALSE in X; hence thesis by Def18; end; end; definition let X; redefine func ALL X -> Element of BOOLEAN; correctness by Def15; end; theorem (not FALSE in X iff ALL(X) = TRUE) & (FALSE in X iff ALL(X) = FALSE) by Def13,Def14,Def18;

Back to top