:: by Grzegorz Bancerek

::

:: Received December 30, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

theorem Th1: :: INSTALG1:1

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for V being V16() 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)) )

for o being OperSymbol of S

for V being V16() 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 V16() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

coherence

for b_{1} being Element of Args (o,(FreeMSA V)) holds b_{1} is DTree-yielding
by Th1;

end;
let V be V16() ManySortedSet of the carrier of S;

let o be OperSymbol of S;

coherence

for b

theorem Th2: :: INSTALG1:2

for S being non empty non void ManySortedSign

for A1, A2 being MSAlgebra over 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) <> {}

for A1, A2 being MSAlgebra over 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 Th3: :: INSTALG1:3

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for V being V16() 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

for o being OperSymbol of S

for V being V16() 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:4

theorem Th5: :: INSTALG1:5

for S being non empty non void ManySortedSign

for A1, A2, B1, B2 being MSAlgebra over 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

for A1, A2, B1, B2 being MSAlgebra over 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:6

for S being non empty non void ManySortedSign

for A1, A2, B1, B2 being MSAlgebra over 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 )

for A1, A2, B1, B2 being MSAlgebra over 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 )

proof 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 = {} ) );

for S being ManySortedSign holds

( S is feasible iff ( the carrier of S = {} implies the carrier' of S = {} ) );

registration

coherence

for b_{1} being ManySortedSign st not b_{1} is empty holds

b_{1} is feasible

for b_{1} being ManySortedSign st b_{1} is void holds

b_{1} is feasible

for b_{1} being ManySortedSign st b_{1} is empty & b_{1} is feasible holds

b_{1} is void

for b_{1} being ManySortedSign st not b_{1} is void & b_{1} is feasible holds

not b_{1} is empty
;

end;
for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

coherence for b

not b

registration
end;

theorem Th8: :: INSTALG1:8

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

proof end;

theorem Th9: :: INSTALG1:9

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 )

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;

begin

definition

let S be feasible ManySortedSign ;

ex b_{1} being ManySortedSign st id the carrier of b_{1}, id the carrier' of b_{1} form_morphism_between b_{1},S

end;
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 id the carrier of it, id the carrier' of it form_morphism_between it,S;

ex b

proof end;

:: deftheorem Def2 defines Subsignature INSTALG1:def 2 :

for S being feasible ManySortedSign

for b_{2} being ManySortedSign holds

( b_{2} is Subsignature of S iff id the carrier of b_{2}, id the carrier' of b_{2} form_morphism_between b_{2},S );

for S being feasible ManySortedSign

for b

( b

theorem Th10: :: INSTALG1:10

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 )

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 ;

coherence

for b_{1} being Subsignature of S holds b_{1} is feasible

end;
coherence

for b

proof end;

theorem Th11: :: INSTALG1:11

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 )

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 Th12: :: INSTALG1:12

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 )

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 Th13: :: INSTALG1:13

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

T is Subsignature of S

proof end;

theorem :: INSTALG1:14

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

T is Subsignature of S

proof end;

theorem :: INSTALG1:16

for S1 being feasible ManySortedSign

for S2 being Subsignature of S1

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

for S2 being Subsignature of S1

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

proof end;

theorem :: INSTALG1:17

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 #)

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 ;

existence

not for b_{1} being Subsignature of S holds b_{1} is empty

end;
existence

not for b

proof end;

registration

let S be non void feasible ManySortedSign ;

existence

not for b_{1} being Subsignature of S holds b_{1} is void

end;
existence

not for b

proof end;

theorem :: INSTALG1:18

for S being feasible ManySortedSign

for S9 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 S9,g | the carrier' of S9 form_morphism_between S9,T

for S9 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 S9,g | the carrier' of S9 form_morphism_between S9,T

proof end;

theorem :: INSTALG1:19

for S being ManySortedSign

for T being feasible ManySortedSign

for T9 being Subsignature of T

for f, g being Function st f,g form_morphism_between S,T9 holds

f,g form_morphism_between S,T

for T being feasible ManySortedSign

for T9 being Subsignature of T

for f, g being Function st f,g form_morphism_between S,T9 holds

f,g form_morphism_between S,T

proof end;

theorem :: INSTALG1:20

for S being ManySortedSign

for T being feasible ManySortedSign

for T9 being Subsignature of T

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

f,g form_morphism_between S,T9

for T being feasible ManySortedSign

for T9 being Subsignature of T

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

f,g form_morphism_between S,T9

proof end;

begin

definition

let S1, S2 be non empty ManySortedSign ;

let A be MSAlgebra over S2;

let f, g be Function;

