:: OSALG_3 semantic presentation

definition
let c1 be non empty Poset;
let c2 be ManySortedFunction of the carrier of c1;
attr a2 is order-sorted means :Def1: :: OSALG_3:def 1
for b1, b2 being Element of a1 st b1 <= b2 holds
for b3 being set st b3 in dom (a2 . b1) holds
( b3 in dom (a2 . b2) & (a2 . b1) . b3 = (a2 . b2) . b3 );
end;

:: deftheorem Def1 defines order-sorted OSALG_3:def 1 :
for b1 being non empty Poset
for b2 being ManySortedFunction of the carrier of b1 holds
( b2 is order-sorted iff for b3, b4 being Element of b1 st b3 <= b4 holds
for b5 being set st b5 in dom (b2 . b3) holds
( b5 in dom (b2 . b4) & (b2 . b3) . b5 = (b2 . b4) . b5 ) );

theorem Th1: :: OSALG_3:1
canceled;

theorem Th2: :: OSALG_3:2
for b1 being non empty Poset
for b2 being ManySortedFunction of the carrier of b1 st b2 is order-sorted holds
for b3, b4 being Element of b1 st b3 <= b4 holds
( dom (b2 . b3) c= dom (b2 . b4) & b2 . b3 c= b2 . b4 )
proof end;

theorem Th3: :: OSALG_3:3
for b1 being non empty Poset
for b2 being OrderSortedSet of b1
for b3 being V2 OrderSortedSet of b1
for b4 being ManySortedFunction of b2,b3 holds
( b4 is order-sorted iff for b5, b6 being Element of b1 st b5 <= b6 holds
for b7 being set st b7 in b2 . b5 holds
(b4 . b5) . b7 = (b4 . b6) . b7 )
proof end;

