:: by Josef Urban

::

:: Received September 19, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

:: deftheorem defines order-sorted OSALG_3:def 1 :

for R being non empty Poset

for F being ManySortedFunction of the carrier of R holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in dom (F . s1) holds

( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) );

for R being non empty Poset

for F being ManySortedFunction of the carrier of R holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in dom (F . s1) holds

( a1 in dom (F . s2) & (F . s1) . a1 = (F . s2) . a1 ) );

theorem Th1: :: OSALG_3:1

for R being non empty Poset

for F being ManySortedFunction of the carrier of R st F is order-sorted holds

for s1, s2 being Element of R st s1 <= s2 holds

( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )

for F being ManySortedFunction of the carrier of R st F is order-sorted holds

for s1, s2 being Element of R st s1 <= s2 holds

( dom (F . s1) c= dom (F . s2) & F . s1 c= F . s2 )

proof end;

theorem Th2: :: OSALG_3:2

for R being non empty Poset

for A being OrderSortedSet of R

for B being V2() OrderSortedSet of R

for F being ManySortedFunction of A,B holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

for A being OrderSortedSet of R

for B being V2() OrderSortedSet of R

for F being ManySortedFunction of A,B holds

( F is order-sorted iff for s1, s2 being Element of R st s1 <= s2 holds

for a1 being set st a1 in A . s1 holds

(F . s1) . a1 = (F . s2) . a1 )

proof end;

theorem :: OSALG_3:3

for R being non empty Poset

for F being ManySortedFunction of the carrier of R st F is order-sorted holds

for w1, w2 being Element of the carrier of R * st w1 <= w2 holds

