:: ALGSPEC1 semantic presentation

theorem Th1: :: ALGSPEC1:1

for b₁, b₂, b₃ being Function st (dom b₁) /\ (dom b₂) c= dom b₃ holds
(b₁ +* b₂) +* b₃ = (b₂ +* b₁) +* b₃

proof end;

theorem Th2: :: ALGSPEC1:2

for b₁, b₂, b₃ being Function st b₁ c= b₂ & (rng b₃) /\ (dom b₂) c= dom b₁ holds
b₂ * b₃ = b₁ * b₃

proof end;

theorem Th3: :: ALGSPEC1:3

for b₁, b₂, b₃ being Function st dom b₁ c= rng b₂ & dom b₁ misses rng b₃ & b₂ .: (dom b₃) misses dom b₁ holds
b₁ * (b₂ +* b₃) = b₁ * b₂

proof end;

theorem Th4: :: ALGSPEC1:4

for b₁, b₂, b₃, b₄ being Function st b₁ tolerates b₂ & b₃ tolerates b₄ holds
b₁ * b₃ tolerates b₂ * b₄

proof end;

theorem Th5: :: ALGSPEC1:5

for b₁, b₂, b₃, b₄ being non empty set
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st b₅ c= b₆ holds
b₅ * c= b₆ *

proof end;

theorem Th6: :: ALGSPEC1:6

for b₁, b₂, b₃, b₄ being non empty set
for b₅ being Function of b₁,b₃
for b₆ being Function of b₂,b₄ st b₅ tolerates b₆ holds
b₅ * tolerates b₆ *

proof end;

definition

let c₁ be set ;
let c₂ be Function;
func c₁ -indexing c₂ -> ManySortedSet of a₁ equals :: ALGSPEC1:def 1
(id a₁) +* (a₂ | a₁);
coherence

proof end;

end;

:: deftheorem Def1 defines -indexing ALGSPEC1:def 1 :

theorem Th7: :: ALGSPEC1:7

for b₁ being set
for b₂ being Function holds rng (b₁ -indexing b₂) = (b₁ \ (dom b₂)) \/ (b₂ .: b₁)

proof end;

theorem Th8: :: ALGSPEC1:8

for b₁ being non empty set
for b₂ being Function
for b₃ being Element of b₁ holds (b₁ -indexing b₂) . b₃ = ((id b₁) +* b₂) . b₃

proof end;

theorem Th9: :: ALGSPEC1:9

for b₁, b₂ being set
for b₃ being Function st b₂ in b₁ holds
( ( b₂ in dom b₃ implies (b₁ -indexing b₃) . b₂ = b₃ . b₂ ) & ( not b₂ in dom b₃ implies (b₁ -indexing b₃) . b₂ = b₂ ) )

proof end;

theorem Th10: :: ALGSPEC1:10

for b₁ being set
for b₂ being Function st dom b₂ = b₁ holds
b₁ -indexing b₂ = b₂

proof end;

theorem Th11: :: ALGSPEC1:11

for b₁ being set
for b₂ being Function holds b₁ -indexing (b₁ -indexing b₂) = b₁ -indexing b₂

proof end;

theorem Th12: :: ALGSPEC1:12

for b₁ being set
for b₂ being Function holds b₁ -indexing ((id b₁) +* b₂) = b₁ -indexing b₂

proof end;

theorem Th13: :: ALGSPEC1:13

for b₁ being set
for b₂ being Function st b₂ c= id b₁ holds
b₁ -indexing b₂ = id b₁

proof end;

theorem Th14: :: ALGSPEC1:14

for b₁ being set holds b₁ -indexing {} = id b₁

proof end;

theorem Th15: :: ALGSPEC1:15

for b₁ being set
for b₂ being Function holds b₁ -indexing (b₂ | b₁) = b₁ -indexing b₂ by RELAT_1:101;

theorem Th16: :: ALGSPEC1:16

for b₁ being set
for b₂ being Function st b₁ c= dom b₂ holds
b₁ -indexing b₂ = b₂ | b₁

proof end;

theorem Th17: :: ALGSPEC1:17

for b₁ being Function holds {} -indexing b₁ = {}

proof end;

theorem Th18: :: ALGSPEC1:18

