begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem defines -indexing ALGSPEC1:def 1 :
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
canceled;
theorem
theorem
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
theorem
:: deftheorem Def2 defines rng-retract ALGSPEC1:def 2 :
theorem Th24:
theorem Th25:
theorem
theorem
theorem Th28:
theorem
begin
:: deftheorem Def3 defines form_a_replacement_in ALGSPEC1:def 3 :
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem Th34:
theorem
definition
let S be non
empty non
void ManySortedSign ;
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:
( 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
for b1, b2 being non empty non void strict ManySortedSign st the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,b1 & the carrier of b1 = rng (the carrier of S -indexing f) & the carrier' of b1 = rng (the carrier' of S -indexing g) & the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,b2 & the carrier of b2 = rng (the carrier of S -indexing f) & the carrier' of b2 = rng (the carrier' of S -indexing g) holds
b1 = b2
existence
ex b1 being non empty non void strict ManySortedSign st
( the carrier of S -indexing f,the carrier' of S -indexing g form_morphism_between S,b1 & the carrier of b1 = rng (the carrier of S -indexing f) & the carrier' of b1 = rng (the carrier' of S -indexing g) )
end;
:: deftheorem Def4 defines with-replacement ALGSPEC1:def 4 :
theorem Th36:
theorem Th37:
theorem Th38:
theorem Th39:
theorem Th40:
theorem Th41:
theorem Th42:
theorem
theorem Th44:
theorem Th45:
begin
:: deftheorem Def5 defines Extension ALGSPEC1:def 5 :
theorem
canceled;
theorem Th47:
theorem Th48:
theorem Th49:
theorem Th50:
theorem Th51:
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
theorem
theorem Th53:
theorem Th54:
theorem
theorem
begin
:: deftheorem Def6 defines Algebra ALGSPEC1:def 6 :
:: deftheorem Def7 defines Algebra ALGSPEC1:def 7 :
theorem
theorem
theorem Th59:
theorem Th60:
theorem
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem