:: Equations in Many Sorted Algebras
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 1997-2018 Association of Mizar Users

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 (() . y) = A & rng (() . y) c= C )
proof end;

theorem :: EQUATION:4
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 Th5: :: EQUATION:5
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 Th6: :: EQUATION:6
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 object st i in I holds
it . i = (F . i) " (A . i);
existence
ex b1 being ManySortedSet of I st
for i being object st i in I holds
b1 . i = (F . i) " (A . i)
proof end;
uniqueness
for b1, b2 being ManySortedSet of I st ( for i being object st i in I holds
b1 . i = (F . i) " (A . i) ) & ( for i being object st i in I holds
b2 . i = (F . i) " (A . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines "" EQUATION:def 1 :
for I being set
for A being ManySortedSet of I
for F being ManySortedFunction of I
for b4 being ManySortedSet of I holds
( b4 = F "" A iff for i being object st i in I holds
b4 . i = (F . i) " (A . i) );

theorem :: EQUATION:7
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: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 A
proof end;

theorem :: EQUATION:9
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:10
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:11
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:12
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 Th13: :: EQUATION:13
for I being set
for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f
proof end;

theorem Th14: :: EQUATION:14
for I being set
for f being ManySortedFunction of I holds f "" (rngs f) = doms f
proof end;

theorem :: EQUATION:15
for I being set
for A being ManySortedSet of I holds (id A) .:.: A = A
proof end;

theorem :: EQUATION:16
for I being set
for A being ManySortedSet of I holds (id A) "" A = A
proof end;

theorem Th17: :: EQUATION:17
for S being non empty non void ManySortedSign
for A being MSAlgebra over S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A, the Charact of A #) by MSUALG_2:5;

theorem Th18: :: EQUATION:18
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over 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 Th19: :: EQUATION:19
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over 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 Th20: :: EQUATION:20
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 object st x in Args (o,B) holds
( (Den (o,B)) . x is Function & (Den (o,())) . x is Function )
proof end;

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

:: deftheorem Def2 defines SuperAlgebraSet EQUATION:def 2 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for B being MSSubAlgebra of A
for b4 being set holds
( b4 = SuperAlgebraSet B iff for x being object holds
( x in b4 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) );

registration
let S be non empty non void ManySortedSign ;
let A be MSAlgebra over S;
let B be MSSubAlgebra of A;
cluster SuperAlgebraSet B -> non empty ;
coherence
not SuperAlgebraSet B is empty
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
cluster strict non-empty free for MSAlgebra over S;
existence
ex b1 being MSAlgebra over S st
( b1 is strict & b1 is non-empty & b1 is free )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
let X be V2() V32() MSSubset of A;
coherence
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra over S;
existence
ex b1 being MSSubAlgebra of A st
( b1 is strict & b1 is non-empty & b1 is finitely-generated )
proof end;
end;

registration
let S be non empty non void ManySortedSign ;
let A be feasible MSAlgebra over S;
cluster feasible for MSSubAlgebra of A;
existence
ex b1 being MSSubAlgebra of A st b1 is feasible
proof end;
end;

theorem Th21: :: EQUATION:21
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for A being MSAlgebra over 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 Th22: :: EQUATION:22
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for A being feasible MSAlgebra over 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:23
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for B being strict non-empty MSAlgebra over 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 Th24: :: EQUATION:24
for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for W being strict non-empty free MSAlgebra over 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 Th25: :: EQUATION:25
for S being non empty non void ManySortedSign
for I being non empty finite set
for A being non-empty MSAlgebra over 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 Th26: :: EQUATION:26
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over 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:27
for SG being non empty non void ManySortedSign
for AG being non-empty MSAlgebra over 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 object 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:28
for S being non empty non void ManySortedSign
for U0 being free feasible MSAlgebra over 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 over S equals :: EQUATION:def 3
FreeMSA ( the carrier of S --> NAT);
correctness
coherence
FreeMSA ( the carrier of S --> NAT) is MSAlgebra over S
;
;
end;

:: deftheorem defines TermAlg EQUATION:def 3 :
for S being non empty non void ManySortedSign holds TermAlg S = FreeMSA ( the carrier of S --> NAT);

registration
let S be non empty non void ManySortedSign ;
coherence
( TermAlg S is strict & TermAlg S is non-empty & TermAlg S is free )
;
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 (), the Sorts of ()|];
correctness
coherence
[| the Sorts of (), the Sorts of ()|] is ManySortedSet of the carrier of S
;
;
end;

:: deftheorem defines Equations EQUATION:def 4 :
for S being non empty non void ManySortedSign holds Equations S = [| the Sorts of (), the Sorts of ()|];

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 () . 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 () . s;
:: original: '='
redefine func x '=' y -> Element of () . s;
coherence
'=' is Element of () . s
proof end;
end;

theorem Th29: :: EQUATION:29
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of () . s holds e 1 in the Sorts of () . s
proof end;

theorem Th30: :: EQUATION:30
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of () . s holds e 2 in the Sorts of () . s
proof end;

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

:: deftheorem defines |= EQUATION:def 5 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for s being SortSymbol of S
for e being Element of () . s holds
( A |= e iff for h being ManySortedFunction of (),A st h is_homomorphism TermAlg S,A holds
(h . s) . (e 1) = (h . s) . (e 2) );

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

:: deftheorem defines |= EQUATION:def 6 :
for S being non empty non void ManySortedSign
for A being MSAlgebra over S
for E being EqualSet of S holds
( A |= E iff for s being SortSymbol of S
for e being Element of () . s st e in E . s holds
A |= e );

theorem Th31: :: EQUATION:31
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of () . s
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= e holds
U2 |= e
proof end;

theorem :: EQUATION:32
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for E being EqualSet of S
for U2 being strict non-empty MSSubAlgebra of U0 st U0 |= E holds
U2 |= E by Th31;

theorem Th33: :: EQUATION:33
for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of () . s st U0,U1 are_isomorphic & U0 |= e holds
U1 |= e
proof end;

theorem :: EQUATION:34
for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for E being EqualSet of S st U0,U1 are_isomorphic & U0 |= E holds
U1 |= E by Th33;

theorem Th35: :: EQUATION:35
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for s being SortSymbol of S
for e being Element of () . s
for R being MSCongruence of U0 st U0 |= e holds
QuotMSAlg (U0,R) |= e
proof end;

theorem :: EQUATION:36
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for E being EqualSet of S
for R being MSCongruence of U0 st U0 |= E holds
QuotMSAlg (U0,R) |= E by Th35;

Lm1: for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of () . 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 Th37: :: EQUATION:37
for I being set
for S being non empty non void ManySortedSign
for s being SortSymbol of S
for e being Element of () . s
for F being MSAlgebra-Family of I,S st ( for i being set st i in I holds
ex A being MSAlgebra over S st
( A = F . i & A |= e ) ) holds
product F |= e
proof end;

theorem :: EQUATION:38
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 over S st
( A = F . i & A |= E ) ) holds
product F |= E
proof end;