:: Three-Argument Operations and Four-Argument Operations :: by Michal Muzalewski and Wojciech Skaba :: :: Received October 2, 1990 :: Copyright (c) 1990-2018 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 FUNCT_1, XBOOLE_0, SUBSET_1, ZFMISC_1, MULTOP_1; notations XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, FUNCT_1, FUNCT_2, MCART_1, DOMAIN_1; constructors FUNCT_2, DOMAIN_1, RELSET_1, XTUPLE_0; registrations XBOOLE_0, SUBSET_1, RELSET_1; requirements SUBSET, BOOLE; theorems FUNCT_2, MCART_1, XTUPLE_0; schemes FUNCT_2; begin :: THREE ARGUMENT OPERATIONS definition let f be Function; let a,b,c be object; func f.(a,b,c) -> set equals f.[a,b,c]; correctness; end; reserve A,B,C,D,E for non empty set, a for Element of A, b for Element of B, c for Element of C, d for Element of D, X,Y,Z,S for set,x,y,z,s,t for object; definition let A,B,C,D; let f be Function of [:A,B,C:],D; let a,b,c; redefine func f.(a,b,c) -> Element of D; coherence proof f.([a,b,c]) is Element of D; hence thesis; end; end; theorem Th1: for f1,f2 being Function of [:X,Y,Z:],D st for x,y,z st x in X & y in Y & z in Z holds f1.[x,y,z] = f2.[x,y,z] holds f1 = f2 proof let f1,f2 be Function of [:X,Y,Z:],D such that A1: for x,y,z st x in X & y in Y & z in Z holds f1.[x,y,z] = f2.[x,y,z]; for t being object st t in [:X,Y,Z:] holds f1.t = f2.t proof let t be object; assume t in [:X,Y,Z:]; then ex x,y,z st x in X & y in Y & z in Z & t = [x,y,z] by MCART_1:68; hence thesis by A1; end; hence thesis by FUNCT_2:12; end; theorem Th2: for f1,f2 being Function of [:A,B,C:],D st for a,b,c holds f1.[a, b,c] = f2.[a,b,c] holds f1 = f2 proof let f1,f2 be Function of [:A,B,C:],D; assume for a,b,c holds f1.[a,b,c] = f2.[a,b,c]; then for x,y,z st x in A & y in B & z in C holds f1.[x,y,z] = f2.[x,y,z]; hence thesis by Th1; end; theorem for f1,f2 being Function of [:A,B,C:],D st for a being Element of A for b being Element of B for c being Element of C holds f1.(a,b,c) = f2.(a,b,c) holds f1 = f2 proof let f1,f2 be Function of [:A,B,C:],D such that A1: for a being Element of A for b being Element of B for c being Element of C holds f1.(a,b,c) = f2.(a,b,c); for a being Element of A for b being Element of B for c being Element of C holds f1.[a,b,c] = f2.[a,b,c] proof let a be Element of A; let b be Element of B; let c be Element of C; f1.(a,b,c) = f1.[a,b,c] & f2.(a,b,c) = f2.[a,b,c]; hence thesis by A1; end; hence thesis by Th2; end; definition let A be set; mode TriOp of A is Function of [:A,A,A:],A; end; scheme FuncEx3D { X,Y,Z,T() -> non empty set, P[object,object,object,object] } : ex f being Function of [:X(),Y(),Z():],T() st for x being Element of X() for y being Element of Y() for z being Element of Z() holds P[x,y,z,f.[x,y,z]] provided A1: for x being Element of X() for y being Element of Y() for z being Element of Z() ex t being Element of T() st P[x,y,z,t] proof defpred Q[set,set] means ( for x being (Element of X()), y being (Element of Y()), z being Element of Z() st \$1 = [x,y,z] holds P[x,y,z,\$2]); A2: for p being Element of [:X(),Y(),Z():] ex t being Element of T() st Q[p, t] proof let p be Element of [:X(),Y(),Z():]; consider x1, y1, z1 be object such that A3: x1 in X() and A4: y1 in Y() and A5: z1 in Z() and A6: p = [x1,y1,z1] by MCART_1:68; reconsider z1 as Element of Z() by A5; reconsider y1 as Element of Y() by A4; reconsider x1 as Element of X() by A3; consider t being Element of T() such that A7: P[x1,y1,z1,t] by A1; take t; let x be (Element of X()), y be (Element of Y()), z be Element of Z(); assume A8: p = [x,y,z]; then x1 = x & y1 = y by A6,XTUPLE_0:3; hence thesis by A6,A7,A8,XTUPLE_0:3; end; consider f being Function of [:X(),Y(),Z():],T() such that A9: for p being Element of [:X(),Y(),Z():] holds Q[p,f.p] from FUNCT_2: sch 3 (A2); take f; let x be Element of X(); let y be Element of Y(); let z be Element of Z(); thus thesis by A9; end; scheme TriOpEx { A()->non empty set, P[ Element of A(), Element of A(), Element of A(), Element of A()] }: ex o being TriOp of A() st for a,b,c being Element of A () holds P[a,b,c,o.(a,b,c)] provided A1: for x,y,z being Element of A() ex t being Element of A() st P[x,y,z, t] proof defpred Q[Element of A(),Element of A(),Element of A(),Element of A()] means for r being Element of A() st r = \$4 holds P[\$1,\$2,\$3,r]; A2: for x,y,z being Element of A() ex t being Element of A() st Q[x,y,z,t] proof let x,y,z be Element of A(); consider t being Element of A() such that A3: P[x,y,z,t] by A1; take t; thus thesis by A3; end; consider f being Function of [:A(),A(),A():],A() such that A4: for a,b,c being Element of A() holds Q[a,b,c,f.[a,b,c]] from FuncEx3D(A2 ); take f; let a,b,c be Element of A(); thus thesis by A4; end; scheme Lambda3D { X, Y, Z, T()->non empty set, F( Element of X(), Element of Y(), Element of Z()) -> Element of T() }: ex f being Function of [:X(),Y(),Z():],T() st for x being Element of X() for y being Element of Y() for z being Element of Z() holds f.[x,y,z]=F(x,y,z) proof defpred Q[Element of X(),Element of Y(),Element of Z(),Element of T()] means \$4 = F(\$1,\$2,\$3); A1: for x being Element of X() for y being Element of Y() for z being Element of Z() ex t being Element of T() st Q[x,y,z,t]; ex f being Function of [:X(),Y(),Z():],T() st for x being Element of X() for y being Element of Y() for z being Element of Z() holds Q[x,y,z,f.[x,y,z]] from FuncEx3D(A1); hence thesis; end; scheme TriOpLambda { A,B,C,D()->non empty set, O( Element of A(), Element of B(), Element of C()) -> Element of D() }: ex o being Function of [:A(),B(),C():],D() st for a being Element of A(), b being Element of B(), c being Element of C() holds o.(a,b,c) = O(a,b,c) proof consider f being Function of [:A(),B(),C():],D() such that A1: for a being Element of A(), b being Element of B(), c being Element of C() holds f.[a,b,c] = O(a,b,c) from Lambda3D; take f; let a be Element of A(), b be Element of B(), c be Element of C(); thus thesis by A1; end; :: FOUR ARGUMENT OPERATIONS definition let f be Function; let a,b,c,d be set; func f.(a,b,c,d) -> set equals f.[a,b,c,d]; correctness; end; definition let A,B,C,D,E; let f be Function of [:A,B,C,D:],E; let a,b,c,d; redefine func f.(a,b,c,d) -> Element of E; coherence proof f.([a,b,c,d]) is Element of E; hence thesis; end; end; theorem Th4: for f1,f2 being Function of [:X,Y,Z,S:],D st for x,y,z,s st x in X & y in Y & z in Z & s in S holds f1.[x,y,z,s] = f2.[x,y,z,s] holds f1 = f2 proof let f1,f2 be Function of [:X,Y,Z,S:],D such that A1: for x,y,z,s st x in X & y in Y & z in Z & s in S holds f1.[x,y,z,s] = f2.[x,y,z,s]; for t being object st t in [:X,Y,Z,S:] holds f1.t = f2.t proof let t be object; assume t in [:X,Y,Z,S:]; then ex x,y,z,s st x in X & y in Y & z in Z & s in S & t = [x,y,z,s] by MCART_1:79; hence thesis by A1; end; hence thesis by FUNCT_2:12; end; theorem Th5: for f1,f2 being Function of [:A,B,C,D:],E st for a,b,c,d holds f1 .[a,b,c,d] = f2.[a,b,c,d] holds f1 = f2 proof let f1,f2 be Function of [:A,B,C,D:],E; assume for a,b,c,d holds f1.[a,b,c,d] = f2.[a,b,c,d]; then for x,y,z,s st x in A & y in B & z in C & s in D holds f1.[x,y,z,s] = f2 .[x,y,z,s]; hence thesis by Th4; end; theorem for f1,f2 being Function of [:A,B,C,D:],E st for a,b,c,d holds f1.(a,b ,c,d) = f2.(a,b,c,d) holds f1 = f2 proof let f1,f2 be Function of [:A,B,C,D:],E such that A1: for a,b,c,d holds f1.(a,b,c,d) = f2.(a,b,c,d); for a,b,c,d holds f1.[a,b,c,d] = f2.[a,b,c,d] proof let a,b,c,d; f1.(a,b,c,d) = f1.[a,b,c,d] & f2.(a,b,c,d) = f2.[a,b,c,d]; hence thesis by A1; end; hence thesis by Th5; end; definition let A; mode QuaOp of A is Function of [:A,A,A,A:],A; end; scheme FuncEx4D { X, Y, Z, S, T() -> non empty set, P[object,object,object,object,object] }: ex f being Function of [:X(),Y(),Z(),S():],T() st for x being Element of X() for y being Element of Y() for z being Element of Z() for s being Element of S() holds P[x,y,z,s,f.[x,y,z,s]] provided A1: for x being Element of X() for y being Element of Y() for z being Element of Z() for s being Element of S() ex t being Element of T() st P[x,y,z, s,t] proof defpred Q[set,set] means for x being (Element of X()), y being (Element of Y ()), z being (Element of Z()), s being Element of S() st \$1 = [x,y,z,s] holds P [x,y,z,s,\$2]; A2: for p being Element of [:X(),Y(),Z(),S():] ex t being Element of T() st Q[p,t] proof let p be Element of [:X(),Y(),Z(),S():]; consider x1, y1, z1, s1 be object such that A3: x1 in X() and A4: y1 in Y() and A5: z1 in Z() and A6: s1 in S() and A7: p = [x1,y1,z1,s1] by MCART_1:79; reconsider s1 as Element of S() by A6; reconsider z1 as Element of Z() by A5; reconsider y1 as Element of Y() by A4; reconsider x1 as Element of X() by A3; consider t being Element of T() such that A8: P[x1,y1,z1,s1,t] by A1; take t; let x be Element of X(), y be Element of Y(), z be Element of Z(), s be Element of S(); assume A9: p = [x,y,z,s]; then A10: z1 = z by A7,XTUPLE_0:5; x1 = x & y1 = y by A7,A9,XTUPLE_0:5; hence thesis by A7,A8,A9,A10,XTUPLE_0:5; end; consider f being Function of [:X(),Y(),Z(),S():],T() such that A11: for p being Element of [:X(),Y(),Z(),S():] holds Q[p,f.p] from FUNCT_2:sch 3(A2); take f; let x be Element of X(); let y be Element of Y(); let z be Element of Z(); let s be Element of S(); thus thesis by A11; end; scheme QuaOpEx { A()->non empty set, P[ Element of A(), Element of A(), Element of A(), Element of A(), Element of A()] }: ex o being QuaOp of A() st for a,b,c,d being Element of A() holds P[a,b,c,d,o.(a,b,c,d)] provided A1: for x,y,z,s being Element of A() ex t being Element of A() st P[x,y, z,s,t] proof defpred Q[Element of A(), Element of A(),Element of A(), Element of A(), Element of A()] means for r being Element of A() st r = \$5 holds P[\$1,\$2,\$3,\$4, \$5]; A2: for x,y,z,s being Element of A() ex t being Element of A() st Q[x,y,z,s, t] proof let x,y,z,s be Element of A(); consider t being Element of A() such that A3: P[x,y,z,s,t] by A1; take t; thus thesis by A3; end; consider f being Function of [:A(),A(),A(),A():],A() such that A4: for a,b,c,d being Element of A() holds Q[a,b,c,d,f.[a,b,c,d]] from FuncEx4D(A2); take f; let a,b,c,d be Element of A(); thus thesis by A4; end; scheme Lambda4D { X, Y, Z, S, T() -> non empty set, F( Element of X(), Element of Y (), Element of Z(), Element of S()) -> Element of T() }: ex f being Function of [:X(),Y(),Z(),S():],T() st for x being Element of X() for y being Element of Y( ) for z being Element of Z() for s being Element of S() holds f.[x,y,z,s]=F(x,y ,z,s) proof defpred P[Element of X(),Element of Y(),Element of Z(),Element of S(), Element of T()] means \$5 = F(\$1,\$2,\$3,\$4); A1: for x being Element of X() for y being Element of Y() for z being Element of Z() for s being Element of S() ex t being Element of T() st P[x,y,z, s,t]; ex f being Function of [:X(),Y(),Z(),S():],T() st for x being Element of X() for y being Element of Y() for z being Element of Z() for s being Element of S() holds P[x,y,z,s,f.[x,y,z,s]] from FuncEx4D(A1); hence thesis; end; scheme QuaOpLambda { A()->non empty set, O( Element of A(), Element of A(), Element of A(), Element of A()) -> Element of A() }: ex o being QuaOp of A() st for a,b ,c,d being Element of A() holds o.(a,b,c,d) = O(a,b,c,d) proof deffunc F(Element of A(),Element of A(),Element of A(),Element of A()) = O( \$1,\$2,\$3,\$4); consider f being Function of [:A(),A(),A(),A():],A() such that A1: for a,b,c,d being Element of A() holds f.[a,b,c,d] = F(a,b,c,d) from Lambda4D; take f; let a,b,c,d be Element of A(); thus thesis by A1; end;