:: Binary Operations Applied to Finite Sequences
:: by Czes{\l}aw Byli\'nski
::
:: Received May 4, 1990
:: Copyright (c) 1990-2021 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 XBOOLE_0, SUBSET_1, FUNCT_1, PARTFUN1, RELAT_1, ZFMISC_1,
FUNCOP_1, TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, ORDINAL4, ARYTM_3, CARD_1,
BINOP_1, SETWISEO, FINSEQOP, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, RELAT_1, EQREL_1, FUNCT_1, FINSEQ_1, RELSET_1, PARTFUN1, FUNCT_2,
BINOP_1, FUNCT_3, FUNCOP_1, FINSEQ_2, SETWISEO;
constructors PARTFUN1, BINOP_1, FUNCT_3, FUNCOP_1, SETWISEO, NAT_1, FINSEQ_2,
RELSET_1, EQREL_1, NUMBERS;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, NAT_1,
FINSEQ_2, ORDINAL1, FINSEQ_1, CARD_1, RELSET_1;
requirements NUMERALS, BOOLE, SUBSET;
begin
reserve x,y for set;
reserve C,C9,D,D9,E for non empty set;
reserve c for Element of C;
reserve c9 for Element of C9;
reserve d,d1,d2,d3,d4,e for Element of D;
reserve d9 for Element of D9;
:: Auxiliary theorems
theorem :: FINSEQOP:1
for f being Function holds <:{},f:> = {} & <:f,{}:> = {};
theorem :: FINSEQOP:2
for f being Function holds [:{},f:] = {} & [:f,{}:] = {};
theorem :: FINSEQOP:3
for F,f being Function holds F.:({},f) = {} & F.:(f,{}) = {};
theorem :: FINSEQOP:4
for F being Function holds F[:]({},x) = {};
theorem :: FINSEQOP:5
for F being Function holds F[;](x,{}) = {};
theorem :: FINSEQOP:6
for X being set, x1,x2 being set holds <:X-->x1,X-->x2:> = X -->[ x1,x2];
theorem :: FINSEQOP:7
for F being Function,X being set, x1,x2 being set st [x1,x2] in
dom F holds F.:(X-->x1,X-->x2) = X --> F.(x1,x2);
reserve i,j for natural Number;
reserve F for Function of [:D,D9:],E;
reserve p,q for FinSequence of D,
p9,q9 for FinSequence of D9;
definition
let D,D9,E,F,p,p9;
redefine func F.:(p,p9) -> FinSequence of E;
end;
definition
let D,D9,E,F,p,d9;
redefine func F[:](p,d9) -> FinSequence of E;
end;
definition
let D,D9,E,F,d,p9;
redefine func F[;](d,p9) -> FinSequence of E;
end;
reserve f,f9 for Function of C,D,
h for Function of D,E;
definition
let D,E be set, p be FinSequence of D, h be Function of D,E;
redefine func h*p -> FinSequence of E;
end;
theorem :: FINSEQOP:8
h*(p^<*d*>) = (h*p)^<*h.d*>;
theorem :: FINSEQOP:9
h*(p^q) = (h*p)^(h*q);
reserve T,T1,T2,T3 for Tuple of i,D;
reserve T9 for Tuple of i, D9;
reserve S for Tuple of j, D;
reserve S9 for Tuple of j, D9;
theorem :: FINSEQOP:10
F.:(T^<*d*>,T9^<*d9*>) = (F.:(T,T9))^<*F.(d,d9)*>;
theorem :: FINSEQOP:11
F.:(T^S,T9^S9) = (F.:(T,T9))^(F.:(S,S9));
theorem :: FINSEQOP:12
F[;](d,p9^<*d9*>) = (F[;](d,p9))^<*F.(d,d9)*>;
theorem :: FINSEQOP:13
F[;](d,p9^q9) = (F[;](d,p9))^(F[;](d,q9));
theorem :: FINSEQOP:14
F[:](p^<*d*>,d9) = (F[:](p,d9))^<*F.(d,d9)*>;
theorem :: FINSEQOP:15
F[:](p^q,d9) = (F[:](p,d9))^(F[:](q,d9));
theorem :: FINSEQOP:16
for h being Function of D,E holds h*(i|->d) = i|->(h.d);
theorem :: FINSEQOP:17
F.:(i|->d,i|->d9) = i |-> (F.(d,d9));
theorem :: FINSEQOP:18
F[;](d,i|->d9) = i |-> (F.(d,d9));
theorem :: FINSEQOP:19
F[:](i|->d,d9) = i |-> (F.(d,d9));
theorem :: FINSEQOP:20
F.:(i|->d,T9) = F[;](d,T9);
theorem :: FINSEQOP:21
F.:(T,i|->d) = F[:](T,d);
theorem :: FINSEQOP:22
F[;](d,T9) = F[;](d,id D9)*T9;
theorem :: FINSEQOP:23
F[:](T,d) = F[:](id D,d)*T;
:: Binary Operations
reserve F,G for BinOp of D;
reserve u for UnOp of D;
reserve H for BinOp of E;
theorem :: FINSEQOP:24
F is associative implies F[;](d,id D)*(F.:(f,f9)) = F.:(F[;](d, id D)*f,f9);
theorem :: FINSEQOP:25
F is associative implies F[:](id D,d)*(F.:(f,f9)) = F.:(f,F[:]( id D,d)*f9);
theorem :: FINSEQOP:26
F is associative implies F[;](d,id D)*(F.:(T1,T2)) = F.:(F[;](d,id D)*
T1,T2 );
theorem :: FINSEQOP:27
F is associative implies F[:](id D,d)*(F.:(T1,T2)) = F.:(T1,F[:](id D,
d)*T2 );
theorem :: FINSEQOP:28
F is associative implies F.:(F.:(T1,T2),T3) = F.:(T1,F.:(T2,T3));
theorem :: FINSEQOP:29
F is associative implies F[:](F[;](d1,T),d2) = F[;](d1,F[:](T,d2));
theorem :: FINSEQOP:30
F is associative implies F.:(F[:](T1,d),T2) = F.:(T1,F[;](d,T2));
theorem :: FINSEQOP:31
F is associative implies F[;](F.(d1,d2),T) = F[;](d1,F[;](d2,T));
theorem :: FINSEQOP:32
F is associative implies F[:](T,F.(d1,d2)) = F[:](F[:](T,d1),d2);
theorem :: FINSEQOP:33
F is commutative implies F.:(T1,T2) = F.:(T2,T1);
theorem :: FINSEQOP:34
F is commutative implies F[;](d,T) = F[:](T,d);
theorem :: FINSEQOP:35
F is_distributive_wrt G implies F[;](G.(d1,d2),f) = G.:(F[;](d1,
f),F[;] (d2,f));
theorem :: FINSEQOP:36
F is_distributive_wrt G implies F[:](f,G.(d1,d2)) = G.:(F[:](f,
d1),F[:] (f,d2));
theorem :: FINSEQOP:37
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F.:(f
,f9)) = H.:(h*f,h*f9);
theorem :: FINSEQOP:38
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[;](
d,f)) = H[;](h.d,h*f);
theorem :: FINSEQOP:39
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[:](
f,d)) = H[:](h*f,h.d);
theorem :: FINSEQOP:40
u is_distributive_wrt F implies u*(F.:(f,f9)) = F.:(u*f,u*f9);
theorem :: FINSEQOP:41
u is_distributive_wrt F implies u*(F[;](d,f)) = F[;](u.d,u*f);
theorem :: FINSEQOP:42
u is_distributive_wrt F implies u*(F[:](f,d)) = F[:](u*f,u.d);
theorem :: FINSEQOP:43
F is having_a_unity implies F.:(C-->the_unity_wrt F,f) = f & F.:
(f,C-->the_unity_wrt F) = f;
theorem :: FINSEQOP:44
F is having_a_unity implies F[;](the_unity_wrt F,f) = f;
theorem :: FINSEQOP:45
F is having_a_unity implies F[:](f,the_unity_wrt F) = f;
theorem :: FINSEQOP:46
F is_distributive_wrt G implies F[;](G.(d1,d2),T) = G.:(F[;](d1,T),F
[;] (d2,T));
theorem :: FINSEQOP:47
F is_distributive_wrt G implies F[:](T,G.(d1,d2)) = G.:(F[:](T,d1),F
[:] (T,d2));
theorem :: FINSEQOP:48
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F.:(
T1,T2)) = H.:(h*T1,h*T2);
theorem :: FINSEQOP:49
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[;](
d,T)) = H[;](h.d,h*T);
theorem :: FINSEQOP:50
(for d1,d2 holds h.(F.(d1,d2)) = H.(h.d1,h.d2)) implies h*(F[:](
T,d)) = H[:](h*T,h.d);
theorem :: FINSEQOP:51
u is_distributive_wrt F implies u*(F.:(T1,T2)) = F.:(u*T1,u*T2);
theorem :: FINSEQOP:52
u is_distributive_wrt F implies u*(F[;](d,T)) = F[;](u.d,u*T);
theorem :: FINSEQOP:53
u is_distributive_wrt F implies u*(F[:](T,d)) = F[:](u*T,u.d);
theorem :: FINSEQOP:54
G is_distributive_wrt F & u = G[;](d,id D) implies u is_distributive_wrt F;
theorem :: FINSEQOP:55
G is_distributive_wrt F & u = G[:](id D,d) implies u is_distributive_wrt F;
theorem :: FINSEQOP:56
F is having_a_unity implies
F.:(i|->the_unity_wrt F,T) = T & F.:(T,i|->the_unity_wrt F) = T;
theorem :: FINSEQOP:57
F is having_a_unity implies F[;](the_unity_wrt F,T) = T;
theorem :: FINSEQOP:58
F is having_a_unity implies F[:](T,the_unity_wrt F) = T;
definition
let D,u,F;
pred u is_an_inverseOp_wrt F means
:: FINSEQOP:def 1
for d holds F.(d,u.d) = the_unity_wrt F & F.(u.d,d) = the_unity_wrt F;
end;
definition
let D,F;
attr F is having_an_inverseOp means
:: FINSEQOP:def 2
ex u st u is_an_inverseOp_wrt F;
end;
definition
let D,F;
assume that
F is having_a_unity and
F is associative and
F is having_an_inverseOp;
func the_inverseOp_wrt F -> UnOp of D means
:: FINSEQOP:def 3
it is_an_inverseOp_wrt F;
end;
theorem :: FINSEQOP:59
F is having_a_unity & F is associative & F is
having_an_inverseOp implies F.((the_inverseOp_wrt F).d,d) = the_unity_wrt F & F
.(d,(the_inverseOp_wrt F).d) = the_unity_wrt F;
theorem :: FINSEQOP:60
F is having_a_unity & F is associative & F is
having_an_inverseOp & F.(d1,d2) = the_unity_wrt F implies d1 = (
the_inverseOp_wrt F).d2 & (the_inverseOp_wrt F).d1 = d2;
theorem :: FINSEQOP:61
F is having_a_unity & F is associative & F is
having_an_inverseOp implies (the_inverseOp_wrt F).(the_unity_wrt F) =
the_unity_wrt F;
theorem :: FINSEQOP:62
F is having_a_unity & F is associative & F is
having_an_inverseOp implies (the_inverseOp_wrt F).((the_inverseOp_wrt F).d) = d
;
theorem :: FINSEQOP:63
F is having_a_unity & F is associative & F is commutative & F is
having_an_inverseOp implies (the_inverseOp_wrt F) is_distributive_wrt F;
theorem :: FINSEQOP:64
F is having_a_unity & F is associative & F is
having_an_inverseOp & (F.(d,d1) = F.(d,d2) or F.(d1,d) = F.(d2,d)) implies d1 =
d2;
theorem :: FINSEQOP:65
F is having_a_unity & F is associative & F is
having_an_inverseOp & (F.(d1,d2) = d2 or F.(d2,d1) = d2) implies d1 =
the_unity_wrt F;
theorem :: FINSEQOP:66
F is associative & F is having_a_unity & F is
having_an_inverseOp & G is_distributive_wrt F & e = the_unity_wrt F implies for
d holds G.(e,d) = e & G.(d,e) = e;
theorem :: FINSEQOP:67
F is having_a_unity & F is associative & F is
having_an_inverseOp & u = the_inverseOp_wrt F & G is_distributive_wrt F implies
u.(G.(d1,d2)) = G.(u.d1,d2) & u.(G.(d1,d2)) = G.(d1,u.d2);
theorem :: FINSEQOP:68
F is having_a_unity & F is associative & F is having_an_inverseOp & u
= the_inverseOp_wrt F & G is_distributive_wrt F & G is having_a_unity implies G
[;](u.(the_unity_wrt G),id D) = u;
theorem :: FINSEQOP:69
F is associative & F is having_a_unity & F is having_an_inverseOp & G
is_distributive_wrt F implies G[;](d,id D).the_unity_wrt F = the_unity_wrt F;
theorem :: FINSEQOP:70
F is associative & F is having_a_unity & F is having_an_inverseOp & G
is_distributive_wrt F implies G[:](id D,d).the_unity_wrt F = the_unity_wrt F;
theorem :: FINSEQOP:71
F is having_a_unity & F is associative & F is
having_an_inverseOp implies F.:(f,(the_inverseOp_wrt F)*f) = C-->the_unity_wrt
F & F.:((the_inverseOp_wrt F)*f,f) = C-->the_unity_wrt F;
theorem :: FINSEQOP:72
F is associative & F is having_an_inverseOp & F is
having_a_unity & F.:(f,f9) = C-->the_unity_wrt F implies f = (the_inverseOp_wrt
F)*f9 & (the_inverseOp_wrt F)*f = f9;
theorem :: FINSEQOP:73
F is having_a_unity & F is associative & F is having_an_inverseOp
implies F.:(T,(the_inverseOp_wrt F)*T) = i|->the_unity_wrt F & F.:((
the_inverseOp_wrt F)*T,T) = i|->the_unity_wrt F;
theorem :: FINSEQOP:74
F is associative & F is having_an_inverseOp & F is having_a_unity & F
.:(T1,T2) = i|->the_unity_wrt F implies T1 = (the_inverseOp_wrt F)*T2 & (
the_inverseOp_wrt F)*T1 = T2;
theorem :: FINSEQOP:75
F is associative & F is having_a_unity & e = the_unity_wrt F & F
is having_an_inverseOp & G is_distributive_wrt F implies G[;](e,f) = C-->e;
theorem :: FINSEQOP:76
F is associative & F is having_a_unity & e = the_unity_wrt F & F is
having_an_inverseOp & G is_distributive_wrt F implies G[;](e,T) = i|->e;
definition
let F,f,g be Function;
func F*(f,g) -> Function equals
:: FINSEQOP:def 4
F*[:f,g:];
end;
theorem :: FINSEQOP:77
for F,f,g being Function st [x,y] in dom(F*(f,g)) holds (F*(f,g)
).(x,y) = F.(f.x,g.y);
::$CT
theorem :: FINSEQOP:79
for F being Function of [:D,D9:],E, f being Function of C,D, g
being Function of C9,D9 holds F*(f,g) is Function of [:C,C9:],E;
theorem :: FINSEQOP:80
for u,u9 being Function of D,D holds F*(u,u9) is BinOp of D;
definition
let D,F;
let f,f9 be Function of D,D;
redefine func F*(f,f9) -> BinOp of D;
end;
theorem :: FINSEQOP:81
for F being Function of [:D,D9:],E, f being Function of C,D, g
being Function of C9,D9 holds (F*(f,g)).(c,c9) = F.(f.c,g.c9);
theorem :: FINSEQOP:82
for u being Function of D,D holds (F*(id D,u)).(d1,d2) = F.(d1,u
.d2) & (F*(u,id D)).(d1,d2) = F.(u.d1,d2);
theorem :: FINSEQOP:83
(F*(id D,u)).:(f,f9) = F.:(f,u*f9);
theorem :: FINSEQOP:84
(F*(id D,u)).:(T1,T2) = F.:(T1,u*T2);
theorem :: FINSEQOP:85
F is associative & F is having_a_unity & F is commutative & F is
having_an_inverseOp & u = the_inverseOp_wrt F implies u.(F*(id D,u).(d1,d2)) =
F*(u,id D).(d1,d2) & F*(id D,u).(d1,d2) = u.(F*(u,id D).(d1,d2));
theorem :: FINSEQOP:86
F is associative & F is having_a_unity & F is having_an_inverseOp
implies (F*(id D,the_inverseOp_wrt F)).(d,d) = the_unity_wrt F;
theorem :: FINSEQOP:87
F is associative & F is having_a_unity & F is having_an_inverseOp
implies (F*(id D,the_inverseOp_wrt F)).(d,the_unity_wrt F) = d;
theorem :: FINSEQOP:88
F is having_a_unity implies (F*(id D,u)).(the_unity_wrt F,d) = u.d;
theorem :: FINSEQOP:89
F is commutative & F is associative & F is having_a_unity & F is
having_an_inverseOp & G = F*(id D,the_inverseOp_wrt F) implies for d1,d2,d3,d4
holds F.(G.(d1,d2),G.(d3,d4))= G.(F.(d1,d3),F.(d2,d4));