:: 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));