:: Three-Argument Operations and Four-Argument Operations
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 2, 1990
:: Copyright (c) 1990-2019 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;
begin :: THREE ARGUMENT OPERATIONS
definition
let f be Function;
let a,b,c be object;
func f.(a,b,c) -> set equals
:: MULTOP_1:def 1
f.[a,b,c];
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;
end;
theorem :: MULTOP_1:1
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;
theorem :: MULTOP_1:2
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;
theorem :: MULTOP_1:3
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;
definition
let A be set;
mode TriOp of A is Function of [:A,A,A:],A;
end;
scheme :: MULTOP_1:sch 1
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
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];
scheme :: MULTOP_1:sch 2
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
for x,y,z being Element of A() ex t being Element of A() st P[x,y,z, t];
scheme :: MULTOP_1:sch 3
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);
scheme :: MULTOP_1:sch 4
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);
:: FOUR ARGUMENT OPERATIONS
definition
let f be Function;
let a,b,c,d be set;
func f.(a,b,c,d) -> set equals
:: MULTOP_1:def 2
f.[a,b,c,d];
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;
end;
theorem :: MULTOP_1:4
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;
theorem :: MULTOP_1:5
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;
theorem :: MULTOP_1:6
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;
definition
let A;
mode QuaOp of A is Function of [:A,A,A,A:],A;
end;
scheme :: MULTOP_1:sch 5
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
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];
scheme :: MULTOP_1:sch 6
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
for x,y,z,s being Element of A() ex t being Element of A() st P[x,y, z,s,t];
scheme :: MULTOP_1:sch 7
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);
scheme :: MULTOP_1:sch 8
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);