:: by Andrzej Trybulec

::

:: Received April 21, 1994

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

definition

attr c_{1} is strict ;

struct ManySortedSign -> 2-sorted ;

aggr ManySortedSign(# carrier, carrier', Arity, ResultSort #) -> ManySortedSign ;

sel Arity c_{1} -> Function of the carrier' of c_{1},( the carrier of c_{1} *);

sel ResultSort c_{1} -> Function of the carrier' of c_{1}, the carrier of c_{1};

end;
struct ManySortedSign -> 2-sorted ;

aggr ManySortedSign(# carrier, carrier', Arity, ResultSort #) -> ManySortedSign ;

sel Arity c

sel ResultSort c

registration

existence

ex b_{1} being ManySortedSign st

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

ex b_{1} being ManySortedSign st

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

end;
ex b

( b

proof end;

existence ex b

( not b

proof end;

definition

let S be non empty ManySortedSign ;

mode SortSymbol of S is Element of S;

mode OperSymbol of S is Element of the carrier' of S;

end;
mode SortSymbol of S is Element of S;

mode OperSymbol of S is Element of the carrier' of S;

definition

let S be non empty non void ManySortedSign ;

let o be OperSymbol of S;

coherence

the Arity of S . o is Element of the carrier of S * ;

coherence

the ResultSort of S . o is Element of S ;

end;
let o be OperSymbol of S;

coherence

the Arity of S . o is Element of the carrier of S * ;

coherence

the ResultSort of S . o is Element of S ;

:: deftheorem defines the_arity_of MSUALG_1:def 1 :

for S being non empty non void ManySortedSign

for o being OperSymbol of S holds the_arity_of o = the Arity of S . o;

for S being non empty non void ManySortedSign

for o being OperSymbol of S holds the_arity_of o = the Arity of S . o;

:: deftheorem defines the_result_sort_of MSUALG_1:def 2 :

for S being non empty non void ManySortedSign

for o being OperSymbol of S holds the_result_sort_of o = the ResultSort of S . o;

for S being non empty non void ManySortedSign

for o being OperSymbol of S holds the_result_sort_of o = the ResultSort of S . o;

definition

let S be 1-sorted ;

attr c_{2} is strict ;

struct many-sorted over S -> ;

aggr many-sorted(# Sorts #) -> many-sorted over S;

sel Sorts c_{2} -> ManySortedSet of the carrier of S;

end;
attr c

struct many-sorted over S -> ;

aggr many-sorted(# Sorts #) -> many-sorted over S;

sel Sorts c

definition

let S be non empty ManySortedSign ;

attr c_{2} is strict ;

struct MSAlgebra over S -> many-sorted over S;

aggr MSAlgebra(# Sorts, Charact #) -> MSAlgebra over S;

sel Charact c_{2} -> ManySortedFunction of ( the Sorts of c_{2} #) * the Arity of S, the Sorts of c_{2} * the ResultSort of S;

end;
attr c

struct MSAlgebra over S -> many-sorted over S;

aggr MSAlgebra(# Sorts, Charact #) -> MSAlgebra over S;

sel Charact c

:: deftheorem Def3 defines non-empty MSUALG_1:def 3 :

for S being 1-sorted

for A being many-sorted over S holds

( A is non-empty iff the Sorts of A is V5() );

for S being 1-sorted

for A being many-sorted over S holds

( A is non-empty iff the Sorts of A is V5() );

registration

let S be non empty ManySortedSign ;

existence

ex b_{1} being MSAlgebra over S st

( b_{1} is strict & b_{1} is non-empty )

end;
existence

ex b

( b

proof end;

registration

let S be 1-sorted ;

existence

ex b_{1} being many-sorted over S st

( b_{1} is strict & b_{1} is non-empty )

end;
existence

ex b

( b

proof end;

registration

let S be 1-sorted ;

let A be non-empty many-sorted over S;

coherence

the Sorts of A is non-empty by Def3;

end;
let A be non-empty many-sorted over S;

coherence

the Sorts of A is non-empty by Def3;

registration

let S be non empty ManySortedSign ;

let A be non-empty MSAlgebra over S;

coherence

for b_{1} being Component of the Sorts of A holds not b_{1} is empty

for b_{1} being Component of ( the Sorts of A #) holds not b_{1} is empty

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

coherence

for b

proof end;

coherence for b

proof end;

definition

let S be non empty non void ManySortedSign ;

let o be OperSymbol of S;

let A be MSAlgebra over S;

(( the Sorts of A #) * the Arity of S) . o is Component of ( the Sorts of A #)

;

( the Sorts of A * the ResultSort of S) . o is Component of the Sorts of A

;

end;
let o be OperSymbol of S;

let A be MSAlgebra over S;

func Args (o,A) -> Component of ( the Sorts of A #) equals :: MSUALG_1:def 4

(( the Sorts of A #) * the Arity of S) . o;

coherence (( the Sorts of A #) * the Arity of S) . o;

(( the Sorts of A #) * the Arity of S) . o is Component of ( the Sorts of A #)

proof end;

correctness ;

func Result (o,A) -> Component of the Sorts of A equals :: MSUALG_1:def 5

( the Sorts of A * the ResultSort of S) . o;

coherence ( the Sorts of A * the ResultSort of S) . o;

( the Sorts of A * the ResultSort of S) . o is Component of the Sorts of A

proof end;

correctness ;

:: deftheorem defines Args MSUALG_1:def 4 :

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being MSAlgebra over S holds Args (o,A) = (( the Sorts of A #) * the Arity of S) . o;

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being MSAlgebra over S holds Args (o,A) = (( the Sorts of A #) * the Arity of S) . o;

:: deftheorem defines Result MSUALG_1:def 5 :

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being MSAlgebra over S holds Result (o,A) = ( the Sorts of A * the ResultSort of S) . o;

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being MSAlgebra over S holds Result (o,A) = ( the Sorts of A * the ResultSort of S) . o;

definition

let S be non empty non void ManySortedSign ;

let o be OperSymbol of S;

let A be MSAlgebra over S;

the Charact of A . o is Function of (Args (o,A)),(Result (o,A)) by PBOOLE:def 15;

end;
let o be OperSymbol of S;

let A be MSAlgebra over S;

func Den (o,A) -> Function of (Args (o,A)),(Result (o,A)) equals :: MSUALG_1:def 6

the Charact of A . o;

coherence the Charact of A . o;

the Charact of A . o is Function of (Args (o,A)),(Result (o,A)) by PBOOLE:def 15;

:: deftheorem defines Den MSUALG_1:def 6 :

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being MSAlgebra over S holds Den (o,A) = the Charact of A . o;

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being MSAlgebra over S holds Den (o,A) = the Charact of A . o;

theorem :: MSUALG_1:1

for S being non empty non void ManySortedSign

for o being OperSymbol of S

for A being non-empty MSAlgebra over S holds not Den (o,A) is empty ;

for o being OperSymbol of S

for A being non-empty MSAlgebra over S holds not Den (o,A) is empty ;

Lm1: for D being non empty set

for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = (arity h) -tuples_on D

proof end;

theorem Th2: :: MSUALG_1:2

for C being set

for A, B being non empty set

for F being PartFunc of C,A

for G being Function of A,B holds G * F is Function of (dom F),B

for A, B being non empty set

for F being PartFunc of C,A

for G being Function of A,B holds G * F is Function of (dom F),B

proof end;

theorem Th3: :: MSUALG_1:3

for D being non empty set

for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = Funcs ((Seg (arity h)),D)

for h being non empty homogeneous quasi_total PartFunc of (D *),D holds dom h = Funcs ((Seg (arity h)),D)

proof end;

:: deftheorem Def7 defines segmental MSUALG_1:def 7 :

for IT being ManySortedSign holds

( IT is segmental iff ex n being Nat st the carrier' of IT = Seg n );

for IT being ManySortedSign holds

( IT is segmental iff ex n being Nat st the carrier' of IT = Seg n );

theorem Th5: :: MSUALG_1:5

for S being non empty ManySortedSign st S is trivial holds

for A being MSAlgebra over S

for c1, c2 being Component of the Sorts of A holds c1 = c2

for A being MSAlgebra over S

for c1, c2 being Component of the Sorts of A holds c1 = c2

proof end;

reconsider z = 0 as Element of {0} by TARSKI:def 1;

Lm2: for A being Universal_Algebra

for f being Function of (dom (signature A)),({0} *) holds

( ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is segmental & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is 1 -element & not ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is void & ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #) is strict )

proof end;

registration

existence

ex b_{1} being ManySortedSign st

( b_{1} is segmental & not b_{1} is void & b_{1} is strict & b_{1} is 1 -element )

end;
ex b

( b

proof end;

definition

let A be Universal_Algebra;

existence

ex b_{1} being trivial non void strict segmental ManySortedSign st

( the carrier of b_{1} = {0} & the carrier' of b_{1} = dom (signature A) & the Arity of b_{1} = (*--> 0) * (signature A) & the ResultSort of b_{1} = (dom (signature A)) --> 0 );

uniqueness

for b_{1}, b_{2} being trivial non void strict segmental ManySortedSign st the carrier of b_{1} = {0} & the carrier' of b_{1} = dom (signature A) & the Arity of b_{1} = (*--> 0) * (signature A) & the ResultSort of b_{1} = (dom (signature A)) --> 0 & the carrier of b_{2} = {0} & the carrier' of b_{2} = dom (signature A) & the Arity of b_{2} = (*--> 0) * (signature A) & the ResultSort of b_{2} = (dom (signature A)) --> 0 holds

b_{1} = b_{2};

end;
func MSSign A -> trivial non void strict segmental ManySortedSign means :Def8: :: MSUALG_1:def 8

( the carrier of it = {0} & the carrier' of it = dom (signature A) & the Arity of it = (*--> 0) * (signature A) & the ResultSort of it = (dom (signature A)) --> 0 );

correctness ( the carrier of it = {0} & the carrier' of it = dom (signature A) & the Arity of it = (*--> 0) * (signature A) & the ResultSort of it = (dom (signature A)) --> 0 );

existence

ex b

( the carrier of b

uniqueness

for b

b

proof end;

:: deftheorem Def8 defines MSSign MSUALG_1:def 8 :

for A being Universal_Algebra

for b_{2} being trivial non void strict segmental ManySortedSign holds

( b_{2} = MSSign A iff ( the carrier of b_{2} = {0} & the carrier' of b_{2} = dom (signature A) & the Arity of b_{2} = (*--> 0) * (signature A) & the ResultSort of b_{2} = (dom (signature A)) --> 0 ) );

for A being Universal_Algebra

for b

( b

definition

let A be Universal_Algebra;

0 .--> the carrier of A is V5() ManySortedSet of the carrier of (MSSign A)

;

end;
func MSSorts A -> V5() ManySortedSet of the carrier of (MSSign A) equals :: MSUALG_1:def 9

0 .--> the carrier of A;

coherence 0 .--> the carrier of A;

0 .--> the carrier of A is V5() ManySortedSet of the carrier of (MSSign A)

proof end;

correctness ;

:: deftheorem defines MSSorts MSUALG_1:def 9 :

for A being Universal_Algebra holds MSSorts A = 0 .--> the carrier of A;

for A being Universal_Algebra holds MSSorts A = 0 .--> the carrier of A;

definition

let A be Universal_Algebra;

the charact of A is ManySortedFunction of ((MSSorts A) #) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A)

;

end;
func MSCharact A -> ManySortedFunction of ((MSSorts A) #) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A) equals :: MSUALG_1:def 10

the charact of A;

coherence the charact of A;

the charact of A is ManySortedFunction of ((MSSorts A) #) * the Arity of (MSSign A),(MSSorts A) * the ResultSort of (MSSign A)

proof end;

correctness ;

:: deftheorem defines MSCharact MSUALG_1:def 10 :

for A being Universal_Algebra holds MSCharact A = the charact of A;

for A being Universal_Algebra holds MSCharact A = the charact of A;

definition

let A be Universal_Algebra;

coherence

MSAlgebra(# (MSSorts A),(MSCharact A) #) is strict MSAlgebra over MSSign A;

;

end;
func MSAlg A -> strict MSAlgebra over MSSign A equals :: MSUALG_1:def 11

MSAlgebra(# (MSSorts A),(MSCharact A) #);

correctness MSAlgebra(# (MSSorts A),(MSCharact A) #);

coherence

MSAlgebra(# (MSSorts A),(MSCharact A) #) is strict MSAlgebra over MSSign A;

;

:: deftheorem defines MSAlg MSUALG_1:def 11 :

for A being Universal_Algebra holds MSAlg A = MSAlgebra(# (MSSorts A),(MSCharact A) #);

for A being Universal_Algebra holds MSAlg A = MSAlgebra(# (MSSorts A),(MSCharact A) #);

registration
end;

:: Manysorted Algebras with 1 Sort Only

definition

let MS be 1 -element ManySortedSign ;

let A be MSAlgebra over MS;

existence

ex b_{1} being set st b_{1} is Component of the Sorts of A

for b_{1}, b_{2} being set st b_{1} is Component of the Sorts of A & b_{2} is Component of the Sorts of A holds

b_{1} = b_{2}
by Th5;

end;
let A be MSAlgebra over MS;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def12 defines the_sort_of MSUALG_1:def 12 :

for MS being 1 -element ManySortedSign

for A being MSAlgebra over MS

for b_{3} being set holds

( b_{3} = the_sort_of A iff b_{3} is Component of the Sorts of A );

for MS being 1 -element ManySortedSign

for A being MSAlgebra over MS

for b

( b

registration

let MS be 1 -element ManySortedSign ;

let A be non-empty MSAlgebra over MS;

coherence

not the_sort_of A is empty

end;
let A be non-empty MSAlgebra over MS;

coherence

not the_sort_of A is empty

proof end;

theorem Th6: :: MSUALG_1:6

for MS being non void 1 -element segmental ManySortedSign

for i being OperSymbol of MS

for A being non-empty MSAlgebra over MS holds Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)

for i being OperSymbol of MS

for A being non-empty MSAlgebra over MS holds Args (i,A) = (len (the_arity_of i)) -tuples_on (the_sort_of A)

proof end;

theorem Th7: :: MSUALG_1:7

for MS being non void 1 -element segmental ManySortedSign

for i being OperSymbol of MS

for A being non-empty MSAlgebra over MS holds Args (i,A) c= (the_sort_of A) *

for i being OperSymbol of MS

for A being non-empty MSAlgebra over MS holds Args (i,A) c= (the_sort_of A) *

proof end;

theorem Th8: :: MSUALG_1:8

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))

for A being non-empty MSAlgebra over MS holds the Charact of A is FinSequence of PFuncs (((the_sort_of A) *),(the_sort_of A))

proof end;

definition

let MS be non void 1 -element segmental ManySortedSign ;

let A be non-empty MSAlgebra over MS;

the Charact of A is PFuncFinSequence of (the_sort_of A) by Th8;

end;
let A be non-empty MSAlgebra over MS;

func the_charact_of A -> PFuncFinSequence of (the_sort_of A) equals :: MSUALG_1:def 13

the Charact of A;

coherence the Charact of A;

the Charact of A is PFuncFinSequence of (the_sort_of A) by Th8;

:: deftheorem defines the_charact_of MSUALG_1:def 13 :

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS holds the_charact_of A = the Charact of A;

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS holds the_charact_of A = the Charact of A;

definition

let MS be non void 1 -element segmental ManySortedSign ;

let A be non-empty MSAlgebra over MS;

UAStr(# (the_sort_of A),(the_charact_of A) #) is strict Universal_Algebra

;

end;
let A be non-empty MSAlgebra over MS;

func 1-Alg A -> strict Universal_Algebra equals :: MSUALG_1:def 14

UAStr(# (the_sort_of A),(the_charact_of A) #);

coherence UAStr(# (the_sort_of A),(the_charact_of A) #);

UAStr(# (the_sort_of A),(the_charact_of A) #) is strict Universal_Algebra

proof end;

correctness ;

:: deftheorem defines 1-Alg MSUALG_1:def 14 :

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS holds 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #);

for MS being non void 1 -element segmental ManySortedSign

for A being non-empty MSAlgebra over MS holds 1-Alg A = UAStr(# (the_sort_of A),(the_charact_of A) #);

theorem :: MSUALG_1:10

for A being Universal_Algebra

for f being Function of (dom (signature A)),({0} *)

for z being Element of {0} st f = (*--> 0) * (signature A) holds

MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #)

for f being Function of (dom (signature A)),({0} *)

for z being Element of {0} st f = (*--> 0) * (signature A) holds

MSSign A = ManySortedSign(# {0},(dom (signature A)),f,((dom (signature A)) --> z) #)

proof end;