:: ALGSPEC1 semantic presentation

theorem Th1: :: ALGSPEC1:1

for f, g, h being Function st (dom f) /\ (dom g) c= dom h holds
(f +* g) +* h = (g +* f) +* h

proof end;

theorem Th2: :: ALGSPEC1:2

for f, g, h being Function st f c= g & (rng h) /\ (dom g) c= dom f holds
g * h = f * h

proof end;

theorem Th3: :: ALGSPEC1:3

for f, g, h being Function st dom f c= rng g & dom f misses rng h & g .: (dom h) misses dom f holds
f * (g +* h) = f * g

proof end;

theorem Th4: :: ALGSPEC1:4

for f1, f2, g1, g2 being Function st f1 tolerates f2 & g1 tolerates g2 holds
f1 * g1 tolerates f2 * g2

proof end;

theorem Th5: :: ALGSPEC1:5

for X1, Y1, X2, Y2 being non empty set
for f being Function of X1,X2
for g being Function of Y1,Y2 st f c= g holds
f * c= g *

proof end;

theorem Th6: :: ALGSPEC1:6

for X1, Y1, X2, Y2 being non empty set
for f being Function of X1,X2
for g being Function of Y1,Y2 st f tolerates g holds
f * tolerates g *

proof end;

definition

let X be set ;
let f be Function;
func X -indexing f -> ManySortedSet of X equals :: ALGSPEC1:def 1
(id X) +* (f | X);
coherence

proof end;

end;

:: deftheorem defines -indexing ALGSPEC1:def 1 :

theorem Th7: :: ALGSPEC1:7

for X being set
for f being Function holds rng (X -indexing f) = (X \ (dom f)) \/ (f .: X)

proof end;

theorem Th8: :: ALGSPEC1:8

for X being non empty set
for f being Function
for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x

proof end;

theorem Th9: :: ALGSPEC1:9

for X, x being set
for f being Function st x in X holds
( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )

proof end;

theorem Th10: :: ALGSPEC1:10

for X being set
for f being Function st dom f = X holds
X -indexing f = f

proof end;

theorem Th11: :: ALGSPEC1:11

for X being set
for f being Function holds X -indexing (X -indexing f) = X -indexing f

proof end;

theorem Th12: :: ALGSPEC1:12

for X being set
for f being Function holds X -indexing ((id X) +* f) = X -indexing f

proof end;

theorem Th13: :: ALGSPEC1:13

for X being set
for f being Function st f c= id X holds
X -indexing f = id X

proof end;

theorem :: ALGSPEC1:14

for X being set holds X -indexing {} = id X

proof end;

theorem Th15: :: ALGSPEC1:15

for X being set
for f being Function holds X -indexing (f | X) = X -indexing f by RELAT_1:101;

theorem Th16: :: ALGSPEC1:16

for X being set
for f being Function st X c= dom f holds
X -indexing f = f | X

proof end;

theorem :: ALGSPEC1:17

for f being Function holds {} -indexing f = {}

proof end;

theorem Th18: :: ALGSPEC1:18

for X, Y being set
for f being Function st X c= Y holds
(Y -indexing f) | X = X -indexing f

proof end;

theorem Th19: :: ALGSPEC1:19

for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)

proof end;

theorem Th20: :: ALGSPEC1:20

for X, Y being set
for f being Function holds X -indexing f tolerates Y -indexing f

proof end;

theorem Th21: :: ALGSPEC1:21

for X, Y being set
for f being Function holds (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)

proof end;

theorem Th22: :: ALGSPEC1:22

for X being non empty set
for f, g being Function st rng g c= X holds
(X -indexing f) * g = ((id X) +* f) * g

proof end;

theorem :: ALGSPEC1:23

for f, g being Function st dom f misses dom g & rng g misses dom f holds
for X being set holds f * (X -indexing g) = f | X

proof end;

definition

