:: Birkhoff Theorem for Many Sorted Algebras
:: by Artur Korni{\l}owicz
::
:: Received June 19, 1997
:: Copyright (c) 1997-2012 Association of Mizar Users


begin

::-------------------------------------------------------------------
:: Acknowledgements:
:: =================
::
:: I would like to thank Professor Andrzej Trybulec
:: for his help in the preparation of the article.
::-------------------------------------------------------------------
definition
let S be non empty non void ManySortedSign ;
let X be V2() ManySortedSet of the carrier of S;
let A be non-empty MSAlgebra over S;
let F be ManySortedFunction of X, the Sorts of A;
funcF -hash  ->  ManySortedFunction of (FreeMSA X),A means :Def1: :: BIRKHOFF:def 1
( it is_homomorphism FreeMSA X,A & it || (FreeGen X) = F ** (Reverse X) );
existence
 ex b1 being ManySortedFunction of (FreeMSA X),A st
( b1 is_homomorphism FreeMSA X,A & b1 || (FreeGen X) = F ** (Reverse X) ) by MSAFREE:def_5;
uniqueness
 for b1, b2 being ManySortedFunction of (FreeMSA X),A st b1 is_homomorphism FreeMSA X,A & b1 || (FreeGen X) = F ** (Reverse X) & b2 is_homomorphism FreeMSA X,A & b2 || (FreeGen X) = F ** (Reverse X) holds
b1 = b2 by EXTENS_1:14;
end;

:: deftheorem Def1 defines -hash BIRKHOFF:def_1_:_
 for S being non empty non void ManySortedSign
for X being V2() ManySortedSet of the carrier of S
for A being non-empty MSAlgebra over S
for F being ManySortedFunction of X, the Sorts of A
for b5 being ManySortedFunction of (FreeMSA X),A holds
( b5 = F -hash iff ( b5 is_homomorphism FreeMSA X,A & b5 || (FreeGen X) = F ** (Reverse X) ) );

theorem Th1: :: BIRKHOFF:1
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra over S
for X being V2() ManySortedSet of the carrier of S
for F being ManySortedFunction of X, the Sorts of A holds rngs F c= rngs (F -hash)
proofend;

scheme :: BIRKHOFF:sch 1
ExFreeAlg1{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), P1[ set ] } :
 ex A being strict non-empty MSAlgebra over F1() ex F being ManySortedFunction of F2(),A st
( P1[A] & F is_epimorphism F2(),A & ( for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(),B st G is_homomorphism F2(),B & P1[B] holds
ex H being ManySortedFunction of A,B st
( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K ** F = G holds
H = K ) ) ) )
provided
A1: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A3: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proofend;

scheme :: BIRKHOFF:sch 2
ExFreeAlg2{ F1() ->  non empty non void ManySortedSign , F2() ->  V2() ManySortedSet of the carrier of F1(), P1[ set ] } :
 ex A being strict non-empty MSAlgebra over F1() ex F being ManySortedFunction of F2(), the Sorts of A st
( P1[A] & ( for B being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(), the Sorts of B st P1[B] holds
ex H being ManySortedFunction of A,B st
( H is_homomorphism A,B & H ** F = G & ( for K being ManySortedFunction of A,B st K is_homomorphism A,B & K ** F = G holds
H = K ) ) ) )
provided
A1: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A3: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proofend;

scheme :: BIRKHOFF:sch 3
Exhash{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), F3() ->  non-empty MSAlgebra over F1(), F4() ->  ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), F5() ->  ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F3(), P1[ set ] } :
 ex H being ManySortedFunction of F2(),F3() st
( H is_homomorphism F2(),F3() & F5() -hash = H ** (F4() -hash) )
provided
A1: P1[F3()] and
A2: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds
ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** F4() )
proofend;

scheme :: BIRKHOFF:sch 4
EqTerms{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), F3() ->  ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), F4() ->  SortSymbol of F1(), F5() ->  Element of the Sorts of (TermAlg F1()) . F4(), F6() ->  Element of the Sorts of (TermAlg F1()) . F4(), P1[ set ] } :
 for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= F5() '=' F6()
provided
A1: ((F3() -hash) . F4()) . F5() = ((F3() -hash) . F4()) . F6() and
A2: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds
ex h being ManySortedFunction of F2(),C st
( h is_homomorphism F2(),C & G = h ** F3() )
proofend;

