The Mizar article:

Many Sorted Algebras

by
Andrzej Trybulec

Received April 21, 1994

Copyright (c) 1994 Association of Mizar Users

MML identifier: MSUALG_1
[ MML identifier index ]


environ

 vocabulary ZF_REFLE, PBOOLE, BOOLE, RELAT_1, FUNCT_1, PRALG_1, TDGROUP,
      CARD_3, FINSEQ_2, FINSEQ_1, FUNCOP_1, FUNCT_2, AMI_1, QC_LANG1, UNIALG_1,
      PARTFUN1, REALSET1, MSUALG_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, NAT_1, RELAT_1, FUNCT_1,
      FUNCT_2, FINSEQ_1, STRUCT_0, FUNCOP_1, PARTFUN1, FINSEQ_2, CARD_3,
      PBOOLE, REALSET1, PRALG_1, UNIALG_1;
 constructors REALSET1, PRALG_1, MEMBERED, XBOOLE_0;
 clusters FUNCT_1, PBOOLE, UNIALG_1, TEX_2, PRALG_1, RELSET_1, STRUCT_0,
      FINSEQ_2, FUNCOP_1, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS,
      ORDINAL2;
 requirements BOOLE, SUBSET;
 definitions TARSKI, PRALG_1, FINSEQ_1, UNIALG_1, PBOOLE, STRUCT_0, XBOOLE_0;
 theorems TARSKI, FUNCT_1, PARTFUN1, FINSEQ_1, FUNCOP_1, UNIALG_1, PBOOLE,
      FUNCT_2, CARD_3, FINSEQ_3, FINSEQ_2, REALSET1, RELAT_1, RELSET_1,
      STRUCT_0;
 schemes ZFREFLE1, FUNCT_1, FRAENKEL, FUNCT_2;

begin :: Preliminaries

reserve i,j for set,
        I for set;

theorem Th1:
 not ex M being non-empty ManySortedSet of I st {} in rng M
 proof let M be non-empty ManySortedSet of I;
  assume
A1:  {} in rng M;
     dom M = I by PBOOLE:def 3;
   then ex i st i in I & M.i = {} by A1,FUNCT_1:def 5;
  hence contradiction by PBOOLE:def 16;
 end;

scheme MSSEx { I() -> set, P[set,set] }:
 ex f being ManySortedSet of I() st
  for i st i in I() holds P[i,f.i]
  provided A1: for i st i in I() ex j st P[i,j]
 proof
   defpred Q[set,set] means P[$1,$2];
   A2: for i st i in I() ex j st Q[i,j] by A1;
   consider f being Function such that
A3: dom f = I() and
A4: for i st i in I() holds Q[i,f.i] from NonUniqFuncEx(A2);
   reconsider f as ManySortedSet of I() by A3,PBOOLE:def 3;
  take f; thus thesis by A4;
 end;

scheme MSSLambda { I() -> set, F(set) -> set }:
 ex f being ManySortedSet of I() st
  for i st i in I() holds f.i = F(i)
 proof
   deffunc G(set)=F($1);
   consider f being Function such that
A1:  dom f = I() and
A2:  for i st i in I() holds f.i = G(i) from Lambda;
   reconsider f as ManySortedSet of I() by A1,PBOOLE:def 3;
  take f; thus thesis by A2;
 end;

definition let I be set; let M be ManySortedSet of I;
 mode Component of M is Element of rng M;
end;

theorem Th2:
 for I being non empty set
 for M being ManySortedSet of I, A being Component of M
  ex i st i in I & A = M.i
 proof let I be non empty set;
  let M be ManySortedSet of I, A be Component of M;
A1: dom M = I by PBOOLE:def 3;
   then rng M <> {} by RELAT_1:65;
  hence ex i st i in I & A = M.i by A1,FUNCT_1:def 5;
 end;

theorem Th3:
 for M being ManySortedSet of I, i st i in I holds M.i is Component of M
 proof let M be ManySortedSet of I, i;
A1: dom M = I by PBOOLE:def 3;
  assume i in I;
  hence thesis by A1,FUNCT_1:def 5;
 end;

definition let I; let B be ManySortedSet of I;
 mode Element of B -> ManySortedSet of I means
   for i st i in I holds it.i is Element of B.i;
 existence
  proof
    defpred Q[set,set] means $2 is Element of B.$1;
A1: for i st i in I ex j st Q[i,j]
proof let i such that i in I;
      consider j being Element of B.i;
      reconsider j as set;
     take j; thus j is Element of B.i;
    end;
   thus ex f being ManySortedSet of I st
     for i st i in I holds Q[i,f.i] from MSSEx(A1);
  end;
end;

begin :: Many Sorted Functions

definition let I;
 let A be ManySortedSet of I, B be ManySortedSet of I;
 mode ManySortedFunction of A,B -> ManySortedSet of I means
:Def2: for i st i in I holds it.i is Function of A.i, B.i;
 correctness
  proof
    defpred P[set,set] means $2 is Function of A.$1,B.$1;
A1: for i st i in I ex j st P[i,j]
  proof let i such that i in I;
      consider j being Function of A.i,B.i;
      reconsider j as set;
     take j; thus j is Function of A.i,B.i;
    end;
   consider f being ManySortedSet of I such that
