:: by Grzegorz Bancerek

::

:: Received September 7, 1999

:: Copyright (c) 1999-2018 Association of Mizar Users

theorem Th3: :: ALGSPEC1:3

for f, g, h being Function st dom f misses rng h & g .: (dom h) misses dom f holds

f * (g +* h) = f * g

f * (g +* h) = f * g

proof end;

theorem Th4: :: ALGSPEC1:4

for f1, f2, g1, g2 being Function st f1 tolerates f2 & g1 tolerates g2 holds

f1 * g1 tolerates f2 * g2

f1 * g1 tolerates f2 * g2

proof end;

theorem Th5: :: ALGSPEC1:5

for X1, Y1, X2, Y2 being non empty set

for f being Function of X1,X2

for g being Function of Y1,Y2 st f c= g holds

f * c= g *

for f being Function of X1,X2

for g being Function of Y1,Y2 st f c= g holds

f * c= g *

proof end;

theorem Th6: :: ALGSPEC1:6

for X1, Y1, X2, Y2 being non empty set

for f being Function of X1,X2

for g being Function of Y1,Y2 st f tolerates g holds

f * tolerates g *

for f being Function of X1,X2

for g being Function of Y1,Y2 st f tolerates g holds

f * tolerates g *

proof end;

definition
end;

:: deftheorem defines -indexing ALGSPEC1:def 1 :

for X being set

for f being Function holds X -indexing f = (id X) +* (f | X);

for X being set

for f being Function holds X -indexing f = (id X) +* (f | X);

theorem Th8: :: ALGSPEC1:8

for X being non empty set

for f being Function

for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x

for f being Function

for x being Element of X holds (X -indexing f) . x = ((id X) +* f) . x

proof end;

theorem Th9: :: ALGSPEC1:9

for X, x being set

for f being Function st x in X holds

( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )

for f being Function st x in X holds

( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )

proof end;

theorem Th18: :: ALGSPEC1:18

for X, Y being set

for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)

for f being Function holds (X \/ Y) -indexing f = (X -indexing f) +* (Y -indexing f)

proof end;

theorem Th20: :: ALGSPEC1:20

for X, Y being set

for f being Function holds (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)

for f being Function holds (X \/ Y) -indexing f = (X -indexing f) \/ (Y -indexing f)

proof end;

theorem Th21: :: ALGSPEC1:21

for X being non empty set

for f, g being Function st rng g c= X holds

(X -indexing f) * g = ((id X) +* f) * g

for f, g being Function st rng g c= X holds

(X -indexing f) * g = ((id X) +* f) * g

proof end;

theorem :: ALGSPEC1:22

for f, g being Function st dom f misses dom g & rng g misses dom f holds

for X being set holds f * (X -indexing g) = f | X

for X being set holds f * (X -indexing g) = f | X

proof end;

definition

let f be Function;

ex b_{1} being Function st

( dom b_{1} = rng f & f * b_{1} = id (rng f) )

end;
mode rng-retract of f -> Function means :Def2: :: ALGSPEC1:def 2

( dom it = rng f & f * it = id (rng f) );

existence ( dom it = rng f & f * it = id (rng f) );

ex b

( dom b

proof end;

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

for f, b_{2} being Function holds

( b_{2} is rng-retract of f iff ( dom b_{2} = rng f & f * b_{2} = id (rng f) ) );

for f, b

( b

theorem Th24: :: ALGSPEC1:24

for f being Function

for g being rng-retract of f

for x being set st x in rng f holds

( g . x in dom f & f . (g . x) = x )

for g being rng-retract of f

for x being set st x in rng f holds

( g . x in dom f & f . (g . x) = x )

proof end;

theorem Th27: :: ALGSPEC1:27

for f1, f2 being Function st f1 tolerates f2 holds

for g1 being rng-retract of f1

for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2

for g1 being rng-retract of f1

for g2 being rng-retract of f2 holds g1 +* g2 is rng-retract of f1 +* f2

proof end;

theorem :: ALGSPEC1:28

for f1, f2 being Function st f1 c= f2 holds

for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2

for g1 being rng-retract of f1 ex g2 being rng-retract of f2 st g1 c= g2

proof end;

definition

let S be non empty non void ManySortedSign ;

let f, g be Function;

end;
let f, g be Function;

pred f,g form_a_replacement_in S means :: ALGSPEC1:def 3

for o1, o2 being OperSymbol of S st ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 holds

( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) );

for o1, o2 being OperSymbol of S st ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 holds

( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) );

