:: ALGSPEC1 semantic presentation

theorem Th1: :: ALGSPEC1:1
for b1, b2, b3 being Function st (dom b1) /\ (dom b2) c= dom b3 holds
(b1 +* b2) +* b3 = (b2 +* b1) +* b3
proof end;

theorem Th2: :: ALGSPEC1:2
for b1, b2, b3 being Function st b1 c= b2 & (rng b3) /\ (dom b2) c= dom b1 holds
b2 * b3 = b1 * b3
proof end;

theorem Th3: :: ALGSPEC1:3
for b1, b2, b3 being Function st dom b1 c= rng b2 & dom b1 misses rng b3 & b2 .: (dom b3) misses dom b1 holds
b1 * (b2 +* b3) = b1 * b2
proof end;

theorem Th4: :: ALGSPEC1:4
for b1, b2, b3, b4 being Function st b1 tolerates b2 & b3 tolerates b4 holds
b1 * b3 tolerates b2 * b4
proof end;

theorem Th5: :: ALGSPEC1:5
for b1, b2, b3, b4 being non empty set
for b5 being Function of b1,b3
for b6 being Function of b2,b4 st b5 c= b6 holds
b5 * c= b6 *
proof end;

theorem Th6: :: ALGSPEC1:6
for b1, b2, b3, b4 being non empty set
for b5 being Function of b1,b3
for b6 being Function of b2,b4 st b5 tolerates b6 holds
b5 * tolerates b6 *
proof end;

definition
let c1 be set ;
let c2 be Function;
func c1 -indexing c2 -> ManySortedSet of a1 equals :: ALGSPEC1:def 1
(id a1) +* (a2 | a1);
coherence
(id c1) +* (c2 | c1) is ManySortedSet of c1
proof end;
end;

:: deftheorem Def1 defines -indexing ALGSPEC1:def 1 :
for b1 being set
for b2 being Function holds b1 -indexing b2 = (id b1) +* (b2 | b1);

theorem Th7: :: ALGSPEC1:7
for b1 being set
for b2 being Function holds rng (b1 -indexing b2) = (b1 \ (dom b2)) \/ (b2 .: b1)
proof end;

theorem Th8: :: ALGSPEC1:8
for b1 being non empty set
for b2 being Function
for b3 being Element of b1 holds (b1 -indexing b2) . b3 = ((id b1) +* b2) . b3
proof end;

theorem Th9: :: ALGSPEC1:9
for b1, b2 being set
for b3 being Function st b2 in b1 holds
( ( b2 in dom b3 implies (b1 -indexing b3) . b2 = b3 . b2 ) & ( not b2 in dom b3 implies (b1 -indexing b3) . b2 = b2 ) )
proof end;

theorem Th10: :: ALGSPEC1:10
for b1 being set
for b2 being Function st dom b2 = b1 holds
b1 -indexing b2 = b2
proof end;

theorem Th11: :: ALGSPEC1:11
for b1 being set
for b2 being Function holds b1 -indexing (b1 -indexing b2) = b1 -indexing b2
proof end;

theorem Th12: :: ALGSPEC1:12
for b1 being set
for b2 being Function holds b1 -indexing ((id b1) +* b2) = b1 -indexing b2
proof end;

theorem Th13: :: ALGSPEC1:13
for b1 being set
for b2 being Function st b2 c= id b1 holds
b1 -indexing b2 = id b1
proof end;

theorem Th14: :: ALGSPEC1:14
for b1 being set holds b1 -indexing {} = id b1
proof end;

theorem Th15: :: ALGSPEC1:15
for b1 being set
for b2 being Function holds b1 -indexing (b2 | b1) = b1 -indexing b2 by RELAT_1:101;

theorem Th16: :: ALGSPEC1:16
for b1 being set
for b2 being Function st b1 c= dom b2 holds
b1 -indexing b2 = b2 | b1
proof end;

theorem Th17: :: ALGSPEC1:17
for b1 being Function holds {} -indexing b1 = {}
proof end;

theorem Th18: :: ALGSPEC1:18
for b1, b2 being set
for b3 being Function st b1 c= b2 holds
(b2 -indexing b3) | b1 = b1 -indexing b3
proof end;

theorem Th19: :: ALGSPEC1:19
for b1, b2 being set
for b3 being Function holds (b1 \/ b2) -indexing b3 = (b1 -indexing b3) +* (b2 -indexing b3)
proof end;

theorem Th20: :: ALGSPEC1:20
for b1, b2 being set
for b3 being Function holds b1 -indexing b3 tolerates b2 -indexing b3
proof end;

