:: Binary Operations on Finite Sequences :: by Wojciech A. Trybulec :: :: Received August 10, 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 NUMBERS, XBOOLE_0, SUBSET_1, FINSEQ_1, FUNCT_1, BINOP_1, FUNCT_2, RELAT_1, FINSEQ_2, SETWISEO, XXREAL_0, CARD_1, ARYTM_3, FUNCOP_1, TARSKI, FUNCT_4, FINSUB_1, ORDINAL4, NAT_1, ARYTM_1, PARTFUN1, FINSOP_1, FUNCT_7; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, BINOP_1, PARTFUN1, FINSEQ_2, FINSEQ_1, FINSEQ_4, RELAT_1, RELSET_1, FUNCT_1, FINSUB_1, SETWISEO, FUNCT_2, NAT_1, FUNCOP_1, FUNCT_4, XXREAL_0; constructors BINOP_1, PARTFUN1, FUNCOP_1, FUNCT_4, SETWISEO, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, FINSEQ_4, RELSET_1, NUMBERS; registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, FINSEQ_1, CARD_1, FINSEQ_2, NAT_1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; begin reserve x,y,y1,y2 for set, D for non empty set, d,d1,d2,d3 for Element of D, F ,G,H,H1,H2 for FinSequence of D, f,f1,f2 for sequence of D, g for BinOp of D, k,n,i,l for Nat, P for Permutation of dom F; definition let D,F,g; assume g is having_a_unity or len F >= 1; func g "**" F -> Element of D means :: FINSOP_1:def 1 it = the_unity_wrt g if g is having_a_unity & len F = 0 otherwise ex f st f.1 = F.1 & (for n being Nat st 0 <> n & n < len F holds f.(n + 1) = g.(f.n,F.(n + 1))) & it = f.(len F); end; theorem :: FINSOP_1:1 len F >= 1 implies ex f st f.1 = F.1 & (for n being Nat st 0 <> n & n < len F holds f.(n + 1) = g.(f.n,F.(n + 1))) & g "**" F = f.(len F); theorem :: FINSOP_1:2 len F >= 1 & (ex f st f.1 = F.1 & (for n being Nat st 0 <> n & n < len F holds f .(n + 1) = g.(f.n,F.(n + 1))) & d = f.(len F)) implies d = g "**" F; definition let A be non empty set, F be sequence of A, p be FinSequence of A; redefine func F +* p -> sequence of A; end; notation let f be FinSequence; synonym findom f for dom f; end; definition let f be FinSequence; redefine func findom f -> Element of Fin NAT; end; theorem :: FINSOP_1:3 (g is having_a_unity or len F >= 1) & g is associative & g is commutative implies g "**" F = g $$(findom F,(NAT-->the_unity_wrt g)+*F); theorem :: FINSOP_1:4 g is having_a_unity or len F >= 1 implies g "**" (F ^ <* d *>) = g.(g "**" F,d); theorem :: FINSOP_1:5 g is associative & (g is having_a_unity or len F >= 1 & len G >= 1) implies g "**" (F ^ G) = g.(g "**" F,g "**" G); theorem :: FINSOP_1:6 g is associative & (g is having_a_unity or len F >= 1) implies g "**" (<* d *> ^ F) = g.(d,g "**" F); theorem :: FINSOP_1:7 g is commutative associative & (g is having_a_unity or len F >= 1 ) & G = F * P implies g "**" F = g "**" G; theorem :: FINSOP_1:8 (g is having_a_unity or len F >= 1) & g is associative commutative & F is one-to-one & G is one-to-one & rng F = rng G implies g "**" F = g "**" G; theorem :: FINSOP_1:9 g is associative commutative & (g is having_a_unity or len F >= 1) & len F = len G & len F = len H & (for k being Nat st k in dom F holds F.k = g.(G.k,H.k)) implies g "**" F = g.(g "**" G,g "**" H); theorem :: FINSOP_1:10 g is having_a_unity implies g "**" <*>D = the_unity_wrt g; theorem :: FINSOP_1:11 g "**" <* d *> = d; theorem :: FINSOP_1:12 g "**" <* d1,d2 *> = g.(d1,d2); theorem :: FINSOP_1:13 g is commutative implies g "**" <* d1,d2 *> = g "**" <* d2,d1 *>; theorem :: FINSOP_1:14 g "**" <* d1,d2,d3 *> = g.(g.(d1,d2),d3); theorem :: FINSOP_1:15 g is commutative implies g "**" <* d1,d2,d3 *> = g "**" <* d2,d1,d3 *>; theorem :: FINSOP_1:16 g "**" (1 |-> d) = d; theorem :: FINSOP_1:17 g "**" (2 |-> d) = g.(d,d); theorem :: FINSOP_1:18 g is associative & (g is having_a_unity or k <> 0 & l <> 0) implies g "**" ((k + l) |-> d) = g.(g "**" (k |-> d),g "**" (l |-> d)); theorem :: FINSOP_1:19 g is associative & (g is having_a_unity or k <> 0 & l <> 0) implies g "**" (k * l |-> d) = g "**" (l |-> (g "**" (k |-> d))); theorem :: FINSOP_1:20 len F = 1 implies g "**" F = F.1; theorem :: FINSOP_1:21 len F = 2 implies g "**" F = g.(F.1,F.2);