:: PRALG_2 semantic presentation

definition

let IT be set ;
attr IT is with_common_domain means :Def1: :: PRALG_2:def 1
for f, g being Function st f in IT & g in IT holds
dom f = dom g;

end;

:: deftheorem Def1 defines with_common_domain PRALG_2:def 1 :

registration

cluster non empty functional with_common_domain set ;
existence

proof end;

end;

theorem :: PRALG_2:1

{{} } is functional with_common_domain set

proof end;

definition

let X be functional with_common_domain set ;
func DOM X -> set means :Def2: :: PRALG_2:def 2
for x being Function st x in X holds
it = dom x if X <> {}
otherwise it = {} ;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def2 defines DOM PRALG_2:def 2 :

definition

let X be non empty functional with_common_domain set ;
:: original: Element
redefine mode Element of X -> ManySortedSet of DOM X;
coherence

proof end;

end;

theorem :: PRALG_2:2

for X being functional with_common_domain set st X = {{} } holds
DOM X = {}

proof end;

registration

let I be set ;
let M be V3 ManySortedSet of I;
cluster product M -> non empty functional with_common_domain ;
coherence

proof end;

end;

definition

let F be Function;
canceled;
canceled;
canceled;
func Commute F -> Function means :Def6: :: PRALG_2:def 6
( ( for x being set holds
( x in dom it iff ex f being Function st
( f in dom F & x = commute f ) ) ) & ( for f being Function st f in dom it holds
it . f = F . (commute f) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem PRALG_2:def 3 :

:: deftheorem PRALG_2:def 4 :

:: deftheorem PRALG_2:def 5 :

:: deftheorem Def6 defines Commute PRALG_2:def 6 :

theorem :: PRALG_2:3

canceled;

theorem :: PRALG_2:4

canceled;

theorem :: PRALG_2:5

canceled;

theorem :: PRALG_2:6

canceled;

theorem :: PRALG_2:7

canceled;

theorem :: PRALG_2:8

for F being Function st dom F = {{} } holds
Commute F = F

proof end;

definition

let f be Function-yielding Function;
canceled;
:: original: Frege
redefine func Frege f -> ManySortedFunction of product (doms f) means :Def8: :: PRALG_2:def 8
for g being Function st g in product (doms f) holds
it . g = f .. g;
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem PRALG_2:def 7 :

:: deftheorem Def8 defines Frege PRALG_2:def 8 :

registration

let I be set ;
let A, B be V3 ManySortedSet of I;
cluster [|A,B|] -> V3 ;
coherence

proof end;

end;

theorem Th9: :: PRALG_2:9

for I being non empty set
for J being set
for A, B being ManySortedSet of I
for f being Function of J,I holds [|A,B|] * f = [|(A * f),(B * f)|]

proof end;

definition

let I be non empty set ;
let J be set ;
let A, B be V3 ManySortedSet of I;
let p be Function of J,I * ;
let r be Function of J,I;
let j be set ;
let f be Function of ((A # ) * p) . j,(A * r) . j;
let g be Function of ((B # ) * p) . j,(B * r) . j;
assume A1: j in J ;
canceled;
func [[:f,g:]] -> Function of (([|A,B|] # ) * p) . j,([|A,B|] * r) . j means :: PRALG_2:def 10
for h being Function st h in (([|A,B|] # ) * p) . j holds
it . h = [(f . (pr1 h)),(g . (pr2 h))];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem PRALG_2:def 9 :

:: deftheorem defines [[: PRALG_2:def 10 :

definition

let I be non empty set ;
let J be set ;
let A, B be V3 ManySortedSet of I;
let p be Function of J,I * ;
let r be Function of J,I;
let F be ManySortedFunction of (A # ) * p,A * r;
let G be ManySortedFunction of (B # ) * p,B * r;
func [[:F,G:]] -> ManySortedFunction of ([|A,B|] # ) * p,[|A,B|] * r means :: PRALG_2:def 11
for j being set st j in J holds
for f being Function of ((A # ) * p) . j,(A * r) . j
for g being Function of ((B # ) * p) . j,(B * r) . j st f = F . j & g = G . j holds
it . j = [[:f,g:]];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines [[: PRALG_2:def 11 :

definition

let I be set ;
let S be non empty ManySortedSign ;
mode MSAlgebra-Family of I,S -> ManySortedSet of I means :Def12: :: PRALG_2:def 12
for i being set st i in I holds
it . i is non-empty MSAlgebra of S;
existence

proof end;

end;

:: deftheorem Def12 defines MSAlgebra-Family PRALG_2:def 12 :

definition

let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let i be Element of I;
:: original: .
redefine func A . i -> non-empty MSAlgebra of S;
coherence by Def12;

end;

definition

let S be non empty ManySortedSign ;
let U1 be MSAlgebra of S;
func |.U1.| -> set equals :: PRALG_2:def 13
union (rng the Sorts of U1);
coherence ;

end;

:: deftheorem defines |. PRALG_2:def 13 :

registration

let S be non empty ManySortedSign ;
let U1 be non-empty MSAlgebra of S;
cluster |.U1.| -> non empty ;
coherence

proof end;

end;

definition

let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func |.A.| -> set equals :: PRALG_2:def 14
union { |.(A . i).| where i is Element of I : verum } ;
coherence ;

end;

:: deftheorem defines |. PRALG_2:def 14 :

registration

let I be non empty set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster |.A.| -> non empty ;
coherence

proof end;

end;

theorem Th10: :: PRALG_2:10

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for o being OperSymbol of S holds
( Args o,U0 = product (the Sorts of U0 * (the_arity_of o)) & dom (the Sorts of U0 * (the_arity_of o)) = dom (the_arity_of o) & Result o,U0 = the Sorts of U0 . (the_result_sort_of o) )

proof end;

theorem Th11: :: PRALG_2:11

for S being non empty non void ManySortedSign
for U0 being MSAlgebra of S
for o being OperSymbol of S st the_arity_of o = {} holds
Args o,U0 = {{} }

proof end;

definition

let S be non empty ManySortedSign ;
let U1, U2 be non-empty MSAlgebra of S;
func [:U1,U2:] -> MSAlgebra of S equals :: PRALG_2:def 15
MSAlgebra(# [|the Sorts of U1,the Sorts of U2|],[[:the Charact of U1,the Charact of U2:]] #);
coherence ;

end;

:: deftheorem defines [: PRALG_2:def 15 :

registration

let S be non empty ManySortedSign ;
let U1, U2 be non-empty MSAlgebra of S;
cluster [:U1,U2:] -> strict ;
coherence ;

end;

definition

let I be set ;
let S be non empty ManySortedSign ;
let s be SortSymbol of S;
let A be MSAlgebra-Family of I,S;
func Carrier A,s -> ManySortedSet of I means :Def16: :: PRALG_2:def 16
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & it . i = the Sorts of U0 . s ) if I <> {}
otherwise it = {} ;
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def16 defines Carrier PRALG_2:def 16 :

registration

let I be set ;
let S be non empty ManySortedSign ;
let s be SortSymbol of S;
let A be MSAlgebra-Family of I,S;
cluster Carrier A,s -> V3 ;
coherence

proof end;

end;

definition

let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func SORTS A -> ManySortedSet of the carrier of S means :Def17: :: PRALG_2:def 17
for s being SortSymbol of S holds it . s = product (Carrier A,s);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines SORTS PRALG_2:def 17 :

registration

let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster SORTS A -> V3 ;
coherence

proof end;

end;

definition

let I be set ;
let S be non empty ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func OPER A -> ManySortedFunction of I means :Def18: :: PRALG_2:def 18
for i being set st i in I holds
ex U0 being MSAlgebra of S st
( U0 = A . i & it . i = the Charact of U0 ) if I <> {}
otherwise it = {} ;
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def18 defines OPER PRALG_2:def 18 :

theorem Th12: :: PRALG_2:12

for I being set
for S being non empty ManySortedSign
for A being MSAlgebra-Family of I,S holds dom (uncurry (OPER A)) = [:I,the OperSymbols of S:]

proof end;

theorem Th13: :: PRALG_2:13

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds commute (OPER A) in Funcs the OperSymbols of S,(Funcs I,(rng (uncurry (OPER A))))

proof end;

definition

let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
let o be OperSymbol of S;
func A ?. o -> ManySortedFunction of I equals :: PRALG_2:def 19
(commute (OPER A)) . o;
coherence

proof end;

end;

:: deftheorem defines ?. PRALG_2:def 19 :

theorem Th14: :: PRALG_2:14

for I being non empty set
for i being Element of I
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds (A ?. o) . i = Den o,(A . i)

proof end;

theorem :: PRALG_2:15

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for x being set st x in rng (Frege (A ?. o)) holds
x is Function

proof end;

theorem Th16: :: PRALG_2:16

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in rng (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Result o,(A . i) ) )

proof end;

theorem Th17: :: PRALG_2:17

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S
for f being Function st f in dom (Frege (A ?. o)) holds
( dom f = I & ( for i being Element of I holds f . i in Args o,(A . i) ) & rng f c= Funcs (dom (the_arity_of o)),|.A.| )

proof end;

theorem Th18: :: PRALG_2:18

for I being non empty set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S
for o being OperSymbol of S holds
( dom (doms (A ?. o)) = I & ( for i being Element of I holds (doms (A ?. o)) . i = Args o,(A . i) ) )

proof end;

definition

let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func OPS A -> ManySortedFunction of ((SORTS A) # ) * the Arity of S,(SORTS A) * the ResultSort of S means :: PRALG_2:def 20
for o being OperSymbol of S holds it . o = IFEQ (the_arity_of o),{} ,(commute (A ?. o)),(Commute (Frege (A ?. o))) if I <> {}
otherwise verum;
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem defines OPS PRALG_2:def 20 :

definition

let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
func product A -> MSAlgebra of S equals :: PRALG_2:def 21
MSAlgebra(# (SORTS A),(OPS A) #);
coherence ;

end;

:: deftheorem defines product PRALG_2:def 21 :

registration

let I be set ;
let S be non empty non void ManySortedSign ;
let A be MSAlgebra-Family of I,S;
cluster product A -> strict ;
coherence ;

end;

theorem :: PRALG_2:19

canceled;

theorem :: PRALG_2:20

for I being set
for S being non empty non void ManySortedSign
for A being MSAlgebra-Family of I,S holds
( the Sorts of (product A) = SORTS A & the Charact of (product A) = OPS A ) ;