:: Institution of Many-sorted Algebras, Part { I } : Signature Reductof an Algebra
:: by Grzegorz Bancerek
::
:: Received December 30, 1996
:: Copyright (c) 1996 Association of Mizar Users

theorem :: INSTALG1:1

canceled;

theorem Th2: :: INSTALG1:2

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for V being V5 ManySortedSet of the carrier of S
for x being set holds
( x is ArgumentSeq of Sym o,V iff x is Element of Args o,(FreeMSA V) )

proof end;

registration

let S be non empty non void ManySortedSign ;
let V be V5 ManySortedSet of the carrier of S;
let o be OperSymbol of S;
cluster -> DTree-yielding Element of Args o,(FreeMSA V);
coherence
for b₁ being Element of Args o,(FreeMSA V) holds b₁ is DTree-yielding by Th2;

end;

theorem Th3: :: INSTALG1:3

for S 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 o being OperSymbol of S st Args o,A1 <> {} holds
Args o,A2 <> {}

proof end;

theorem Th4: :: INSTALG1:4

for S being non empty non void ManySortedSign
for o being OperSymbol of S
for V being V5 ManySortedSet of the carrier of S
for x being Element of Args o,(FreeMSA V) holds (Den o,(FreeMSA V)) . x = [o,the carrier of S] -tree x

proof end;

theorem :: INSTALG1:5

