:: PRALG_2 semantic presentation

definition

let c₁ be set ;
attr a₁ is with_common_domain means :Def1: :: PRALG_2:def 1
for b₁, b₂ being Function st b₁ in a₁ & b₂ in a₁ holds
dom b₁ = dom b₂;

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 Th1: :: PRALG_2:1

{{} } is functional with_common_domain set

proof end;

definition

let c₁ be functional with_common_domain set ;
func DOM c₁ -> set means :Def2: :: PRALG_2:def 2
for b₁ being Function st b₁ in a₁ holds
a₂ = dom b₁ if a₁ <> {}
otherwise a₂ = {} ;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def2 defines DOM PRALG_2:def 2 :

definition

let c₁ be non empty functional with_common_domain set ;
redefine mode Element as Element of c₁ -> ManySortedSet of DOM a₁;
coherence

proof end;

end;

theorem Th2: :: PRALG_2:2

for b₁ being functional with_common_domain set st b₁ = {{} } holds
DOM b₁ = {}

proof end;

registration

let c₁ be set ;
let c₂ be V3 ManySortedSet of c₁;
cluster product a₂ -> non empty functional with_common_domain ;
coherence

proof end;

end;

definition

let c₁ be Function;
canceled;
canceled;
canceled;
func Commute c₁ -> Function means :Def6: :: PRALG_2:def 6
( ( for b₁ being set holds
( b₁ in dom a₂ iff ex b₂ being Function st
( b₂ in dom a₁ & b₁ = commute b₂ ) ) ) & ( for b₁ being Function st b₁ in dom a₂ holds
a₂ . b₁ = a₁ . (commute b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 PRALG_2:def 3 :

:: deftheorem Def4 PRALG_2:def 4 :

:: deftheorem Def5 PRALG_2:def 5 :

:: deftheorem Def6 defines Commute PRALG_2:def 6 :

theorem Th3: :: PRALG_2:3

canceled;

theorem Th4: :: PRALG_2:4

canceled;

theorem Th5: :: PRALG_2:5

canceled;

theorem Th6: :: PRALG_2:6

canceled;

theorem Th7: :: PRALG_2:7

canceled;

theorem Th8: :: PRALG_2:8

for b₁ being Function st dom b₁ = {{} } holds
Commute b₁ = b₁

proof end;

definition

let c₁ be Function-yielding Function;
canceled;
redefine func Frege as Frege c₁ -> ManySortedFunction of product (doms a₁) means :Def8: :: PRALG_2:def 8
for b₁ being Function st b₁ in product (doms a₁) holds
a₂ . b₁ = a₁ .. b₁;
coherence

proof end;

compatibility

proof end;

end;

:: deftheorem Def7 PRALG_2:def 7 :

:: deftheorem Def8 defines Frege PRALG_2:def 8 :

registration

let c₁ be set ;
let c₂, c₃ be V3 ManySortedSet of c₁;
cluster [|a₂,a₃|] -> V3 ;
coherence

proof end;

end;

theorem Th9: :: PRALG_2:9

for b₁ being non empty set
for b₂ being set
for b₃, b₄ being ManySortedSet of b₁
for b₅ being Function of b₂,b₁ holds [|b₃,b₄|] * b₅ = [|(b₃ * b₅),(b₄ * b₅)|]

proof end;

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃, c₄ be V3 ManySortedSet of c₁;
let c₅ be Function of c₂,c₁ * ;
let c₆ be Function of c₂,c₁;
let c₇ be set ;
let c₈ be Function of ((c₃ # ) * c₅) . c₇,(c₃ * c₆) . c₇;
let c₉ be Function of ((c₄ # ) * c₅) . c₇,(c₄ * c₆) . c₇;
assume E6: c₇ in c₂ ;
canceled;
func [[:c₈,c₉:]] -> Function of (([|a₃,a₄|] # ) * a₅) . a₇,([|a₃,a₄|] * a₆) . a₇ means :: PRALG_2:def 10
for b₁ being Function st b₁ in (([|a₃,a₄|] # ) * a₅) . a₇ holds
a₁₀ . b₁ = [(a₈ . (pr1 b₁)),(a₉ . (pr2 b₁))];
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 PRALG_2:def 9 :

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

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃, c₄ be V3 ManySortedSet of c₁;
let c₅ be Function of c₂,c₁ * ;
let c₆ be Function of c₂,c₁;
let c₇ be ManySortedFunction of (c₃ # ) * c₅,c₃ * c₆;
let c₈ be ManySortedFunction of (c₄ # ) * c₅,c₄ * c₆;
func [[:c₇,c₈:]] -> ManySortedFunction of ([|a₃,a₄|] # ) * a₅,[|a₃,a₄|] * a₆ means :: PRALG_2:def 11
for b₁ being set st b₁ in a₂ holds
for b₂ being Function of ((a₃ # ) * a₅) . b₁,(a₃ * a₆) . b₁
for b₃ being Function of ((a₄ # ) * a₅) . b₁,(a₄ * a₆) . b₁ st b₂ = a₇ . b₁ & b₃ = a₈ . b₁ holds
a₉ . b₁ = [[:b₂,b₃:]];
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be set ;
let c₂ be non empty ManySortedSign ;
mode MSAlgebra-Family of c₁,c₂ -> ManySortedSet of a₁ means :Def12: :: PRALG_2:def 12
for b₁ being set st b₁ in a₁ holds
a₃ . b₁ is non-empty MSAlgebra of a₂;
existence

proof end;

end;

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

definition

let c₁ be non empty set ;
let c₂ be non empty ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
let c₄ be Element of c₁;
redefine func . as c₃ . c₄ -> non-empty MSAlgebra of a₂;
coherence by Def12;

end;

definition

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

end;

:: deftheorem Def13 defines |. PRALG_2:def 13 :

registration

let c₁ be non empty ManySortedSign ;
let c₂ be non-empty MSAlgebra of c₁;
cluster |.a₂.| -> non empty ;
coherence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
func |.c₃.| -> set equals :: PRALG_2:def 14
union { |.(a₃ . b₁).| where B is Element of a₁ : verum } ;
coherence ;

end;

:: deftheorem Def14 defines |. PRALG_2:def 14 :

registration

let c₁ be non empty set ;
let c₂ be non empty ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
cluster |.a₃.| -> non empty ;
coherence

proof end;

end;

theorem Th10: :: PRALG_2:10

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being OperSymbol of b₁ holds
( Args b₃,b₂ = product (the Sorts of b₂ * (the_arity_of b₃)) & dom (the Sorts of b₂ * (the_arity_of b₃)) = dom (the_arity_of b₃) & Result b₃,b₂ = the Sorts of b₂ . (the_result_sort_of b₃) )

proof end;

theorem Th11: :: PRALG_2:11

for b₁ being non empty non void ManySortedSign
for b₂ being MSAlgebra of b₁
for b₃ being OperSymbol of b₁ st the_arity_of b₃ = {} holds
Args b₃,b₂ = {{} }

proof end;

definition

let c₁ be non empty ManySortedSign ;
let c₂, c₃ be non-empty MSAlgebra of c₁;
func [:c₂,c₃:] -> MSAlgebra of a₁ equals :: PRALG_2:def 15
MSAlgebra(# [|the Sorts of a₂,the Sorts of a₃|],[[:the Charact of a₂,the Charact of a₃:]] #);
coherence ;

end;

:: deftheorem Def15 defines [: PRALG_2:def 15 :

registration

let c₁ be non empty ManySortedSign ;
let c₂, c₃ be non-empty MSAlgebra of c₁;
cluster [:a₂,a₃:] -> strict ;
coherence ;

end;

definition

let c₁ be set ;
let c₂ be non empty ManySortedSign ;
let c₃ be SortSymbol of c₂;
let c₄ be MSAlgebra-Family of c₁,c₂;
func Carrier c₄,c₃ -> ManySortedSet of a₁ means :Def16: :: PRALG_2:def 16
for b₁ being set st b₁ in a₁ holds
ex b₂ being MSAlgebra of a₂ st
( b₂ = a₄ . b₁ & a₅ . b₁ = the Sorts of b₂ . a₃ ) if a₁ <> {}
otherwise a₅ = {} ;
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def16 defines Carrier PRALG_2:def 16 :

registration

let c₁ be set ;
let c₂ be non empty ManySortedSign ;
let c₃ be SortSymbol of c₂;
let c₄ be MSAlgebra-Family of c₁,c₂;
cluster Carrier a₄,a₃ -> V3 ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
func SORTS c₃ -> ManySortedSet of the carrier of a₂ means :Def17: :: PRALG_2:def 17
for b₁ being SortSymbol of a₂ holds a₄ . b₁ = product (Carrier a₃,b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def17 defines SORTS PRALG_2:def 17 :

registration

let c₁ be set ;
let c₂ be non empty ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
cluster SORTS a₃ -> V3 ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be non empty ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
func OPER c₃ -> ManySortedFunction of a₁ means :Def18: :: PRALG_2:def 18
for b₁ being set st b₁ in a₁ holds
ex b₂ being MSAlgebra of a₂ st
( b₂ = a₃ . b₁ & a₄ . b₁ = the Charact of b₂ ) if a₁ <> {}
otherwise a₄ = {} ;
existence

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def18 defines OPER PRALG_2:def 18 :

theorem Th12: :: PRALG_2:12

for b₁ being set
for b₂ being non empty ManySortedSign
for b₃ being MSAlgebra-Family of b₁,b₂ holds dom (uncurry (OPER b₃)) = [:b₁,the OperSymbols of b₂:]

proof end;

theorem Th13: :: PRALG_2:13

for b₁ being non empty set
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra-Family of b₁,b₂
for b₄ being OperSymbol of b₂ holds commute (OPER b₃) in Funcs the OperSymbols of b₂,(Funcs b₁,(rng (uncurry (OPER b₃))))

proof end;

definition

let c₁ be set ;
let c₂ be non empty non void ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
let c₄ be OperSymbol of c₂;
func c₃ ?. c₄ -> ManySortedFunction of a₁ equals :: PRALG_2:def 19
(commute (OPER a₃)) . a₄;
coherence

proof end;

end;

:: deftheorem Def19 defines ?. PRALG_2:def 19 :

theorem Th14: :: PRALG_2:14

for b₁ being non empty set
for b₂ being Element of b₁
for b₃ being non empty non void ManySortedSign
for b₄ being MSAlgebra-Family of b₁,b₃
for b₅ being OperSymbol of b₃ holds (b₄ ?. b₅) . b₂ = Den b₅,(b₄ . b₂)

proof end;

theorem Th15: :: PRALG_2:15

for b₁ being non empty set
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra-Family of b₁,b₂
for b₄ being OperSymbol of b₂
for b₅ being set st b₅ in rng (Frege (b₃ ?. b₄)) holds
b₅ is Function

proof end;

theorem Th16: :: PRALG_2:16

for b₁ being non empty set
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra-Family of b₁,b₂
for b₄ being OperSymbol of b₂
for b₅ being Function st b₅ in rng (Frege (b₃ ?. b₄)) holds
( dom b₅ = b₁ & ( for b₆ being Element of b₁ holds b₅ . b₆ in Result b₄,(b₃ . b₆) ) )

proof end;

theorem Th17: :: PRALG_2:17

for b₁ being non empty set
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra-Family of b₁,b₂
for b₄ being OperSymbol of b₂
for b₅ being Function st b₅ in dom (Frege (b₃ ?. b₄)) holds
( dom b₅ = b₁ & ( for b₆ being Element of b₁ holds b₅ . b₆ in Args b₄,(b₃ . b₆) ) & rng b₅ c= Funcs (dom (the_arity_of b₄)),|.b₃.| )

proof end;

theorem Th18: :: PRALG_2:18

for b₁ being non empty set
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra-Family of b₁,b₂
for b₄ being OperSymbol of b₂ holds
( dom (doms (b₃ ?. b₄)) = b₁ & ( for b₅ being Element of b₁ holds (doms (b₃ ?. b₄)) . b₅ = Args b₄,(b₃ . b₅) ) )

proof end;

definition

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

proof end;

uniqueness

proof end;

correctness ;

end;

:: deftheorem Def20 defines OPS PRALG_2:def 20 :

definition

let c₁ be set ;
let c₂ be non empty non void ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
func product c₃ -> MSAlgebra of a₂ equals :: PRALG_2:def 21
MSAlgebra(# (SORTS a₃),(OPS a₃) #);
coherence ;

end;

:: deftheorem Def21 defines product PRALG_2:def 21 :

registration

let c₁ be set ;
let c₂ be non empty non void ManySortedSign ;
let c₃ be MSAlgebra-Family of c₁,c₂;
cluster product a₃ -> strict ;
coherence ;

end;

theorem Th19: :: PRALG_2:19

canceled;

theorem Th20: :: PRALG_2:20

for b₁ being set
for b₂ being non empty non void ManySortedSign
for b₃ being MSAlgebra-Family of b₁,b₂ holds
( the Sorts of (product b₃) = SORTS b₃ & the Charact of (product b₃) = OPS b₃ ) ;