:: Three-Argument Operations and Four-Argument Operations
:: by Michal Muzalewski and Wojciech Skaba
::
:: Received October 2, 1990
:: Copyright (c) 1990-2026 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; :: redefines . (MULTOP_1, definition)
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; :: redefines . (MULTOP_1, definition)
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;