for b₁, b₂ being set
for b₃ being Function st b₁ c= b₂ holds
(b₂ -indexing b₃) | b₁ = b₁ -indexing b₃

proof end;

theorem Th19: :: ALGSPEC1:19

for b₁, b₂ being set
for b₃ being Function holds (b₁ \/ b₂) -indexing b₃ = (b₁ -indexing b₃) +* (b₂ -indexing b₃)

proof end;

theorem Th20: :: ALGSPEC1:20

for b₁, b₂ being set
for b₃ being Function holds b₁ -indexing b₃ tolerates b₂ -indexing b₃

proof end;

theorem Th21: :: ALGSPEC1:21

for b₁, b₂ being set
for b₃ being Function holds (b₁ \/ b₂) -indexing b₃ = (b₁ -indexing b₃) \/ (b₂ -indexing b₃)

proof end;

theorem Th22: :: ALGSPEC1:22

for b₁ being non empty set
for b₂, b₃ being Function st rng b₃ c= b₁ holds
(b₁ -indexing b₂) * b₃ = ((id b₁) +* b₂) * b₃

proof end;

theorem Th23: :: ALGSPEC1:23

for b₁, b₂ being Function st dom b₁ misses dom b₂ & rng b₂ misses dom b₁ holds
for b₃ being set holds b₁ * (b₃ -indexing b₂) = b₁ | b₃

proof end;

definition

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

proof end;

end;

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

theorem Th24: :: ALGSPEC1:24

for b₁ being Function
for b₂ being rng-retract of b₁ holds rng b₂ c= dom b₁

proof end;

theorem Th25: :: ALGSPEC1:25

for b₁ being Function
for b₂ being rng-retract of b₁
for b₃ being set st b₃ in rng b₁ holds
( b₂ . b₃ in dom b₁ & b₁ . (b₂ . b₃) = b₃ )

proof end;

theorem Th26: :: ALGSPEC1:26

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

proof end;

theorem Th27: :: ALGSPEC1:27

for b₁ being Function st b₁ is one-to-one holds
for b₂ being rng-retract of b₁ holds b₂ = b₁ "

proof end;

theorem Th28: :: ALGSPEC1:28

for b₁, b₂ being Function st b₁ tolerates b₂ holds
for b₃ being rng-retract of b₁
for b₄ being rng-retract of b₂ holds b₃ +* b₄ is rng-retract of b₁ +* b₂

proof end;

theorem Th29: :: ALGSPEC1:29

for b₁, b₂ being Function st b₁ c= b₂ holds
for b₃ being rng-retract of b₁ ex b₄ being rng-retract of b₂ st b₃ c= b₄

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂, c₃ be Function;
pred c₂,c₃ form_a_replacement_in c₁ means :Def3: :: ALGSPEC1:def 3
for b₁, b₂ being OperSymbol of a₁ st ((id the OperSymbols of a₁) +* a₃) . b₁ = ((id the OperSymbols of a₁) +* a₃) . b₂ holds
( ((id the carrier of a₁) +* a₂) * (the_arity_of b₁) = ((id the carrier of a₁) +* a₂) * (the_arity_of b₂) & ((id the carrier of a₁) +* a₂) . (the_result_sort_of b₁) = ((id the carrier of a₁) +* a₂) . (the_result_sort_of b₂) );

end;

:: deftheorem Def3 defines form_a_replacement_in ALGSPEC1:def 3 :

theorem Th30: :: ALGSPEC1:30

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being Function holds
( b₂,b₃ form_a_replacement_in b₁ iff for b₄, b₅ being OperSymbol of b₁ st (the OperSymbols of b₁ -indexing b₃) . b₄ = (the OperSymbols of b₁ -indexing b₃) . b₅ holds
( (the carrier of b₁ -indexing b₂) * (the_arity_of b₄) = (the carrier of b₁ -indexing b₂) * (the_arity_of b₅) & (the carrier of b₁ -indexing b₂) . (the_result_sort_of b₄) = (the carrier of b₁ -indexing b₂) . (the_result_sort_of b₅) ) )

proof end;

theorem Th31: :: ALGSPEC1:31

