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

theorem Th1: :: EQUATION:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: EQUATION:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being ManySortedSet of I st
for i being set 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 set st i in I holds
b1 . i = (F . i) " (A . i) ) & ( for i being set 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 set st i in I holds
b4 . i = (F . i) " (A . i) );

theorem :: EQUATION:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for f being ManySortedFunction of I holds f .:.: (doms f) = rngs f
proof end;

theorem Th15: :: EQUATION:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for f being ManySortedFunction of I holds f "" (rngs f) = doms f
proof end;

theorem :: EQUATION:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds (id A) .:.: A = A
proof end;

theorem :: EQUATION:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for I being set
for A being ManySortedSet of I holds (id A) "" A = A
proof end;

theorem :: EQUATION:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th19: :: EQUATION:19  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 MSAlgebra of S holds A is MSSubAlgebra of MSAlgebra(# the Sorts of A,the Charact of A #)
proof end;

theorem Th20: :: EQUATION:20  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 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  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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
ex b1 being set st
for x being set 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 set holds
( x in b1 iff ex C being strict MSSubAlgebra of A st
( x = C & B is MSSubAlgebra of C ) ) ) & ( for x being set 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 of S
for B being MSSubAlgebra of A
for b4 being set holds
( b4 = SuperAlgebraSet B iff for x being set 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 of 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 MSAlgebra of S;
existence
ex b1 being MSAlgebra of 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 of S;
let X be V2 locally-finite MSSubset of A;
cluster GenMSAlg X -> finitely-generated ;
coherence
GenMSAlg X is finitely-generated
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
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 of S;
cluster feasible MSSubAlgebra of A;
existence
ex b1 being MSSubAlgebra of A st b1 is feasible
proof end;
end;

theorem Th23: :: EQUATION:23  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 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  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 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  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 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  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 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  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 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  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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  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 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
coherence
FreeMSA (the carrier of S --> NAT ) is MSAlgebra of 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 ;
cluster TermAlg S -> strict non-empty free ;
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 (TermAlg S),the Sorts of (TermAlg S)|];
correctness
coherence
[|the Sorts of (TermAlg S),the Sorts of (TermAlg S)|] 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 (TermAlg S),the Sorts of (TermAlg S)|];

registration
let S be non empty non void ManySortedSign ;
cluster Equations S -> V2 ;
coherence
Equations S is non-empty
;
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
'=' is Element of (Equations S) . s
proof end;
end;

theorem Th31: :: EQUATION:31  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 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  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 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 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for s being SortSymbol of S
for e being Element of (Equations S) . s holds
( A |= e iff for h being ManySortedFunction of (TermAlg S),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 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 :
for S being non empty non void ManySortedSign
for A being MSAlgebra of S
for E being EqualSet of S holds
( A |= E iff for s being SortSymbol of S
for e being Element of (Equations S) . s st e in E . s holds
A |= e );

theorem Th33: :: EQUATION:33  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 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  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 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  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 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  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 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  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 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  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 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;