theorem Th21: :: ALGSPEC1:21
for b1, b2 being set
for b3 being Function holds (b1 \/ b2) -indexing b3 = (b1 -indexing b3) \/ (b2 -indexing b3)
proof end;

theorem Th22: :: ALGSPEC1:22
for b1 being non empty set
for b2, b3 being Function st rng b3 c= b1 holds
(b1 -indexing b2) * b3 = ((id b1) +* b2) * b3
proof end;

theorem Th23: :: ALGSPEC1:23
for b1, b2 being Function st dom b1 misses dom b2 & rng b2 misses dom b1 holds
for b3 being set holds b1 * (b3 -indexing b2) = b1 | b3
proof end;

definition
let c1 be Function;
mode rng-retract of c1 -> Function means :Def2: :: ALGSPEC1:def 2
( dom a2 = rng a1 & a1 * a2 = id (rng a1) );
existence
ex b1 being Function st
( dom b1 = rng c1 & c1 * b1 = id (rng c1) )
proof end;
end;

:: deftheorem Def2 defines rng-retract ALGSPEC1:def 2 :
for b1, b2 being Function holds
( b2 is rng-retract of b1 iff ( dom b2 = rng b1 & b1 * b2 = id (rng b1) ) );

theorem Th24: :: ALGSPEC1:24
for b1 being Function
for b2 being rng-retract of b1 holds rng b2 c= dom b1
proof end;

theorem Th25: :: ALGSPEC1:25
for b1 being Function
for b2 being rng-retract of b1
for b3 being set st b3 in rng b1 holds
( b2 . b3 in dom b1 & b1 . (b2 . b3) = b3 )
proof end;

theorem Th26: :: ALGSPEC1:26
for b1 being Function st b1 is one-to-one holds
b1 " is rng-retract of b1
proof end;

theorem Th27: :: ALGSPEC1:27
for b1 being Function st b1 is one-to-one holds
for b2 being rng-retract of b1 holds b2 = b1 "
proof end;

theorem Th28: :: ALGSPEC1:28
for b1, b2 being Function st b1 tolerates b2 holds
for b3 being rng-retract of b1
for b4 being rng-retract of b2 holds b3 +* b4 is rng-retract of b1 +* b2
proof end;

theorem Th29: :: ALGSPEC1:29
for b1, b2 being Function st b1 c= b2 holds
for b3 being rng-retract of b1 ex b4 being rng-retract of b2 st b3 c= b4
proof end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be Function;
pred c2,c3 form_a_replacement_in c1 means :Def3: :: ALGSPEC1:def 3
for b1, b2 being OperSymbol of a1 st ((id the OperSymbols of a1) +* a3) . b1 = ((id the OperSymbols of a1) +* a3) . b2 holds
( ((id the carrier of a1) +* a2) * (the_arity_of b1) = ((id the carrier of a1) +* a2) * (the_arity_of b2) & ((id the carrier of a1) +* a2) . (the_result_sort_of b1) = ((id the carrier of a1) +* a2) . (the_result_sort_of b2) );
end;

:: deftheorem Def3 defines form_a_replacement_in ALGSPEC1:def 3 :
for b1 being non empty non void ManySortedSign
for b2, b3 being Function holds
( b2,b3 form_a_replacement_in b1 iff for b4, b5 being OperSymbol of b1 st ((id the OperSymbols of b1) +* b3) . b4 = ((id the OperSymbols of b1) +* b3) . b5 holds
( ((id the carrier of b1) +* b2) * (the_arity_of b4) = ((id the carrier of b1) +* b2) * (the_arity_of b5) & ((id the carrier of b1) +* b2) . (the_result_sort_of b4) = ((id the carrier of b1) +* b2) . (the_result_sort_of b5) ) );

theorem Th30: :: ALGSPEC1:30
for b1 being non empty non void ManySortedSign
for b2, b3 being Function holds
( b2,b3 form_a_replacement_in b1 iff for b4, b5 being OperSymbol of b1 st (the OperSymbols of b1 -indexing b3) . b4 = (the OperSymbols of b1 -indexing b3) . b5 holds
( (the carrier of b1 -indexing b2) * (the_arity_of b4) = (the carrier of b1 -indexing b2) * (the_arity_of b5) & (the carrier of b1 -indexing b2) . (the_result_sort_of b4) = (the carrier of b1 -indexing b2) . (the_result_sort_of b5) ) )
proof end;

theorem Th31: :: ALGSPEC1:31
for b1 being non empty non void ManySortedSign
for b2, b3 being Function holds
( b2,b3 form_a_replacement_in b1 iff the carrier of b1 -indexing b2,the OperSymbols of b1 -indexing b3 form_a_replacement_in b1 )
proof end;