for b₁ being non empty non void ManySortedSign
for b₂, b₃ being Function holds
( b₂,b₃ form_a_replacement_in b₁ iff the carrier of b₁ -indexing b₂,the OperSymbols of b₁ -indexing b₃ form_a_replacement_in b₁ )

proof end;

theorem Th32: :: ALGSPEC1:32

for b₁, b₂ being non void Signature
for b₃, b₄ being Function st b₃,b₄ form_morphism_between b₁,b₂ holds
b₃,b₄ form_a_replacement_in b₁

proof end;

theorem Th33: :: ALGSPEC1:33

for b₁ being non void Signature
for b₂ being Function holds b₂, {} form_a_replacement_in b₁

proof end;

theorem Th34: :: ALGSPEC1:34

for b₁ being non void Signature
for b₂, b₃ being Function st b₂ is one-to-one & the OperSymbols of b₁ /\ (rng b₂) c= dom b₂ holds
b₃,b₂ form_a_replacement_in b₁

proof end;

theorem Th35: :: ALGSPEC1:35

for b₁ being non void Signature
for b₂, b₃ being Function st b₂ is one-to-one & rng b₂ misses the OperSymbols of b₁ holds
b₃,b₂ form_a_replacement_in b₁

proof end;

registration

let c₁ be set ;
let c₂ be non empty set ;
let c₃ be Function of c₂,c₁ * ;
let c₄ be Function of c₂,c₁;
cluster ManySortedSign(# a₁,a₂,a₃,a₄ #) -> non void ;
coherence by MSUALG_1:def 5;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂, c₃ be Function;
assume E30: c₂,c₃ form_a_replacement_in c₁ ;
func c₁ with-replacement c₂,c₃ -> non empty strict non void ManySortedSign means :Def4: :: ALGSPEC1:def 4
( the carrier of a₁ -indexing a₂,the OperSymbols of a₁ -indexing a₃ form_morphism_between a₁,a₄ & the carrier of a₄ = rng (the carrier of a₁ -indexing a₂) & the OperSymbols of a₄ = rng (the OperSymbols of a₁ -indexing a₃) );
uniqueness

proof end;

existence

proof end;

end;

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

theorem Th36: :: ALGSPEC1:36

for b₁, b₂ being non void Signature
for b₃ being Function of the carrier of b₁,the carrier of b₂
for b₄ being Function st b₃,b₄ form_morphism_between b₁,b₂ holds
(b₃ * ) * the Arity of b₁ = the Arity of b₂ * b₄

proof end;

theorem Th37: :: ALGSPEC1:37

for b₁ being non void Signature
for b₂, b₃ being Function st b₂,b₃ form_a_replacement_in b₁ holds
the carrier of b₁ -indexing b₂ is Function of the carrier of b₁,the carrier of (b₁ with-replacement b₂,b₃)

proof end;

theorem Th38: :: ALGSPEC1:38

for b₁ being non void Signature
for b₂, b₃ being Function st b₂,b₃ form_a_replacement_in b₁ holds
for b₄ being Function of the carrier of b₁,the carrier of (b₁ with-replacement b₂,b₃) st b₄ = the carrier of b₁ -indexing b₂ holds
for b₅ being rng-retract of the OperSymbols of b₁ -indexing b₃ holds the Arity of (b₁ with-replacement b₂,b₃) = ((b₄ * ) * the Arity of b₁) * b₅

proof end;

theorem Th39: :: ALGSPEC1:39

for b₁ being non void Signature
for b₂, b₃ being Function st b₂,b₃ form_a_replacement_in b₁ holds
for b₄ being rng-retract of the OperSymbols of b₁ -indexing b₃ holds the ResultSort of (b₁ with-replacement b₂,b₃) = ((the carrier of b₁ -indexing b₂) * the ResultSort of b₁) * b₄

proof end;

theorem Th40: :: ALGSPEC1:40

for b₁, b₂ being non void Signature
for b₃, b₄ being Function st b₃,b₄ form_morphism_between b₁,b₂ holds
b₁ with-replacement b₃,b₄ is Subsignature of b₂

proof end;

theorem Th41: :: ALGSPEC1:41

for b₁ being non void Signature
for b₂, b₃ being Function holds
( b₂,b₃ form_a_replacement_in b₁ iff the carrier of b₁ -indexing b₂,the OperSymbols of b₁ -indexing b₃ form_morphism_between b₁,b₁ with-replacement b₂,b₃ )

proof end;

theorem Th42: :: ALGSPEC1:42

for b₁ being non void Signature
for b₂, b₃ being Function st dom b₂ c= the carrier of b₁ & dom b₃ c= the OperSymbols of b₁ & b₂,b₃ form_a_replacement_in b₁ holds
(id the carrier of b₁) +* b₂,(id the OperSymbols of b₁) +* b₃ form_morphism_between b₁,b₁ with-replacement b₂,b₃

proof end;

theorem Th43: :: ALGSPEC1:43

for b₁ being non void Signature
for b₂, b₃ being Function st dom b₂ = the carrier of b₁ & dom b₃ = the OperSymbols of b₁ & b₂,b₃ form_a_replacement_in b₁ holds
b₂,b₃ form_morphism_between b₁,b₁ with-replacement b₂,b₃

proof end;

theorem Th44: :: ALGSPEC1:44

for b₁ being non void Signature
for b₂, b₃ being Function st b₂,b₃ form_a_replacement_in b₁ holds
b₁ with-replacement (the carrier of b₁ -indexing b₂),b₃ = b₁ with-replacement b₂,b₃

proof end;

theorem Th45: :: ALGSPEC1:45

for b₁ being non void Signature
for b₂, b₃ being Function st b₂,b₃ form_a_replacement_in b₁ holds
b₁ with-replacement b₂,(the OperSymbols of b₁ -indexing b₃) = b₁ with-replacement b₂,b₃

proof end;

definition

let c₁ be Signature;
mode Extension of c₁ -> Signature means :Def5: :: ALGSPEC1:def 5
a₁ is Subsignature of a₂;
existence

proof end;

end;

:: deftheorem Def5 defines Extension ALGSPEC1:def 5 :

theorem Th46: :: ALGSPEC1:46

canceled;

theorem Th47: :: ALGSPEC1:47

for b₁ being Signature holds b₁ is Extension of b₁

proof end;

theorem Th48: :: ALGSPEC1:48

for b₁ being Signature
for b₂ being Extension of b₁
for b₃ being Extension of b₂ holds b₃ is Extension of b₁

proof end;

theorem Th49: :: ALGSPEC1:49

for b₁, b₂ being non empty Signature st b₁ tolerates b₂ holds
b₁ +* b₂ is Extension of b₁

proof end;

theorem Th50: :: ALGSPEC1:50

for b₁, b₂ being non empty Signature holds b₁ +* b₂ is Extension of b₂

proof end;

theorem Th51: :: ALGSPEC1:51

for b₁, b₂, b₃ being non empty ManySortedSign
for b₄, b₅, b₆, b₇ being Function st b₄ tolerates b₆ & b₄,b₅ form_morphism_between b₁,b₃ & b₆,b₇ form_morphism_between b₂,b₃ holds
b₄ +* b₆,b₅ +* b₇ form_morphism_between b₁ +* b₂,b₃

proof end;

theorem Th52: :: ALGSPEC1:52

for b₁, b₂, b₃ being non empty Signature holds
( b₃ is Extension of b₁ & b₃ is Extension of b₂ iff ( b₁ tolerates b₂ & b₃ is Extension of b₁ +* b₂ ) )

proof end;

registration

let c₁ be non empty Signature;
cluster -> non empty Extension of a₁;
coherence

proof end;

end;

registration

let c₁ be non void Signature;
cluster -> non empty non void Extension of a₁;
coherence

proof end;

end;

theorem Th53: :: ALGSPEC1:53

for b₁, b₂ being Signature st b₁ is empty holds
b₂ is Extension of b₁

proof end;

registration

let c₁ be Signature;
cluster non empty strict non void Extension of a₁;
existence

proof end;

end;

theorem Th54: :: ALGSPEC1:54

for b₁, b₂ being Function
for b₃ being non void Signature
for b₄ being Extension of b₃ st b₁,b₂ form_a_replacement_in b₄ holds
b₁,b₂ form_a_replacement_in b₃

proof end;

theorem Th55: :: ALGSPEC1:55

for b₁, b₂ being Function
for b₃ being non void Signature
for b₄ being Extension of b₃ st b₁,b₂ form_a_replacement_in b₄ holds
b₄ with-replacement b₁,b₂ is Extension of b₃ with-replacement b₁,b₂

proof end;

theorem Th56: :: ALGSPEC1:56

for b₁, b₂ being non void Signature st b₁ tolerates b₂ holds
for b₃, b₄ being Function st b₃,b₄ form_a_replacement_in b₁ +* b₂ holds
(b₁ +* b₂) with-replacement b₃,b₄ = (b₁ with-replacement b₃,b₄) +* (b₂ with-replacement b₃,b₄)

proof end;

definition

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

proof end;

end;

:: deftheorem Def6 defines Algebra ALGSPEC1:def 6 :

definition

let c₁ be Signature;
mode Algebra of c₁ -> Algebra means :Def7: :: ALGSPEC1:def 7
ex b₁ being non void Extension of a₁ st a₂ is feasible MSAlgebra of b₁;
existence

proof end;

end;

:: deftheorem Def7 defines Algebra ALGSPEC1:def 7 :

theorem Th57: :: ALGSPEC1:57

for b₁ being non void Signature
for b₂ being feasible MSAlgebra of b₁ holds b₂ is Algebra of b₁

proof end;

theorem Th58: :: ALGSPEC1:58

for b₁ being Signature
for b₂ being Extension of b₁
for b₃ being Algebra of b₂ holds b₃ is Algebra of b₁

proof end;

theorem Th59: :: ALGSPEC1:59

for b₁ being Signature
for b₂ being non empty Signature
for b₃ being MSAlgebra of b₂ st b₃ is Algebra of b₁ holds
( the carrier of b₁ c= the carrier of b₂ & the OperSymbols of b₁ c= the OperSymbols of b₂ )

proof end;

theorem Th60: :: ALGSPEC1:60

for b₁ being non void Signature
for b₂ being non empty Signature
for b₃ being MSAlgebra of b₂ st b₃ is Algebra of b₁ holds
for b₄ being OperSymbol of b₁ holds the Charact of b₃ . b₄ is Function of (the Sorts of b₃ # ) . (the_arity_of b₄),the Sorts of b₃ . (the_result_sort_of b₄)

proof end;

theorem Th61: :: ALGSPEC1:61

for b₁ being non empty Signature
for b₂ being Algebra of b₁
for b₃ being non empty ManySortedSign st b₂ is MSAlgebra of b₃ holds
b₂ is MSAlgebra of b₃ +* b₁

proof end;

theorem Th62: :: ALGSPEC1:62

for b₁, b₂ being non empty Signature
for b₃ being MSAlgebra of b₁ st b₃ is MSAlgebra of b₂ holds
( the carrier of b₁ = the carrier of b₂ & the OperSymbols of b₁ = the OperSymbols of b₂ )

proof end;

theorem Th63: :: ALGSPEC1:63

for b₁ being non void Signature
for b₂ being non-empty disjoint_valued MSAlgebra of b₁ holds the Sorts of b₂ is one-to-one

proof end;

theorem Th64: :: ALGSPEC1:64

for b₁ being non void Signature
for b₂ being disjoint_valued MSAlgebra of b₁
for b₃, b₄ being Component of the Sorts of b₂ holds
( b₃ = b₄ or b₃ misses b₄ )

proof end;

theorem Th65: :: ALGSPEC1:65

for b₁, b₂ being non void Signature
for b₃ being non-empty disjoint_valued MSAlgebra of b₁ st b₃ is MSAlgebra of b₂ holds
ManySortedSign(# the carrier of b₁,the OperSymbols of b₁,the Arity of b₁,the ResultSort of b₁ #) = ManySortedSign(# the carrier of b₂,the OperSymbols of b₂,the Arity of b₂,the ResultSort of b₂ #)

proof end;

theorem Th66: :: ALGSPEC1:66

for b₁, b₂ being non void Signature
for b₃ being non-empty disjoint_valued MSAlgebra of b₁ st b₃ is Algebra of b₂ holds
b₁ is Extension of b₂

proof end;