:: OSALG_1 semantic presentation

registration

let c₁ be set ;
let c₂ be ManySortedSet of c₁;
let c₃ be FinSequence of c₁;
cluster a₃ * a₂ -> FinSequence-like ;
coherence

proof end;

end;

Lemma1: for b₁ being set
for b₂ being ManySortedSet of b₁
for b₃ being FinSequence of b₁ holds
( dom (b₂ * b₃) = dom b₃ & len (b₂ * b₃) = len b₃ )

proof end;

definition

let c₁ be non empty ManySortedSign ;
mode SortSymbol of a₁ is Element of a₁;

end;

definition

let c₁ be non empty ManySortedSign ;
mode OperSymbol of a₁ is Element of the OperSymbols of a₁;

end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be OperSymbol of c₁;
redefine func the_result_sort_of as the_result_sort_of c₂ -> Element of a₁;
coherence ;

end;

definition

attr a₁ is strict;
struct OverloadedMSSign -> ManySortedSign ;
aggr OverloadedMSSign(# carrier, OperSymbols, Overloading, Arity, ResultSort #) -> OverloadedMSSign ;
sel Overloading c₁ -> Equivalence_Relation of the OperSymbols of a₁;

end;

definition

attr a₁ is strict;
struct RelSortedSign -> ManySortedSign , RelStr ;
aggr RelSortedSign(# carrier, InternalRel, OperSymbols, Arity, ResultSort #) -> RelSortedSign ;

end;

definition

attr a₁ is strict;
struct OverloadedRSSign -> OverloadedMSSign , RelSortedSign ;
aggr OverloadedRSSign(# carrier, InternalRel, OperSymbols, Overloading, Arity, ResultSort #) -> OverloadedRSSign ;

end;

theorem Th1: :: OSALG_1:1

for b₁, b₂ being non empty set
for b₃ being Order of b₁
for b₄ being Equivalence_Relation of b₂
for b₅ being Function of b₂,b₁ *
for b₆ being Function of b₂,b₁ holds
( not OverloadedRSSign(# b₁,b₃,b₂,b₄,b₅,b₆ #) is empty & not OverloadedRSSign(# b₁,b₃,b₂,b₄,b₅,b₆ #) is void & OverloadedRSSign(# b₁,b₃,b₂,b₄,b₅,b₆ #) is reflexive & OverloadedRSSign(# b₁,b₃,b₂,b₄,b₅,b₆ #) is transitive & OverloadedRSSign(# b₁,b₃,b₂,b₄,b₅,b₆ #) is antisymmetric )

proof end;

registration

let c₁ be non empty set ;
let c₂ be Order of c₁;
let c₃ be non empty set ;
let c₄ be Equivalence_Relation of c₃;
let c₅ be Function of c₃,c₁ * ;
let c₆ be Function of c₃,c₁;
cluster OverloadedRSSign(# a₁,a₂,a₃,a₄,a₅,a₆ #) -> non empty reflexive transitive antisymmetric ;
coherence by Th1;

end;

definition

let c₁ be OverloadedRSSign ;
canceled;
attr a₁ is order-sorted means :Def2: :: OSALG_1:def 2
( a₁ is reflexive & a₁ is transitive & a₁ is antisymmetric );

end;

:: deftheorem Def1 OSALG_1:def 1 :

:: deftheorem Def2 defines order-sorted OSALG_1:def 2 :

registration

cluster order-sorted -> reflexive transitive antisymmetric OverloadedRSSign ;
coherence by Def2;
cluster non empty non void strict order-sorted OverloadedRSSign ;
existence

proof end;

end;

registration

cluster non empty non void OverloadedMSSign ;
existence

proof end;

end;

definition

let c₁ be non empty non void OverloadedMSSign ;
let c₂, c₃ be OperSymbol of c₁;
pred c₂ ~= c₃ means :Def3: :: OSALG_1:def 3
[a₂,a₃] in the Overloading of a₁;
symmetry

proof end;

reflexivity

proof end;

end;

:: deftheorem Def3 defines ~= OSALG_1:def 3 :

theorem Th2: :: OSALG_1:2

for b₁ being non empty non void OverloadedMSSign
for b₂, b₃, b₄ being OperSymbol of b₁ st b₂ ~= b₃ & b₃ ~= b₄ holds
b₂ ~= b₄

proof end;

definition

let c₁ be non empty non void OverloadedMSSign ;
attr a₁ is discernable means :Def4: :: OSALG_1:def 4
for b₁, b₂ being OperSymbol of a₁ st b₁ ~= b₂ & the_arity_of b₁ = the_arity_of b₂ & the_result_sort_of b₁ = the_result_sort_of b₂ holds
b₁ = b₂;
attr a₁ is op-discrete means :Def5: :: OSALG_1:def 5
the Overloading of a₁ = id the OperSymbols of a₁;

end;

:: deftheorem Def4 defines discernable OSALG_1:def 4 :

:: deftheorem Def5 defines op-discrete OSALG_1:def 5 :

theorem Th3: :: OSALG_1:3

for b₁ being non empty non void OverloadedMSSign holds
( b₁ is op-discrete iff for b₂, b₃ being OperSymbol of b₁ st b₂ ~= b₃ holds
b₂ = b₃ )

proof end;

theorem Th4: :: OSALG_1:4

for b₁ being non empty non void OverloadedMSSign st b₁ is op-discrete holds
b₁ is discernable

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
func OSSign c₁ -> non empty non void strict order-sorted OverloadedRSSign means :Def6: :: OSALG_1:def 6
( the carrier of a₁ = the carrier of a₂ & id the carrier of a₁ = the InternalRel of a₂ & the OperSymbols of a₁ = the OperSymbols of a₂ & id the OperSymbols of a₁ = the Overloading of a₂ & the Arity of a₁ = the Arity of a₂ & the ResultSort of a₁ = the ResultSort of a₂ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines OSSign OSALG_1:def 6 :

theorem Th5: :: OSALG_1:5

for b₁ being non empty non void ManySortedSign holds
( OSSign b₁ is discrete & OSSign b₁ is op-discrete )

proof end;

registration

cluster non empty reflexive transitive antisymmetric discrete non void strict order-sorted discernable op-discrete OverloadedRSSign ;
existence

proof end;

end;

registration

cluster non empty non void op-discrete -> non empty non void discernable OverloadedRSSign ;
coherence by Th4;

end;

registration

let c₁ be non empty non void ManySortedSign ;
cluster OSSign a₁ -> non empty reflexive transitive antisymmetric discrete non void strict order-sorted discernable op-discrete ;
coherence by Th5;

end;

definition

mode OrderSortedSign is non empty non void order-sorted discernable OverloadedRSSign ;

end;

definition

let c₁ be non empty Poset;
let c₂, c₃ be Element of the carrier of c₁ * ;
pred c₂ <= c₃ means :Def7: :: OSALG_1:def 7
( len a₂ = len a₃ & ( for b₁ being set st b₁ in dom a₂ holds
for b₂, b₃ being Element of a₁ st b₂ = a₂ . b₁ & b₃ = a₃ . b₁ holds
b₂ <= b₃ ) );
reflexivity ;

end;

:: deftheorem Def7 defines <= OSALG_1:def 7 :

theorem Th6: :: OSALG_1:6

for b₁ being non empty Poset
for b₂, b₃ being Element of the carrier of b₁ * st b₂ <= b₃ & b₃ <= b₂ holds
b₂ = b₃

proof end;

theorem Th7: :: OSALG_1:7

for b₁ being non empty Poset
for b₂, b₃ being Element of the carrier of b₁ * st b₁ is discrete & b₂ <= b₃ holds
b₂ = b₃

proof end;

theorem Th8: :: OSALG_1:8

for b₁ being OrderSortedSign
for b₂, b₃ being OperSymbol of b₁ st b₁ is discrete & b₂ ~= b₃ & the_arity_of b₂ <= the_arity_of b₃ & the_result_sort_of b₂ <= the_result_sort_of b₃ holds
b₂ = b₃

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be OperSymbol of c₁;
attr a₂ is monotone means :Def8: :: OSALG_1:def 8
for b₁ being OperSymbol of a₁ st a₂ ~= b₁ & the_arity_of a₂ <= the_arity_of b₁ holds
the_result_sort_of a₂ <= the_result_sort_of b₁;

end;

:: deftheorem Def8 defines monotone OSALG_1:def 8 :

definition

let c₁ be OrderSortedSign;
attr a₁ is monotone means :Def9: :: OSALG_1:def 9
for b₁ being OperSymbol of a₁ holds b₁ is monotone;

end;

:: deftheorem Def9 defines monotone OSALG_1:def 9 :

theorem Th9: :: OSALG_1:9

for b₁ being OrderSortedSign st b₁ is op-discrete holds
b₁ is monotone

proof end;

registration

cluster monotone OverloadedRSSign ;
existence

proof end;

end;

registration

let c₁ be monotone OrderSortedSign;
cluster monotone Element of the OperSymbols of a₁;
existence

proof end;

end;

registration

let c₁ be monotone OrderSortedSign;
cluster -> monotone Element of the OperSymbols of a₁;
coherence by Def9;

end;

registration

cluster op-discrete -> reflexive transitive antisymmetric monotone OverloadedRSSign ;
coherence by Th9;

end;

theorem Th10: :: OSALG_1:10

for b₁ being OrderSortedSign
for b₂, b₃ being OperSymbol of b₁ st b₁ is monotone & the_arity_of b₂ = {} & b₂ ~= b₃ & the_arity_of b₃ = {} holds
b₂ = b₃

proof end;

definition

let c₁ be OrderSortedSign;
let c₂, c₃ be OperSymbol of c₁;
let c₄ be Element of the carrier of c₁ * ;
pred c₃ has_least_args_for c₂,c₄ means :Def10: :: OSALG_1:def 10
( a₂ ~= a₃ & a₄ <= the_arity_of a₃ & ( for b₁ being OperSymbol of a₁ st a₂ ~= b₁ & a₄ <= the_arity_of b₁ holds
the_arity_of a₃ <= the_arity_of b₁ ) );
pred c₃ has_least_sort_for c₂,c₄ means :Def11: :: OSALG_1:def 11
( a₂ ~= a₃ & a₄ <= the_arity_of a₃ & ( for b₁ being OperSymbol of a₁ st a₂ ~= b₁ & a₄ <= the_arity_of b₁ holds
the_result_sort_of a₃ <= the_result_sort_of b₁ ) );

end;

:: deftheorem Def10 defines has_least_args_for OSALG_1:def 10 :

:: deftheorem Def11 defines has_least_sort_for OSALG_1:def 11 :

definition

let c₁ be OrderSortedSign;
let c₂, c₃ be OperSymbol of c₁;
let c₄ be Element of the carrier of c₁ * ;
pred c₃ has_least_rank_for c₂,c₄ means :Def12: :: OSALG_1:def 12
( a₃ has_least_args_for a₂,a₄ & a₃ has_least_sort_for a₂,a₄ );

end;

:: deftheorem Def12 defines has_least_rank_for OSALG_1:def 12 :

definition

let c₁ be OrderSortedSign;
let c₂ be OperSymbol of c₁;
attr a₂ is regular means :Def13: :: OSALG_1:def 13
( a₂ is monotone & ( for b₁ being Element of the carrier of a₁ * st b₁ <= the_arity_of a₂ holds
ex b₂ being OperSymbol of a₁ st b₂ has_least_args_for a₂,b₁ ) );

end;

:: deftheorem Def13 defines regular OSALG_1:def 13 :

definition

let c₁ be monotone OrderSortedSign;
attr a₁ is regular means :Def14: :: OSALG_1:def 14
for b₁ being OperSymbol of a₁ holds b₁ is regular;

end;

:: deftheorem Def14 defines regular OSALG_1:def 14 :

theorem Th11: :: OSALG_1:11

for b₁ being monotone OrderSortedSign holds
( b₁ is regular iff for b₂ being OperSymbol of b₁
for b₃ being Element of the carrier of b₁ * st b₃ <= the_arity_of b₂ holds
ex b₄ being OperSymbol of b₁ st b₄ has_least_rank_for b₂,b₃ )

proof end;

theorem Th12: :: OSALG_1:12

for b₁ being monotone OrderSortedSign st b₁ is op-discrete holds
b₁ is regular

proof end;

registration

cluster monotone regular OverloadedRSSign ;
existence

proof end;

end;

registration

cluster op-discrete monotone -> reflexive transitive antisymmetric monotone regular OverloadedRSSign ;
coherence by Th12;

end;

registration

let c₁ be monotone regular OrderSortedSign;
cluster -> monotone regular Element of the OperSymbols of a₁;
coherence by Def14;

end;

theorem Th13: :: OSALG_1:13

for b₁ being monotone regular OrderSortedSign
for b₂, b₃, b₄ being OperSymbol of b₁
for b₅ being Element of the carrier of b₁ * st b₅ <= the_arity_of b₂ & b₃ has_least_args_for b₂,b₅ & b₄ has_least_args_for b₂,b₅ holds
b₃ = b₄

proof end;

definition

let c₁ be monotone regular OrderSortedSign;
let c₂ be OperSymbol of c₁;
let c₃ be Element of the carrier of c₁ * ;
assume E27: c₃ <= the_arity_of c₂ ;
func LBound c₂,c₃ -> OperSymbol of a₁ means :Def15: :: OSALG_1:def 15
a₄ has_least_args_for a₂,a₃;
existence by E27, Def13;
uniqueness by E27, Th13;

end;

:: deftheorem Def15 defines LBound OSALG_1:def 15 :

theorem Th14: :: OSALG_1:14

for b₁ being monotone regular OrderSortedSign
for b₂ being OperSymbol of b₁
for b₃ being Element of the carrier of b₁ * st b₃ <= the_arity_of b₂ holds
LBound b₂,b₃ has_least_rank_for b₂,b₃

proof end;

definition

let c₁ be non empty Poset;
let c₂ be non empty set ;
func ConstOSSet c₁,c₂ -> ManySortedSet of the carrier of a₁ equals :: OSALG_1:def 16
the carrier of a₁ --> a₂;
correctness

proof end;

end;

:: deftheorem Def16 defines ConstOSSet OSALG_1:def 16 :

theorem Th15: :: OSALG_1:15

for b₁ being non empty Poset
for b₂ being non empty set holds
( ConstOSSet b₁,b₂ is non-empty & ( for b₃, b₄ being Element of b₁ st b₃ <= b₄ holds
(ConstOSSet b₁,b₂) . b₃ c= (ConstOSSet b₁,b₂) . b₄ ) )

proof end;

definition

let c₁ be non empty Poset;
let c₂ be ManySortedSet of c₁;
canceled;
attr a₂ is order-sorted means :Def18: :: OSALG_1:def 18
for b₁, b₂ being Element of a₁ st b₁ <= b₂ holds
a₂ . b₁ c= a₂ . b₂;

end;

:: deftheorem Def17 OSALG_1:def 17 :

:: deftheorem Def18 defines order-sorted OSALG_1:def 18 :

theorem Th16: :: OSALG_1:16

for b₁ being non empty Poset
for b₂ being non empty set holds ConstOSSet b₁,b₂ is order-sorted

proof end;

registration

let c₁ be non empty Poset;
cluster order-sorted ManySortedSet of the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be non empty Poset;
let c₂ be non empty set ;
redefine func ConstOSSet as ConstOSSet c₁,c₂ -> order-sorted ManySortedSet of a₁;
coherence by Th16;

end;

definition

let c₁ be non empty Poset;
mode OrderSortedSet of a₁ is order-sorted ManySortedSet of a₁;

end;

registration

let c₁ be non empty Poset;
cluster V2 ManySortedSet of the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be MSAlgebra of c₁;
attr a₂ is order-sorted means :Def19: :: OSALG_1:def 19
for b₁, b₂ being SortSymbol of a₁ st b₁ <= b₂ holds
the Sorts of a₂ . b₁ c= the Sorts of a₂ . b₂;

end;

:: deftheorem Def19 defines order-sorted OSALG_1:def 19 :

theorem Th17: :: OSALG_1:17

for b₁ being OrderSortedSign
for b₂ being MSAlgebra of b₁ holds
( b₂ is order-sorted iff the Sorts of b₂ is OrderSortedSet of b₁ )

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be non empty set ;
let c₃ be ManySortedFunction of ((ConstOSSet c₁,c₂) # ) * the Arity of c₁,(ConstOSSet c₁,c₂) * the ResultSort of c₁;
func ConstOSA c₁,c₂,c₃ -> strict non-empty MSAlgebra of a₁ means :Def20: :: OSALG_1:def 20
( the Sorts of a₄ = ConstOSSet a₁,a₂ & the Charact of a₄ = a₃ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def20 defines ConstOSA OSALG_1:def 20 :

theorem Th18: :: OSALG_1:18

for b₁ being OrderSortedSign
for b₂ being non empty set
for b₃ being ManySortedFunction of ((ConstOSSet b₁,b₂) # ) * the Arity of b₁,(ConstOSSet b₁,b₂) * the ResultSort of b₁ holds ConstOSA b₁,b₂,b₃ is order-sorted

proof end;

registration

let c₁ be OrderSortedSign;
cluster strict non-empty order-sorted MSAlgebra of a₁;
existence

proof end;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be non empty set ;
let c₃ be ManySortedFunction of ((ConstOSSet c₁,c₂) # ) * the Arity of c₁,(ConstOSSet c₁,c₂) * the ResultSort of c₁;
cluster ConstOSA a₁,a₂,a₃ -> strict non-empty order-sorted ;
coherence by Th18;

end;

definition

let c₁ be OrderSortedSign;
mode OSAlgebra of a₁ is order-sorted MSAlgebra of a₁;

end;

theorem Th19: :: OSALG_1:19

for b₁ being discrete OrderSortedSign
for b₂ being MSAlgebra of b₁ holds b₂ is order-sorted

proof end;

registration

let c₁ be discrete OrderSortedSign;
cluster -> order-sorted MSAlgebra of a₁;
coherence by Th19;

end;

theorem Th20: :: OSALG_1:20

for b₁ being OrderSortedSign
for b₂, b₃ being Element of the carrier of b₁ *
for b₄ being OSAlgebra of b₁ st b₂ <= b₃ holds
(the Sorts of b₄ # ) . b₂ c= (the Sorts of b₄ # ) . b₃

proof end;

definition

let c₁ be non empty non void ManySortedSign ;
let c₂ be MSAlgebra of c₁;
func OSAlg c₂ -> strict OSAlgebra of OSSign a₁ means :: OSALG_1:def 21
( the Sorts of a₃ = the Sorts of a₂ & the Charact of a₃ = the Charact of a₂ );
uniqueness ;
existence

proof end;

end;

:: deftheorem Def21 defines OSAlg OSALG_1:def 21 :

theorem Th21: :: OSALG_1:21

for b₁ being OrderSortedSign
for b₂, b₃, b₄ being Element of the carrier of b₁ * st b₂ <= b₃ & b₃ <= b₄ holds
b₂ <= b₄

proof end;

definition

let c₁ be OrderSortedSign;
let c₂, c₃ be OperSymbol of c₁;
pred c₂ <= c₃ means :Def22: :: OSALG_1:def 22
( a₂ ~= a₃ & the_arity_of a₂ <= the_arity_of a₃ & the_result_sort_of a₂ <= the_result_sort_of a₃ );
reflexivity ;

end;

:: deftheorem Def22 defines <= OSALG_1:def 22 :

theorem Th22: :: OSALG_1:22

for b₁ being OrderSortedSign
for b₂, b₃ being OperSymbol of b₁ st b₂ <= b₃ & b₃ <= b₂ holds
b₂ = b₃

proof end;

theorem Th23: :: OSALG_1:23

for b₁ being OrderSortedSign
for b₂, b₃, b₄ being OperSymbol of b₁ st b₂ <= b₃ & b₃ <= b₄ holds
b₂ <= b₄

proof end;

theorem Th24: :: OSALG_1:24

for b₁ being OrderSortedSign
for b₂, b₃ being OperSymbol of b₁
for b₄ being OSAlgebra of b₁ st the_result_sort_of b₂ <= the_result_sort_of b₃ holds
Result b₂,b₄ c= Result b₃,b₄

proof end;

theorem Th25: :: OSALG_1:25

for b₁ being OrderSortedSign
for b₂, b₃ being OperSymbol of b₁
for b₄ being OSAlgebra of b₁ st the_arity_of b₂ <= the_arity_of b₃ holds
Args b₂,b₄ c= Args b₃,b₄

proof end;

theorem Th26: :: OSALG_1:26

for b₁ being OrderSortedSign
for b₂, b₃ being OperSymbol of b₁
for b₄ being OSAlgebra of b₁ st b₂ <= b₃ holds
( Args b₂,b₄ c= Args b₃,b₄ & Result b₂,b₄ c= Result b₃,b₄ )

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be OSAlgebra of c₁;
attr a₂ is monotone means :Def23: :: OSALG_1:def 23
for b₁, b₂ being OperSymbol of a₁ st b₁ <= b₂ holds
(Den b₂,a₂) | (Args b₁,a₂) = Den b₁,a₂;

end;

:: deftheorem Def23 defines monotone OSALG_1:def 23 :

theorem Th27: :: OSALG_1:27

for b₁ being OrderSortedSign
for b₂ being non-empty OSAlgebra of b₁ holds
( b₂ is monotone iff for b₃, b₄ being OperSymbol of b₁ st b₃ <= b₄ holds
Den b₃,b₂ c= Den b₄,b₂ )

proof end;

theorem Th28: :: OSALG_1:28

for b₁ being OrderSortedSign
for b₂ being OSAlgebra of b₁ st ( b₁ is discrete or b₁ is op-discrete ) holds
b₂ is monotone

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be non empty set ;
let c₃ be Element of c₂;
func TrivialOSA c₁,c₂,c₃ -> strict OSAlgebra of a₁ means :Def24: :: OSALG_1:def 24
( the Sorts of a₄ = ConstOSSet a₁,a₂ & ( for b₁ being OperSymbol of a₁ holds Den b₁,a₄ = (Args b₁,a₄) --> a₃ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines TrivialOSA OSALG_1:def 24 :

theorem Th29: :: OSALG_1:29

for b₁ being OrderSortedSign
for b₂ being non empty set
for b₃ being Element of b₂ holds
( TrivialOSA b₁,b₂,b₃ is non-empty & TrivialOSA b₁,b₂,b₃ is monotone )

proof end;

registration

let c₁ be OrderSortedSign;
cluster strict non-empty monotone MSAlgebra of a₁;
existence

proof end;

end;

registration

let c₁ be OrderSortedSign;
let c₂ be non empty set ;
let c₃ be Element of c₂;
cluster TrivialOSA a₁,a₂,a₃ -> strict non-empty monotone ;
coherence by Th29;

end;

definition

let c₁ be OrderSortedSign;
func OperNames c₁ -> non empty Subset-Family of the OperSymbols of a₁ equals :: OSALG_1:def 25
Class the Overloading of a₁;
coherence ;

end;

:: deftheorem Def25 defines OperNames OSALG_1:def 25 :

registration

let c₁ be OrderSortedSign;
cluster -> non empty Element of OperNames a₁;
coherence

proof end;

end;

definition

let c₁ be OrderSortedSign;
mode OperName of a₁ is Element of OperNames a₁;

end;

definition

let c₁ be OrderSortedSign;
let c₂ be OperSymbol of c₁;
func Name c₂ -> OperName of a₁ equals :: OSALG_1:def 26
Class the Overloading of a₁,a₂;
coherence by EQREL_1:def 5;

end;

:: deftheorem Def26 defines Name OSALG_1:def 26 :

theorem Th30: :: OSALG_1:30

for b₁ being OrderSortedSign
for b₂, b₃ being OperSymbol of b₁ holds
( b₂ ~= b₃ iff b₃ in Class the Overloading of b₁,b₂ )

proof end;

theorem Th31: :: OSALG_1:31

for b₁ being OrderSortedSign
for b₂, b₃ being OperSymbol of b₁ holds
( b₂ ~= b₃ iff Name b₂ = Name b₃ )

proof end;

theorem Th32: :: OSALG_1:32

for b₁ being OrderSortedSign
for b₂ being set holds
( b₂ is OperName of b₁ iff ex b₃ being OperSymbol of b₁ st b₂ = Name b₃ )

proof end;

definition

let c₁ be OrderSortedSign;
let c₂ be OperName of c₁;
redefine mode Element as Element of c₂ -> OperSymbol of a₁;
coherence

proof end;

end;

theorem Th33: :: OSALG_1:33

for b₁ being OrderSortedSign
for b₂ being OperName of b₁
for b₃ being OperSymbol of b₁ holds
( b₃ is Element of b₂ iff Name b₃ = b₂ )

proof end;

theorem Th34: :: OSALG_1:34

for b₁ being monotone regular OrderSortedSign
for b₂, b₃ being OperSymbol of b₁
for b₄ being Element of the carrier of b₁ * st b₂ ~= b₃ & len (the_arity_of b₂) = len (the_arity_of b₃) & b₄ <= the_arity_of b₂ & b₄ <= the_arity_of b₃ holds
LBound b₂,b₄ = LBound b₃,b₄

proof end;

definition

let c₁ be monotone regular OrderSortedSign;
let c₂ be OperName of c₁;
let c₃ be Element of the carrier of c₁ * ;
assume E50: ex b₁ being Element of c₂ st c₃ <= the_arity_of b₁ ;
func LBound c₂,c₃ -> Element of a₂ means :: OSALG_1:def 27
for b₁ being Element of a₂ st a₃ <= the_arity_of b₁ holds
a₄ = LBound b₁,a₃;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def27 defines LBound OSALG_1:def 27 :

theorem Th35: :: OSALG_1:35

for b₁ being monotone regular OrderSortedSign
for b₂ being OperSymbol of b₁
for b₃ being Element of the carrier of b₁ * st b₃ <= the_arity_of b₂ holds
LBound b₂,b₃ <= b₂

proof end;