:: BIRKHOFF semantic presentation

definition
let c1 be non empty non void ManySortedSign ;
let c2 be V2 ManySortedSet of the carrier of c1;
let c3 be non-empty MSAlgebra of c1;
let c4 be ManySortedFunction of c2,the Sorts of c3;
func c4 -hash -> ManySortedFunction of (FreeMSA a2),a3 means :Def1: :: BIRKHOFF:def 1
( a5 is_homomorphism FreeMSA a2,a3 & a5 || (FreeGen a2) = a4 ** (Reverse a2) );
existence
ex b1 being ManySortedFunction of (FreeMSA c2),c3 st
( b1 is_homomorphism FreeMSA c2,c3 & b1 || (FreeGen c2) = c4 ** (Reverse c2) ) by MSAFREE:def 5;
uniqueness
for b1, b2 being ManySortedFunction of (FreeMSA c2),c3 st b1 is_homomorphism FreeMSA c2,c3 & b1 || (FreeGen c2) = c4 ** (Reverse c2) & b2 is_homomorphism FreeMSA c2,c3 & b2 || (FreeGen c2) = c4 ** (Reverse c2) holds
b1 = b2 by EXTENS_1:18;
end;

:: deftheorem Def1 defines -hash BIRKHOFF:def 1 :
for b1 being non empty non void ManySortedSign
for b2 being V2 ManySortedSet of the carrier of b1
for b3 being non-empty MSAlgebra of b1
for b4 being ManySortedFunction of b2,the Sorts of b3
for b5 being ManySortedFunction of (FreeMSA b2),b3 holds
( b5 = b4 -hash iff ( b5 is_homomorphism FreeMSA b2,b3 & b5 || (FreeGen b2) = b4 ** (Reverse b2) ) );

theorem Th1: :: BIRKHOFF:1
for b1 being non empty non void ManySortedSign
for b2 being non-empty MSAlgebra of b1
for b3 being V2 ManySortedSet of the carrier of b1
for b4 being ManySortedFunction of b3,the Sorts of b2 holds rngs b4 c= rngs (b4 -hash )
proof end;

scheme :: BIRKHOFF:sch 1
s1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), P1[ set ] } :
ex b1 being strict non-empty MSAlgebra of F1()ex b2 being ManySortedFunction of F2(),b1 st
( P1[b1] & b2 is_epimorphism F2(),b1 & ( for b3 being non-empty MSAlgebra of F1()
for b4 being ManySortedFunction of F2(),b3 st b4 is_homomorphism F2(),b3 & P1[b3] holds
ex b5 being ManySortedFunction of b1,b3 st
( b5 is_homomorphism b1,b3 & b5 ** b2 = b4 & ( for b6 being ManySortedFunction of b1,b3 st b6 ** b2 = b4 holds
b5 = b6 ) ) ) )
provided
E3: for b1, b2 being non-empty MSAlgebra of F1() st b1,b2 are_isomorphic & P1[b1] holds
P1[b2] and
E4: for b1 being non-empty MSAlgebra of F1()
for b2 being strict non-empty MSSubAlgebra of b1 st P1[b1] holds
P1[b2] and
E5: for b1 being set
for b2 being MSAlgebra-Family of b1,F1() st ( for b3 being set st b3 in b1 holds
ex b4 being MSAlgebra of F1() st
( b4 = b2 . b3 & P1[b4] ) ) holds
P1[ product b2]
proof end;

scheme :: BIRKHOFF:sch 2
s2{ F1() -> non empty non void ManySortedSign , F2() -> V2 ManySortedSet of the carrier of F1(), P1[ set ] } :
ex b1 being strict non-empty MSAlgebra of F1()ex b2 being ManySortedFunction of F2(),the Sorts of b1 st
( P1[b1] & ( for b3 being non-empty MSAlgebra of F1()
for b4 being ManySortedFunction of F2(),the Sorts of b3 st P1[b3] holds
ex b5 being ManySortedFunction of b1,b3 st
( b5 is_homomorphism b1,b3 & b5 ** b2 = b4 & ( for b6 being ManySortedFunction of b1,b3 st b6 is_homomorphism b1,b3 & b6 ** b2 = b4 holds
b5 = b6 ) ) ) )
provided
E3: for b1, b2 being non-empty MSAlgebra of F1() st b1,b2 are_isomorphic & P1[b1] holds
P1[b2] and
E4: for b1 being non-empty MSAlgebra of F1()
for b2 being strict non-empty MSSubAlgebra of b1 st P1[b1] holds
P1[b2] and
E5: for b1 being set
for b2 being MSAlgebra-Family of b1,F1() st ( for b3 being set st b3 in b1 holds
ex b4 being MSAlgebra of F1() st
( b4 = b2 . b3 & P1[b4] ) ) holds
P1[ product b2]
proof end;

