:: BIRKHOFF semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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 of S;
let F be ManySortedFunction of X,the Sorts of A;
func F -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:18;
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 of 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being non empty non void ManySortedSign
for A being non-empty MSAlgebra of 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 )
proof end;

scheme :: BIRKHOFF:sch 1
ExFreeAlg1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), P1[ set ] } :
ex A being strict non-empty MSAlgebra of F1() ex F being ManySortedFunction of F2(),A st
( P1[A] & F is_epimorphism F2(),A & ( for B being non-empty MSAlgebra of 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 of F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra of 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 of F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;

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 of F1() ex F being ManySortedFunction of F2(),the Sorts of A st
( P1[A] & ( for B being non-empty MSAlgebra of 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 of F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra of 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 of F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;

scheme :: BIRKHOFF:sch 3
Exhash{ 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 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 of 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() )
proof end;

scheme :: BIRKHOFF:sch 4
EqTerms{ 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 B being non-empty MSAlgebra of 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 of 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() )
proof end;

scheme :: BIRKHOFF:sch 5
FreeIsGen{ 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
A1: for C being non-empty MSAlgebra of 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 of F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B]
proof end;

scheme :: BIRKHOFF:sch 6
Hashisonto{ 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
A1: for C being non-empty MSAlgebra of 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 of F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B]
proof end;

scheme :: BIRKHOFF:sch 7
FinGenAlgInVar{ 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
A1: P2[F2()] and
A2: P1[F3()] and
A3: for C being non-empty MSAlgebra of 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 of F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A5: for A being non-empty MSAlgebra of F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg A,R]
proof end;

scheme :: BIRKHOFF:sch 8
QuotEpi{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), F3() -> non-empty MSAlgebra of 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 of F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A4: for A being non-empty MSAlgebra of F1()
for R being MSCongruence of A st P1[A] holds
P1[ QuotMSAlg A,R]
proof end;

scheme :: BIRKHOFF:sch 9
AllFinGen{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of 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 of F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A3: for A being non-empty MSAlgebra of F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A4: for A being non-empty MSAlgebra of 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 of F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;

scheme :: BIRKHOFF:sch 10
FreeInModIsInVar1{ F1() -> non empty non void ManySortedSign , F2() -> non-empty MSAlgebra of F1(), P1[ set ], P2[ set ] } :
P2[F2()]
provided
A1: for A being non-empty MSAlgebra of 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 of F1() st P1[B] holds
B |= e ) holds
A |= e ) and
A2: P1[F2()]
proof end;

scheme :: BIRKHOFF:sch 11
FreeInModIsInVar{ 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
A1: for A being non-empty MSAlgebra of 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 of F1() st P1[B] holds
B |= e ) holds
A |= e ) and
A2: for C being non-empty MSAlgebra of 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 of F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A5: for A being non-empty MSAlgebra of 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 of F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;

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 of F1() holds
( P1[A] iff A |= E )
provided
A1: for A, B being non-empty MSAlgebra of F1() st A,B are_isomorphic & P1[A] holds
P1[B] and
A2: for A being non-empty MSAlgebra of F1()
for B being strict non-empty MSSubAlgebra of A st P1[A] holds
P1[B] and
A3: for A being non-empty MSAlgebra of 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 of F1() st
( A = F . i & P1[A] ) ) holds
P1[ product F]
proof end;