begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
for
S being non
empty non
void ManySortedSign for
A1,
A2,
B1,
B2 being
MSAlgebra of
S st
MSAlgebra(# the
Sorts of
A1,the
Charact of
A1 #)
= MSAlgebra(# the
Sorts of
B1,the
Charact of
B1 #) &
MSAlgebra(# the
Sorts of
A2,the
Charact of
A2 #)
= MSAlgebra(# the
Sorts of
B2,the
Charact of
B2 #) holds
for
f being
ManySortedFunction of
A1,
A2 for
g being
ManySortedFunction of
B1,
B2 st
f = g holds
for
o being
OperSymbol of
S st
Args o,
A1 <> {} &
Args o,
A2 <> {} holds
for
x being
Element of
Args o,
A1 for
y being
Element of
Args o,
B1 st
x = y holds
f # x = g # y
theorem
for
S being non
empty non
void ManySortedSign for
A1,
A2,
B1,
B2 being
MSAlgebra of
S st
MSAlgebra(# the
Sorts of
A1,the
Charact of
A1 #)
= MSAlgebra(# the
Sorts of
B1,the
Charact of
B1 #) &
MSAlgebra(# the
Sorts of
A2,the
Charact of
A2 #)
= MSAlgebra(# the
Sorts of
B2,the
Charact of
B2 #) & the
Sorts of
A1 is_transformable_to the
Sorts of
A2 holds
for
h being
ManySortedFunction of
A1,
A2 st
h is_homomorphism A1,
A2 holds
ex
h9 being
ManySortedFunction of
B1,
B2 st
(
h9 = h &
h9 is_homomorphism B1,
B2 )
:: deftheorem Def1 defines feasible INSTALG1:def 1 :
theorem Th8:
theorem Th9:
theorem Th10:
begin
:: deftheorem Def2 defines Subsignature INSTALG1:def 2 :
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
theorem Th16:
theorem
theorem
theorem
theorem
theorem
begin
:: deftheorem Def3 defines | INSTALG1:def 3 :
:: deftheorem defines | INSTALG1:def 4 :
theorem
for
S1,
S2 being non
empty ManySortedSign for
A,
B being
MSAlgebra of
S2 st
MSAlgebra(# the
Sorts of
A,the
Charact of
A #)
= MSAlgebra(# the
Sorts of
B,the
Charact of
B #) holds
for
f,
g being
Function st
f,
g form_morphism_between S1,
S2 holds
A | S1,
f,
g = B | S1,
f,
g
theorem Th23:
theorem Th24:
theorem Th25:
for
S1,
S2 being non
empty non
void ManySortedSign for
f,
g being
Function st
f,
g form_morphism_between S1,
S2 holds
for
A being
MSAlgebra of
S2 for
o1 being
OperSymbol of
S1 for
o2 being
OperSymbol of
S2 st
o2 = g . o1 holds
(
Args o2,
A = Args o1,
(A | S1,f,g) &
Result o1,
(A | S1,f,g) = Result o2,
A )
theorem Th26:
theorem
theorem Th28:
for
S1,
S2,
S3 being non
empty ManySortedSign for
f1,
g1 being
Function st
f1,
g1 form_morphism_between S1,
S2 holds
for
f2,
g2 being
Function st
f2,
g2 form_morphism_between S2,
S3 holds
for
A being
MSAlgebra of
S3 holds
A | S1,
(f2 * f1),
(g2 * g1) = (A | S2,f2,g2) | S1,
f1,
g1
theorem
theorem Th30:
for
S1,
S2 being non
empty ManySortedSign 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
for
A1,
A2 being
MSAlgebra of
S2 for
h being
ManySortedFunction of the
Sorts of
A1,the
Sorts of
A2 holds
h * f is
ManySortedFunction of the
Sorts of
(A1 | S1,f,g),the
Sorts of
(A2 | S1,f,g)
theorem
theorem Th32:
theorem
theorem Th34:
for
S1,
S2 being non
empty non
void ManySortedSign for
f,
g being
Function st
f,
g form_morphism_between S1,
S2 holds
for
A,
B being
MSAlgebra of
S2 for
h2 being
ManySortedFunction of
A,
B for
h1 being
ManySortedFunction of
(A | S1,f,g),
(B | S1,f,g) st
h1 = h2 * f holds
for
o1 being
OperSymbol of
S1 for
o2 being
OperSymbol of
S2 st
o2 = g . o1 &
Args o2,
A <> {} &
Args o2,
B <> {} holds
for
x2 being
Element of
Args o2,
A for
x1 being
Element of
Args o1,
(A | S1,f,g) st
x2 = x1 holds
h1 # x1 = h2 # x2
theorem Th35:
for
S,
S9 being non
empty non
void ManySortedSign for
A1,
A2 being
MSAlgebra of
S st the
Sorts of
A1 is_transformable_to the
Sorts of
A2 holds
for
h being
ManySortedFunction of
A1,
A2 st
h is_homomorphism A1,
A2 holds
for
f being
Function of the
carrier of
S9,the
carrier of
S for
g being
Function st
f,
g form_morphism_between S9,
S holds
ex
h9 being
ManySortedFunction of
(A1 | S9,f,g),
(A2 | S9,f,g) st
(
h9 = h * f &
h9 is_homomorphism A1 | S9,
f,
g,
A2 | S9,
f,
g )
theorem
theorem Th37:
for
S,
S9 being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra of
S for
f being
Function of the
carrier of
S9,the
carrier of
S for
g being
Function st
f,
g form_morphism_between S9,
S holds
for
B being
non-empty MSAlgebra of
S9 st
B = A | S9,
f,
g holds
for
s1,
s2 being
SortSymbol of
S9 for
t being
Function st
t is_e.translation_of B,
s1,
s2 holds
t is_e.translation_of A,
f . s1,
f . s2
Lm1:
for S, S9 being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for f being Function of the carrier of S9,the carrier of S
for g being Function st f,g form_morphism_between S9,S holds
for B being non-empty MSAlgebra of S9 st B = A | S9,f,g holds
for s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds
( TranslationRel S reduces f . s1,f . s2 & ( for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 ) )
theorem
theorem
for
S,
S9 being non
empty non
void ManySortedSign for
A being
non-empty MSAlgebra of
S for
f being
Function of the
carrier of
S9,the
carrier of
S for
g being
Function st
f,
g form_morphism_between S9,
S holds
for
B being
non-empty MSAlgebra of
S9 st
B = A | S9,
f,
g holds
for
s1,
s2 being
SortSymbol of
S9 st
TranslationRel S9 reduces s1,
s2 holds
for
t being
Translation of
B,
s1,
s2 holds
t is
Translation of
A,
f . s1,
f . s2 by Lm1;
begin
theorem Th40:
definition
let S1,
S2 be non
empty non
void ManySortedSign ;
let X be
V5()
ManySortedSet of the
carrier of
S2;
let f be
Function of the
carrier of
S1,the
carrier of
S2;
let g be
Function;
assume A1:
f,
g form_morphism_between S1,
S2
;
func hom f,
g,
X,
S1,
S2 -> ManySortedFunction of
(FreeMSA (X * f)),
((FreeMSA X) | S1,f,g) means :
Def5:
(
it is_homomorphism FreeMSA (X * f),
(FreeMSA X) | S1,
f,
g & ( for
s being
SortSymbol of
S1 for
x being
Element of
(X * f) . s holds
(it . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) );
existence
ex b1 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | S1,f,g) st
( b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | S1,f,g & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) )
uniqueness
for b1, b2 being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | S1,f,g) st b1 is_homomorphism FreeMSA (X * f),(FreeMSA X) | S1,f,g & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b1 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & b2 is_homomorphism FreeMSA (X * f),(FreeMSA X) | S1,f,g & ( for s being SortSymbol of S1
for x being Element of (X * f) . s holds (b2 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) holds
b1 = b2
end;
:: deftheorem Def5 defines hom INSTALG1:def 5 :
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
V5()
ManySortedSet of the
carrier of
S2 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
for
b6 being
ManySortedFunction of
(FreeMSA (X * f)),
((FreeMSA X) | S1,f,g) holds
(
b6 = hom f,
g,
X,
S1,
S2 iff (
b6 is_homomorphism FreeMSA (X * f),
(FreeMSA X) | S1,
f,
g & ( for
s being
SortSymbol of
S1 for
x being
Element of
(X * f) . s holds
(b6 . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) );
theorem Th41:
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
V5()
ManySortedSet of the
carrier of
S2 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
for
o being
OperSymbol of
S1 for
p being
Element of
Args o,
(FreeMSA (X * f)) for
q being
FinSequence st
q = (hom f,g,X,S1,S2) # p holds
((hom f,g,X,S1,S2) . (the_result_sort_of o)) . ([o,the carrier of S1] -tree p) = [(g . o),the carrier of S2] -tree q
theorem Th42:
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
V5()
ManySortedSet of the
carrier of
S2 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
for
t being
Term of
S1,
(X * f) holds
(
((hom f,g,X,S1,S2) . (the_sort_of t)) . t is
CompoundTerm of
S2,
X iff
t is
CompoundTerm of
S1,
X * f )
theorem
for
S1,
S2 being non
empty non
void ManySortedSign for
X being
V5()
ManySortedSet of the
carrier of
S2 for
f being
Function of the
carrier of
S1,the
carrier of
S2 for
g being
one-to-one Function st
f,
g form_morphism_between S1,
S2 holds
hom f,
g,
X,
S1,
S2 is_monomorphism FreeMSA (X * f),
(FreeMSA X) | S1,
f,
g
theorem
theorem
for
S1,
S2,
S3 being non
empty non
void ManySortedSign for
X being
V5()
ManySortedSet of the
carrier of
S3 for
f1 being
Function of the
carrier of
S1,the
carrier of
S2 for
g1 being
Function st
f1,
g1 form_morphism_between S1,
S2 holds
for
f2 being
Function of the
carrier of
S2,the
carrier of
S3 for
g2 being
Function st
f2,
g2 form_morphism_between S2,
S3 holds
hom (f2 * f1),
(g2 * g1),
X,
S1,
S3 = ((hom f2,g2,X,S2,S3) * f1) ** (hom f1,g1,(X * f2),S1,S2)