:: INSTALG1 semantic presentation
theorem Th1: :: INSTALG1:1
canceled;
theorem Th2: :: INSTALG1:2
theorem Th3: :: INSTALG1:3
theorem Th4: :: INSTALG1:4
theorem Th5: :: INSTALG1:5
theorem Th6: :: INSTALG1:6
for
b1 being non
empty non
void ManySortedSign for
b2,
b3,
b4,
b5 being
MSAlgebra of
b1 st
MSAlgebra(# the
Sorts of
b2,the
Charact of
b2 #)
= MSAlgebra(# the
Sorts of
b4,the
Charact of
b4 #) &
MSAlgebra(# the
Sorts of
b3,the
Charact of
b3 #)
= MSAlgebra(# the
Sorts of
b5,the
Charact of
b5 #) holds
for
b6 being
ManySortedFunction of
b2,
b3 for
b7 being
ManySortedFunction of
b4,
b5 st
b6 = b7 holds
for
b8 being
OperSymbol of
b1 st
Args b8,
b2 <> {} &
Args b8,
b3 <> {} holds
for
b9 being
Element of
Args b8,
b2 for
b10 being
Element of
Args b8,
b4 st
b9 = b10 holds
b6 # b9 = b7 # b10
theorem Th7: :: INSTALG1:7
for
b1 being non
empty non
void ManySortedSign for
b2,
b3,
b4,
b5 being
MSAlgebra of
b1 st
MSAlgebra(# the
Sorts of
b2,the
Charact of
b2 #)
= MSAlgebra(# the
Sorts of
b4,the
Charact of
b4 #) &
MSAlgebra(# the
Sorts of
b3,the
Charact of
b3 #)
= MSAlgebra(# the
Sorts of
b5,the
Charact of
b5 #) & the
Sorts of
b2 is_transformable_to the
Sorts of
b3 holds
for
b6 being
ManySortedFunction of
b2,
b3 st
b6 is_homomorphism b2,
b3 holds
ex
b7 being
ManySortedFunction of
b4,
b5 st
(
b7 = b6 &
b7 is_homomorphism b4,
b5 )
:: deftheorem Def1 defines feasible INSTALG1:def 1 :
theorem Th8: :: INSTALG1:8
theorem Th9: :: INSTALG1:9
theorem Th10: :: INSTALG1:10
:: deftheorem Def2 defines Subsignature INSTALG1:def 2 :
theorem Th11: :: INSTALG1:11
theorem Th12: :: INSTALG1:12
theorem Th13: :: INSTALG1:13
theorem Th14: :: INSTALG1:14
theorem Th15: :: INSTALG1:15
theorem Th16: :: INSTALG1:16
theorem Th17: :: INSTALG1:17
theorem Th18: :: INSTALG1:18
theorem Th19: :: INSTALG1:19
theorem Th20: :: INSTALG1:20
theorem Th21: :: INSTALG1:21
:: deftheorem Def3 defines | INSTALG1:def 3 :
:: deftheorem Def4 defines | INSTALG1:def 4 :
theorem Th22: :: INSTALG1:22
for
b1,
b2 being non
empty ManySortedSign for
b3,
b4 being
MSAlgebra of
b2 st
MSAlgebra(# the
Sorts of
b3,the
Charact of
b3 #)
= MSAlgebra(# the
Sorts of
b4,the
Charact of
b4 #) holds
for
b5,
b6 being
Function st
b5,
b6 form_morphism_between b1,
b2 holds
b3 | b1,
b5,
b6 = b4 | b1,
b5,
b6
theorem Th23: :: INSTALG1:23
theorem Th24: :: INSTALG1:24
theorem Th25: :: INSTALG1:25
for
b1,
b2 being non
empty non
void ManySortedSign for
b3,
b4 being
Function st
b3,
b4 form_morphism_between b1,
b2 holds
for
b5 being
MSAlgebra of
b2 for
b6 being
OperSymbol of
b1 for
b7 being
OperSymbol of
b2 st
b7 = b4 . b6 holds
(
Args b7,
b5 = Args b6,
(b5 | b1,b3,b4) &
Result b6,
(b5 | b1,b3,b4) = Result b7,
b5 )
theorem Th26: :: INSTALG1:26
theorem Th27: :: INSTALG1:27
theorem Th28: :: INSTALG1:28
for
b1,
b2,
b3 being non
empty ManySortedSign for
b4,
b5 being
Function st
b4,
b5 form_morphism_between b1,
b2 holds
for
b6,
b7 being
Function st
b6,
b7 form_morphism_between b2,
b3 holds
for
b8 being
MSAlgebra of
b3 holds
b8 | b1,
(b6 * b4),
(b7 * b5) = (b8 | b2,b6,b7) | b1,
b4,
b5
theorem Th29: :: INSTALG1:29
theorem Th30: :: INSTALG1:30
for
b1,
b2 being non
empty ManySortedSign for
b3 being
Function of the
carrier of
b1,the
carrier of
b2 for
b4 being
Function st
b3,
b4 form_morphism_between b1,
b2 holds
for
b5,
b6 being
MSAlgebra of
b2 for
b7 being
ManySortedFunction of the
Sorts of
b5,the
Sorts of
b6 holds
b7 * b3 is
ManySortedFunction of the
Sorts of
(b5 | b1,b3,b4),the
Sorts of
(b6 | b1,b3,b4)
theorem Th31: :: INSTALG1:31
theorem Th32: :: INSTALG1:32
theorem Th33: :: INSTALG1:33
theorem Th34: :: INSTALG1:34
for
b1,
b2 being non
empty non
void ManySortedSign for
b3,
b4 being
Function st
b3,
b4 form_morphism_between b1,
b2 holds
for
b5,
b6 being
MSAlgebra of
b2 for
b7 being
ManySortedFunction of
b5,
b6 for
b8 being
ManySortedFunction of
(b5 | b1,b3,b4),
(b6 | b1,b3,b4) st
b8 = b7 * b3 holds
for
b9 being
OperSymbol of
b1 for
b10 being
OperSymbol of
b2 st
b10 = b4 . b9 &
Args b10,
b5 <> {} &
Args b10,
b6 <> {} holds
for
b11 being
Element of
Args b10,
b5 for
b12 being
Element of
Args b9,
(b5 | b1,b3,b4) st
b11 = b12 holds
b8 # b12 = b7 # b11
theorem Th35: :: INSTALG1:35
for
b1,
b2 being non
empty non
void ManySortedSign for
b3,
b4 being
MSAlgebra of
b1 st the
Sorts of
b3 is_transformable_to the
Sorts of
b4 holds
for
b5 being
ManySortedFunction of
b3,
b4 st
b5 is_homomorphism b3,
b4 holds
for
b6 being
Function of the
carrier of
b2,the
carrier of
b1 for
b7 being
Function st
b6,
b7 form_morphism_between b2,
b1 holds
ex
b8 being
ManySortedFunction of
(b3 | b2,b6,b7),
(b4 | b2,b6,b7) st
(
b8 = b5 * b6 &
b8 is_homomorphism b3 | b2,
b6,
b7,
b4 | b2,
b6,
b7 )
theorem Th36: :: INSTALG1:36
theorem Th37: :: INSTALG1:37
for
b1,
b2 being non
empty non
void ManySortedSign for
b3 being
non-empty MSAlgebra of
b1 for
b4 being
Function of the
carrier of
b2,the
carrier of
b1 for
b5 being
Function st
b4,
b5 form_morphism_between b2,
b1 holds
for
b6 being
non-empty MSAlgebra of
b2 st
b6 = b3 | b2,
b4,
b5 holds
for
b7,
b8 being
SortSymbol of
b2 for
b9 being
Function st
b9 is_e.translation_of b6,
b7,
b8 holds
b9 is_e.translation_of b3,
b4 . b7,
b4 . b8
Lemma26:
for b1, b2 being non empty non void ManySortedSign
for b3 being non-empty MSAlgebra of b1
for b4 being Function of the carrier of b2,the carrier of b1
for b5 being Function st b4,b5 form_morphism_between b2,b1 holds
for b6 being non-empty MSAlgebra of b2 st b6 = b3 | b2,b4,b5 holds
for b7, b8 being SortSymbol of b2 st TranslationRel b2 reduces b7,b8 holds
( TranslationRel b1 reduces b4 . b7,b4 . b8 & ( for b9 being Translation of b6,b7,b8 holds b9 is Translation of b3,b4 . b7,b4 . b8 ) )
theorem Th38: :: INSTALG1:38
theorem Th39: :: INSTALG1:39
for
b1,
b2 being non
empty non
void ManySortedSign for
b3 being
non-empty MSAlgebra of
b1 for
b4 being
Function of the
carrier of
b2,the
carrier of
b1 for
b5 being
Function st
b4,
b5 form_morphism_between b2,
b1 holds
for
b6 being
non-empty MSAlgebra of
b2 st
b6 = b3 | b2,
b4,
b5 holds
for
b7,
b8 being
SortSymbol of
b2 st
TranslationRel b2 reduces b7,
b8 holds
for
b9 being
Translation of
b6,
b7,
b8 holds
b9 is
Translation of
b3,
b4 . b7,
b4 . b8 by Lemma26;
theorem Th40: :: INSTALG1:40
definition
let c1,
c2 be non
empty non
void ManySortedSign ;
let c3 be
V3 ManySortedSet of the
carrier of
c2;
let c4 be
Function of the
carrier of
c1,the
carrier of
c2;
let c5 be
Function;
assume E28:
c4,
c5 form_morphism_between c1,
c2
;
func hom c4,
c5,
c3,
c1,
c2 -> ManySortedFunction of
(FreeMSA (a3 * a4)),
((FreeMSA a3) | a1,a4,a5) means :
Def5:
:: INSTALG1:def 5
(
a6 is_homomorphism FreeMSA (a3 * a4),
(FreeMSA a3) | a1,
a4,
a5 & ( for
b1 being
SortSymbol of
a1 for
b2 being
Element of
(a3 * a4) . b1 holds
(a6 . b1) . (root-tree [b2,b1]) = root-tree [b2,(a4 . b1)] ) );
existence
ex b1 being ManySortedFunction of (FreeMSA (c3 * c4)),((FreeMSA c3) | c1,c4,c5) st
( b1 is_homomorphism FreeMSA (c3 * c4),(FreeMSA c3) | c1,c4,c5 & ( for b2 being SortSymbol of c1
for b3 being Element of (c3 * c4) . b2 holds (b1 . b2) . (root-tree [b3,b2]) = root-tree [b3,(c4 . b2)] ) )
uniqueness
for b1, b2 being ManySortedFunction of (FreeMSA (c3 * c4)),((FreeMSA c3) | c1,c4,c5) st b1 is_homomorphism FreeMSA (c3 * c4),(FreeMSA c3) | c1,c4,c5 & ( for b3 being SortSymbol of c1
for b4 being Element of (c3 * c4) . b3 holds (b1 . b3) . (root-tree [b4,b3]) = root-tree [b4,(c4 . b3)] ) & b2 is_homomorphism FreeMSA (c3 * c4),(FreeMSA c3) | c1,c4,c5 & ( for b3 being SortSymbol of c1
for b4 being Element of (c3 * c4) . b3 holds (b2 . b3) . (root-tree [b4,b3]) = root-tree [b4,(c4 . b3)] ) holds
b1 = b2
end;
:: deftheorem Def5 defines hom INSTALG1:def 5 :
for
b1,
b2 being non
empty non
void ManySortedSign for
b3 being
V3 ManySortedSet of the
carrier of
b2 for
b4 being
Function of the
carrier of
b1,the
carrier of
b2 for
b5 being
Function st
b4,
b5 form_morphism_between b1,
b2 holds
for
b6 being
ManySortedFunction of
(FreeMSA (b3 * b4)),
((FreeMSA b3) | b1,b4,b5) holds
(
b6 = hom b4,
b5,
b3,
b1,
b2 iff (
b6 is_homomorphism FreeMSA (b3 * b4),
(FreeMSA b3) | b1,
b4,
b5 & ( for
b7 being
SortSymbol of
b1 for
b8 being
Element of
(b3 * b4) . b7 holds
(b6 . b7) . (root-tree [b8,b7]) = root-tree [b8,(b4 . b7)] ) ) );
theorem Th41: :: INSTALG1:41
for
b1,
b2 being non
empty non
void ManySortedSign for
b3 being
V3 ManySortedSet of the
carrier of
b2 for
b4 being
Function of the
carrier of
b1,the
carrier of
b2 for
b5 being
Function st
b4,
b5 form_morphism_between b1,
b2 holds
for
b6 being
OperSymbol of
b1 for
b7 being
Element of
Args b6,
(FreeMSA (b3 * b4)) for
b8 being
FinSequence st
b8 = (hom b4,b5,b3,b1,b2) # b7 holds
((hom b4,b5,b3,b1,b2) . (the_result_sort_of b6)) . ([b6,the carrier of b1] -tree b7) = [(b5 . b6),the carrier of b2] -tree b8
theorem Th42: :: INSTALG1:42
for
b1,
b2 being non
empty non
void ManySortedSign for
b3 being
V3 ManySortedSet of the
carrier of
b2 for
b4 being
Function of the
carrier of
b1,the
carrier of
b2 for
b5 being
Function st
b4,
b5 form_morphism_between b1,
b2 holds
for
b6 being
Term of
b1,
(b3 * b4) holds
(
((hom b4,b5,b3,b1,b2) . (the_sort_of b6)) . b6 is
CompoundTerm of
b2,
b3 iff
b6 is
CompoundTerm of
b1,
b3 * b4 )
theorem Th43: :: INSTALG1:43
for
b1,
b2 being non
empty non
void ManySortedSign for
b3 being
V3 ManySortedSet of the
carrier of
b2 for
b4 being
Function of the
carrier of
b1,the
carrier of
b2 for
b5 being
one-to-one Function st
b4,
b5 form_morphism_between b1,
b2 holds
hom b4,
b5,
b3,
b1,
b2 is_monomorphism FreeMSA (b3 * b4),
(FreeMSA b3) | b1,
b4,
b5
theorem Th44: :: INSTALG1:44
theorem Th45: :: INSTALG1:45
for
b1,
b2,
b3 being non
empty non
void ManySortedSign for
b4 being
V3 ManySortedSet of the
carrier of
b3 for
b5 being
Function of the
carrier of
b1,the
carrier of
b2 for
b6 being
Function st
b5,
b6 form_morphism_between b1,
b2 holds
for
b7 being
Function of the
carrier of
b2,the
carrier of
b3 for
b8 being
Function st
b7,
b8 form_morphism_between b2,
b3 holds
hom (b7 * b5),
(b8 * b6),
b4,
b1,
b3 = ((hom b7,b8,b4,b2,b3) * b5) ** (hom b5,b6,(b4 * b7),b1,b2)