:: EQUATION semantic presentation

theorem Th1: :: EQUATION:1

for A being set
for B, C being non empty set
for f being Function of A,B
for g being Function of B,C st rng (g * f) = C holds
rng g = C

proof end;

theorem :: EQUATION:2

for I being set
for A being ManySortedSet of I
for B, C being V2 ManySortedSet of I
for f being ManySortedFunction of A,B
for g being ManySortedFunction of B,C st g ** f is "onto" holds
g is "onto"

proof end;

theorem Th3: :: EQUATION:3

for A, B being non empty set
for C, y being set
for f being Function st f in Funcs A,(Funcs B,C) & y in B holds
( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )

proof end;

theorem :: EQUATION:4

canceled;

theorem :: EQUATION:5

for I being set
for A, B being ManySortedSet of I st A is_transformable_to B holds
for f being ManySortedFunction of I st doms f = A & rngs f c= B holds
f is ManySortedFunction of A,B

proof end;

theorem Th6: :: EQUATION:6

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B
for C, E being ManySortedSubset of A
for D being ManySortedSubset of C st E = D holds
(F || C) || D = F || E

proof end;

theorem Th7: :: EQUATION:7

for I being set
for B being V2 ManySortedSet of I
for C being ManySortedSet of I
for A being ManySortedSubset of C
for F being ManySortedFunction of A,B ex G being ManySortedFunction of C,B st G || A = F

proof end;

definition

let I be set ;
let A be ManySortedSet of I;
let F be ManySortedFunction of I;
func F "" A -> ManySortedSet of I means :Def1: :: EQUATION:def 1
for i being set st i in I holds
it . i = (F . i) " (A . i);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines "" EQUATION:def 1 :

theorem :: EQUATION:8

for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B holds F .:.: C is ManySortedSubset of B

proof end;

theorem :: EQUATION:9

for I being set
for A, B, C being ManySortedSet of I
for F being ManySortedFunction of A,B holds F "" C is ManySortedSubset of A

proof end;

theorem :: EQUATION:10

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st F is "onto" holds
F .:.: A = B

proof end;

theorem :: EQUATION:11

for I being set
for A, B being ManySortedSet of I
for F being ManySortedFunction of A,B st A is_transformable_to B holds
F "" B = A

proof end;

theorem :: EQUATION:12

for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I st A c= rngs F holds
F .:.: (F "" A) = A

proof end;

theorem :: EQUATION:13

for I being set
for f being ManySortedFunction of I
for X being ManySortedSet of I holds f .:.: X c= rngs f

proof end;

theorem Th14: :: EQUATION:14

for I being set
for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f

proof end;

theorem Th15: :: EQUATION:15

for I being set
for f being ManySortedFunction of I holds f "" (rngs f) = doms f

proof end;

theorem :: EQUATION:16

for I being set
for A being ManySortedSet of I holds (id A) .:.: A = A

proof end;

theorem :: EQUATION:17

for I being set
for A being ManySortedSet of I holds (id A) "" A = A

proof end;

theorem :: EQUATION:18

canceled;

theorem Th19: :: EQUATION:19

for S being non empty non void ManySortedSign
for A being MSAlgebra of S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A,the Charact of A #)

proof end;

theorem Th20: :: EQUATION:20

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args o,A holds
x in Args o,U0

proof end;

theorem Th21: :: EQUATION:21

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args o,A holds
(Den o,A) . x = (Den o,U0) . x

proof end;

theorem Th22: :: EQUATION:22

for I being set
for S being non empty non void ManySortedSign
for F being MSAlgebra-Family of I,S
for B being MSSubAlgebra of product F
for o being OperSymbol of S
for x being set st x in Args o,B holds
( (Den o,B) . x is Function & (Den o,(product F)) . x is Function )

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let B be MSSubAlgebra of A;
func SuperAlgebraSet B -> set means :Def2: :: EQUATION:def 2
for x being set holds
( x in it iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines SuperAlgebraSet EQUATION:def 2 :

registration

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let B be MSSubAlgebra of A;
cluster SuperAlgebraSet B -> non empty ;
coherence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
cluster strict non-empty free MSAlgebra of S;
existence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
let X be V2 locally-finite MSSubset of A;
cluster GenMSAlg X -> finitely-generated ;
coherence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
cluster strict non-empty finitely-generated MSSubAlgebra of A;
existence

proof end;

end;

registration

let S be non empty non void ManySortedSign ;
let A be feasible MSAlgebra of S;
cluster feasible MSSubAlgebra of A;
existence

proof end;

end;

theorem Th23: :: EQUATION:23

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for A being MSAlgebra of S
for C being MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0
for g being ManySortedFunction of C,U0 st g = h || D holds
for o being OperSymbol of S
for x being Element of Args o,A
for y being Element of Args o,C st Args o,C <> {} & x = y holds
h # x = g # y

proof end;

theorem Th24: :: EQUATION:24

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for A being feasible MSAlgebra of S
for C being feasible MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0

proof end;

theorem :: EQUATION:25

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for B being strict non-empty MSAlgebra of S
for G being GeneratorSet of U0
for H being V2 GeneratorSet of B
for f being ManySortedFunction of U0,B st H c= f .:.: G & f is_homomorphism U0,B holds
f is_epimorphism U0,B

proof end;

theorem Th26: :: EQUATION:26

for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra of S
for W being strict non-empty free MSAlgebra of S
for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )

proof end;

theorem Th27: :: EQUATION:27

for S being non empty non void ManySortedSign
for I being non empty finite set
for A being non-empty MSAlgebra of S
for F being MSAlgebra-Family of I,S st ( for i being Element of I ex C being strict non-empty finitely-generated MSSubAlgebra of A st C = F . i ) holds
ex B being strict non-empty finitely-generated MSSubAlgebra of A st
for i being Element of I holds F . i is MSSubAlgebra of B

proof end;

theorem Th28: :: EQUATION:28

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M & B is MSSubAlgebra of M )

proof end;

theorem :: EQUATION:29

for SG being non empty non void ManySortedSign
for AG being non-empty MSAlgebra of SG
for C being set st C = { A where A is Element of MSSub AG : ex R being strict non-empty finitely-generated MSSubAlgebra of AG st R = A } holds
for F being MSAlgebra-Family of C,SG st ( for c being set st c in C holds
c = F . c ) holds
ex PS being strict non-empty MSSubAlgebra of product F ex BA being ManySortedFunction of PS,AG st BA is_epimorphism PS,AG

proof end;

theorem :: EQUATION:30

for S being non empty non void ManySortedSign
for U0 being free feasible MSAlgebra of S
for A being free GeneratorSet of U0
for Z being MSSubset of U0 st Z c= A & GenMSAlg Z is feasible holds
GenMSAlg Z is free

proof end;

definition

let S be non empty non void ManySortedSign ;
func TermAlg S -> MSAlgebra of S equals :: EQUATION:def 3
FreeMSA (the carrier of S --> NAT );
correctness ;

end;

:: deftheorem defines TermAlg EQUATION:def 3 :

registration

let S be non empty non void ManySortedSign ;
cluster TermAlg S -> strict non-empty free ;
coherence ;

end;

definition

let S be non empty non void ManySortedSign ;
func Equations S -> ManySortedSet of the carrier of S equals :: EQUATION:def 4
[|the Sorts of (TermAlg S),the Sorts of (TermAlg S)|];
correctness ;

end;

:: deftheorem defines Equations EQUATION:def 4 :

registration

let S be non empty non void ManySortedSign ;
cluster Equations S -> V2 ;
coherence ;

end;

definition

let S be non empty non void ManySortedSign ;
mode EqualSet of S is ManySortedSubset of Equations S;

end;

notation

let S be non empty non void ManySortedSign ;
let s be SortSymbol of S;
let x, y be Element of the Sorts of (TermAlg S) . s;
synonym x '=' y for [S,s];

end;

definition

let S be non empty non void ManySortedSign ;
let s be SortSymbol of S;
let x, y be Element of the Sorts of (TermAlg S) . s;
:: original: '='
redefine func x '=' y -> Element of (Equations S) . s;
coherence

proof end;

end;

theorem Th31: :: EQUATION:31

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s holds e `1 in the Sorts of (TermAlg S) . s

proof end;

theorem Th32: :: EQUATION:32

for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s holds e `2 in the Sorts of (TermAlg S) . s

proof end;

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let s be SortSymbol of S;
let e be Element of (Equations S) . s;
pred A |= e means :Def5: :: EQUATION:def 5
for h being ManySortedFunction of (TermAlg S),A st h is_homomorphism TermAlg S,A holds
(h . s) . (e `1 ) = (h . s) . (e `2 );

end;

:: deftheorem Def5 defines |= EQUATION:def 5 :

definition

let S be non empty non void ManySortedSign ;
let A be MSAlgebra of S;
let E be EqualSet of S;
pred A |= E means :Def6: :: EQUATION:def 6
for s being SortSymbol of S
for e being Element of (Equations S) . s st e in E . s holds
A |= e;

end;

:: deftheorem Def6 defines |= EQUATION:def 6 :

theorem Th33: :: EQUATION:33

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for s being SortSymbol of S
for e being Element of (Equations S) . s
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= e

proof end;

theorem :: EQUATION:34

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for E being EqualSet of S
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds
U2 |= E

proof end;

theorem Th35: :: EQUATION:35

for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra of S
for s being SortSymbol of S
for e being Element of (Equations S) . s st U0,U1 are_isomorphic & U0 |= e holds
U1 |= e

proof end;

theorem :: EQUATION:36

for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra of S
for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds
U1 |= E

proof end;

theorem Th37: :: EQUATION:37

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for s being SortSymbol of S
for e being Element of (Equations S) . s
for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg U0,R |= e

proof end;

theorem :: EQUATION:38

for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra of S
for E being EqualSet of S
for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg U0,R |= E

proof end;

Lm1: for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s
for I being non empty set
for A being MSAlgebra-Family of I,S st ( for i being Element of I holds A . i |= e ) holds
product A |= e

proof end;

theorem Th39: :: EQUATION:39

for I being set
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of (Equations S) . s
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra of S st
( A = F . i & A |= e ) ) holds
product F |= e

proof end;

theorem :: EQUATION:40

for I being set
for S being non empty non void ManySortedSign
for E being EqualSet of S
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra of S st
( A = F . i & A |= E ) ) holds
product F |= E

proof end;