A2:  for i st i in I holds P[i,f.i] from MSSEx(A1);
      f is Function-yielding
     proof let i;
      assume i in dom f;
       then i in I by PBOOLE:def 3;
      hence f.i is Function by A2;
     end;
    then reconsider f as ManySortedFunction of I;
   take f;
   let i;
   assume i in I;
   hence f.i is Function of A.i,B.i by A2;
  end;
end;

definition let I;
 let A be ManySortedSet of I, B be ManySortedSet of I;
 cluster ->Function-yielding ManySortedFunction of A,B;
  coherence
   proof let f be ManySortedFunction of A,B;
    let i;
     assume i in dom f;
      then i in I by PBOOLE:def 3;
     hence f.i is Function by Def2;
   end;
end;

definition let I be set; let M be ManySortedSet of I;
 func M# -> ManySortedSet of I* means
:Def3: for i being Element of I* holds it.i = product(M*i);
 existence
  proof
    defpred P[set,set] means ex j being Element of I* st j = $1
           & $2 = product(M*j);
A1: for i st i in I* ex j st P[i,j]
   proof let i; assume
      i in I*;
      then reconsider j = i as Element of I*;
      reconsider e = product(M*j) as set;
     take e,j;
     thus j = i & e = product(M*j);
    end;
    consider f being ManySortedSet of I* such that
A2:   for i st i in I* holds P[i,f.i]
    from MSSEx(A1);
   take f; let i be Element of I*;
      ex j being Element of I* st j = i & f.i = product(M*j) by A2;
   hence thesis;
  end;
 uniqueness
  proof let N1,N2 be ManySortedSet of I* such that
A3: for i being Element of I* holds N1.i = product(M*i) and
A4: for i being Element of I* holds N2.i = product(M*i);
      now let i;
     assume
      i in I*;
      then reconsider e = i as Element of I*;
     thus N1.i = product(M*e) by A3 .= N2.i by A4;
    end;
   hence thesis by PBOOLE:3;
  end;
end;

definition let I be set; let M be non-empty ManySortedSet of I;
 cluster M# -> non-empty;
 coherence
  proof
      M# is non-empty
    proof let i;
     assume
      i in I*;
      then reconsider f = i as Element of I*;
        not {} in rng M by Th1;
      then not {} in rng(M*f) by FUNCT_1:25;
      then product(M*f) <> {} by CARD_3:37;
     hence M#.i is non empty by Def3;
    end;
   hence thesis;
  end;
end;

definition let I; let J be non empty set;
 let O be Function of I,J;
 let F be ManySortedSet of J;
 redefine func F*O -> ManySortedSet of I;
  coherence
   proof
     rng O c= J & dom O = I & dom F = J
       by FUNCT_2:def 1,PBOOLE:def 3,RELSET_1:12;
    hence dom(F*O) = I by RELAT_1:46;
   end;
end;

definition let I; let J be non empty set;
 let O be Function of I,J;
 let F be non-empty ManySortedSet of J;
 redefine func F*O -> non-empty ManySortedSet of I;
  coherence
  proof
      F*O is non-empty
     proof let i;
      assume
A1:     i in I;
       then O.i in J by FUNCT_2:7;
       then A2:      F.(O.i) is non empty by PBOOLE:def 16;
         dom O = I by FUNCT_2:def 1;
      hence (F*O).i is non empty by A1,A2,FUNCT_1:23;
     end;
   hence thesis;
  end;
end;

definition let a be set;
 func *-->a -> Function of NAT,{a}* means
:Def4: for n being Nat holds it.n = n |-> a;
  existence
   proof
     defpred P[Element of NAT,Element of {a}*] means $2 = $1 |-> a;
A1:  for x being Element of NAT ex y being Element of {a}* st P[x,y]
   proof let n be Nat;
        a is Element of {a} by TARSKI:def 1;
      then n |-> a is FinSequence of {a} by FINSEQ_2:77;
      then reconsider u = n |-> a as Element of {a}* by FINSEQ_1:def 11;
     take u;
     thus u = n |-> a;
    end;
     ex f being Function of NAT,{a}* st for x being Element of NAT
         holds P[x,f.x]  from FuncExD(A1);
    hence thesis;
   end;
  uniqueness
   proof let f1,f2 be Function of NAT,{a}* such that
A2: for n being Nat holds f1.n = n |-> a and
A3: for n being Nat holds f2.n = n |-> a;
       now let k be Nat;
      thus f1.k = k |-> a by A2
        .= f2.k by A3;
     end;
    hence f1 = f2 by FUNCT_2:113;
   end;
end;

 reserve D for non empty set,
         n for Nat;

theorem Th4:
 for a,b being set holds ({a} --> b)*(n|->a) = n |-> b
 proof let a,b be set;
A1: now let x be set;
    hereby assume x in dom (n |-> b);
      then A2:     x in Seg n by FINSEQ_2:68;
     hence x in dom(n|->a) by FINSEQ_2:68;
A3:    dom({a} --> b) = {a} by FUNCOP_1:19;
        (n|->a).x = a by A2,FINSEQ_2:70;
     hence (n|->a).x in dom({a} --> b) by A3,TARSKI:def 1;
    end;
    assume that
A4:  x in dom(n|->a) and (n|->a).x in dom({a} --> b);
       x in Seg n by A4,FINSEQ_2:68;
    hence x in dom (n |-> b) by FINSEQ_2:68;
   end;
     now let x be set;
    assume
     x in dom (n |-> b);
     then A5:   x in Seg n by FINSEQ_2:68;