(F #) . w1 c= (F #) . w2

for F being ManySortedFunction of the carrier of R st F is order-sorted holds

for w1, w2 being Element of the carrier of R * st w1 <= w2 holds

(F #) . w1 c= (F #) . w2

proof end;

registration
end;

theorem Th5: :: OSALG_3:5

for R being non empty Poset

for A being OrderSortedSet of R

for B, C being V2() OrderSortedSet of R

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds

G ** F is order-sorted

for A being OrderSortedSet of R

for B, C being V2() OrderSortedSet of R

for F being ManySortedFunction of A,B

for G being ManySortedFunction of B,C st F is order-sorted & G is order-sorted holds

G ** F is order-sorted

proof end;

theorem Th6: :: OSALG_3:6

for R being non empty Poset

for A, B being OrderSortedSet of R

for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds

F "" is order-sorted

for A, B being OrderSortedSet of R

for F being ManySortedFunction of A,B st F is "1-1" & F is "onto" & F is order-sorted holds

F "" is order-sorted

proof end;

:: this could be done via by cluster, when non clusterable attrs removed

theorem Th7: :: OSALG_3:7

for R being non empty Poset

for A being OrderSortedSet of R

for F being ManySortedFunction of the carrier of R st F is order-sorted holds

F .:.: A is OrderSortedSet of R

for A being OrderSortedSet of R

for F being ManySortedFunction of the carrier of R st F is order-sorted holds

F .:.: A is OrderSortedSet of R

proof end;

definition

let S1 be OrderSortedSign;

let U1, U2 be OSAlgebra of S1;

end;
let U1, U2 be OSAlgebra of S1;

pred U1,U2 are_os_isomorphic means :: OSALG_3:def 2

ex F being ManySortedFunction of U1,U2 st

( F is_isomorphism U1,U2 & F is order-sorted );

ex F being ManySortedFunction of U1,U2 st

( F is_isomorphism U1,U2 & F is order-sorted );

:: deftheorem defines are_os_isomorphic OSALG_3:def 2 :

for S1 being OrderSortedSign

for U1, U2 being OSAlgebra of S1 holds

( U1,U2 are_os_isomorphic iff ex F being ManySortedFunction of U1,U2 st

( F is_isomorphism U1,U2 & F is order-sorted ) );

for S1 being OrderSortedSign

for U1, U2 being OSAlgebra of S1 holds

( U1,U2 are_os_isomorphic iff ex F being ManySortedFunction of U1,U2 st

( F is_isomorphism U1,U2 & F is order-sorted ) );

theorem Th9: :: OSALG_3:9

for S1 being OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds

U2,U1 are_os_isomorphic

for U1, U2 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds

U2,U1 are_os_isomorphic

proof end;

definition

let S1 be OrderSortedSign;

let U1, U2 be OSAlgebra of S1;

:: original: are_os_isomorphic

redefine pred U1,U2 are_os_isomorphic ;

reflexivity

for U1 being OSAlgebra of S1 holds (S1,b_{1},b_{1})
by Th8;

end;
let U1, U2 be OSAlgebra of S1;

:: original: are_os_isomorphic

redefine pred U1,U2 are_os_isomorphic ;

reflexivity

for U1 being OSAlgebra of S1 holds (S1,b

definition

let S1 be OrderSortedSign;

let U1, U2 be non-empty OSAlgebra of S1;

:: original: are_os_isomorphic

redefine pred U1,U2 are_os_isomorphic ;

symmetry

for U1, U2 being non-empty OSAlgebra of S1 st (S1,b_{1},b_{2}) holds

(S1,b_{2},b_{1})
by Th9;

end;
let U1, U2 be non-empty OSAlgebra of S1;

:: original: are_os_isomorphic

redefine pred U1,U2 are_os_isomorphic ;

symmetry

for U1, U2 being non-empty OSAlgebra of S1 st (S1,b

(S1,b

:: prove for order-sorted

theorem :: OSALG_3:10

for S1 being OrderSortedSign

for U1, U2, U3 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic holds

U1,U3 are_os_isomorphic

for U1, U2, U3 being non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic & U2,U3 are_os_isomorphic holds

U1,U3 are_os_isomorphic

proof end;

:: again, should be done as cluster or redefine

theorem Th11: :: OSALG_3:11

for S1 being OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds

Image F is order-sorted

for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds

Image F is order-sorted

proof end;

theorem Th12: :: OSALG_3:12

for S1 being OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is order-sorted holds

for o1, o2 being OperSymbol of S1 st o1 <= o2 holds

for x being Element of Args (o1,U1)

for x1 being Element of Args (o2,U1) st x = x1 holds

F # x = F # x1

for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is order-sorted holds

for o1, o2 being OperSymbol of S1 st o1 <= o2 holds

for x being Element of Args (o1,U1)

for x1 being Element of Args (o2,U1) st x = x1 holds

F # x = F # x1

proof end;

theorem Th13: :: OSALG_3:13

for S1 being OrderSortedSign

for U1 being non-empty monotone OSAlgebra of S1

for U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds

( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )

for U1 being non-empty monotone OSAlgebra of S1

for U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is order-sorted & F is_homomorphism U1,U2 holds

( Image F is order-sorted & Image F is monotone OSAlgebra of S1 )

proof end;

theorem Th14: :: OSALG_3:14

for S1 being OrderSortedSign

for U1 being monotone OSAlgebra of S1

for U2 being OSSubAlgebra of U1 holds U2 is monotone

for U1 being monotone OSAlgebra of S1

for U2 being OSSubAlgebra of U1 holds U2 is monotone

proof end;

registration

let S1 be OrderSortedSign;

let U1 be monotone OSAlgebra of S1;

existence

ex b_{1} being OSSubAlgebra of U1 st b_{1} is monotone

end;
let U1 be monotone OSAlgebra of S1;

existence

ex b

proof end;

registration

let S1 be OrderSortedSign;

let U1 be monotone OSAlgebra of S1;

coherence

for b_{1} being OSSubAlgebra of U1 holds b_{1} is monotone
by Th14;

end;
let U1 be monotone OSAlgebra of S1;

coherence

for b

theorem Th15: :: OSALG_3:15

for S1 being OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is order-sorted & G is_epimorphism U1, Image F )

for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

ex G being ManySortedFunction of U1,(Image F) st

( F = G & G is order-sorted & G is_epimorphism U1, Image F )

proof end;

theorem :: OSALG_3:16

for S1 being OrderSortedSign

for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st

( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )

for U1, U2 being non-empty OSAlgebra of S1

for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds

ex F1 being ManySortedFunction of U1,(Image F) ex F2 being ManySortedFunction of (Image F),U2 st

( F1 is_epimorphism U1, Image F & F2 is_monomorphism Image F,U2 & F = F2 ** F1 & F1 is order-sorted & F2 is order-sorted )

proof end;

registration

let S1 be OrderSortedSign;

let U1 be OSAlgebra of S1;

coherence

MSAlgebra(# the Sorts of U1, the Charact of U1 #) is order-sorted

end;
let U1 be OSAlgebra of S1;

coherence

MSAlgebra(# the Sorts of U1, the Charact of U1 #) is order-sorted

proof end;

:: very strange, the "strict" attribute is quite unfriendly

:: could Grzegorz's suggestion for struct implementation fix this?

:: hard to generalize to some useful scheme

:: could Grzegorz's suggestion for struct implementation fix this?

:: hard to generalize to some useful scheme

theorem :: OSALG_3:17

for S1 being OrderSortedSign

for U1 being OSAlgebra of S1 holds

( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )

for U1 being OSAlgebra of S1 holds

( U1 is monotone iff MSAlgebra(# the Sorts of U1, the Charact of U1 #) is monotone )

proof end;

:: proving the non strict version is painful, I'll do it only

:: if it is necessary, see TWiki.StructureImplementation for some suggestions

:: if it is necessary, see TWiki.StructureImplementation for some suggestions

theorem :: OSALG_3:18

for S1 being OrderSortedSign

for U1, U2 being strict non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds

( U1 is monotone iff U2 is monotone )

for U1, U2 being strict non-empty OSAlgebra of S1 st U1,U2 are_os_isomorphic holds

( U1 is monotone iff U2 is monotone )

proof end;

:: REVISE the prf of cluster in MSUALG_3