assume B1: f,g form_morphism_between S1,S2 ;

ex b_{1} being strict MSAlgebra over S1 st

( the Sorts of b_{1} = the Sorts of A * f & the Charact of b_{1} = the Charact of A * g )

uniqueness

for b_{1}, b_{2} being strict MSAlgebra over S1 st the Sorts of b_{1} = the Sorts of A * f & the Charact of b_{1} = the Charact of A * g & the Sorts of b_{2} = the Sorts of A * f & the Charact of b_{2} = the Charact of A * g holds

b_{1} = b_{2};

;

end;
let A be MSAlgebra over S2;

let f, g be Function;

assume B1: f,g form_morphism_between S1,S2 ;

func A | (S1,f,g) -> strict MSAlgebra over 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 ( the Sorts of it = the Sorts of A * f & the Charact of it = the Charact of A * g );

ex b

( the Sorts of b

proof end;

correctness uniqueness

for b

b

;

:: deftheorem Def3 defines | INSTALG1:def 3 :

for S1, S2 being non empty ManySortedSign

for A being MSAlgebra over S2

for f, g being Function st f,g form_morphism_between S1,S2 holds

for b_{6} being strict MSAlgebra over S1 holds

( b_{6} = A | (S1,f,g) iff ( the Sorts of b_{6} = the Sorts of A * f & the Charact of b_{6} = the Charact of A * g ) );

for S1, S2 being non empty ManySortedSign

for A being MSAlgebra over S2

for f, g being Function st f,g form_morphism_between S1,S2 holds

for b

( b

definition

let S2, S1 be non empty ManySortedSign ;

let A be MSAlgebra over S2;

coherence

A | (S1,(id the carrier of S1),(id the carrier' of S1)) is strict MSAlgebra over S1;

;

end;
let A be MSAlgebra over S2;

func A | S1 -> strict MSAlgebra over S1 equals :: INSTALG1:def 4

A | (S1,(id the carrier of S1),(id the carrier' of S1));

correctness A | (S1,(id the carrier of S1),(id the carrier' of S1));

coherence

A | (S1,(id the carrier of S1),(id the carrier' of S1)) is strict MSAlgebra over S1;

;

:: deftheorem defines | INSTALG1:def 4 :

for S2, S1 being non empty ManySortedSign

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

for S2, S1 being non empty ManySortedSign

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

theorem :: INSTALG1:21

for S1, S2 being non empty ManySortedSign

for A, B being MSAlgebra over 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)

for A, B being MSAlgebra over 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 Th22: :: INSTALG1:22

for S1, S2 being non empty ManySortedSign

for A being non-empty MSAlgebra over S2

for f, g being Function st f,g form_morphism_between S1,S2 holds

A | (S1,f,g) is non-empty

for A being non-empty MSAlgebra over 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 over S2;

coherence

A | S1 is non-empty

end;
let S1 be non empty Subsignature of S2;

let A be non-empty MSAlgebra over S2;

coherence

A | S1 is non-empty

proof end;

theorem Th23: :: INSTALG1:23

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 over 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)

for f, g being Function st f,g form_morphism_between S1,S2 holds

for A being MSAlgebra over 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 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 over 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) )

for f, g being Function st f,g form_morphism_between S1,S2 holds

for A being MSAlgebra over 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 Th25: :: INSTALG1:25

for S being non empty ManySortedSign

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

for A being MSAlgebra over 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:26

theorem Th27: :: INSTALG1:27

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 over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)

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 over S3 holds A | (S1,(f2 * f1),(g2 * g1)) = (A | (S2,f2,g2)) | (S1,f1,g1)

proof end;

theorem :: INSTALG1:28

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 over S1 holds A | S3 = (A | S2) | S3

for S2 being non empty Subsignature of S1

for S3 being non empty Subsignature of S2

for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3

proof end;

theorem Th29: :: INSTALG1:29

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 over 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))

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 over 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:30

for S1 being non empty ManySortedSign

for S2 being non empty Subsignature of S1

for A1, A2 being MSAlgebra over 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)

for S2 being non empty Subsignature of S1

for A1, A2 being MSAlgebra over 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 Th31: :: INSTALG1:31

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 over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))

for f, g being Function st f,g form_morphism_between S1,S2 holds

for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))

proof end;

theorem :: INSTALG1:32

for S1 being non empty ManySortedSign

for S2 being non empty Subsignature of S1

for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

for S2 being non empty Subsignature of S1

for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)

proof end;

theorem Th33: :: INSTALG1:33

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 over 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

for f, g being Function st f,g form_morphism_between S1,S2 holds