for S being non empty non void ManySortedSign
for A, B being MSAlgebra of S st MSAlgebra(# the Sorts of A,the Charact of A #) = MSAlgebra(# the Sorts of B,the Charact of B #) holds
for o being OperSymbol of S holds Den o,A = Den o,B ;

theorem Th6: :: INSTALG1:6

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

proof end;

theorem :: INSTALG1:7

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 h' being ManySortedFunction of B1,B2 st
( h' = h & h' is_homomorphism B1,B2 )

proof end;

definition

let S be ManySortedSign ;
attr S is feasible means :Def1: :: INSTALG1:def 1
( the carrier of S = {} implies the carrier' of S = {} );

end;

:: deftheorem Def1 defines feasible INSTALG1:def 1 :

for S being ManySortedSign holds
( S is feasible iff ( the carrier of S = {} implies the carrier' of S = {} ) );

theorem Th8: :: INSTALG1:8

for S being ManySortedSign holds
( S is feasible iff dom the ResultSort of S = the carrier' of S )

proof end;

registration

cluster non empty -> feasible ManySortedSign ;
coherence
for b₁ being ManySortedSign st not b₁ is empty holds
b₁ is feasible

proof end;

cluster void -> feasible ManySortedSign ;
coherence
for b₁ being ManySortedSign st b₁ is void holds
b₁ is feasible

proof end;

cluster empty feasible -> void ManySortedSign ;
coherence
for b₁ being ManySortedSign st b₁ is empty & b₁ is feasible holds
b₁ is void

proof end;

cluster non void feasible -> non empty ManySortedSign ;
coherence
for b₁ being ManySortedSign st not b₁ is void & b₁ is feasible holds
not b₁ is empty ;

end;

registration

cluster non empty non void ManySortedSign ;
existence
ex b₁ being ManySortedSign st
( not b₁ is void & not b₁ is empty )

proof end;

end;

theorem Th9: :: INSTALG1:9

for S being feasible ManySortedSign holds id the carrier of S, id the carrier' of S form_morphism_between S,S

proof end;

theorem Th10: :: INSTALG1:10

for S1, S2 being ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
( f is Function of the carrier of S1,the carrier of S2 & g is Function of the carrier' of S1,the carrier' of S2 )

proof end;

definition

let S be feasible ManySortedSign ;
mode Subsignature of S -> ManySortedSign means :Def2: :: INSTALG1:def 2
id the carrier of it, id the carrier' of it form_morphism_between it,S;
existence
ex b₁ being ManySortedSign st id the carrier of b₁, id the carrier' of b₁ form_morphism_between b₁,S

proof end;

end;

:: deftheorem Def2 defines Subsignature INSTALG1:def 2 :

for S being feasible ManySortedSign
for b₂ being ManySortedSign holds
( b₂ is Subsignature of S iff id the carrier of b₂, id the carrier' of b₂ form_morphism_between b₂,S );

theorem Th11: :: INSTALG1:11

for S being feasible ManySortedSign
for T being Subsignature of S holds
( the carrier of T c= the carrier of S & the carrier' of T c= the carrier' of S )

proof end;

registration

let S be feasible ManySortedSign ;
cluster -> feasible Subsignature of S;
coherence
for b₁ being Subsignature of S holds b₁ is feasible

proof end;

end;

theorem Th12: :: INSTALG1:12

for S being feasible ManySortedSign
for T being Subsignature of S holds
( the ResultSort of T c= the ResultSort of S & the Arity of T c= the Arity of S )

proof end;

theorem Th13: :: INSTALG1:13

for S being feasible ManySortedSign
for T being Subsignature of S holds
( the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T )

proof end;

theorem Th14: :: INSTALG1:14

for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S & the Arity of T c= the Arity of S & the ResultSort of T c= the ResultSort of S holds
T is Subsignature of S

proof end;

theorem :: INSTALG1:15

for S, T being feasible ManySortedSign st the carrier of T c= the carrier of S & the Arity of T = the Arity of S | the carrier' of T & the ResultSort of T = the ResultSort of S | the carrier' of T holds
T is Subsignature of S

proof end;

theorem Th16: :: INSTALG1:16

for S being feasible ManySortedSign holds S is Subsignature of S

proof end;

theorem :: INSTALG1:17

for S1 being feasible ManySortedSign
for S2 being Subsignature of S1
for S3 being Subsignature of S2 holds S3 is Subsignature of S1

proof end;

theorem :: INSTALG1:18

for S1 being feasible ManySortedSign
for S2 being Subsignature of S1 st S1 is Subsignature of S2 holds
ManySortedSign(# the carrier of S1,the carrier' of S1,the Arity of S1,the ResultSort of S1 #) = ManySortedSign(# the carrier of S2,the carrier' of S2,the Arity of S2,the ResultSort of S2 #)

proof end;

registration

let S be non empty ManySortedSign ;
cluster non empty feasible Subsignature of S;
existence
not for b₁ being Subsignature of S holds b₁ is empty

proof end;

end;

registration

let S be non void feasible ManySortedSign ;
cluster non void feasible Subsignature of S;
existence
not for b₁ being Subsignature of S holds b₁ is void

proof end;

end;

theorem :: INSTALG1:19

for S being feasible ManySortedSign
for S' being Subsignature of S
for T being ManySortedSign
for f, g being Function st f,g form_morphism_between S,T holds
f | the carrier of S',g | the carrier' of S' form_morphism_between S',T

proof end;

theorem :: INSTALG1:20

for S being ManySortedSign
for T being feasible ManySortedSign
for T' being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T' holds
f,g form_morphism_between S,T

proof end;

theorem :: INSTALG1:21

for S being ManySortedSign
for T being feasible ManySortedSign
for T' being Subsignature of T
for f, g being Function st f,g form_morphism_between S,T & rng f c= the carrier of T' & rng g c= the carrier' of T' holds
f,g form_morphism_between S,T'

proof end;

definition

let S1, S2 be non empty ManySortedSign ;
let A be MSAlgebra of S2;
let f, g be Function;
assume A1: f,g form_morphism_between S1,S2 ;
func A | S1,f,g -> strict MSAlgebra of S1 means :Def3: :: INSTALG1:def 3
( the Sorts of it = the Sorts of A * f & the Charact of it = the Charact of A * g );
existence
ex b₁ being strict MSAlgebra of S1 st
( the Sorts of b₁ = the Sorts of A * f & the Charact of b₁ = the Charact of A * g )

proof end;

correctness
uniqueness
for b₁, b₂ being strict MSAlgebra of S1 st the Sorts of b₁ = the Sorts of A * f & the Charact of b₁ = the Charact of A * g & the Sorts of b₂ = the Sorts of A * f & the Charact of b₂ = the Charact of A * g holds
b₁ = b₂;
;

end;

:: deftheorem Def3 defines | INSTALG1:def 3 :

for S1, S2 being non empty ManySortedSign
for A being MSAlgebra of S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
for b₆ being strict MSAlgebra of S1 holds
( b₆ = A | S1,f,g iff ( the Sorts of b₆ = the Sorts of A * f & the Charact of b₆ = the Charact of A * g ) );

definition

let S2, S1 be non empty ManySortedSign ;
let A be MSAlgebra of S2;
func A | S1 -> strict MSAlgebra of S1 equals :: INSTALG1:def 4
A | S1,(id the carrier of S1),(id the carrier' of S1);
correctness
coherence
A | S1,(id the carrier of S1),(id the carrier' of S1) is strict MSAlgebra of S1;
;

end;

:: deftheorem defines | INSTALG1:def 4 :

for S2, S1 being non empty ManySortedSign
for A being MSAlgebra of S2 holds A | S1 = A | S1,(id the carrier of S1),(id the carrier' of S1);

theorem :: INSTALG1:22

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

proof end;

theorem Th23: :: INSTALG1:23

for S1, S2 being non empty ManySortedSign
for A being non-empty MSAlgebra of S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | S1,f,g is non-empty

proof end;

registration

let S2 be non empty ManySortedSign ;
let S1 be non empty Subsignature of S2;
let A be non-empty MSAlgebra of S2;
cluster A | S1 -> strict non-empty ;
coherence
A | S1 is non-empty

proof end;

end;

theorem Th24: :: INSTALG1:24

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
Den o1,(A | S1,f,g) = Den o2,A

proof end;

theorem Th25: :: INSTALG1:25

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 )

proof end;

theorem Th26: :: INSTALG1:26

for S being non empty ManySortedSign
for A being MSAlgebra of S holds A | S,(id the carrier of S),(id the carrier' of S) = MSAlgebra(# the Sorts of A,the Charact of A #)

proof end;

theorem :: INSTALG1:27

for S being non empty ManySortedSign
for A being MSAlgebra of S holds A | S = MSAlgebra(# the Sorts of A,the Charact of A #) by Th26;

theorem Th28: :: INSTALG1:28

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

proof end;

theorem :: INSTALG1:29

for S1 being non empty feasible ManySortedSign
for S2 being non empty Subsignature of S1
for S3 being non empty Subsignature of S2
for A being MSAlgebra of S1 holds A | S3 = (A | S2) | S3

proof end;

theorem Th30: :: INSTALG1:30

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)

proof end;

theorem :: INSTALG1:31

for S1 being non empty ManySortedSign
for S2 being non empty Subsignature of S1
for A1, A2 being MSAlgebra of S1
for h being ManySortedFunction of the Sorts of A1,the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2),the Sorts of (A2 | S2)

proof end;

theorem Th32: :: INSTALG1:32

for S1, S2 being non empty ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra of S2 holds (id the Sorts of A) * f = id the Sorts of (A | S1,f,g)

proof end;

theorem :: INSTALG1:33

for S1 being non empty ManySortedSign
for S2 being non empty Subsignature of S1
for A being MSAlgebra of S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

proof end;

theorem Th34: :: INSTALG1:34

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

proof end;

theorem Th35: :: INSTALG1:35

for S, S' 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 S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
ex h' being ManySortedFunction of (A1 | S',f,g),(A2 | S',f,g) st
( h' = h * f & h' is_homomorphism A1 | S',f,g,A2 | S',f,g )

proof end;

theorem :: INSTALG1:36

for S being non void feasible ManySortedSign
for S' being non void Subsignature of S
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
ex h' being ManySortedFunction of (A1 | S'),(A2 | S') st
( h' = h | the carrier of S' & h' is_homomorphism A1 | S',A2 | S' )

proof end;

theorem Th37: :: INSTALG1:37

for S, S' being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S'
for t being Function st t is_e.translation_of B,s1,s2 holds
t is_e.translation_of A,f . s1,f . s2

proof end;

Lm1: for S, S' being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S' st TranslationRel S' 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 ) )

proof end;

theorem :: INSTALG1:38

for S, S' being non empty non void ManySortedSign
for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
TranslationRel S reduces f . s1,f . s2

proof end;

theorem :: INSTALG1:39

for S, S' being non empty non void ManySortedSign
for A being non-empty MSAlgebra of S
for f being Function of the carrier of S',the carrier of S
for g being Function st f,g form_morphism_between S',S holds
for B being non-empty MSAlgebra of S' st B = A | S',f,g holds
for s1, s2 being SortSymbol of S' st TranslationRel S' reduces s1,s2 holds
for t being Translation of B,s1,s2 holds t is Translation of A,f . s1,f . s2 by Lm1;

scheme :: INSTALG1:sch 1
GenFuncEx{ F₁() -> non empty non void ManySortedSign , F₂() -> non-empty MSAlgebra of F₁(), F₃() -> V5 ManySortedSet of the carrier of F₁(), F₄( set , set ) -> set } :

ex h being ManySortedFunction of (FreeMSA F₃()),F₂() st
( h is_homomorphism FreeMSA F₃(),F₂() & ( for s being SortSymbol of F₁()
for x being Element of F₃() . s holds (h . s) . (root-tree [x,s]) = F₄(x,s) ) )

provided

A1: for s being SortSymbol of F₁()
for x being Element of F₃() . s holds F₄(x,s) in the Sorts of F₂() . s

proof end;

theorem Th40: :: INSTALG1:40

for I being set
for A, B being ManySortedSet of I
for C being ManySortedSubset of A
for F being ManySortedFunction of A,B
for i being set st i in I holds
for f, g being Function st f = F . i & g = (F || C) . i holds
for x being set st x in C . i holds
g . x = f . x

proof end;

registration

let S be non empty non void ManySortedSign ;
let X be V5 ManySortedSet of the carrier of S;
cluster FreeGen X -> V5 ;
coherence
FreeGen X is non-empty ;

end;

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: :: INSTALG1:def 5
( 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 b₁ being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | S1,f,g) st
( b₁ 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 (b₁ . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) )

proof end;

uniqueness
for b₁, b₂ being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | S1,f,g) st b₁ 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 (b₁ . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & b₂ 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 (b₂ . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) holds
b₁ = b₂

proof end;

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 b₆ being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | S1,f,g) holds
( b₆ = hom f,g,X,S1,S2 iff ( b₆ 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 (b₆ . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) );

theorem Th41: :: INSTALG1:41

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

proof end;

theorem Th42: :: INSTALG1:42

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 )

proof end;

theorem :: INSTALG1:43

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

proof end;

theorem :: INSTALG1:44

for S being non empty non void ManySortedSign
for X being V5 ManySortedSet of the carrier of S holds hom (id the carrier of S),(id the carrier' of S),X,S,S = id the Sorts of (FreeMSA X)

proof end;

theorem :: INSTALG1:45

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)

proof end;