:: deftheorem defines form_a_replacement_in ALGSPEC1:def 3 :

for S being non empty non void ManySortedSign

for f, g being Function holds

( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 holds

( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) );

for S being non empty non void ManySortedSign

for f, g being Function holds

( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ((id the carrier' of S) +* g) . o1 = ((id the carrier' of S) +* g) . o2 holds

( ((id the carrier of S) +* f) * (the_arity_of o1) = ((id the carrier of S) +* f) * (the_arity_of o2) & ((id the carrier of S) +* f) . (the_result_sort_of o1) = ((id the carrier of S) +* f) . (the_result_sort_of o2) ) );

theorem Th29: :: ALGSPEC1:29

for S being non empty non void ManySortedSign

for f, g being Function holds

( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds

( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) )

for f, g being Function holds

( f,g form_a_replacement_in S iff for o1, o2 being OperSymbol of S st ( the carrier' of S -indexing g) . o1 = ( the carrier' of S -indexing g) . o2 holds

( ( the carrier of S -indexing f) * (the_arity_of o1) = ( the carrier of S -indexing f) * (the_arity_of o2) & ( the carrier of S -indexing f) . (the_result_sort_of o1) = ( the carrier of S -indexing f) . (the_result_sort_of o2) ) )

proof end;

theorem Th30: :: ALGSPEC1:30

for S being non empty non void ManySortedSign

for f, g being Function holds

( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S )

for f, g being Function holds

( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_a_replacement_in S )

proof end;

theorem Th31: :: ALGSPEC1:31

for S, S9 being non void Signature

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

f,g form_a_replacement_in S

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

f,g form_a_replacement_in S

proof end;

theorem :: ALGSPEC1:32

theorem Th33: :: ALGSPEC1:33

for S being non void Signature

for f, g being Function st g is one-to-one & the carrier' of S /\ (rng g) c= dom g holds

f,g form_a_replacement_in S

for f, g being Function st g is one-to-one & the carrier' of S /\ (rng g) c= dom g holds

f,g form_a_replacement_in S

proof end;

theorem :: ALGSPEC1:34

for S being non void Signature

for f, g being Function st g is one-to-one & rng g misses the carrier' of S holds

f,g form_a_replacement_in S

for f, g being Function st g is one-to-one & rng g misses the carrier' of S holds

f,g form_a_replacement_in S

proof end;

registration

let X be set ;

let Y be non empty set ;

let a be Function of Y,(X *);

let r be Function of Y,X;

coherence

not ManySortedSign(# X,Y,a,r #) is void ;

end;
let Y be non empty set ;

let a be Function of Y,(X *);

let r be Function of Y,X;

coherence

not ManySortedSign(# X,Y,a,r #) is void ;

definition

let S be non empty non void ManySortedSign ;

let f, g be Function;

assume A1: f,g form_a_replacement_in S ;

for b_{1}, b_{2} being non empty non void strict ManySortedSign st the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b_{1} & the carrier of b_{1} = rng ( the carrier of S -indexing f) & the carrier' of b_{1} = rng ( the carrier' of S -indexing g) & the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b_{2} & the carrier of b_{2} = rng ( the carrier of S -indexing f) & the carrier' of b_{2} = rng ( the carrier' of S -indexing g) holds

b_{1} = b_{2}

ex b_{1} being non empty non void strict ManySortedSign st

( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b_{1} & the carrier of b_{1} = rng ( the carrier of S -indexing f) & the carrier' of b_{1} = rng ( the carrier' of S -indexing g) )

end;
let f, g be Function;

assume A1: f,g form_a_replacement_in S ;

func S with-replacement (f,g) -> non empty non void strict ManySortedSign means :Def4: :: ALGSPEC1:def 4

( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,it & the carrier of it = rng ( the carrier of S -indexing f) & the carrier' of it = rng ( the carrier' of S -indexing g) );

uniqueness ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,it & the carrier of it = rng ( the carrier of S -indexing f) & the carrier' of it = rng ( the carrier' of S -indexing g) );

for b

b

proof end;

existence ex b

( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b

proof end;

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

for S being non empty non void ManySortedSign

for f, g being Function st f,g form_a_replacement_in S holds

for b_{4} being non empty non void strict ManySortedSign holds

( b_{4} = S with-replacement (f,g) iff ( the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,b_{4} & the carrier of b_{4} = rng ( the carrier of S -indexing f) & the carrier' of b_{4} = rng ( the carrier' of S -indexing g) ) );

for S being non empty non void ManySortedSign

for f, g being Function st f,g form_a_replacement_in S holds

for b

( b

theorem Th35: :: ALGSPEC1:35

for S1, S2 being non void Signature

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

(f *) * the Arity of S1 = the Arity of S2 * 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

(f *) * the Arity of S1 = the Arity of S2 * g

proof end;

theorem Th36: :: ALGSPEC1:36

for S being non void Signature

for f, g being Function st f,g form_a_replacement_in S holds

the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g))

for f, g being Function st f,g form_a_replacement_in S holds

the carrier of S -indexing f is Function of the carrier of S, the carrier of (S with-replacement (f,g))

proof end;

theorem Th37: :: ALGSPEC1:37

for S being non void Signature

for f, g being Function st f,g form_a_replacement_in S holds

for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds

for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9

for f, g being Function st f,g form_a_replacement_in S holds

for f9 being Function of the carrier of S, the carrier of (S with-replacement (f,g)) st f9 = the carrier of S -indexing f holds

for g9 being rng-retract of the carrier' of S -indexing g holds the Arity of (S with-replacement (f,g)) = ((f9 *) * the Arity of S) * g9

proof end;

theorem Th38: :: ALGSPEC1:38

for S being non void Signature

for f, g being Function st f,g form_a_replacement_in S holds

for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement (f,g)) = (( the carrier of S -indexing f) * the ResultSort of S) * g9

for f, g being Function st f,g form_a_replacement_in S holds

for g9 being rng-retract of the carrier' of S -indexing g holds the ResultSort of (S with-replacement (f,g)) = (( the carrier of S -indexing f) * the ResultSort of S) * g9

proof end;

theorem Th39: :: ALGSPEC1:39

for S, S9 being non void Signature

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

S with-replacement (f,g) is Subsignature of S9

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

S with-replacement (f,g) is Subsignature of S9

proof end;

theorem Th40: :: ALGSPEC1:40

for S being non void Signature

for f, g being Function holds

( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) ) by Th30, Th31, Def4;

for f, g being Function holds