let f be Function;
mode rng-retract of f -> Function means :Def2: :: ALGSPEC1:def 2
( dom it = rng f & f * it = id (rng f) );
existence

proof end;

end;

:: deftheorem Def2 defines rng-retract ALGSPEC1:def 2 :

theorem Th24: :: ALGSPEC1:24

for f being Function
for g being rng-retract of f holds rng g c= dom f

proof end;

theorem Th25: :: ALGSPEC1:25

for f being Function
for g being rng-retract of f
for x being set st x in rng f holds
( g . x in dom f & f . (g . x) = x )

proof end;

theorem :: ALGSPEC1:26

for f being Function st f is one-to-one holds
f " is rng-retract of f

proof end;

theorem :: ALGSPEC1:27

for f being Function st f is one-to-one holds
for g being rng-retract of f holds g = f "

proof end;

theorem Th28: :: ALGSPEC1:28

for f1, f2 being Function st f1 tolerates f2 holds
for g1 being rng-retract of f1
for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2

proof end;

theorem :: ALGSPEC1:29

for f1, f2 being Function st f1 c= f2 holds
for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2

proof end;

definition

let S be non empty non void ManySortedSign ;
let f, g be Function;
pred f,g form_a_replacement_in S means :Def3: :: ALGSPEC1:def 3
for o1, o2 being OperSymbol of S st ((id the OperSymbols of S) +* g) . o1 = ((id the OperSymbols of S) +* g) . o2 holds
( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) );

end;

:: deftheorem Def3 defines form_a_replacement_in ALGSPEC1:def 3 :

theorem Th30: :: ALGSPEC1:30

for S being non empty non void ManySortedSign
for f, g being Function holds
( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st (the OperSymbols of S -indexing g) . o1 = (the OperSymbols of S -indexing g) . o2 holds
( (the carrier of S -indexing f) * (the_arity_of o1) = (the carrier of S -indexing f) * (the_arity_of o2) & (the carrier of S -indexing f) . (the_result_sort_of o1) = (the carrier of S -indexing f) . (the_result_sort_of o2) ) )

proof end;

theorem Th31: :: ALGSPEC1:31

for S being non empty non void ManySortedSign
for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f,the OperSymbols of S -indexing g form_a_replacement_in S )

proof end;

theorem Th32: :: ALGSPEC1:32

for S, S' being non void Signature
for f, g being Function st f,g form_morphism_between S,S' holds
f,g form_a_replacement_in S

proof end;

theorem :: ALGSPEC1:33

for S being non void Signature
for f being Function holds f, {} form_a_replacement_in S

proof end;

theorem Th34: :: ALGSPEC1:34

for S being non void Signature
for g, f being Function st g is one-to-one & the OperSymbols of S /\ (rng g) c= dom g holds
f,g form_a_replacement_in S

proof end;

theorem :: ALGSPEC1:35

for S being non void Signature
for g, f being Function st g is one-to-one & rng g misses the OperSymbols of S holds
f,g form_a_replacement_in S

proof end;

registration

let X be set ;
let Y be non empty set ;
let a be Function of Y,X * ;
let r be Function of Y,X;
cluster ManySortedSign(# X,Y,a,r #) -> non void ;
coherence by MSUALG_1:def 5;

end;

definition

let S be non empty non void ManySortedSign ;
let f, g be Function;
assume A1: f,g form_a_replacement_in S ;
func S with-replacement f,g -> non empty strict non void ManySortedSign means :Def4: :: ALGSPEC1:def 4
( the carrier of S -indexing f,the OperSymbols of S -indexing g form_morphism_between S,it & the carrier of it = rng (the carrier of S -indexing f) & the OperSymbols of it = rng (the OperSymbols of S -indexing g) );
uniqueness

proof end;

existence

proof end;

end;

:: deftheorem Def4 defines with-replacement ALGSPEC1:def 4 :

theorem Th36: :: ALGSPEC1:36

for S1, S2 being non void Signature
for f being Function of the carrier of S1,the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
(f * ) * the Arity of S1 = the Arity of S2 * g

proof end;

theorem Th37: :: ALGSPEC1:37

for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
the carrier of S -indexing f is Function of the carrier of S,the carrier of (S with-replacement f,g)

proof end;

theorem Th38: :: ALGSPEC1:38

for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
for f' being Function of the carrier of S,the carrier of (S with-replacement f,g) st f' = the carrier of S -indexing f holds
for g' being rng-retract of the OperSymbols of S -indexing g holds the Arity of (S with-replacement f,g) = ((f' * ) * the Arity of S) * g'