theorem Th4: :: OSALG_3:4
for b1 being non empty Poset
for b2 being ManySortedFunction of the carrier of b1 st b2 is order-sorted holds
for b3, b4 being Element of the carrier of b1 * st b3 <= b4 holds
(b2 # ) . b3 c= (b2 # ) . b4
proof end;

theorem Th5: :: OSALG_3:5
for b1 being non empty Poset
for b2 being OrderSortedSet of b1 holds id b2 is order-sorted
proof end;

registration
let c1 be non empty Poset;
let c2 be OrderSortedSet of c1;
cluster id a2 -> order-sorted ;
coherence
id c2 is order-sorted by Th5;
end;

theorem Th6: :: OSALG_3:6
for b1 being non empty Poset
for b2 being OrderSortedSet of b1
for b3, b4 being V2 OrderSortedSet of b1
for b5 being ManySortedFunction of b2,b3
for b6 being ManySortedFunction of b3,b4 st b5 is order-sorted & b6 is order-sorted holds
b6 ** b5 is order-sorted
proof end;

theorem Th7: :: OSALG_3:7
for b1 being non empty Poset
for b2, b3 being OrderSortedSet of b1
for b4 being ManySortedFunction of b2,b3 st b4 is "1-1" & b4 is "onto" & b4 is order-sorted holds
b4 "" is order-sorted
proof end;

theorem Th8: :: OSALG_3:8
for b1 being non empty Poset
for b2 being OrderSortedSet of b1
for b3 being ManySortedFunction of the carrier of b1 st b3 is order-sorted holds
b3 .:.: b2 is OrderSortedSet of b1
proof end;

definition
let c1 be OrderSortedSign;
let c2, c3 be OSAlgebra of c1;
pred c2,c3 are_os_isomorphic means :Def2: :: OSALG_3:def 2
ex b1 being ManySortedFunction of a2,a3 st
( b1 is_isomorphism a2,a3 & b1 is order-sorted );
end;

:: deftheorem Def2 defines are_os_isomorphic OSALG_3:def 2 :
for b1 being OrderSortedSign
for b2, b3 being OSAlgebra of b1 holds
( b2,b3 are_os_isomorphic iff ex b4 being ManySortedFunction of b2,b3 st
( b4 is_isomorphism b2,b3 & b4 is order-sorted ) );

theorem Th9: :: OSALG_3:9
for b1 being OrderSortedSign
for b2 being OSAlgebra of b1 holds b2,b2 are_os_isomorphic
proof end;

theorem Th10: :: OSALG_3:10
for b1 being OrderSortedSign
for b2, b3 being non-empty OSAlgebra of b1 st b2,b3 are_os_isomorphic holds
b3,b2 are_os_isomorphic
proof end;

definition
let c1 be OrderSortedSign;
let c2, c3 be OSAlgebra of c1;
redefine pred are_os_isomorphic as c2,c3 are_os_isomorphic ;
reflexivity
for b1 being OSAlgebra of c1 holds b1,b1 are_os_isomorphic by Th9;
end;

definition
let c1 be OrderSortedSign;
let c2, c3 be non-empty OSAlgebra of c1;
redefine pred are_os_isomorphic as c2,c3 are_os_isomorphic ;
symmetry
for b1, b2 being non-empty OSAlgebra of c1 st b1,b2 are_os_isomorphic holds
b2,b1 are_os_isomorphic by Th10;
end;

theorem Th11: :: OSALG_3:11
for b1 being OrderSortedSign
for b2, b3, b4 being non-empty OSAlgebra of b1 st b2,b3 are_os_isomorphic & b3,b4 are_os_isomorphic holds
b2,b4 are_os_isomorphic
proof end;

theorem Th12: :: OSALG_3:12
for b1 being OrderSortedSign
for b2, b3 being non-empty OSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is order-sorted & b4 is_homomorphism b2,b3 holds
Image b4 is order-sorted
proof end;

theorem Th13: :: OSALG_3:13
for b1 being OrderSortedSign
for b2, b3 being non-empty OSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is order-sorted holds
for b5, b6 being OperSymbol of b1 st b5 <= b6 holds
for b7 being Element of Args b5,b2
for b8 being Element of Args b6,b2 st b7 = b8 holds
b4 # b7 = b4 # b8
proof end;

theorem Th14: :: OSALG_3:14
for b1 being OrderSortedSign
for b2 being non-empty monotone OSAlgebra of b1
for b3 being non-empty OSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is order-sorted & b4 is_homomorphism b2,b3 holds
( Image b4 is order-sorted & Image b4 is monotone OSAlgebra of b1 )
proof end;

theorem Th15: :: OSALG_3:15
for b1 being OrderSortedSign
for b2 being monotone OSAlgebra of b1
for b3 being OSSubAlgebra of b2 holds b3 is monotone
proof end;

registration
let c1 be OrderSortedSign;
let c2 be monotone OSAlgebra of c1;
cluster monotone MSSubAlgebra of a2;
existence
ex b1 being OSSubAlgebra of c2 st b1 is monotone
proof end;
end;

registration
let c1 be OrderSortedSign;
let c2 be monotone OSAlgebra of c1;
cluster -> monotone MSSubAlgebra of a2;
coherence
for b1 being OSSubAlgebra of c2 holds b1 is monotone by Th15;
end;

theorem Th16: :: OSALG_3:16
for b1 being OrderSortedSign
for b2, b3 being non-empty OSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 & b4 is order-sorted holds
ex b5 being ManySortedFunction of b2,(Image b4) st
( b4 = b5 & b5 is order-sorted & b5 is_epimorphism b2, Image b4 )
proof end;

theorem Th17: :: OSALG_3:17
for b1 being OrderSortedSign
for b2, b3 being non-empty OSAlgebra of b1
for b4 being ManySortedFunction of b2,b3 st b4 is_homomorphism b2,b3 & b4 is order-sorted holds
ex b5 being ManySortedFunction of b2,(Image b4)ex b6 being ManySortedFunction of (Image b4),b3 st
( b5 is_epimorphism b2, Image b4 & b6 is_monomorphism Image b4,b3 & b4 = b6 ** b5 & b5 is order-sorted & b6 is order-sorted )
proof end;

registration
let c1 be OrderSortedSign;
let c2 be OSAlgebra of c1;
cluster MSAlgebra(# the Sorts of a2,the Charact of a2 #) -> order-sorted ;
coherence
MSAlgebra(# the Sorts of c2,the Charact of c2 #) is order-sorted
proof end;
end;

theorem Th18: :: OSALG_3:18
for b1 being OrderSortedSign
for b2 being OSAlgebra of b1 holds
( b2 is monotone iff MSAlgebra(# the Sorts of b2,the Charact of b2 #) is monotone )
proof end;

theorem Th19: :: OSALG_3:19
for b1 being OrderSortedSign
for b2, b3 being strict non-empty OSAlgebra of b1 st b2,b3 are_os_isomorphic holds
( b2 is monotone iff b3 is monotone )
proof end;