:: EQUATION semantic presentation

theorem Th1: :: EQUATION:1

for b₁ being set
for b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st rng (b₅ * b₄) = b₃ holds
rng b₅ = b₃

proof end;

theorem Th2: :: EQUATION:2

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃, b₄ being V2 ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,b₃
for b₆ being ManySortedFunction of b₃,b₄ st b₆ ** b₅ is "onto" holds
b₆ is "onto"

proof end;

theorem Th3: :: EQUATION:3

for b₁, b₂ being non empty set
for b₃, b₄ being set
for b₅ being Function st b₅ in Funcs b₁,(Funcs b₂,b₃) & b₄ in b₂ holds
( dom ((commute b₅) . b₄) = b₁ & rng ((commute b₅) . b₄) c= b₃ )

proof end;

theorem Th4: :: EQUATION:4

canceled;

theorem Th5: :: EQUATION:5

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁ st b₂ is_transformable_to b₃ holds
for b₄ being ManySortedFunction of b₁ st doms b₄ = b₂ & rngs b₄ c= b₃ holds
b₄ is ManySortedFunction of b₂,b₃

proof end;

theorem Th6: :: EQUATION:6

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃
for b₅, b₆ being ManySortedSubset of b₂
for b₇ being ManySortedSubset of b₅ st b₆ = b₇ holds
(b₄ || b₅) || b₇ = b₄ || b₆

proof end;

theorem Th7: :: EQUATION:7

for b₁ being set
for b₂ being V2 ManySortedSet of b₁
for b₃ being ManySortedSet of b₁
for b₄ being ManySortedSubset of b₃
for b₅ being ManySortedFunction of b₄,b₂ ex b₆ being ManySortedFunction of b₃,b₂ st b₆ || b₄ = b₅

proof end;

definition

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be ManySortedFunction of c₁;
func c₃ "" c₂ -> ManySortedSet of a₁ means :Def1: :: EQUATION:def 1
for b₁ being set st b₁ in a₁ holds
a₄ . b₁ = (a₃ . b₁) " (a₂ . b₁);
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th8: :: EQUATION:8

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,b₃ holds b₅ .:.: b₄ is ManySortedSubset of b₃

proof end;

theorem Th9: :: EQUATION:9

for b₁ being set
for b₂, b₃, b₄ being ManySortedSet of b₁
for b₅ being ManySortedFunction of b₂,b₃ holds b₅ "" b₄ is ManySortedSubset of b₂

proof end;

theorem Th10: :: EQUATION:10

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₄ is "onto" holds
b₄ .:.: b₂ = b₃

proof end;

theorem Th11: :: EQUATION:11

for b₁ being set
for b₂, b₃ being ManySortedSet of b₁
for b₄ being ManySortedFunction of b₂,b₃ st b₂ is_transformable_to b₃ holds
b₄ "" b₃ = b₂

proof end;

theorem Th12: :: EQUATION:12

for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being ManySortedFunction of b₁ st b₂ c= rngs b₃ holds
b₃ .:.: (b₃ "" b₂) = b₂

proof end;

theorem Th13: :: EQUATION:13

for b₁ being set
for b₂ being ManySortedFunction of b₁
for b₃ being ManySortedSet of b₁ holds b₂ .:.: b₃ c= rngs b₂

proof end;

theorem Th14: :: EQUATION:14

for b₁ being set
for b₂ being ManySortedFunction of b₁ holds b₂ .:.: (doms b₂) = rngs b₂

proof end;

theorem Th15: :: EQUATION:15

for b₁ being set
for b₂ being ManySortedFunction of b₁ holds b₂ "" (rngs b₂) = doms b₂

proof end;

theorem Th16: :: EQUATION:16

for b₁ being set
for b₂ being ManySortedSet of b₁ holds (id b₂) .:.: b₂ = b₂

proof end;

theorem Th17: :: EQUATION:17

for b₁ being set
for b₂ being ManySortedSet of b₁ holds (id b₂) "" b₂ = b₂

proof end;

theorem Th18: :: EQUATION:18

canceled;