proof end;

theorem Th39: :: ALGSPEC1:39

for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
for g' being rng-retract of the OperSymbols of S -indexing g holds the ResultSort of (S with-replacement f,g) = ((the carrier of S -indexing f) * the ResultSort of S) * g'

proof end;

theorem Th40: :: ALGSPEC1:40

for S, S' being non void Signature
for f, g being Function st f,g form_morphism_between S,S' holds
S with-replacement f,g is Subsignature of S'

proof end;

theorem Th41: :: ALGSPEC1:41

for S being non void Signature
for f, g being Function holds
( f,g form_a_replacement_in S iff the carrier of S -indexing f,the OperSymbols of S -indexing g form_morphism_between S,S with-replacement f,g )

proof end;

theorem Th42: :: ALGSPEC1:42

for S being non void Signature
for f, g being Function st dom f c= the carrier of S & dom g c= the OperSymbols of S & f,g form_a_replacement_in S holds
(id the carrier of S) +* f,(id the OperSymbols of S) +* g form_morphism_between S,S with-replacement f,g

proof end;

theorem :: ALGSPEC1:43

for S being non void Signature
for f, g being Function st dom f = the carrier of S & dom g = the OperSymbols of S & f,g form_a_replacement_in S holds
f,g form_morphism_between S,S with-replacement f,g

proof end;

theorem Th44: :: ALGSPEC1:44

for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
S with-replacement (the carrier of S -indexing f),g = S with-replacement f,g

proof end;

theorem Th45: :: ALGSPEC1:45

for S being non void Signature
for f, g being Function st f,g form_a_replacement_in S holds
S with-replacement f,(the OperSymbols of S -indexing g) = S with-replacement f,g

proof end;

definition

let S be Signature;
mode Extension of S -> Signature means :Def5: :: ALGSPEC1:def 5
S is Subsignature of it;
existence

proof end;

end;

:: deftheorem Def5 defines Extension ALGSPEC1:def 5 :

theorem :: ALGSPEC1:46

canceled;

theorem Th47: :: ALGSPEC1:47

for S being Signature holds S is Extension of S

proof end;

theorem Th48: :: ALGSPEC1:48

for S1 being Signature
for S2 being Extension of S1
for S3 being Extension of S2 holds S3 is Extension of S1

proof end;

theorem Th49: :: ALGSPEC1:49

for S1, S2 being non empty Signature st S1 tolerates S2 holds
S1 +* S2 is Extension of S1

proof end;

theorem Th50: :: ALGSPEC1:50

for S1, S2 being non empty Signature holds S1 +* S2 is Extension of S2

proof end;

theorem Th51: :: ALGSPEC1:51

for S1, S2, S being non empty ManySortedSign
for f1, g1, f2, g2 being Function st f1 tolerates f2 & f1,g1 form_morphism_between S1,S & f2,g2 form_morphism_between S2,S holds
f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,S

proof end;

theorem :: ALGSPEC1:52

for S1, S2, E being non empty Signature holds
( E is Extension of S1 & E is Extension of S2 iff ( S1 tolerates S2 & E is Extension of S1 +* S2 ) )

proof end;

registration

let S be non empty Signature;
cluster -> non empty Extension of S;
coherence

proof end;

end;