scheme :: BIRKHOFF:sch 3
s3{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3() -> non-empty MSAlgebra of 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 b1 being ManySortedFunction of F2(),F3() st
( b1 is_homomorphism F2(),F3() & F5() -hash = b1 ** (F4() -hash ) )
provided
E3: P1[F3()] and
E4: for b1 being non-empty MSAlgebra of F1()
for b2 being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of b1 st P1[b1] holds
ex b3 being ManySortedFunction of F2(),b1 st
( b3 is_homomorphism F2(),b1 & b2 = b3 ** F4() )
proof end;

scheme :: BIRKHOFF:sch 4
s4{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of 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 b1 being non-empty MSAlgebra of F1() st P1[b1] holds
b1 |= F5() '=' F6()
provided
E3: ((F3() -hash ) . F4()) . F5() = ((F3() -hash ) . F4()) . F6() and
E4: for b1 being non-empty MSAlgebra of F1()
for b2 being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of b1 st P1[b1] holds
ex b3 being ManySortedFunction of F2(),b1 st
( b3 is_homomorphism F2(),b1 & b2 = b3 ** F3() )
proof end;

scheme :: BIRKHOFF:sch 5
s5{ F1() -> non empty non void ManySortedSign , F2() -> V2 ManySortedSet of the carrier of F1(), F3() -> strict non-empty MSAlgebra of F1(), F4() -> ManySortedFunction of F2(),the Sorts of F3(), P1[ set ] } :
F4() .:.: F2() is V2 GeneratorSet of F3()
provided
E3: for b1 being non-empty MSAlgebra of F1()
for b2 being ManySortedFunction of F2(),the Sorts of b1 st P1[b1] holds
ex b3 being ManySortedFunction of F3(),b1 st
( b3 is_homomorphism F3(),b1 & b3 ** F4() = b2 & ( for b4 being ManySortedFunction of F3(),b1 st b4 is_homomorphism F3(),b1 & b4 ** F4() = b2 holds
b3 = b4 ) ) and
E4: P1[F3()] and
E5: for b1 being non-empty MSAlgebra of F1()
for b2 being strict non-empty MSSubAlgebra of b1 st P1[b1] holds
P1[b2]
proof end;

scheme :: BIRKHOFF:sch 6
s6{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty MSAlgebra of 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
E3: for b1 being non-empty MSAlgebra of F1()
for b2 being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of b1 st P1[b1] holds
ex b3 being ManySortedFunction of F2(),b1 st
( b3 is_homomorphism F2(),b1 & b3 ** F3() = b2 & ( for b4 being ManySortedFunction of F2(),b1 st b4 is_homomorphism F2(),b1 & b4 ** F3() = b2 holds
b3 = b4 ) ) and
E4: P1[F2()] and
E5: for b1 being non-empty MSAlgebra of F1()
for b2 being strict non-empty MSSubAlgebra of b1 st P1[b1] holds
P1[b2]
proof end;

scheme :: BIRKHOFF:sch 7
s7{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty finitely-generated MSAlgebra of F1(), F3() -> non-empty MSAlgebra of F1(), F4() -> ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of F3(), P1[ set ], P2[ set ] } :
P1[F2()]
provided
E3: P2[F2()] and
E4: P1[F3()] and
E5: for b1 being non-empty MSAlgebra of F1()
for b2 being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of b1 st P2[b1] holds
ex b3 being ManySortedFunction of F3(),b1 st
( b3 is_homomorphism F3(),b1 & b2 = b3 ** F4() ) and
E6: for b1, b2 being non-empty MSAlgebra of F1() st b1,b2 are_isomorphic & P1[b1] holds
P1[b2] and
E7: for b1 being non-empty MSAlgebra of F1()
for b2 being MSCongruence of b1 st P1[b1] holds
P1[ QuotMSAlg b1,b2]
proof end;

scheme :: BIRKHOFF:sch 8
s8{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3() -> non-empty MSAlgebra of F1(), P1[ set ] } :
P1[F3()]
provided
E3: ex b1 being ManySortedFunction of F2(),F3() st b1 is_epimorphism F2(),F3() and
E4: P1[F2()] and
E5: for b1, b2 being non-empty MSAlgebra of F1() st b1,b2 are_isomorphic & P1[b1] holds
P1[b2] and
E6: for b1 being non-empty MSAlgebra of F1()
for b2 being MSCongruence of b1 st P1[b1] holds
P1[ QuotMSAlg b1,b2]
proof end;

scheme :: BIRKHOFF:sch 9
s9{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), P1[ set ] } :
P1[F2()]
provided
E3: for b1 being strict non-empty finitely-generated MSSubAlgebra of F2() holds P1[b1] and
E4: for b1, b2 being non-empty MSAlgebra of F1() st b1,b2 are_isomorphic & P1[b1] holds
P1[b2] and
E5: for b1 being non-empty MSAlgebra of F1()
for b2 being strict non-empty MSSubAlgebra of b1 st P1[b1] holds
P1[b2] and
E6: for b1 being non-empty MSAlgebra of F1()
for b2 being MSCongruence of b1 st P1[b1] holds
P1[ QuotMSAlg b1,b2] and
E7: for b1 being set
for b2 being MSAlgebra-Family of b1,F1() st ( for b3 being set st b3 in b1 holds
ex b4 being MSAlgebra of F1() st
( b4 = b2 . b3 & P1[b4] ) ) holds
P1[ product b2]
proof end;

scheme :: BIRKHOFF:sch 10
s10{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), P1[ set ], P2[ set ] } :
P2[F2()]
provided
E3: for b1 being non-empty MSAlgebra of F1() holds
( P2[b1] iff for b2 being SortSymbol of F1()
for b3 being Element of (Equations F1()) . b2 st ( for b4 being non-empty MSAlgebra of F1() st P1[b4] holds
b4 |= b3 ) holds
b1 |= b3 ) and
E4: P1[F2()]
proof end;

scheme :: BIRKHOFF:sch 11
s11{ F1() -> non empty non void ManySortedSign , F2() -> strict non-empty MSAlgebra of F1(), F3() -> ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of F2(), P1[ set ], P2[ set ] } :
P1[F2()]
provided
E3: for b1 being non-empty MSAlgebra of F1() holds
( P2[b1] iff for b2 being SortSymbol of F1()
for b3 being Element of (Equations F1()) . b2 st ( for b4 being non-empty MSAlgebra of F1() st P1[b4] holds
b4 |= b3 ) holds
b1 |= b3 ) and
E4: for b1 being non-empty MSAlgebra of F1()
for b2 being ManySortedFunction of the carrier of F1() --> NAT ,the Sorts of b1 st P2[b1] holds
ex b3 being ManySortedFunction of F2(),b1 st
( b3 is_homomorphism F2(),b1 & b3 ** F3() = b2 & ( for b4 being ManySortedFunction of F2(),b1 st b4 is_homomorphism F2(),b1 & b4 ** F3() = b2 holds
b3 = b4 ) ) and
E5: P2[F2()] and
E6: for b1, b2 being non-empty MSAlgebra of F1() st b1,b2 are_isomorphic & P1[b1] holds
P1[b2] and
E7: for b1 being non-empty MSAlgebra of F1()
for b2 being strict non-empty MSSubAlgebra of b1 st P1[b1] holds
P1[b2] and
E8: for b1 being set
for b2 being MSAlgebra-Family of b1,F1() st ( for b3 being set st b3 in b1 holds
ex b4 being MSAlgebra of F1() st
( b4 = b2 . b3 & P1[b4] ) ) holds
P1[ product b2]
proof end;

scheme :: BIRKHOFF:sch 12
s12{ F1() -> non empty non void ManySortedSign , P1[ set ] } :
ex b1 being EqualSet of F1() st
for b2 being non-empty MSAlgebra of F1() holds
( P1[b2] iff b2 |= b1 )
provided
E3: for b1, b2 being non-empty MSAlgebra of F1() st b1,b2 are_isomorphic & P1[b1] holds
P1[b2] and
E4: for b1 being non-empty MSAlgebra of F1()
for b2 being strict non-empty MSSubAlgebra of b1 st P1[b1] holds
P1[b2] and
E5: for b1 being non-empty MSAlgebra of F1()
for b2 being MSCongruence of b1 st P1[b1] holds
P1[ QuotMSAlg b1,b2] and
E6: for b1 being set
for b2 being MSAlgebra-Family of b1,F1() st ( for b3 being set st b3 in b1 holds
ex b4 being MSAlgebra of F1() st
( b4 = b2 . b3 & P1[b4] ) ) holds
P1[ product b2]
proof end;