The abstract of the Mizar article:

Binary Operations on Finite Sequences

by

Wojciech A. Trybulec

Received August 10, 1990

MML identifier: FINSOP_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FINSEQ_1, FUNCT_1, BINOP_1, FUNCT_2, RELAT_1, FINSEQ_2, SETWISEO,
      FUNCOP_1, FUNCT_4, BOOLE, FINSUB_1, ARYTM_1, FINSEQ_4, FINSOP_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, BINOP_1,
      FINSEQ_2, FINSEQ_1, FINSEQ_4, RELAT_1, RELSET_1, FUNCT_1, FINSUB_1,
      SETWISEO, FUNCT_2, NAT_1, FUNCOP_1, FUNCT_4;
 constructors BINOP_1, FINSEQ_4, SETWISEO, REAL_1, NAT_1, FUNCOP_1, FUNCT_4,
      FINSEQ_2, XREAL_0, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, RELSET_1, XREAL_0, FINSEQ_1, ARYTM_3, FUNCT_2, MEMBERED,
      ZFMISC_1, XBOOLE_0, ORDINAL2, SUBSET_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 Function of NAT,D,
        g for BinOp of D,
        k,n,i,j,l for Nat,
        P for Permutation of dom F;

definition let D,n,d;
 redefine func n |-> d -> FinSequence of D;
end;

definition let D,F,g;
 assume  g has_a_unity or len F >= 1;
 func g "**" F -> Element of D means
:: FINSOP_1:def 1
   it = the_unity_wrt g if g has_a_unity & len F = 0 otherwise
    ex f st f.1 = F.1 &
     (for n st 0 <> n & n < len F holds
       f.(n + 1) = g.(f.n,F.(n + 1))) & it = f.(len F);
end;

canceled;

theorem :: FINSOP_1:2
 len F >= 1 implies ex f st f.1 = F.1 & (for n st 0 <> n & n < len F holds
  f.(n + 1) = g.(f.n,F.(n + 1))) & g "**" F = f.(len F);

theorem :: FINSOP_1:3
   len F >= 1 & (ex f st f.1 = F.1 & (for n 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 B,A be non empty set, b be Element of B;
 redefine func A --> b -> Function of A,B;
end;

definition let A be non empty set,
   F be Function of NAT,A, p be FinSequence of A;
 redefine func F +* p -> Function of NAT,A;
end;

definition let f be FinSequence;
 redefine func dom f -> Element of Fin NAT;
end;

theorem :: FINSOP_1:4
   (g has_a_unity or len F >= 1) & g is associative & g is commutative implies
  g "**" F = g $$(dom F,(NAT-->the_unity_wrt g)+*F);

theorem :: FINSOP_1:5
 g has_a_unity or len F >= 1 implies g "**" (F ^ <* d *>) = g.(g "**" F,d);

theorem :: FINSOP_1:6
 g is associative & (g has_a_unity or len F >= 1 & len G >= 1) implies
  g "**" (F ^ G) = g.(g "**" F,g "**" G);

theorem :: FINSOP_1:7
 g is associative & (g has_a_unity or len F >= 1) implies
  g "**" (<* d *> ^ F) = g.(d,g "**" F);

theorem :: FINSOP_1:8
 g is commutative associative & (g has_a_unity or len F >= 1) &
  G = F * P implies g "**" F = g "**" G;

theorem :: FINSOP_1:9
   (g has_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:10
   g is associative commutative & (g has_a_unity or len F >= 1) &
 len F = len G & len F = len H &
 (for k st k in dom F holds F.k = g.(G.k,H.k)) implies
  g "**" F = g.(g "**" G,g "**" H);

theorem :: FINSOP_1:11
   g has_a_unity implies g "**" <*>D = the_unity_wrt g;

theorem :: FINSOP_1:12
   g "**" <* d *> = d;

theorem :: FINSOP_1:13
 g "**" <* d1,d2 *> = g.(d1,d2);

theorem :: FINSOP_1:14
   g is commutative implies g "**" <* d1,d2 *> = g "**" <* d2,d1 *>;

theorem :: FINSOP_1:15
 g "**" <* d1,d2,d3 *> = g.(g.(d1,d2),d3);

theorem :: FINSOP_1:16
   g is commutative implies g "**" <* d1,d2,d3 *> = g "**" <* d2,d1,d3 *>;

theorem :: FINSOP_1:17
 g "**" (1 |-> d) = d;

theorem :: FINSOP_1:18
   g "**" (2 |-> d) = g.(d,d);

theorem :: FINSOP_1:19
 g is associative & (g has_a_unity or k <> 0 & l <> 0) implies
  g "**" ((k + l) |-> d) = g.(g "**" (k |-> d),g "**" (l |-> d));

theorem :: FINSOP_1:20
   g is associative & (g has_a_unity or k <> 0 & l <> 0) implies
  g "**" (k * l |-> d) = g "**" (l |-> (g "**" (k |-> d)));

theorem :: FINSOP_1:21
   len F = 1 implies g "**" F = F.1;

theorem :: FINSOP_1:22
   len F = 2 implies g "**" F = g.(F.1,F.2);