A6:   a in {a} by TARSKI:def 1;
    thus (n |-> b).x = b by A5,FINSEQ_2:70
     .= ({a} --> b).a by A6,FUNCOP_1:13
     .= ({a} --> b).((n|->a).x) by A5,FINSEQ_2:70;
   end;
  hence ({a} --> b)*(n|->a) = n |-> b by A1,FUNCT_1:20;
 end;

theorem Th5:
 for a being set
 for M being ManySortedSet of {a} st M = {a} --> D
   holds (M#**-->a).n = Funcs(Seg n, D)
 proof let a be set;
  let M be ManySortedSet of {a} such that
A1: M = {a} --> D;
   A2: dom(*-->a) = NAT by FUNCT_2:def 1;
     a is Element of {a} by TARSKI:def 1;
   then n |-> a is FinSequence of {a} by FINSEQ_2:77;
   then A3: n |-> a in {a}* by FINSEQ_1:def 11;
  thus (M#**-->a).n = M#.((*-->a).n) by A2,FUNCT_1:23
     .= M#.(n|->a) by Def4
     .= product(({a} --> D)*(n|->a)) by A1,A3,Def3
     .= product(n |-> D) by Th4
     .= product(Seg(n) --> D) by FINSEQ_2:def 2
     .= Funcs(Seg n, D) by CARD_3:20;
 end;

definition let I,i;
 redefine func I --> i -> Function of I,{i};
 coherence
  proof
      dom (I --> i) = I & rng (I --> i) c= {i} by FUNCOP_1:19;
   hence I --> i is Function of I,{i} by FUNCT_2:def 1,RELSET_1:11;
  end;
end;

begin :: Many Sorted Signatures

definition
 struct(1-sorted) ManySortedSign
       (# carrier -> set,
         OperSymbols -> set,
         Arity -> Function of the OperSymbols, the carrier*,
         ResultSort -> Function of the OperSymbols, the carrier
       #);
end;

definition let IT be ManySortedSign;
 attr IT is void means
:Def5: the OperSymbols of IT = {};
end;

definition
 cluster void strict non empty ManySortedSign;
 existence
  proof
      {} in {{}}* by FINSEQ_1:66;
    then reconsider f = {}-->{} as Function of {},{{}}* by FUNCOP_1:58;
    reconsider g = {}-->{} as Function of {},{{}};
   take ManySortedSign(#{{}},{},f,g#);
   thus thesis by Def5,STRUCT_0:def 1;
  end;
 cluster non void strict non empty ManySortedSign;
  existence
  proof
      {} in {{}}* by FINSEQ_1:66;
    then reconsider f = {{}}-->{} as Function of {{}},{{}}* by FUNCOP_1:58;
    reconsider g = {{}}-->{} as Function of {{}},{{}};
   take ManySortedSign(#{{}},{{}},f,g#);
   thus thesis by Def5,STRUCT_0:def 1;
  end;
end;

reserve S for non empty ManySortedSign;

definition let S;
 mode SortSymbol of S is Element of S;
 mode OperSymbol of S is Element of the OperSymbols of S;
end;

definition let S be non void non empty ManySortedSign;
 let o be OperSymbol of S;
 func the_arity_of o -> Element of (the carrier of S)* equals
:Def6:  (the Arity of S).o;
 coherence
  proof the OperSymbols of S <> {} by Def5;
    then o in the OperSymbols of S;
    then o in dom(the Arity of S) by FUNCT_2:def 1;
then A1:   (the Arity of S).o in rng(the Arity of S) by FUNCT_1:def 5;
      rng(the Arity of S) c= (the carrier of S)* by RELSET_1:12;
    hence thesis by A1;
  end;
 correctness;
 func the_result_sort_of o -> Element of S equals
    (the ResultSort of S).o;
 coherence
  proof the OperSymbols of S <> {} by Def5;
    then o in the OperSymbols of S;
    then o in dom(the ResultSort of S) by FUNCT_2:def 1;
    then A2:   (the ResultSort of S).o in rng(the ResultSort of S) by FUNCT_1:
def 5;
      rng(the ResultSort of S) c= the carrier of S by RELSET_1:12;
    hence thesis by A2;
  end;
end;

begin :: Many Sorted Algebras

definition let S be 1-sorted;
 struct many-sorted over S (# Sorts -> ManySortedSet of the carrier of S #);
end;

definition let S;
 struct(many-sorted over S) MSAlgebra over S (#
      Sorts -> ManySortedSet of the carrier of S,
      Charact -> ManySortedFunction of
       (the Sorts)# * the Arity of S, the Sorts * the ResultSort of S#);
end;

definition let S be 1-sorted; let A be many-sorted over S;
 attr A is non-empty means
:Def8: the Sorts of A is non-empty;
end;

definition let S;
 cluster strict non-empty MSAlgebra over S;
 existence
  proof
     dom((the carrier of S) --> {0}) = the carrier of S by FUNCOP_1:19;
   then reconsider s = (the carrier of S) --> {0}
            as ManySortedSet of the carrier of S by PBOOLE:def 3;
   consider o being ManySortedFunction of
       s# * the Arity of S, s * the ResultSort of S;
   take MSAlgebra(#s,o#);
   thus MSAlgebra(#s,o#) is strict;
   let i be set;
   assume i in the carrier of S;
   hence thesis by FUNCOP_1:13;
  end;
end;

definition let S be 1-sorted;
  cluster strict non-empty many-sorted over S;
  existence
  proof
     dom ((the carrier of S) --> {0}) = the carrier of S by FUNCOP_1:19;
   then reconsider s = (the carrier of S) --> {0}
            as ManySortedSet of the carrier of S by PBOOLE:def 3;
   take many-sorted(#s#);
   thus many-sorted (#s#) is strict;
   let i be set;
   assume i in the carrier of S;
   hence thesis by FUNCOP_1:13;
  end;
end;

definition let S be 1-sorted; let A be non-empty many-sorted over S;
 cluster the Sorts of A -> non-empty;
  coherence by Def8;
end;

definition let S; let A be non-empty MSAlgebra over S;
 cluster -> non empty Component of the Sorts of A;
  coherence
   proof let C be Component of the Sorts of A;
       ex i st i in the carrier of S & C = (the Sorts of A).i by Th2;
    hence thesis by PBOOLE:def 16;
   end;
 cluster -> non empty Component of (the Sorts of A)#;
  coherence
   proof let C be Component of (the Sorts of A)#;
       ex i st i in (the carrier of S)* & C = (the Sorts of A)#.i by Th2;
    hence thesis by PBOOLE:def 16;
   end;
end;

definition let S be non void non empty ManySortedSign;
 let o be OperSymbol of S; let A be MSAlgebra over S;
 func Args(o,A) -> Component of (the Sorts of A)# equals
:Def9:  ((the Sorts of A)# * the Arity of S).o;
 coherence
  proof
      the OperSymbols of S <> {} by Def5;
    then o in the OperSymbols of S;
    then o in dom((the Sorts of A)# * the Arity of S) by PBOOLE:def 3;
    then ((the Sorts of A)# * the Arity of S).o
         in rng((the Sorts of A)# * the Arity of S) by FUNCT_1:def 5;
   hence thesis by FUNCT_1:25;
  end;
 correctness;
 func Result(o,A) -> Component of the Sorts of A equals
:Def10: ((the Sorts of A) * the ResultSort of S).o;
 coherence
  proof
      the OperSymbols of S <> {} by Def5;
    then o in the OperSymbols of S;
    then o in dom((the Sorts of A) * the ResultSort of S) by PBOOLE:def 3;
    then ((the Sorts of A) * the ResultSort of S).o
         in rng((the Sorts of A) * the ResultSort of S) by FUNCT_1:def 5;
   hence thesis by FUNCT_1:25;
  end;
 correctness;
end;

definition let S be non void non empty ManySortedSign;
 let o be OperSymbol of S; let A be MSAlgebra over S;
 func Den(o,A) -> Function of Args(o,A), Result(o,A) equals
:Def11:  (the Charact of A).o;
 coherence
  proof
    A1: the OperSymbols of S <> {} by Def5;
      Result(o,A) = ((the Sorts of A) * the ResultSort of S).o &
    Args(o,A) = ((the Sorts of A)# * the Arity of S).o by Def9,Def10;
   hence thesis by A1,Def2;
  end;
end;

theorem Th6:
 for S being non void non empty ManySortedSign, o being OperSymbol of S,
     A being non-empty MSAlgebra over S
  holds Den(o,A) is non empty
 proof let S be non void non empty ManySortedSign, o be OperSymbol of S,
       A be non-empty MSAlgebra over S;
   thus Den(o,A) is non empty by FUNCT_2:def 1,RELAT_1:60;
 end;

begin :: On the one-sorted algebras

 Lm1:
 for h being homogeneous quasi_total non empty PartFunc of D*,D
  holds dom h = (arity h)-tuples_on D
 proof let h be homogeneous quasi_total non empty PartFunc of D*,D;
A1: dom h c= D* by RELSET_1:12;
  thus dom h c= (arity h)-tuples_on D
   proof let x be set;
    assume
A2:   x in dom h;
     then reconsider f = x as FinSequence of D by A1,FINSEQ_1:def 11;
A3:   len f = arity h by A2,UNIALG_1:def 10;
       f is Element of (len f)-tuples_on D by FINSEQ_2:110;
    hence x in (arity h)-tuples_on D by A3;
   end;
  let x be set;
  assume x in (arity h)-tuples_on D;
   then reconsider f = x as Element of (arity h)-tuples_on D;
   consider x0 being Element of dom h;
   A4: dom h <> {} by RELAT_1:64;
   then x0 in dom h;
   then reconsider x0 as FinSequence of D by A1,FINSEQ_1:def 11;
     len x0 = arity h by A4,UNIALG_1:def 10 .= len f by FINSEQ_2:109;
  hence x in dom h by A4,UNIALG_1:def 2;
 end;

theorem Th7:
 for C being set, A,B being non empty set,
     F being PartFunc of C,A, G being Function of A,B
 holds G*F is Function of dom F,B
 proof let C be set; let A,B be non empty set;
 let F be PartFunc of C,A; let G be Function of A,B;
    now dom G = A by FUNCT_2:def 1;
    then rng F c= dom G by RELSET_1:12;
   hence dom(G*F) = dom F by RELAT_1:46;
   thus rng(G*F) c= B by RELSET_1:12;
  end;
 hence G*F is Function of dom F,B by FUNCT_2:def 1,RELSET_1:11;
end;

theorem Th8:
 for h being homogeneous quasi_total non empty PartFunc of D*,D
  holds dom h = Funcs(Seg(arity h),D)
  proof let h be homogeneous quasi_total non empty PartFunc of D*,D;
   thus dom h = (arity h)-tuples_on D by Lm1
             .= Funcs(Seg(arity h),D) by FINSEQ_2:111;
  end;

theorem Th9:
 for A being Universal_Algebra holds signature A is non empty
  proof let A be Universal_Algebra;
      len(the charact of A) <> 0 by FINSEQ_1:25;
    then len(signature A) <> 0 by UNIALG_1:def 11;
   hence signature A is non empty by FINSEQ_1:25;
  end;

begin :: Relationship to one sorted algebras

definition let A be Universal_Algebra;
 redefine func signature A -> FinSequence of NAT;
 coherence;
end;

definition let IT be ManySortedSign;
 attr IT is segmental means
:Def12:  ex n st the OperSymbols of IT = Seg n;
end;

theorem Th10:
 for S being non empty ManySortedSign st S is trivial
 for A being MSAlgebra over S,
     c1,c2 being Component of the Sorts of A holds c1 = c2
 proof let S be non empty ManySortedSign such that
A1: S is trivial;
  let A be MSAlgebra over S, c1,c2 be Component of the Sorts of A;
   consider i1 being set such that
A2: i1 in the carrier of S and
A3: c1 = (the Sorts of A).i1 by Th2;
   consider i2 being set such that
A4: i2 in the carrier of S and
A5: c2 = (the Sorts of A).i2 by Th2;
  thus c1 = c2 by A1,A2,A3,A4,A5,REALSET1:def 20;
 end;

Lm2:
 for A being Universal_Algebra
 for f being Function of dom signature A, {0}*
  st f = (*-->0)*(signature A)
 holds
 ManySortedSign
    (#{0},dom signature(A),f,dom signature(A)-->0#)
    is non empty segmental trivial non void strict
  proof let A be Universal_Algebra;
   let f be Function of dom signature A, {0}* such that
    f = (*-->0)*(signature A);
   set S = ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#);
   thus
     the carrier of S is non empty;
      signature A <> {} by Th9;
    then A1: the OperSymbols of S <> {} by RELAT_1:64;
      S is segmental
     proof
      take len signature(A);
      thus the OperSymbols of S = Seg len signature(A) by FINSEQ_1:def 3;
     end;
   hence thesis by A1,Def5,REALSET1:def 13;
  end;


definition
 cluster segmental trivial non void strict non empty ManySortedSign;
 existence
  proof consider A being Universal_Algebra;
    reconsider f = (*-->0)*(signature A) as Function of dom signature A, {0}*
             by Th7;
      ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#)
     is segmental trivial non void strict non empty by Lm2;
   hence thesis;
  end;
end;

definition let A be Universal_Algebra;
 func MSSign A -> non void strict segmental trivial ManySortedSign means
:Def13:
  the carrier of it = {0} &
  the OperSymbols of it = dom signature A &
  the Arity of it = (*-->0)*signature A &
  the ResultSort of it = dom signature(A)-->0;
 correctness
  proof
    reconsider f = (*-->0)*(signature A) as Function of dom signature A, {0}*
             by Th7;
      ManySortedSign(#{0},dom signature(A),f,dom signature(A)-->0#)
     is segmental trivial non void strict by Lm2;
   hence thesis;
  end;
end;

definition let A be Universal_Algebra;
 cluster MSSign A -> non empty;
 coherence
  proof
   thus the carrier of MSSign A is non empty by Def13;
  end;
end;

definition let A be Universal_Algebra;
 func MSSorts A -> non-empty ManySortedSet of the carrier of MSSign A equals
:Def14: {0}-->the carrier of A;
 coherence
  proof
    A1: the carrier of MSSign A = {0} &
    the OperSymbols of MSSign A = dom signature A &
    the Arity of MSSign A = (*-->0)*signature A &
    the ResultSort of MSSign A = dom signature(A)-->0 by Def13;
    set M = {0}-->the carrier of A;
    dom M = the carrier of MSSign A by A1,FUNCOP_1:19;
    then reconsider M as ManySortedSet of the carrier of MSSign A
     by PBOOLE:def 3;
      M is non-empty
     proof let i;
      assume
       i in the carrier of MSSign A;
      hence thesis by A1,FUNCOP_1:13;
     end;
   hence thesis;
  end;
 correctness;
end;

definition let A be Universal_Algebra;
 func MSCharact A -> ManySortedFunction of
  (MSSorts A)# * the Arity of MSSign A, (MSSorts A)* the ResultSort of MSSign A
     equals
:Def15:  the charact of A;
 coherence
  proof
   reconsider OS = the OperSymbols of MSSign A as non empty set by Def5;
    A1: the carrier of MSSign A = {0} &
    the OperSymbols of MSSign A = dom signature A &
    the Arity of MSSign A = (*-->0)*signature A &
    the ResultSort of MSSign A = dom signature(A)-->0 by Def13;
     len signature A = len the charact of A by UNIALG_1:def 11;
   then A2:  dom the charact of A = OS by A1,FINSEQ_3:31;
   then reconsider O = the charact of A as ManySortedSet of OS
     by PBOOLE:def 3;
     O is Function-yielding
    proof let i;
     assume
A3:    i in dom O;
        dom O = dom the charact of A;
      then reconsider n = i as Nat by A3;
        O.n is Function by A3,UNIALG_1:5;
     hence O.i is Function;
    end;
   then reconsider O as ManySortedFunction of OS;
   reconsider DO = (MSSorts A)# * the Arity of MSSign A,
               RO = (MSSorts A)* the ResultSort of MSSign A
    as ManySortedSet of OS;
     O is ManySortedFunction of DO,RO
   proof let i;
    assume
A4:   i in OS;
     then reconsider o = i as Element of OS;
     reconsider n = i as Nat by A1,A4;
     set D = the carrier of A;
     reconsider h = O.n as homogeneous quasi_total non empty PartFunc of D*,D
                             by A2,A4,UNIALG_1:5,def 4,def 5,def 6;
       dom({0}-->D) = {0} by FUNCOP_1:19;
     then reconsider M = {0}-->D as ManySortedSet of {0} by PBOOLE:def 3;
     A5:   n in dom(dom signature(A)-->0) by A1,A4,FUNCOP_1:19;
A6:   0 in {0} by TARSKI:def 1;
A7:   DO.i = ((MSSorts A)#*(*-->0)*signature A).n by A1,RELAT_1:55
         .= ((MSSorts A)#*(*-->0)).((signature A).n) by A1,A4,FUNCT_1:23
         .= (M#*(*-->0)).((signature A).n) by A1,Def14
         .= (M#*(*-->0)).arity h by A1,A4,UNIALG_1:def 11
         .= Funcs(Seg arity h,D) by Th5
         .= dom(O.o) by Th8;
A8:   RO.i = (MSSorts A).((dom signature(A)-->0).n) by A1,A5,FUNCT_1:23
         .= (MSSorts A).0 by A1,A4,FUNCOP_1:13
         .= ({0}-->the carrier of A).0 by Def14
         .= the carrier of A by A6,FUNCOP_1:13;
     then rng h c= RO.i by RELSET_1:12;
    hence O.i is Function of DO.i,RO.i by A7,A8,FUNCT_2:def 1,RELSET_1:11;
   end;
   hence thesis;
  end;
 correctness;
end;

definition let A be Universal_Algebra;
 func MSAlg A -> strict MSAlgebra over MSSign A equals
:Def16:  MSAlgebra(#MSSorts A,MSCharact A#);
 correctness;
end;

definition let A be Universal_Algebra;
 cluster MSAlg A -> non-empty;
 coherence
  proof
      MSAlg A = MSAlgebra(#MSSorts A,MSCharact A#) by Def16;
   hence the Sorts of MSAlg A is non-empty;
  end;
end;

:: Manysorted Algebras with 1 Sort Only

definition let MS be trivial non empty ManySortedSign;
 let A be MSAlgebra over MS;
 func the_sort_of A -> set means
:Def17: ex c being Component of the Sorts of A st it = c;
 existence
  proof consider c being Component of the Sorts of A;
   take c; thus thesis;
  end;
 uniqueness by Th10;
end;

definition let MS be trivial non empty ManySortedSign;
 let A be non-empty MSAlgebra over MS;
 cluster the_sort_of A -> non empty;
 coherence
  proof
      ex c being Component of the Sorts of A st the_sort_of A = c by Def17;
   hence thesis;
  end;
end;

theorem Th11:
 for MS being segmental trivial non void non empty ManySortedSign,
     i being OperSymbol of MS,
     A being non-empty MSAlgebra over MS
 holds Args(i,A) = (len the_arity_of i)-tuples_on the_sort_of A
proof
 let MS be segmental trivial non void non empty ManySortedSign,
     i be OperSymbol of MS,
     A be non-empty MSAlgebra over MS;
  set m = len the_arity_of i;
A1: the OperSymbols of MS <> {} by Def5;
A2:    dom(the Arity of MS) = the OperSymbols of MS by FUNCT_2:def 1;
A3: Args(i,A) = ((the Sorts of A)# * the Arity of MS).i by Def9
            .= (the Sorts of A)# .((the Arity of MS).i) by A1,A2,FUNCT_1:23
            .= (the Sorts of A)# .the_arity_of i by Def6
            .= product((the Sorts of A)*the_arity_of i) by Def3;
   consider n being Nat such that
A4:  dom the_arity_of i = Seg n by FINSEQ_1:def 2;
A5: rng the_arity_of i c= the carrier of MS by FINSEQ_1:def 4;
  then rng the_arity_of i c= dom the Sorts of A by PBOOLE:def 3;
  then A6: dom((the Sorts of A)*the_arity_of i) = dom the_arity_of i by RELAT_1
:46;
 thus Args(i,A) c= m-tuples_on the_sort_of A
  proof
   let x be set;
   assume x in Args(i,A);
    then consider g being Function such that
  A7: x = g and
  A8: dom g = dom((the Sorts of A)*the_arity_of i) and
  A9: for j being set st j in dom((the Sorts of A)*the_arity_of i)
         holds g.j in ((the Sorts of A)*the_arity_of i).j by A3,CARD_3:def 5;
    reconsider p = g as FinSequence by A4,A6,A8,FINSEQ_1:def 2;
      rng p c= the_sort_of A
     proof let j be set;
      assume j in rng p;
       then consider u being set such that
  A10:   u in dom g and
  A11:   p.u = j by FUNCT_1:def 5;
         g.u in ((the Sorts of A)*the_arity_of i).u by A8,A9,A10;
       then A12:    g.u in (the Sorts of A).((the_arity_of i).u) by A6,A8,A10,
FUNCT_1:23;
         (the_arity_of i).u in rng the_arity_of i by A6,A8,A10,FUNCT_1:def 5;
       then (the Sorts of A).((the_arity_of i).u) is
        Component of the Sorts of A by A5,Th3;
      hence j in the_sort_of A by A11,A12,Def17;
     end;
    then A13:   p is FinSequence of the_sort_of A by FINSEQ_1:def 4;
      len p = m by A6,A8,FINSEQ_3:31;
    then x is Element of m-tuples_on the_sort_of A by A7,A13,FINSEQ_2:110;
   hence x in m-tuples_on the_sort_of A;
 end;
 let x be set;
 assume x in m-tuples_on the_sort_of A;
  then x in Funcs(Seg m, the_sort_of A) by FINSEQ_2:111;
  then consider g being Function such that
A14: x = g and
A15: dom g = Seg m and
A16: rng g c= the_sort_of A by FUNCT_2:def 2;
A17: dom g = dom((the Sorts of A)*the_arity_of i) by A6,A15,FINSEQ_1:def 3;
    now let x be set;
   assume
A18:  x in dom((the Sorts of A)*the_arity_of i);
    then g.x in rng g by A17,FUNCT_1:def 5;
    then A19:   g.x in the_sort_of A by A16;
      (the_arity_of i).x in rng the_arity_of i by A6,A18,FUNCT_1:def 5;
    then (the Sorts of A).((the_arity_of i).x) is
     Component of the Sorts of A by A5,Th3;
    then g.x in (the Sorts of A).((the_arity_of i).x) by A19,Def17;
   hence g.x in ((the Sorts of A)*the_arity_of i).x by A6,A18,FUNCT_1:23;
  end;
 hence x in Args(i,A) by A3,A14,A17,CARD_3:18;
end;

theorem Th12:
 for A being non empty set, n holds n-tuples_on A c= A*
  proof let A be non empty set, n;
    defpred P[Element of A*] means len $1 = n;
      { s where s is Element of A*: P[s] } c= A* from Fr_Set0;
   hence n-tuples_on A c= A* by FINSEQ_2:def 4;
  end;

theorem Th13:
 for MS being segmental trivial non void non empty ManySortedSign,
     i being OperSymbol of MS,
     A being non-empty MSAlgebra over MS holds Args(i,A) c= (the_sort_of A)*
proof
 let MS be segmental trivial non void non empty ManySortedSign,
     i be OperSymbol of MS,
     A be non-empty MSAlgebra over MS;
   Args(i,A) = (len the_arity_of i)-tuples_on the_sort_of A by Th11;
 hence Args(i,A) c= (the_sort_of A)* by Th12;
end;

theorem Th14:
 for MS being segmental trivial non void non empty ManySortedSign,
     A being non-empty MSAlgebra over MS holds
  the Charact of A is FinSequence of PFuncs((the_sort_of A)*,the_sort_of A)
 proof
  let MS be segmental trivial non void non empty ManySortedSign,
      A be non-empty MSAlgebra over MS;
A1: dom the Charact of A = the OperSymbols of MS by PBOOLE:def 3;
     ex n st the OperSymbols of MS = Seg n by Def12;
   then reconsider f = the Charact of A as FinSequence by A1,FINSEQ_1:def 2;
     f is FinSequence of PFuncs((the_sort_of A)*,the_sort_of A)
    proof let x be set;
     assume x in rng f;
      then consider i such that
A2:    i in the OperSymbols of MS and
A3:    f.i = x by A1,FUNCT_1:def 5;
      reconsider i as OperSymbol of MS by A2;
A4:    dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1;
A5:    ((the Sorts of A)# * the Arity of MS).i = Args(i,A) by Def9;
        (the ResultSort of MS).i in the carrier of MS by A2,FUNCT_2:7;
      then A6:    (the Sorts of A).((the ResultSort of MS).i)
       is Component of the Sorts of A by Th3;
A7:    Args(i,A) c= (the_sort_of A)* by Th13;
        ((the Sorts of A)*the ResultSort of MS).i
            = (the Sorts of A).((the ResultSort of MS).i) by A2,A4,FUNCT_1:23
           .= the_sort_of A by A6,Def17;
      then x is Function of Args(i,A),the_sort_of A by A2,A3,A5,Def2;
      then x is PartFunc of (the_sort_of A)*,the_sort_of A by A7,PARTFUN1:30;
     hence x in PFuncs((the_sort_of A)*,the_sort_of A) by PARTFUN1:119;
    end;
  hence thesis;
 end;

definition let MS be segmental trivial non void non empty ManySortedSign;
 let A be non-empty MSAlgebra over MS;
 func the_charact_of A -> PFuncFinSequence of the_sort_of A equals
:Def18: the Charact of A;
 coherence by Th14;
end;

reserve MS for segmental trivial non void non empty ManySortedSign,
        A for non-empty MSAlgebra over MS,
        h for PartFunc of (the_sort_of A)*,(the_sort_of A),
        x,y for FinSequence of the_sort_of A;

definition let MS,A;
 func 1-Alg A -> non-empty strict Universal_Algebra equals
:Def19:   UAStr(#the_sort_of A, the_charact_of A#);
 coherence
  proof
    A1: the_charact_of A is quasi_total
     proof let n,h such that
A2:    n in dom(the_charact_of A) and
A3:    h = (the_charact_of A).n;
      let x,y such that
A4:   len x = len y and
A5:   x in dom h;
A6:     dom(the_charact_of A) = dom the Charact of A by Def18
          .= the OperSymbols of MS by PBOOLE:def 3;
       then reconsider o = n as OperSymbol of MS by A2;
A7:    dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1;
A8:   ((the Sorts of A)# * the Arity of MS).o = Args(o,A) by Def9;
       (the ResultSort of MS).o in the carrier of MS by A2,A6,FUNCT_2:7;
     then A9:   (the Sorts of A).((the ResultSort of MS).o)
       is Component of the Sorts of A by Th3;
    A10: ((the Sorts of A)*the ResultSort of MS).o
          = (the Sorts of A).((the ResultSort of MS).o) by A2,A6,A7,FUNCT_1:23
         .= the_sort_of A by A9,Def17;
         h = (the Charact of A).o by A3,Def18;
       then h is Function of
          ((the Sorts of A)# * the Arity of MS).o,
          ((the Sorts of A) * the ResultSort of MS).o by A2,A6,Def2;

       then A11:     dom h = ((the Sorts of A)# * the Arity of MS).o by A10,
FUNCT_2:def 1
            .= (len the_arity_of o)-tuples_on the_sort_of A by A8,Th11;
       then len y = len the_arity_of o by A4,A5,FINSEQ_2:109;
       then y is Element of dom h by A11,FINSEQ_2:110;
      hence y in dom h by A5;
     end;
    A12: the_charact_of A is homogeneous
     proof let n,h such that
A13:    n in dom(the_charact_of A) and
A14:    h = (the_charact_of A).n;
      let x,y such that
A15:     x in dom h & y in dom h;
A16:     dom(the_charact_of A) = dom the Charact of A by Def18
          .= the OperSymbols of MS by PBOOLE:def 3;
       then reconsider o = n as OperSymbol of MS by A13;
A17:    dom(the ResultSort of MS) = the OperSymbols of MS by FUNCT_2:def 1;
A18:   ((the Sorts of A)# * the Arity of MS).o = Args(o,A) by Def9;
       (the ResultSort of MS).o in the carrier of MS by A13,A16,FUNCT_2:7;
     then A19:   (the Sorts of A).((the ResultSort of MS).o)
       is Component of the Sorts of A by Th3;
    A20: ((the Sorts of A)*the ResultSort of MS).o
          = (the Sorts of A).((the ResultSort of MS).o) by A13,A16,A17,FUNCT_1:
23
         .= the_sort_of A by A19,Def17;
         h = (the Charact of A).o by A14,Def18;
       then h is Function of
          ((the Sorts of A)# * the Arity of MS).o,
          ((the Sorts of A) * the ResultSort of MS).o by A13,A16,Def2;

       then A21:     dom h = ((the Sorts of A)# * the Arity of MS).o by A20,
FUNCT_2:def 1
            .= (len the_arity_of o)-tuples_on the_sort_of A by A18,Th11;
      hence len x = len the_arity_of o by A15,FINSEQ_2:109
        .= len y by A15,A21,FINSEQ_2:109;
     end;
    the OperSymbols of MS <> {} by Def5;
    then the Charact of A <> {} by PBOOLE:def 3,RELAT_1:60;
    then A22:  the_charact_of A <> {} by Def18;
      the_charact_of A is non-empty
     proof let n be set such that
A23:   n in dom the_charact_of A;
     set h = (the_charact_of A).n;
       dom(the_charact_of A) = dom the Charact of A by Def18
          .= the OperSymbols of MS by PBOOLE:def 3;
       then reconsider o = n as OperSymbol of MS by A23;
         h = (the Charact of A).o by Def18
        .= Den(o,A) by Def11;
      hence h is non empty by Th6;
     end;
   hence thesis by A1,A12,A22,UNIALG_1:def 7,def 8,def 9;
  end;
 correctness;
end;

theorem
   for A being strict Universal_Algebra holds
  A = 1-Alg MSAlg A
proof let A be strict Universal_Algebra;
A1: MSAlg A = MSAlgebra(#MSSorts A,MSCharact A#) by Def16;
     the carrier of A in {the carrier of A} by TARSKI:def 1;
   then the carrier of A in rng({0}-->the carrier of A) by FUNCOP_1:14;
   then the carrier of A in rng the Sorts of MSAlg A by A1,Def14;
   then A2: the carrier of A = the_sort_of MSAlg A by Def17;
    the charact of A = MSCharact A by Def15
        .= the_charact_of MSAlg A by A1,Def18;
 hence A = 1-Alg MSAlg A by A2,Def19;
end;

theorem
   for A being Universal_Algebra
 for f being Function of dom signature A, {0}*
  st f = (*-->0)*signature A
 holds MSSign A = ManySortedSign(#{0},dom signature A,f,dom signature(A)-->0#)
proof let A be Universal_Algebra;
    the carrier of MSSign A = {0} &
  the OperSymbols of MSSign A = dom signature A &
  the Arity of MSSign A = (*-->0)*signature A &
  the ResultSort of MSSign A = dom signature(A)-->0 by Def13;
 hence thesis;
end;

Back to top