theorem Th19: :: EQUATION:19

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁ holds b₂ is MSSubAlgebra of MSAlgebra(# the Sorts of b₂,the Charact of b₂ #)

proof end;

theorem Th20: :: EQUATION:20

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubAlgebra of b₂
for b₄ being OperSymbol of b₁
for b₅ being set st b₅ in Args b₄,b₃ holds
b₅ in Args b₄,b₂

proof end;

theorem Th21: :: EQUATION:21

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being MSSubAlgebra of b₂
for b₄ being OperSymbol of b₁
for b₅ being set st b₅ in Args b₄,b₃ holds
(Den b₄,b₃) . b₅ = (Den b₄,b₂) . b₅

proof end;

theorem Th22: :: EQUATION:22

for b₁ being set
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra-Family of b₁,b₂
for b₄ being MSSubAlgebra of product b₃
for b₅ being OperSymbol of b₂
for b₆ being set st b₆ in Args b₅,b₄ holds
( (Den b₅,b₄) . b₆ is Function & (Den b₅,(product b₃)) . b₆ is Function )

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubAlgebra of c₂;
func SuperAlgebraSet c₃ -> set means :Def2: :: EQUATION:def 2
for b₁ being set holds
( b₁ in a₄ iff ex b₂ being strict MSSubAlgebra of a₂ st
( b₁ = b₂ & a₃ is MSSubAlgebra of b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines SuperAlgebraSet EQUATION:def 2 :

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be MSSubAlgebra of c₂;
cluster SuperAlgebraSet a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
cluster strict non-empty free MSAlgebra of a₁;
existence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
let c₃ be V2 locally-finite MSSubset of c₂;
cluster GenMSAlg a₃ -> finitely-generated ;
coherence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster strict non-empty finitely-generated MSSubAlgebra of a₂;
existence

proof end;

end;

registration

let c₁ be non empty non void ManySortedSign ;
let c₂ be feasible MSAlgebra of c₁;
cluster feasible MSSubAlgebra of a₂;
existence

proof end;

end;

theorem Th23: :: EQUATION:23

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being MSAlgebra of b₁
for b₄ being MSSubAlgebra of b₃
for b₅ being ManySortedSubset of the Sorts of b₃ st b₅ = the Sorts of b₄ holds
for b₆ being ManySortedFunction of b₃,b₂
for b₇ being ManySortedFunction of b₄,b₂ st b₇ = b₆ || b₅ holds
for b₈ being OperSymbol of b₁
for b₉ being Element of Args b₈,b₃
for b₁₀ being Element of Args b₈,b₄ st Args b₈,b₄ <> {} & b₉ = b₁₀ holds
b₆ # b₉ = b₇ # b₁₀

proof end;

theorem Th24: :: EQUATION:24

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being feasible MSAlgebra of b₁
for b₄ being feasible MSSubAlgebra of b₃
for b₅ being ManySortedSubset of the Sorts of b₃ st b₅ = the Sorts of b₄ holds
for b₆ being ManySortedFunction of b₃,b₂ st b₆ is_homomorphism b₃,b₂ holds
for b₇ being ManySortedFunction of b₄,b₂ st b₇ = b₆ || b₅ holds
b₇ is_homomorphism b₄,b₂

proof end;

theorem Th25: :: EQUATION:25

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being strict non-empty MSAlgebra of b₁
for b₄ being GeneratorSet of b₂
for b₅ being V2 GeneratorSet of b₃
for b₆ being ManySortedFunction of b₂,b₃ st b₅ c= b₆ .:.: b₄ & b₆ is_homomorphism b₂,b₃ holds
b₆ is_epimorphism b₂,b₃

proof end;

theorem Th26: :: EQUATION:26

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being strict non-empty free MSAlgebra of b₁
for b₅ being ManySortedFunction of b₂,b₃ st b₅ is_epimorphism b₂,b₃ holds
for b₆ being ManySortedFunction of b₄,b₃ st b₆ is_homomorphism b₄,b₃ holds
ex b₇ being ManySortedFunction of b₄,b₂ st
( b₇ is_homomorphism b₄,b₂ & b₆ = b₅ ** b₇ )

proof end;

theorem Th27: :: EQUATION:27

for b₁ being non empty non void ManySortedSign
for b₂ being non empty finite set
for b₃ being non-empty MSAlgebra of b₁
for b₄ being MSAlgebra-Family of b₂,b₁ st ( for b₅ being Element of b₂ ex b₆ being strict non-empty finitely-generated MSSubAlgebra of b₃ st b₆ = b₄ . b₅ ) holds
ex b₅ being strict non-empty finitely-generated MSSubAlgebra of b₃ st
for b₆ being Element of b₂ holds b₄ . b₆ is MSSubAlgebra of b₅

proof end;

theorem Th28: :: EQUATION:28

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃, b₄ being strict non-empty finitely-generated MSSubAlgebra of b₂ ex b₅ being strict non-empty finitely-generated MSSubAlgebra of b₂ st
( b₃ is MSSubAlgebra of b₅ & b₄ is MSSubAlgebra of b₅ )

proof end;

theorem Th29: :: EQUATION:29

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being set st b₃ = { b₄ where B is Element of MSSub b₂ : ex b₁ being strict non-empty finitely-generated MSSubAlgebra of b₂ st b₅ = b₄ } holds
for b₄ being MSAlgebra-Family of b₃,b₁ st ( for b₅ being set st b₅ in b₃ holds
b₅ = b₄ . b₅ ) holds
ex b₅ being strict non-empty MSSubAlgebra of product b₄ex b₆ being ManySortedFunction of b₅,b₂ st b₆ is_epimorphism b₅,b₂

proof end;

theorem Th30: :: EQUATION:30

for b₁ being non empty non void ManySortedSign
for b₂ being free feasible MSAlgebra of b₁
for b₃ being free GeneratorSet of b₂
for b₄ being MSSubset of b₂ st b₄ c= b₃ & GenMSAlg b₄ is feasible holds
GenMSAlg b₄ is free

proof end;

definition

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

end;

:: deftheorem Def3 defines TermAlg EQUATION:def 3 :

registration

let c₁ be non empty non void ManySortedSign ;
cluster TermAlg a₁ -> strict non-empty free ;
coherence ;

end;

definition

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

end;

:: deftheorem Def4 defines Equations EQUATION:def 4 :

registration

let c₁ be non empty non void ManySortedSign ;
cluster Equations a₁ -> V2 ;
coherence ;

end;

definition

let c₁ be non empty non void ManySortedSign ;
mode EqualSet of a₁ is ManySortedSubset of Equations a₁;

end;

notation

let c₁ be non empty non void ManySortedSign ;
let c₂ be SortSymbol of c₁;
let c₃, c₄ be Element of the Sorts of (TermAlg c₁) . c₂;
synonym c₃ '=' c₄ for [c₁,c₂];

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be SortSymbol of c₁;
let c₃, c₄ be Element of the Sorts of (TermAlg c₁) . c₂;
redefine func '=' as c₃ '=' c₄ -> Element of (Equations a₁) . a₂;
coherence

proof end;

end;

theorem Th31: :: EQUATION:31

for b₁ being non empty non void ManySortedSign
for b₂ being SortSymbol of b₁
for b₃ being Element of (Equations b₁) . b₂ holds b₃ `1 in the Sorts of (TermAlg b₁) . b₂

proof end;

theorem Th32: :: EQUATION:32

for b₁ being non empty non void ManySortedSign
for b₂ being SortSymbol of b₁
for b₃ being Element of (Equations b₁) . b₂ holds b₃ `2 in the Sorts of (TermAlg b₁) . b₂

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be SortSymbol of c₁;
let c₄ be Element of (Equations c₁) . c₃;
pred c₂ |= c₄ means :Def5: :: EQUATION:def 5
for b₁ being ManySortedFunction of (TermAlg a₁),a₂ st b₁ is_homomorphism TermAlg a₁,a₂ holds
(b₁ . a₃) . (a₄ `1 ) = (b₁ . a₃) . (a₄ `2 );

end;

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

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
let c₃ be EqualSet of c₁;
pred c₂ |= c₃ means :Def6: :: EQUATION:def 6
for b₁ being SortSymbol of a₁
for b₂ being Element of (Equations a₁) . b₁ st b₂ in a₃ . b₁ holds
a₂ |= b₂;

end;

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

theorem Th33: :: EQUATION:33

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being SortSymbol of b₁
for b₄ being Element of (Equations b₁) . b₃
for b₅ being strict non-empty MSSubAlgebra of b₂ st b₂ |= b₄ holds
b₅ |= b₄

proof end;

theorem Th34: :: EQUATION:34

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being EqualSet of b₁
for b₄ being strict non-empty MSSubAlgebra of b₂ st b₂ |= b₃ holds
b₄ |= b₃

proof end;

theorem Th35: :: EQUATION:35

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being SortSymbol of b₁
for b₅ being Element of (Equations b₁) . b₄ st b₂,b₃ are_isomorphic & b₂ |= b₅ holds
b₃ |= b₅

proof end;

theorem Th36: :: EQUATION:36

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being non-empty MSAlgebra of b₁
for b₄ being EqualSet of b₁ st b₂,b₃ are_isomorphic & b₂ |= b₄ holds
b₃ |= b₄

proof end;

theorem Th37: :: EQUATION:37

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being SortSymbol of b₁
for b₄ being Element of (Equations b₁) . b₃
for b₅ being MSCongruence of b₂ st b₂ |= b₄ holds
QuotMSAlg b₂,b₅ |= b₄

proof end;

theorem Th38: :: EQUATION:38

for b₁ being non empty non void ManySortedSign
for b₂ being non-empty MSAlgebra of b₁
for b₃ being EqualSet of b₁
for b₄ being MSCongruence of b₂ st b₂ |= b₃ holds
QuotMSAlg b₂,b₄ |= b₃

proof end;

Lemma25: for b₁ being non empty non void ManySortedSign
for b₂ being SortSymbol of b₁
for b₃ being Element of (Equations b₁) . b₂
for b₄ being non empty set
for b₅ being MSAlgebra-Family of b₄,b₁ st ( for b₆ being Element of b₄ holds b₅ . b₆ |= b₃ ) holds
product b₅ |= b₃

proof end;

theorem Th39: :: EQUATION:39

for b₁ being set
for b₂ being non empty non void ManySortedSign
for b₃ being SortSymbol of b₂
for b₄ being Element of (Equations b₂) . b₃
for b₅ being MSAlgebra-Family of b₁,b₂ st ( for b₆ being set st b₆ in b₁ holds
ex b₇ being MSAlgebra of b₂ st
( b₇ = b₅ . b₆ & b₇ |= b₄ ) ) holds
product b₅ |= b₄

proof end;

theorem Th40: :: EQUATION:40

for b₁ being set
for b₂ being non empty non void ManySortedSign
for b₃ being EqualSet of b₂
for b₄ being MSAlgebra-Family of b₁,b₂ st ( for b₅ being set st b₅ in b₁ holds
ex b₆ being MSAlgebra of b₂ st
( b₆ = b₄ . b₅ & b₆ |= b₃ ) ) holds
product b₄ |= b₃

proof end;