for A, B being MSAlgebra over 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 Th34: :: INSTALG1:34

for S, S9 being non empty non void ManySortedSign

for A1, A2 being MSAlgebra over 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) )

for A1, A2 being MSAlgebra over 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) )

proof end;

theorem :: INSTALG1:35

for S being non void feasible ManySortedSign

for S9 being non void Subsignature of S

for A1, A2 being MSAlgebra over 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 h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

for S9 being non void Subsignature of S

for A1, A2 being MSAlgebra over 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 h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st

( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )

proof end;

theorem Th36: :: INSTALG1:36

for S, S9 being non empty non void ManySortedSign

for A being non-empty MSAlgebra over 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 over 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

for A being non-empty MSAlgebra over 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 over 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

proof end;

Lm1: for S, S9 being non empty non void ManySortedSign

for A being non-empty MSAlgebra over 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 over 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 ) )

proof end;

theorem :: INSTALG1:37

for S, S9 being non empty non void ManySortedSign

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 s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2

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 s1, s2 being SortSymbol of S9 st TranslationRel S9 reduces s1,s2 holds

TranslationRel S reduces f . s1,f . s2

proof end;

theorem :: INSTALG1:38

for S, S9 being non empty non void ManySortedSign

for A being non-empty MSAlgebra over 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 over 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;

for A being non-empty MSAlgebra over 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 over 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

scheme :: INSTALG1:sch 1

GenFuncEx{ F_{1}() -> non empty non void ManySortedSign , F_{2}() -> non-empty MSAlgebra over F_{1}(), F_{3}() -> V16() ManySortedSet of the carrier of F_{1}(), F_{4}( set , set ) -> set } :

GenFuncEx{ F

ex h being ManySortedFunction of (FreeMSA F_{3}()),F_{2}() st

( h is_homomorphism FreeMSA F_{3}(),F_{2}() & ( for s being SortSymbol of F_{1}()

for x being Element of F_{3}() . s holds (h . s) . (root-tree [x,s]) = F_{4}(x,s) ) )

provided( h is_homomorphism FreeMSA F

for x being Element of F

A1:
for s being SortSymbol of F_{1}()

for x being Element of F_{3}() . s holds F_{4}(x,s) in the Sorts of F_{2}() . s

for x being Element of F

proof end;

theorem Th39: :: INSTALG1:39

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

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 V16() ManySortedSet of the carrier of S;

coherence

FreeGen X is non-empty ;

end;
let X be V16() ManySortedSet of the carrier of S;

coherence

FreeGen X is non-empty ;

definition

let S1, S2 be non empty non void ManySortedSign ;

let X be V16() ManySortedSet of the carrier of S2;

let f be Function of the carrier of S1, the carrier of S2;

let g be Function;

assume B1: f,g form_morphism_between S1,S2 ;

ex b_{1} being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st

( b_{1} 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_{1} . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) )

for b_{1}, b_{2} being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) st b_{1} 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_{1} . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) & b_{2} 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_{2} . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) holds

b_{1} = b_{2}

end;
let X be V16() ManySortedSet of the carrier of S2;

let f be Function of the carrier of S1, the carrier of S2;

let g be Function;

assume B1: 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 ( 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)] ) );

ex b

( b

for x being Element of (X * f) . s holds (b

proof end;

uniqueness for b

for x being Element of (X * f) . s holds (b

for x being Element of (X * f) . s holds (b

b

proof end;

:: deftheorem Def5 defines hom INSTALG1:def 5 :

for S1, S2 being non empty non void ManySortedSign

for X being V16() 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_{6} being ManySortedFunction of (FreeMSA (X * f)),((FreeMSA X) | (S1,f,g)) holds

( b_{6} = hom (f,g,X,S1,S2) iff ( b_{6} 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_{6} . s) . (root-tree [x,s]) = root-tree [x,(f . s)] ) ) );

for S1, S2 being non empty non void ManySortedSign

for X being V16() 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

( b

for x being Element of (X * f) . s holds (b

theorem Th40: :: INSTALG1:40

for S1, S2 being non empty non void ManySortedSign

for X being V16() 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

for X being V16() 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 Th41: :: INSTALG1:41

for S1, S2 being non empty non void ManySortedSign

for X being V16() 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 )

for X being V16() 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:42

for S1, S2 being non empty non void ManySortedSign

for X being V16() 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)

for X being V16() 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:43

for S being non empty non void ManySortedSign

for X being V16() 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)

for X being V16() 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:44

for S1, S2, S3 being non empty non void ManySortedSign

for X being V16() 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))

for X being V16() 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;