scheme :: BIRKHOFF:sch 5
FreeIsGen{ F1() ->  non empty non void ManySortedSign , F2() ->  V2() ManySortedSet of the carrier of F1(), F3() ->  strict non-empty MSAlgebra over F1(), F4() ->  ManySortedFunction of F2(), the Sorts of F3(), P1[ set ] } :
 F4() .:.: F2() is V2() GeneratorSet of F3()
provided
A1: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of F2(), the Sorts of C st P1[C] holds
ex H being ManySortedFunction of F3(),C st
( H is_homomorphism F3(),C & H ** F4() = G & ( for K being ManySortedFunction of F3(),C st K is_homomorphism F3(),C & K ** F4() = G holds
H = K ) ) and
A2: P1[F3()] and
A3: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B]
proofend;

scheme :: BIRKHOFF:sch 6
Hashisonto{ F1() ->  non empty non void ManySortedSign , F2() ->  strict non-empty MSAlgebra over F1(), F3() ->  ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), P1[ set ] } :
 F3() -hash is_epimorphism FreeMSA ( the carrier of F1() --> NAT),F2()
provided
A1: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P1[C] holds
ex H being ManySortedFunction of F2(),C st
( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds
H = K ) ) and
A2: P1[F2()] and
A3: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B]
proofend;

scheme :: BIRKHOFF:sch 7
FinGenAlgInVar{ F1() ->  non empty non void ManySortedSign , F2() ->  strict non-empty finitely-generated MSAlgebra over F1(), F3() ->  non-empty MSAlgebra over F1(), F4() ->  ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F3(), P1[ set ], P2[ set ] } :
 P1[F2()]
provided
A1: P2[F2()] and
A2: P1[F3()] and
A3: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds
ex h being ManySortedFunction of F3(),C st
( h is_homomorphism F3(),C & G = h ** F4() ) and
A4: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A5: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)]
proofend;

scheme :: BIRKHOFF:sch 8
QuotEpi{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), F3() ->  non-empty MSAlgebra over F1(), P1[ set ] } :
 P1[F3()]
provided
A1: ex H being ManySortedFunction of F2(),F3() st H is_epimorphism F2(),F3() and
A2: P1[F2()] and
A3: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A4: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)]
proofend;

scheme :: BIRKHOFF:sch 9
AllFinGen{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), P1[ set ] } :
 P1[F2()]
provided
A1: for B being strict non-empty finitely-generated MSSubAlgebra of F2() holds P1[B] and
A2: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A3: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A4: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)] and
A5: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proofend;

scheme :: BIRKHOFF:sch 10
FreeInModIsInVar1{ F1() ->  non empty non void ManySortedSign , F2() ->  non-empty MSAlgebra over F1(), P1[ set ], P2[ set ] } :
 P2[F2()]
provided
A1: for A being non-empty MSAlgebra over F1() holds
( P2[A] iff for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= e ) holds
A |= e ) and
A2: P1[F2()]
proofend;

scheme :: BIRKHOFF:sch 11
FreeInModIsInVar{ F1() ->  non empty non void ManySortedSign , F2() ->  strict non-empty MSAlgebra over F1(), F3() ->  ManySortedFunction of the carrier of F1() --> NAT, the Sorts of F2(), P1[ set ], P2[ set ] } :
 P1[F2()]
provided
A1: for A being non-empty MSAlgebra over F1() holds
( P2[A] iff for s being SortSymbol of F1()
for e being Element of (Equations F1()) . s st ( for B being non-empty MSAlgebra over F1() st P1[B] holds
B |= e ) holds
A |= e ) and
A2: for C being non-empty MSAlgebra over F1()
for G being ManySortedFunction of the carrier of F1() --> NAT, the Sorts of C st P2[C] holds
ex H being ManySortedFunction of F2(),C st
( H is_homomorphism F2(),C & H ** F3() = G & ( for K being ManySortedFunction of F2(),C st K is_homomorphism F2(),C & K ** F3() = G holds
H = K ) ) and
A3: P2[F2()] and
A4: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A5: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A6: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proofend;

scheme :: BIRKHOFF:sch 12
Birkhoff{ F1() ->  non empty non void ManySortedSign , P1[ set ] } :
 ex E being EqualSet of F1() st
for A being non-empty MSAlgebra over F1() holds
( P1[A] iff A |= E )
provided
A1: for A, B being non-empty MSAlgebra over F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra over F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A3: for A being non-empty MSAlgebra over F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg (A,R)] and
A4: for I being set
for F being MSAlgebra-Family of I,F1() st ( for i being set st i in I holds
ex A being MSAlgebra over F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proofend;