registration

let S be non void Signature;
cluster -> non empty non void Extension of S;
coherence

proof end;

end;

theorem Th53: :: ALGSPEC1:53

for S, T being Signature st S is empty holds
T is Extension of S

proof end;

registration

let S be Signature;
cluster non empty strict non void Extension of S;
existence

proof end;

end;

theorem Th54: :: ALGSPEC1:54

for f, g being Function
for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
f,g form_a_replacement_in S

proof end;

theorem :: ALGSPEC1:55

for f, g being Function
for S being non void Signature
for E being Extension of S st f,g form_a_replacement_in E holds
E with-replacement f,g is Extension of S with-replacement f,g

proof end;

theorem :: ALGSPEC1:56

for S1, S2 being non void Signature st S1 tolerates S2 holds
for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds
(S1 +* S2) with-replacement f,g = (S1 with-replacement f,g) +* (S2 with-replacement f,g)

proof end;

definition

mode Algebra -> set means :Def6: :: ALGSPEC1:def 6
ex S being non void Signature st it is feasible MSAlgebra of S;
existence

proof end;

end;

:: deftheorem Def6 defines Algebra ALGSPEC1:def 6 :

definition

let S be Signature;
mode Algebra of S -> Algebra means :Def7: :: ALGSPEC1:def 7
ex E being non void Extension of S st it is feasible MSAlgebra of E;
existence

proof end;

end;

:: deftheorem Def7 defines Algebra ALGSPEC1:def 7 :

theorem :: ALGSPEC1:57

for S being non void Signature
for A being feasible MSAlgebra of S holds A is Algebra of S

proof end;

theorem :: ALGSPEC1:58

for S being Signature
for E being Extension of S
for A being Algebra of E holds A is Algebra of S

proof end;

theorem Th59: :: ALGSPEC1:59

for S being Signature
for E being non empty Signature
for A being MSAlgebra of E st A is Algebra of S holds
( the carrier of S c= the carrier of E & the OperSymbols of S c= the OperSymbols of E )

proof end;

theorem Th60: :: ALGSPEC1:60

for S being non void Signature
for E being non empty Signature
for A being MSAlgebra of E st A is Algebra of S holds
for o being OperSymbol of S holds the Charact of A . o is Function of (the Sorts of A # ) . (the_arity_of o),the Sorts of A . (the_result_sort_of o)

proof end;

theorem :: ALGSPEC1:61

for S being non empty Signature
for A being Algebra of S
for E being non empty ManySortedSign st A is MSAlgebra of E holds
A is MSAlgebra of E +* S

proof end;

theorem Th62: :: ALGSPEC1:62

for S1, S2 being non empty Signature
for A being MSAlgebra of S1 st A is MSAlgebra of S2 holds
( the carrier of S1 = the carrier of S2 & the OperSymbols of S1 = the OperSymbols of S2 )

proof end;

theorem Th63: :: ALGSPEC1:63

for S being non void Signature
for A being non-empty disjoint_valued MSAlgebra of S holds the Sorts of A is one-to-one

proof end;

theorem Th64: :: ALGSPEC1:64

for S being non void Signature
for A being disjoint_valued MSAlgebra of S
for C1, C2 being Component of the Sorts of A holds
( C1 = C2 or C1 misses C2 )

proof end;

theorem Th65: :: ALGSPEC1:65

for S, S' being non void Signature
for A being non-empty disjoint_valued MSAlgebra of S st A is MSAlgebra of S' holds
ManySortedSign(# the carrier of S,the OperSymbols of S,the Arity of S,the ResultSort of S #) = ManySortedSign(# the carrier of S',the OperSymbols of S',the Arity of S',the ResultSort of S' #)

proof end;

theorem :: ALGSPEC1:66

for S, S' being non void Signature
for A being non-empty disjoint_valued MSAlgebra of S st A is Algebra of S' holds
S is Extension of S'

proof end;