theorem Th32: :: ALGSPEC1:32
for b1, b2 being non void Signature
for b3, b4 being Function st b3,b4 form_morphism_between b1,b2 holds
b3,b4 form_a_replacement_in b1
proof end;

theorem Th33: :: ALGSPEC1:33
for b1 being non void Signature
for b2 being Function holds b2, {} form_a_replacement_in b1
proof end;

theorem Th34: :: ALGSPEC1:34
for b1 being non void Signature
for b2, b3 being Function st b2 is one-to-one & the OperSymbols of b1 /\ (rng b2) c= dom b2 holds
b3,b2 form_a_replacement_in b1
proof end;

theorem Th35: :: ALGSPEC1:35
for b1 being non void Signature
for b2, b3 being Function st b2 is one-to-one & rng b2 misses the OperSymbols of b1 holds
b3,b2 form_a_replacement_in b1
proof end;

registration
let c1 be set ;
let c2 be non empty set ;
let c3 be Function of c2,c1 * ;
let c4 be Function of c2,c1;
cluster ManySortedSign(# a1,a2,a3,a4 #) -> non void ;
coherence
not ManySortedSign(# c1,c2,c3,c4 #) is void
by MSUALG_1:def 5;
end;

definition
let c1 be non empty non void ManySortedSign ;
let c2, c3 be Function;
assume E30: c2,c3 form_a_replacement_in c1 ;
func c1 with-replacement c2,c3 -> non empty strict non void ManySortedSign means :Def4: :: ALGSPEC1:def 4
( the carrier of a1 -indexing a2,the OperSymbols of a1 -indexing a3 form_morphism_between a1,a4 & the carrier of a4 = rng (the carrier of a1 -indexing a2) & the OperSymbols of a4 = rng (the OperSymbols of a1 -indexing a3) );
uniqueness
for b1, b2 being non empty strict non void ManySortedSign st the carrier of c1 -indexing c2,the OperSymbols of c1 -indexing c3 form_morphism_between c1,b1 & the carrier of b1 = rng (the carrier of c1 -indexing c2) & the OperSymbols of b1 = rng (the OperSymbols of c1 -indexing c3) & the carrier of c1 -indexing c2,the OperSymbols of c1 -indexing c3 form_morphism_between c1,b2 & the carrier of b2 = rng (the carrier of c1 -indexing c2) & the OperSymbols of b2 = rng (the OperSymbols of c1 -indexing c3) holds
b1 = b2
proof end;
existence
ex b1 being non empty strict non void ManySortedSign st
( the carrier of c1 -indexing c2,the OperSymbols of c1 -indexing c3 form_morphism_between c1,b1 & the carrier of b1 = rng (the carrier of c1 -indexing c2) & the OperSymbols of b1 = rng (the OperSymbols of c1 -indexing c3) )
proof end;
end;

:: deftheorem Def4 defines with-replacement ALGSPEC1:def 4 :
for b1 being non empty non void ManySortedSign
for b2, b3 being Function st b2,b3 form_a_replacement_in b1 holds
for b4 being non empty strict non void ManySortedSign holds
( b4 = b1 with-replacement b2,b3 iff ( the carrier of b1 -indexing b2,the OperSymbols of b1 -indexing b3 form_morphism_between b1,b4 & the carrier of b4 = rng (the carrier of b1 -indexing b2) & the OperSymbols of b4 = rng (the OperSymbols of b1 -indexing b3) ) );

theorem Th36: :: ALGSPEC1:36
for b1, b2 being non void Signature
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
(b3 * ) * the Arity of b1 = the Arity of b2 * b4
proof end;

theorem Th37: :: ALGSPEC1:37
for b1 being non void Signature
for b2, b3 being Function st b2,b3 form_a_replacement_in b1 holds
the carrier of b1 -indexing b2 is Function of the carrier of b1,the carrier of (b1 with-replacement b2,b3)
proof end;

theorem Th38: :: ALGSPEC1:38
for b1 being non void Signature
for b2, b3 being Function st b2,b3 form_a_replacement_in b1 holds
for b4 being Function of the carrier of b1,the carrier of (b1 with-replacement b2,b3) st b4 = the carrier of b1 -indexing b2 holds
for b5 being rng-retract of the OperSymbols of b1 -indexing b3 holds the Arity of (b1 with-replacement b2,b3) = ((b4 * ) * the Arity of b1) * b5
proof end;

theorem Th39: :: ALGSPEC1:39
for b1 being non void Signature
for b2, b3 being Function st b2,b3 form_a_replacement_in b1 holds
for b4 being rng-retract of the OperSymbols of b1 -indexing b3 holds the ResultSort of (b1 with-replacement b2,b3) = ((the carrier of b1 -indexing b2) * the ResultSort of b1) * b4
proof end;

theorem Th40: :: ALGSPEC1:40
for b1, b2 being non void Signature
for b3, b4 being Function st b3,b4 form_morphism_between b1,b2 holds
b1 with-replacement b3,b4 is Subsignature of b2
proof end;

theorem Th41: :: ALGSPEC1:41
for b1 being non void Signature
for b2, b3 being Function holds
( b2,b3 form_a_replacement_in b1 iff the carrier of b1 -indexing b2,the OperSymbols of b1 -indexing b3 form_morphism_between b1,b1 with-replacement b2,b3 )
proof end;

theorem Th42: :: ALGSPEC1:42
for b1 being non void Signature
for b2, b3 being Function st dom b2 c= the carrier of b1 & dom b3 c= the OperSymbols of b1 & b2,b3 form_a_replacement_in b1 holds
(id the carrier of b1) +* b2,(id the OperSymbols of b1) +* b3 form_morphism_between b1,b1 with-replacement b2,b3
proof end;

theorem Th43: :: ALGSPEC1:43
for b1 being non void Signature
for b2, b3 being Function st dom b2 = the carrier of b1 & dom b3 = the OperSymbols of b1 & b2,b3 form_a_replacement_in b1 holds
b2,b3 form_morphism_between b1,b1 with-replacement b2,b3
proof end;

theorem Th44: :: ALGSPEC1:44
for b1 being non void Signature
for b2, b3 being Function st b2,b3 form_a_replacement_in b1 holds
b1 with-replacement (the carrier of b1 -indexing b2),b3 = b1 with-replacement b2,b3
proof end;

theorem Th45: :: ALGSPEC1:45
for b1 being non void Signature
for b2, b3 being Function st b2,b3 form_a_replacement_in b1 holds
b1 with-replacement b2,(the OperSymbols of b1 -indexing b3) = b1 with-replacement b2,b3
proof end;

definition
let c1 be Signature;
mode Extension of c1 -> Signature means :Def5: :: ALGSPEC1:def 5
a1 is Subsignature of a2;
existence
ex b1 being Signature st c1 is Subsignature of b1
proof end;
end;

:: deftheorem Def5 defines Extension ALGSPEC1:def 5 :
for b1, b2 being Signature holds
( b2 is Extension of b1 iff b1 is Subsignature of b2 );

theorem Th46: :: ALGSPEC1:46
canceled;

theorem Th47: :: ALGSPEC1:47
for b1 being Signature holds b1 is Extension of b1
proof end;

theorem Th48: :: ALGSPEC1:48
for b1 being Signature
for b2 being Extension of b1
for b3 being Extension of b2 holds b3 is Extension of b1
proof end;

theorem Th49: :: ALGSPEC1:49
for b1, b2 being non empty Signature st b1 tolerates b2 holds
b1 +* b2 is Extension of b1
proof end;

theorem Th50: :: ALGSPEC1:50
for b1, b2 being non empty Signature holds b1 +* b2 is Extension of b2
proof end;

theorem Th51: :: ALGSPEC1:51
for b1, b2, b3 being non empty ManySortedSign
for b4, b5, b6, b7 being Function st b4 tolerates b6 & b4,b5 form_morphism_between b1,b3 & b6,b7 form_morphism_between b2,b3 holds
b4 +* b6,b5 +* b7 form_morphism_between b1 +* b2,b3
proof end;

theorem Th52: :: ALGSPEC1:52
for b1, b2, b3 being non empty Signature holds
( b3 is Extension of b1 & b3 is Extension of b2 iff ( b1 tolerates b2 & b3 is Extension of b1 +* b2 ) )
proof end;

registration
let c1 be non empty Signature;
cluster -> non empty Extension of a1;
coherence
for b1 being Extension of c1 holds not b1 is empty
proof end;
end;

registration
let c1 be non void Signature;
cluster -> non empty non void Extension of a1;
coherence
for b1 being Extension of c1 holds not b1 is void
proof end;
end;

theorem Th53: :: ALGSPEC1:53
for b1, b2 being Signature st b1 is empty holds
b2 is Extension of b1
proof end;

registration
let c1 be Signature;
cluster non empty strict non void Extension of a1;
existence
ex b1 being Extension of c1 st
( not b1 is empty & not b1 is void & b1 is strict )
proof end;
end;

theorem Th54: :: ALGSPEC1:54
for b1, b2 being Function
for b3 being non void Signature
for b4 being Extension of b3 st b1,b2 form_a_replacement_in b4 holds
b1,b2 form_a_replacement_in b3
proof end;

theorem Th55: :: ALGSPEC1:55
for b1, b2 being Function
for b3 being non void Signature
for b4 being Extension of b3 st b1,b2 form_a_replacement_in b4 holds
b4 with-replacement b1,b2 is Extension of b3 with-replacement b1,b2
proof end;

theorem Th56: :: ALGSPEC1:56
for b1, b2 being non void Signature st b1 tolerates b2 holds
for b3, b4 being Function st b3,b4 form_a_replacement_in b1 +* b2 holds
(b1 +* b2) with-replacement b3,b4 = (b1 with-replacement b3,b4) +* (b2 with-replacement b3,b4)
proof end;

definition
mode Algebra -> set means :Def6: :: ALGSPEC1:def 6
ex b1 being non void Signature st a1 is feasible MSAlgebra of b1;
existence
ex b1 being set ex b2 being non void Signature st b1 is feasible MSAlgebra of b2
proof end;
end;

:: deftheorem Def6 defines Algebra ALGSPEC1:def 6 :
for b1 being set holds
( b1 is Algebra iff ex b2 being non void Signature st b1 is feasible MSAlgebra of b2 );

definition
let c1 be Signature;
mode Algebra of c1 -> Algebra means :Def7: :: ALGSPEC1:def 7
ex b1 being non void Extension of a1 st a2 is feasible MSAlgebra of b1;
existence
ex b1 being Algebra ex b2 being non void Extension of c1 st b1 is feasible MSAlgebra of b2
proof end;
end;

:: deftheorem Def7 defines Algebra ALGSPEC1:def 7 :
for b1 being Signature
for b2 being Algebra holds
( b2 is Algebra of b1 iff ex b3 being non void Extension of b1 st b2 is feasible MSAlgebra of b3 );

theorem Th57: :: ALGSPEC1:57
for b1 being non void Signature
for b2 being feasible MSAlgebra of b1 holds b2 is Algebra of b1
proof end;

theorem Th58: :: ALGSPEC1:58
for b1 being Signature
for b2 being Extension of b1
for b3 being Algebra of b2 holds b3 is Algebra of b1
proof end;

theorem Th59: :: ALGSPEC1:59
for b1 being Signature
for b2 being non empty Signature
for b3 being MSAlgebra of b2 st b3 is Algebra of b1 holds
( the carrier of b1 c= the carrier of b2 & the OperSymbols of b1 c= the OperSymbols of b2 )
proof end;

theorem Th60: :: ALGSPEC1:60
for b1 being non void Signature
for b2 being non empty Signature
for b3 being MSAlgebra of b2 st b3 is Algebra of b1 holds
for b4 being OperSymbol of b1 holds the Charact of b3 . b4 is Function of (the Sorts of b3 # ) . (the_arity_of b4),the Sorts of b3 . (the_result_sort_of b4)
proof end;

theorem Th61: :: ALGSPEC1:61
for b1 being non empty Signature
for b2 being Algebra of b1
for b3 being non empty ManySortedSign st b2 is MSAlgebra of b3 holds
b2 is MSAlgebra of b3 +* b1
proof end;

theorem Th62: :: ALGSPEC1:62
for b1, b2 being non empty Signature
for b3 being MSAlgebra of b1 st b3 is MSAlgebra of b2 holds
( the carrier of b1 = the carrier of b2 & the OperSymbols of b1 = the OperSymbols of b2 )
proof end;

theorem Th63: :: ALGSPEC1:63
for b1 being non void Signature
for b2 being non-empty disjoint_valued MSAlgebra of b1 holds the Sorts of b2 is one-to-one
proof end;

theorem Th64: :: ALGSPEC1:64
for b1 being non void Signature
for b2 being disjoint_valued MSAlgebra of b1
for b3, b4 being Component of the Sorts of b2 holds
( b3 = b4 or b3 misses b4 )
proof end;

theorem Th65: :: ALGSPEC1:65
for b1, b2 being non void Signature
for b3 being non-empty disjoint_valued MSAlgebra of b1 st b3 is MSAlgebra of b2 holds
ManySortedSign(# the carrier of b1,the OperSymbols of b1,the Arity of b1,the ResultSort of b1 #) = ManySortedSign(# the carrier of b2,the OperSymbols of b2,the Arity of b2,the ResultSort of b2 #)
proof end;

theorem Th66: :: ALGSPEC1:66
for b1, b2 being non void Signature
for b3 being non-empty disjoint_valued MSAlgebra of b1 st b3 is Algebra of b2 holds
b1 is Extension of b2
proof end;