( f,g form_a_replacement_in S iff the carrier of S -indexing f, the carrier' of S -indexing g form_morphism_between S,S with-replacement (f,g) ) by Th30, Th31, Def4;

theorem Th41: :: ALGSPEC1:41

for S being non void Signature

for f, g being Function st dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S holds

(id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g)

for f, g being Function st dom f c= the carrier of S & dom g c= the carrier' of S & f,g form_a_replacement_in S holds

(id the carrier of S) +* f,(id the carrier' of S) +* g form_morphism_between S,S with-replacement (f,g)

proof end;

theorem :: ALGSPEC1:42

for S being non void Signature

for f, g being Function st dom f = the carrier of S & dom g = the carrier' of S & f,g form_a_replacement_in S holds

f,g form_morphism_between S,S with-replacement (f,g)

for f, g being Function st dom f = the carrier of S & dom g = the carrier' of S & f,g form_a_replacement_in S holds

f,g form_morphism_between S,S with-replacement (f,g)

proof end;

theorem Th43: :: ALGSPEC1:43

for S being non void Signature

for f, g being Function st f,g form_a_replacement_in S holds

S with-replacement (( the carrier of S -indexing f),g) = S with-replacement (f,g)

for f, g being Function st f,g form_a_replacement_in S holds

S with-replacement (( the carrier of S -indexing f),g) = S with-replacement (f,g)

proof end;

theorem Th44: :: ALGSPEC1:44

for S being non void Signature

for f, g being Function st f,g form_a_replacement_in S holds

S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g)

for f, g being Function st f,g form_a_replacement_in S holds

S with-replacement (f,( the carrier' of S -indexing g)) = S with-replacement (f,g)

proof end;

definition
end;

:: deftheorem Def5 defines Extension ALGSPEC1:def 5 :

for S, b_{2} being Signature holds

( b_{2} is Extension of S iff S is Subsignature of b_{2} );

for S, b

( b

theorem Th46: :: ALGSPEC1:46

for S1 being Signature

for S2 being Extension of S1

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

for S2 being Extension of S1

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

proof end;

theorem Th49: :: ALGSPEC1:49

for S1, S2, S being non empty ManySortedSign

for f1, g1, f2, g2 being Function st f1 tolerates f2 & f1,g1 form_morphism_between S1,S & f2,g2 form_morphism_between S2,S holds

f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,S

for f1, g1, f2, g2 being Function st f1 tolerates f2 & f1,g1 form_morphism_between S1,S & f2,g2 form_morphism_between S2,S holds

f1 +* f2,g1 +* g2 form_morphism_between S1 +* S2,S

proof end;

theorem :: ALGSPEC1:50

for S1, S2, E being non empty Signature holds

( E is Extension of S1 & E is Extension of S2 iff ( S1 tolerates S2 & E is Extension of S1 +* S2 ) )

( E is Extension of S1 & E is Extension of S2 iff ( S1 tolerates S2 & E is Extension of S1 +* S2 ) )

proof end;

registration

let S be non empty Signature;

coherence

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

end;
coherence

for b

proof end;

registration

let S be non void Signature;

coherence

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

end;
coherence

for b

proof end;

registration

let S be Signature;

existence

ex b_{1} being Extension of S st

( not b_{1} is empty & not b_{1} is void & b_{1} is strict )

end;
existence

ex b

( not b

proof end;

theorem Th52: :: ALGSPEC1:52

for f, g being Function

for S being non void Signature

for E being Extension of S st f,g form_a_replacement_in E holds

f,g form_a_replacement_in S

for S being non void Signature

for E being Extension of S st f,g form_a_replacement_in E holds

f,g form_a_replacement_in S

proof end;

theorem :: ALGSPEC1:53

for f, g being Function

for S being non void Signature

for E being Extension of S st f,g form_a_replacement_in E holds

E with-replacement (f,g) is Extension of S with-replacement (f,g)

for S being non void Signature

for E being Extension of S st f,g form_a_replacement_in E holds

E with-replacement (f,g) is Extension of S with-replacement (f,g)

proof end;

theorem :: ALGSPEC1:54

for S1, S2 being non void Signature st S1 tolerates S2 holds

for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds

(S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g))

for f, g being Function st f,g form_a_replacement_in S1 +* S2 holds

(S1 +* S2) with-replacement (f,g) = (S1 with-replacement (f,g)) +* (S2 with-replacement (f,g))

proof end;

definition

ex b_{1} being object ex S being non void Signature st b_{1} is feasible MSAlgebra over S
end;

mode Algebra -> object means :Def6: :: ALGSPEC1:def 6

ex S being non void Signature st it is feasible MSAlgebra over S;

existence ex S being non void Signature st it is feasible MSAlgebra over S;

ex b

proof end;

:: deftheorem Def6 defines Algebra ALGSPEC1:def 6 :

for b_{1} being object holds

( b_{1} is Algebra iff ex S being non void Signature st b_{1} is feasible MSAlgebra over S );

for b

( b

definition

let S be Signature;

ex b_{1} being Algebra ex E being non void Extension of S st b_{1} is feasible MSAlgebra over E

end;
mode Algebra of S -> Algebra means :Def7: :: ALGSPEC1:def 7

ex E being non void Extension of S st it is feasible MSAlgebra over E;

existence ex E being non void Extension of S st it is feasible MSAlgebra over E;

ex b

proof end;

:: deftheorem Def7 defines Algebra ALGSPEC1:def 7 :

for S being Signature

for b_{2} being Algebra holds

( b_{2} is Algebra of S iff ex E being non void Extension of S st b_{2} is feasible MSAlgebra over E );

for S being Signature

for b

( b

theorem Th57: :: ALGSPEC1:57

for S being Signature

for E being non empty Signature

for A being MSAlgebra over E st A is Algebra of S holds

( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )

for E being non empty Signature

for A being MSAlgebra over E st A is Algebra of S holds

( the carrier of S c= the carrier of E & the carrier' of S c= the carrier' of E )

proof end;

theorem Th58: :: ALGSPEC1:58

for S being non void Signature

for E being non empty Signature

for A being MSAlgebra over E st A is Algebra of S holds

for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))

for E being non empty Signature

for A being MSAlgebra over E st A is Algebra of S holds

for o being OperSymbol of S holds the Charact of A . o is Function of (( the Sorts of A #) . (the_arity_of o)),( the Sorts of A . (the_result_sort_of o))

proof end;

theorem :: ALGSPEC1:59

for S being non empty Signature

for A being Algebra of S

for E being non empty ManySortedSign st A is MSAlgebra over E holds

A is MSAlgebra over E +* S

for A being Algebra of S

for E being non empty ManySortedSign st A is MSAlgebra over E holds

A is MSAlgebra over E +* S

proof end;

theorem Th60: :: ALGSPEC1:60

for S1, S2 being non empty Signature

for A being MSAlgebra over S1 st A is MSAlgebra over S2 holds

( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )

for A being MSAlgebra over S1 st A is MSAlgebra over S2 holds

( the carrier of S1 = the carrier of S2 & the carrier' of S1 = the carrier' of S2 )

proof end;

registration

let S be non void Signature;

let A be non-empty disjoint_valued MSAlgebra over S;

coherence

the Sorts of A is one-to-one

end;
let A be non-empty disjoint_valued MSAlgebra over S;

coherence

the Sorts of A is one-to-one

proof end;

theorem Th61: :: ALGSPEC1:61

for S being non void Signature

for A being disjoint_valued MSAlgebra over S

for C1, C2 being Component of the Sorts of A holds

( C1 = C2 or C1 misses C2 )

for A being disjoint_valued MSAlgebra over S

for C1, C2 being Component of the Sorts of A holds

( C1 = C2 or C1 misses C2 )

proof end;

theorem Th62: :: ALGSPEC1:62

for S, S9 being non void Signature

for A being non-empty disjoint_valued MSAlgebra over S st A is MSAlgebra over S9 holds

ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of S9, the carrier' of S9, the Arity of S9, the ResultSort of S9 #)

for A being non-empty disjoint_valued MSAlgebra over S st A is MSAlgebra over S9 holds

ManySortedSign(# the carrier of S, the carrier' of S, the Arity of S, the ResultSort of S #) = ManySortedSign(# the carrier of S9, the carrier' of S9, the Arity of S9, the ResultSort of S9 #)

proof end;

theorem :: ALGSPEC1:63

for S, S9 being non void Signature

for A being non-empty disjoint_valued MSAlgebra over S st A is Algebra of S9 holds

S is Extension of S9

for A being non-empty disjoint_valued MSAlgebra over S st A is Algebra of S9 holds

S is Extension of S9

proof end;