:: by Josef Urban

::

:: Received September 19, 2002

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

definition

let S be OrderSortedSign;

let U0 be OSAlgebra of S;

ex b_{1} being MSSubset of U0 st

for O being OSSubset of U0 st O = OSCl b_{1} holds

the Sorts of (GenOSAlg O) = the Sorts of U0

end;
let U0 be OSAlgebra of S;

mode OSGeneratorSet of U0 -> MSSubset of U0 means :Def1: :: OSAFREE:def 1

for O being OSSubset of U0 st O = OSCl it holds

the Sorts of (GenOSAlg O) = the Sorts of U0;

existence for O being OSSubset of U0 st O = OSCl it holds

the Sorts of (GenOSAlg O) = the Sorts of U0;

ex b

for O being OSSubset of U0 st O = OSCl b

the Sorts of (GenOSAlg O) = the Sorts of U0

proof end;

:: deftheorem Def1 defines OSGeneratorSet OSAFREE:def 1 :

for S being OrderSortedSign

for U0 being OSAlgebra of S

for b_{3} being MSSubset of U0 holds

( b_{3} is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl b_{3} holds

the Sorts of (GenOSAlg O) = the Sorts of U0 );

for S being OrderSortedSign

for U0 being OSAlgebra of S

for b

( b

the Sorts of (GenOSAlg O) = the Sorts of U0 );

theorem :: OSAFREE:1

for S being OrderSortedSign

for U0 being strict non-empty OSAlgebra of S

for A being MSSubset of U0 holds

( A is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl A holds

GenOSAlg O = U0 )

for U0 being strict non-empty OSAlgebra of S

for A being MSSubset of U0 holds

( A is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl A holds

GenOSAlg O = U0 )

proof end;

:: renaming to osfree - if OSGeneratorSet and GeneratorSet become

:: attributes, Mizar would be puzzled

:: we do this for monotone osas only, though more general approach is possible

:: attributes, Mizar would be puzzled

:: we do this for monotone osas only, though more general approach is possible

definition

let S be OrderSortedSign;

let U0 be monotone OSAlgebra of S;

let IT be OSGeneratorSet of U0;

end;
let U0 be monotone OSAlgebra of S;

let IT be OSGeneratorSet of U0;

attr IT is osfree means :: OSAFREE:def 2

for U1 being non-empty monotone OSAlgebra of S

for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st

( h is_homomorphism U0,U1 & h is order-sorted & h || IT = f );

for U1 being non-empty monotone OSAlgebra of S

for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st

( h is_homomorphism U0,U1 & h is order-sorted & h || IT = f );

:: deftheorem defines osfree OSAFREE:def 2 :

for S being OrderSortedSign

for U0 being monotone OSAlgebra of S

for IT being OSGeneratorSet of U0 holds

( IT is osfree iff for U1 being non-empty monotone OSAlgebra of S

for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st

( h is_homomorphism U0,U1 & h is order-sorted & h || IT = f ) );

for S being OrderSortedSign

for U0 being monotone OSAlgebra of S

for IT being OSGeneratorSet of U0 holds

( IT is osfree iff for U1 being non-empty monotone OSAlgebra of S

for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st

( h is_homomorphism U0,U1 & h is order-sorted & h || IT = f ) );

:: deftheorem defines osfree OSAFREE:def 3 :

for S being OrderSortedSign

for IT being monotone OSAlgebra of S holds

( IT is osfree iff ex G being OSGeneratorSet of IT st G is osfree );

for S being OrderSortedSign

for IT being monotone OSAlgebra of S holds

( IT is osfree iff ex G being OSGeneratorSet of IT st G is osfree );

::

:: Construction of Free Order Sorted Algebras for Given Signature

::

:: Construction of Free Order Sorted Algebras for Given Signature

::

definition

let S be OrderSortedSign;

let X be ManySortedSet of S;

ex b_{1} being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st

for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b_{1} iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) )

for b_{1}, b_{2} being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) st ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b_{1} iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b_{2} iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) ) ) holds

b_{1} = b_{2}

end;
let X be ManySortedSet of S;

func OSREL X -> Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) means :Def4: :: OSAFREE:def 4

for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in it iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) );

existence for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in it iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) );

ex b

for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) )

proof end;

uniqueness for b

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) ) ) & ( for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) ) ) holds

b

proof end;

:: deftheorem Def4 defines OSREL OSAFREE:def 4 :

for S being OrderSortedSign

for X being ManySortedSet of S

for b_{3} being Relation of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) *) holds

( b_{3} = OSREL X iff for a being Element of [: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b_{3} iff ( a in [: the carrier' of S,{ the carrier of S}:] & ( for o being OperSymbol of S st [o, the carrier of S] = a holds

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) ) );

for S being OrderSortedSign

for X being ManySortedSet of S

for b

( b

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [a,b] in b

( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) ) ) ) );

theorem Th2: :: OSAFREE:2

for S being OrderSortedSign

for X being ManySortedSet of S

for o being OperSymbol of S

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [[o, the carrier of S],b] in OSREL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) )

for X being ManySortedSet of S

for o being OperSymbol of S

for b being Element of ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))) * holds

( [[o, the carrier of S],b] in OSREL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds

( ( b . x in [: the carrier' of S,{ the carrier of S}:] implies for o1 being OperSymbol of S st [o1, the carrier of S] = b . x holds

the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st

( i <= (the_arity_of o) /. x & b . x in coprod (i,X) ) ) ) ) ) )

proof end;

definition

let S be OrderSortedSign;

let X be ManySortedSet of S;

coherence

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #) is DTConstrStr ;

;

end;
let X be ManySortedSet of S;

func DTConOSA X -> DTConstrStr equals :: OSAFREE:def 5

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #);

correctness DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #);

coherence

DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #) is DTConstrStr ;

;

:: deftheorem defines DTConOSA OSAFREE:def 5 :

for S being OrderSortedSign

for X being ManySortedSet of S holds DTConOSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #);

for S being OrderSortedSign

for X being ManySortedSet of S holds DTConOSA X = DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #);

registration

let S be OrderSortedSign;

let X be ManySortedSet of S;

coherence

( DTConOSA X is strict & not DTConOSA X is empty ) ;

end;
let X be ManySortedSet of S;

coherence

( DTConOSA X is strict & not DTConOSA X is empty ) ;

theorem Th3: :: OSAFREE:3

for S being OrderSortedSign

for X being V2() ManySortedSet of S holds

( NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConOSA X) = Union (coprod X) )

for X being V2() ManySortedSet of S holds

( NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:] & Terminals (DTConOSA X) = Union (coprod X) )

proof end;

registration

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

coherence

( DTConOSA X is with_terminals & DTConOSA X is with_nonterminals & DTConOSA X is with_useful_nonterminals )

end;
let X be V2() ManySortedSet of S;

coherence

( DTConOSA X is with_terminals & DTConOSA X is with_nonterminals & DTConOSA X is with_useful_nonterminals )

proof end;

theorem Th4: :: OSAFREE:4

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for t being set holds

( t in Terminals (DTConOSA X) iff ex s being Element of S ex x being set st

( x in X . s & t = [x,s] ) )

for X being V2() ManySortedSet of S

for t being set holds

( t in Terminals (DTConOSA X) iff ex s being Element of S ex x being set st

( x in X . s & t = [x,s] ) )

proof end;

:: have to rename

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let o be OperSymbol of S;

coherence

[o, the carrier of S] is Symbol of (DTConOSA X)

end;
let X be V2() ManySortedSet of S;

let o be OperSymbol of S;

coherence

[o, the carrier of S] is Symbol of (DTConOSA X)

proof end;

:: deftheorem defines OSSym OSAFREE:def 6 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S holds OSSym (o,X) = [o, the carrier of S];

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S holds OSSym (o,X) = [o, the carrier of S];

:: originally FreeSort, but it is not a good name in order-sorted context

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let s be Element of S;

{ a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st

( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } is Subset of (TS (DTConOSA X))

end;
let X be V2() ManySortedSet of S;

let s be Element of S;

func ParsedTerms (X,s) -> Subset of (TS (DTConOSA X)) equals :: OSAFREE:def 7

{ a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st

( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } ;

coherence { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st

( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } ;

{ a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st

( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } is Subset of (TS (DTConOSA X))

proof end;

:: deftheorem defines ParsedTerms OSAFREE:def 7 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S holds ParsedTerms (X,s) = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st

( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } ;

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S holds ParsedTerms (X,s) = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st

( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) } ;

registration

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let s be Element of S;

coherence

not ParsedTerms (X,s) is empty

end;
let X be V2() ManySortedSet of S;

let s be Element of S;

coherence

not ParsedTerms (X,s) is empty

proof end;

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being OrderSortedSet of S st

for s being Element of S holds b_{1} . s = ParsedTerms (X,s)

for b_{1}, b_{2} being OrderSortedSet of S st ( for s being Element of S holds b_{1} . s = ParsedTerms (X,s) ) & ( for s being Element of S holds b_{2} . s = ParsedTerms (X,s) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func ParsedTerms X -> OrderSortedSet of S means :Def8: :: OSAFREE:def 8

for s being Element of S holds it . s = ParsedTerms (X,s);

existence for s being Element of S holds it . s = ParsedTerms (X,s);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines ParsedTerms OSAFREE:def 8 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being OrderSortedSet of S holds

( b_{3} = ParsedTerms X iff for s being Element of S holds b_{3} . s = ParsedTerms (X,s) );

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

registration

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

coherence

ParsedTerms X is non-empty

end;
let X be V2() ManySortedSet of S;

coherence

ParsedTerms X is non-empty

proof end;

theorem Th5: :: OSAFREE:5

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being set st x in (((ParsedTerms X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConOSA X)

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being set st x in (((ParsedTerms X) #) * the Arity of S) . o holds

x is FinSequence of TS (DTConOSA X)

proof end;

theorem Th6: :: OSAFREE:6

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for p being FinSequence of TS (DTConOSA X) holds

( p in (((ParsedTerms X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds

p . n in ParsedTerms (X,((the_arity_of o) /. n)) ) ) )

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for p being FinSequence of TS (DTConOSA X) holds

( p in (((ParsedTerms X) #) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds

p . n in ParsedTerms (X,((the_arity_of o) /. n)) ) ) )

proof end;

theorem Th7: :: OSAFREE:7

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for p being FinSequence of TS (DTConOSA X) holds

( OSSym (o,X) ==> roots p iff p in (((ParsedTerms X) #) * the Arity of S) . o )

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for p being FinSequence of TS (DTConOSA X) holds

( OSSym (o,X) ==> roots p iff p in (((ParsedTerms X) #) * the Arity of S) . o )

proof end;

theorem Th8: :: OSAFREE:8

for S being OrderSortedSign

for X being V2() ManySortedSet of S holds union (rng (ParsedTerms X)) = TS (DTConOSA X)

for X being V2() ManySortedSet of S holds union (rng (ParsedTerms X)) = TS (DTConOSA X)

proof end;

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let o be OperSymbol of S;

ex b_{1} being Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) st

for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds

b_{1} . p = (OSSym (o,X)) -tree p

for b_{1}, b_{2} being Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) st ( for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds

b_{1} . p = (OSSym (o,X)) -tree p ) & ( for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds

b_{2} . p = (OSSym (o,X)) -tree p ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

let o be OperSymbol of S;

func PTDenOp (o,X) -> Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) means :Def9: :: OSAFREE:def 9

for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds

it . p = (OSSym (o,X)) -tree p;

existence for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds

it . p = (OSSym (o,X)) -tree p;

ex b

for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def9 defines PTDenOp OSAFREE:def 9 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for b_{4} being Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) holds

( b_{4} = PTDenOp (o,X) iff for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds

b_{4} . p = (OSSym (o,X)) -tree p );

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for b

( b

b

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S st

for o being OperSymbol of S holds b_{1} . o = PTDenOp (o,X)

for b_{1}, b_{2} being ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S st ( for o being OperSymbol of S holds b_{1} . o = PTDenOp (o,X) ) & ( for o being OperSymbol of S holds b_{2} . o = PTDenOp (o,X) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func PTOper X -> ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S means :Def10: :: OSAFREE:def 10

for o being OperSymbol of S holds it . o = PTDenOp (o,X);

existence for o being OperSymbol of S holds it . o = PTDenOp (o,X);

ex b

for o being OperSymbol of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def10 defines PTOper OSAFREE:def 10 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S holds

( b_{3} = PTOper X iff for o being OperSymbol of S holds b_{3} . o = PTDenOp (o,X) );

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

MSAlgebra(# (ParsedTerms X),(PTOper X) #) is OSAlgebra of S by OSALG_1:17;

end;
let X be V2() ManySortedSet of S;

func ParsedTermsOSA X -> OSAlgebra of S equals :: OSAFREE:def 11

MSAlgebra(# (ParsedTerms X),(PTOper X) #);

coherence MSAlgebra(# (ParsedTerms X),(PTOper X) #);

MSAlgebra(# (ParsedTerms X),(PTOper X) #) is OSAlgebra of S by OSALG_1:17;

:: deftheorem defines ParsedTermsOSA OSAFREE:def 11 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S holds ParsedTermsOSA X = MSAlgebra(# (ParsedTerms X),(PTOper X) #);

for S being OrderSortedSign

for X being V2() ManySortedSet of S holds ParsedTermsOSA X = MSAlgebra(# (ParsedTerms X),(PTOper X) #);

registration

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

coherence

( ParsedTermsOSA X is strict & ParsedTermsOSA X is non-empty ) by MSUALG_1:def 3;

end;
let X be V2() ManySortedSet of S;

coherence

( ParsedTermsOSA X is strict & ParsedTermsOSA X is non-empty ) by MSUALG_1:def 3;

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let o be OperSymbol of S;

:: original: OSSym

redefine func OSSym (o,X) -> NonTerminal of (DTConOSA X);

coherence

OSSym (o,X) is NonTerminal of (DTConOSA X)

end;
let X be V2() ManySortedSet of S;

let o be OperSymbol of S;

:: original: OSSym

redefine func OSSym (o,X) -> NonTerminal of (DTConOSA X);

coherence

OSSym (o,X) is NonTerminal of (DTConOSA X)

proof end;

theorem Th9: :: OSAFREE:9

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S holds the Sorts of (ParsedTermsOSA X) . s = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st

( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) }

for X being V2() ManySortedSet of S

for s being Element of S holds the Sorts of (ParsedTermsOSA X) . s = { a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being object st

( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st

( [o, the carrier of S] = a . {} & the_result_sort_of o <= s ) ) }

proof end;

theorem Th10: :: OSAFREE:10

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for s, s1 being Element of S

for x being set st x in X . s holds

( root-tree [x,s] is Element of TS (DTConOSA X) & ( for z being set holds [z, the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )

for X being V2() ManySortedSet of S

for s, s1 being Element of S

for x being set st x in X . s holds

( root-tree [x,s] is Element of TS (DTConOSA X) & ( for z being set holds [z, the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )

proof end;

theorem Th11: :: OSAFREE:11

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X)

for o being OperSymbol of S st t . {} = [o, the carrier of S] holds

( ex p being SubtreeSeq of OSSym (o,X) st

( t = (OSSym (o,X)) -tree p & OSSym (o,X) ==> roots p & p in Args (o,(ParsedTermsOSA X)) & t = (Den (o,(ParsedTermsOSA X))) . p ) & ( for s2 being Element of S

for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds

( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X)

for o being OperSymbol of S st t . {} = [o, the carrier of S] holds

( ex p being SubtreeSeq of OSSym (o,X) st

( t = (OSSym (o,X)) -tree p & OSSym (o,X) ==> roots p & p in Args (o,(ParsedTermsOSA X)) & t = (Den (o,(ParsedTermsOSA X))) . p ) & ( for s2 being Element of S

for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds

( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )

proof end;

theorem Th12: :: OSAFREE:12

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st

( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(ParsedTermsOSA X))) . ts & ( for s1 being Element of S holds

( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) ) )

for X being V2() ManySortedSet of S

for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st

( nt = [o, the carrier of S] & ts in Args (o,(ParsedTermsOSA X)) & nt -tree ts = (Den (o,(ParsedTermsOSA X))) . ts & ( for s1 being Element of S holds

( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) ) )

proof end;

:: Element of Args is FinSequence (if clusters MSUALG_9)

theorem Th13: :: OSAFREE:13

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being FinSequence holds

( x in Args (o,(ParsedTermsOSA X)) iff ( x is FinSequence of TS (DTConOSA X) & OSSym (o,X) ==> roots x ) )

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being FinSequence holds

( x in Args (o,(ParsedTermsOSA X)) iff ( x is FinSequence of TS (DTConOSA X) & OSSym (o,X) ==> roots x ) )

proof end;

:: this should be done more generally for leastsorted osas (and

:: then remove the LeastSorts func), however, it is better here

:: to have it defined for terms (and not Elements of osa)

:: then remove the LeastSorts func), however, it is better here

:: to have it defined for terms (and not Elements of osa)

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let t be Element of TS (DTConOSA X);

ex b_{1} being SortSymbol of S st

( t in the Sorts of (ParsedTermsOSA X) . b_{1} & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds

b_{1} <= s1 ) )

for b_{1}, b_{2} being SortSymbol of S st t in the Sorts of (ParsedTermsOSA X) . b_{1} & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds

b_{1} <= s1 ) & t in the Sorts of (ParsedTermsOSA X) . b_{2} & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds

b_{2} <= s1 ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

let t be Element of TS (DTConOSA X);

func LeastSort t -> SortSymbol of S means :Def12: :: OSAFREE:def 12

( t in the Sorts of (ParsedTermsOSA X) . it & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds

it <= s1 ) );

existence ( t in the Sorts of (ParsedTermsOSA X) . it & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds

it <= s1 ) );

ex b

( t in the Sorts of (ParsedTermsOSA X) . b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def12 defines LeastSort OSAFREE:def 12 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X)

for b_{4} being SortSymbol of S holds

( b_{4} = LeastSort t iff ( t in the Sorts of (ParsedTermsOSA X) . b_{4} & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds

b_{4} <= s1 ) ) );

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X)

for b

( b

b

:: REVISE: the clusters needed to make the def from MSAFREE3 work

:: are too demanding, make it more easily accessible (or include

:: the clusters if it is too hard)

:: are too demanding, make it more easily accessible (or include

:: the clusters if it is too hard)

definition

let S be non empty non void ManySortedSign ;

let A be non-empty MSAlgebra over S;

mode Element of A is Element of Union the Sorts of A;

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

mode Element of A is Element of Union the Sorts of A;

theorem Th14: :: OSAFREE:14

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for x being set holds

( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) )

for X being V2() ManySortedSet of S

for x being set holds

( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) )

proof end;

theorem Th15: :: OSAFREE:15

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for x being set st x in the Sorts of (ParsedTermsOSA X) . s holds

x is Element of TS (DTConOSA X)

for X being V2() ManySortedSet of S

for s being Element of S

for x being set st x in the Sorts of (ParsedTermsOSA X) . s holds

x is Element of TS (DTConOSA X)

proof end;

theorem :: OSAFREE:16

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for x being set st x in X . s holds

for t being Element of TS (DTConOSA X) st t = root-tree [x,s] holds

LeastSort t = s

for X being V2() ManySortedSet of S

for s being Element of S

for x being set st x in X . s holds

for t being Element of TS (DTConOSA X) st t = root-tree [x,s] holds

LeastSort t = s

proof end;

theorem Th17: :: OSAFREE:17

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being Element of Args (o,(ParsedTermsOSA X))

for t being Element of TS (DTConOSA X) st t = (Den (o,(ParsedTermsOSA X))) . x holds

LeastSort t = the_result_sort_of o

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being Element of Args (o,(ParsedTermsOSA X))

for t being Element of TS (DTConOSA X) st t = (Den (o,(ParsedTermsOSA X))) . x holds

LeastSort t = the_result_sort_of o

proof end;

:: WHY is this necessary??? bug?

registration

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let o2 be OperSymbol of S;

coherence

not Args (o2,(ParsedTermsOSA X)) is empty ;

end;
let X be V2() ManySortedSet of S;

let o2 be OperSymbol of S;

coherence

not Args (o2,(ParsedTermsOSA X)) is empty ;

:: REVISE: was probably needed for casting, but try if

:: LeastSort * x does the work and if so, remove this

:: LeastSort * x does the work and if so, remove this

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let x be FinSequence of TS (DTConOSA X);

ex b_{1} being Element of the carrier of S * st

( dom b_{1} = dom x & ( for y being Nat st y in dom x holds

ex t being Element of TS (DTConOSA X) st

( t = x . y & b_{1} . y = LeastSort t ) ) )

for b_{1}, b_{2} being Element of the carrier of S * st dom b_{1} = dom x & ( for y being Nat st y in dom x holds

ex t being Element of TS (DTConOSA X) st

( t = x . y & b_{1} . y = LeastSort t ) ) & dom b_{2} = dom x & ( for y being Nat st y in dom x holds

ex t being Element of TS (DTConOSA X) st

( t = x . y & b_{2} . y = LeastSort t ) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

let x be FinSequence of TS (DTConOSA X);

func LeastSorts x -> Element of the carrier of S * means :Def13: :: OSAFREE:def 13

( dom it = dom x & ( for y being Nat st y in dom x holds

ex t being Element of TS (DTConOSA X) st

( t = x . y & it . y = LeastSort t ) ) );

existence ( dom it = dom x & ( for y being Nat st y in dom x holds

ex t being Element of TS (DTConOSA X) st

( t = x . y & it . y = LeastSort t ) ) );

ex b

( dom b

ex t being Element of TS (DTConOSA X) st

( t = x . y & b

proof end;

uniqueness for b

ex t being Element of TS (DTConOSA X) st

( t = x . y & b

ex t being Element of TS (DTConOSA X) st

( t = x . y & b

b

proof end;

:: deftheorem Def13 defines LeastSorts OSAFREE:def 13 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for x being FinSequence of TS (DTConOSA X)

for b_{4} being Element of the carrier of S * holds

( b_{4} = LeastSorts x iff ( dom b_{4} = dom x & ( for y being Nat st y in dom x holds

ex t being Element of TS (DTConOSA X) st

( t = x . y & b_{4} . y = LeastSort t ) ) ) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for x being FinSequence of TS (DTConOSA X)

for b

( b

ex t being Element of TS (DTConOSA X) st

( t = x . y & b

:: all these should be generalized to any leastsorted osa

theorem Th18: :: OSAFREE:18

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being FinSequence of TS (DTConOSA X) holds

( LeastSorts x <= the_arity_of o iff x in Args (o,(ParsedTermsOSA X)) )

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being FinSequence of TS (DTConOSA X) holds

( LeastSorts x <= the_arity_of o iff x in Args (o,(ParsedTermsOSA X)) )

proof end;

registration

ex b_{1} being monotone OrderSortedSign st

( b_{1} is locally_directed & b_{1} is regular )
end;

cluster non empty non void V66() reflexive transitive antisymmetric order-sorted discernable monotone regular locally_directed for OrderSortedSign;

existence ex b

( b

proof end;

:: just casting funcs necessary for the usage of schemes

definition

let S be monotone regular locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let o be OperSymbol of S;

let x be FinSequence of TS (DTConOSA X);

assume A1: OSSym ((LBound (o,(LeastSorts x))),X) ==> roots x ;

coherence

(OSSym ((LBound (o,(LeastSorts x))),X)) -tree x is Element of TS (DTConOSA X);

by A1, Th12;

end;
let X be V2() ManySortedSet of S;

let o be OperSymbol of S;

let x be FinSequence of TS (DTConOSA X);

assume A1: OSSym ((LBound (o,(LeastSorts x))),X) ==> roots x ;

func pi (o,x) -> Element of TS (DTConOSA X) equals :Def14: :: OSAFREE:def 14

(OSSym ((LBound (o,(LeastSorts x))),X)) -tree x;

correctness (OSSym ((LBound (o,(LeastSorts x))),X)) -tree x;

coherence

(OSSym ((LBound (o,(LeastSorts x))),X)) -tree x is Element of TS (DTConOSA X);

by A1, Th12;

:: deftheorem Def14 defines pi OSAFREE:def 14 :

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being FinSequence of TS (DTConOSA X) st OSSym ((LBound (o,(LeastSorts x))),X) ==> roots x holds

pi (o,x) = (OSSym ((LBound (o,(LeastSorts x))),X)) -tree x;

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for o being OperSymbol of S

for x being FinSequence of TS (DTConOSA X) st OSSym ((LBound (o,(LeastSorts x))),X) ==> roots x holds

pi (o,x) = (OSSym ((LBound (o,(LeastSorts x))),X)) -tree x;

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let t be Symbol of (DTConOSA X);

assume A1: ex p being FinSequence st t ==> p ;

existence

ex b_{1} being OperSymbol of S st [b_{1}, the carrier of S] = t

for b_{1}, b_{2} being OperSymbol of S st [b_{1}, the carrier of S] = t & [b_{2}, the carrier of S] = t holds

b_{1} = b_{2}
by XTUPLE_0:1;

end;
let X be V2() ManySortedSet of S;

let t be Symbol of (DTConOSA X);

assume A1: ex p being FinSequence st t ==> p ;

existence

ex b

proof end;

uniqueness for b

b

:: deftheorem Def15 defines @ OSAFREE:def 15 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for t being Symbol of (DTConOSA X) st ex p being FinSequence st t ==> p holds

for b_{4} being OperSymbol of S holds

( b_{4} = @ (X,t) iff [b_{4}, the carrier of S] = t );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for t being Symbol of (DTConOSA X) st ex p being FinSequence st t ==> p holds

for b

( b

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let t be Symbol of (DTConOSA X);

assume A1: t in Terminals (DTConOSA X) ;

correctness

coherence

root-tree t is Element of TS (DTConOSA X);

by A1, DTCONSTR:def 1;

end;
let X be V2() ManySortedSet of S;

let t be Symbol of (DTConOSA X);

assume A1: t in Terminals (DTConOSA X) ;

correctness

coherence

root-tree t is Element of TS (DTConOSA X);

by A1, DTCONSTR:def 1;

:: deftheorem Def16 defines pi OSAFREE:def 16 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

pi t = root-tree t;

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

pi t = root-tree t;

:: the least monotone OSCongruence

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being monotone OSCongruence of ParsedTermsOSA X st

for R being monotone OSCongruence of ParsedTermsOSA X holds b_{1} c= R

for b_{1}, b_{2} being monotone OSCongruence of ParsedTermsOSA X st ( for R being monotone OSCongruence of ParsedTermsOSA X holds b_{1} c= R ) & ( for R being monotone OSCongruence of ParsedTermsOSA X holds b_{2} c= R ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func LCongruence X -> monotone OSCongruence of ParsedTermsOSA X means :Def17: :: OSAFREE:def 17

for R being monotone OSCongruence of ParsedTermsOSA X holds it c= R;

existence for R being monotone OSCongruence of ParsedTermsOSA X holds it c= R;

ex b

for R being monotone OSCongruence of ParsedTermsOSA X holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def17 defines LCongruence OSAFREE:def 17 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being monotone OSCongruence of ParsedTermsOSA X holds

( b_{3} = LCongruence X iff for R being monotone OSCongruence of ParsedTermsOSA X holds b_{3} c= R );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

coherence

QuotOSAlg ((ParsedTermsOSA X),(LCongruence X)) is strict non-empty monotone OSAlgebra of S;

;

end;
let X be V2() ManySortedSet of S;

func FreeOSA X -> strict non-empty monotone OSAlgebra of S equals :: OSAFREE:def 18

QuotOSAlg ((ParsedTermsOSA X),(LCongruence X));

correctness QuotOSAlg ((ParsedTermsOSA X),(LCongruence X));

coherence

QuotOSAlg ((ParsedTermsOSA X),(LCongruence X)) is strict non-empty monotone OSAlgebra of S;

;

:: deftheorem defines FreeOSA OSAFREE:def 18 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds FreeOSA X = QuotOSAlg ((ParsedTermsOSA X),(LCongruence X));

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds FreeOSA X = QuotOSAlg ((ParsedTermsOSA X),(LCongruence X));

:: now we need an explicit description of a sufficiently small

:: monotone OSCongruence on PTA; the PTCongruence turns out to

:: be LCongruence on regular signatures, and is also used to describe

:: minimal terms there

:: just casting funcs necessary for the usage of schemes,

:: remove when Frankel behaves better

:: monotone OSCongruence on PTA; the PTCongruence turns out to

:: be LCongruence on regular signatures, and is also used to describe

:: minimal terms there

:: just casting funcs necessary for the usage of schemes,

:: remove when Frankel behaves better

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let t be Symbol of (DTConOSA X);

coherence

{ [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st

( x in X . s & t = [x,s] & s <= s1 ) } is Subset of [:(TS (DTConOSA X)), the carrier of S:];

end;
let X be V2() ManySortedSet of S;

let t be Symbol of (DTConOSA X);

func @ t -> Subset of [:(TS (DTConOSA X)), the carrier of S:] equals :: OSAFREE:def 19

{ [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st

( x in X . s & t = [x,s] & s <= s1 ) } ;

correctness { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st

( x in X . s & t = [x,s] & s <= s1 ) } ;

coherence

{ [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st

( x in X . s & t = [x,s] & s <= s1 ) } is Subset of [:(TS (DTConOSA X)), the carrier of S:];

proof end;

:: deftheorem defines @ OSAFREE:def 19 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for t being Symbol of (DTConOSA X) holds @ t = { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st

( x in X . s & t = [x,s] & s <= s1 ) } ;

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for t being Symbol of (DTConOSA X) holds @ t = { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st

( x in X . s & t = [x,s] & s <= s1 ) } ;

definition

let S be OrderSortedSign;

let X be V2() ManySortedSet of S;

let nt be Symbol of (DTConOSA X);

let x be FinSequence of bool [:(TS (DTConOSA X)), the carrier of S:];

coherence

{ [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st

( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st

( dom w3 = dom x & ( for y being Nat st y in dom x holds

[(x2 . y),(w3 /. y)] in x . y ) ) ) } is Subset of [:(TS (DTConOSA X)), the carrier of S:];

end;
let X be V2() ManySortedSet of S;

let nt be Symbol of (DTConOSA X);

let x be FinSequence of bool [:(TS (DTConOSA X)), the carrier of S:];

func @ (nt,x) -> Subset of [:(TS (DTConOSA X)), the carrier of S:] equals :: OSAFREE:def 20

{ [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st

( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st

( dom w3 = dom x & ( for y being Nat st y in dom x holds

[(x2 . y),(w3 /. y)] in x . y ) ) ) } ;

correctness { [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st

( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st

( dom w3 = dom x & ( for y being Nat st y in dom x holds

[(x2 . y),(w3 /. y)] in x . y ) ) ) } ;

coherence

{ [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st

( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st

( dom w3 = dom x & ( for y being Nat st y in dom x holds

[(x2 . y),(w3 /. y)] in x . y ) ) ) } is Subset of [:(TS (DTConOSA X)), the carrier of S:];

proof end;

:: deftheorem defines @ OSAFREE:def 20 :

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for nt being Symbol of (DTConOSA X)

for x being FinSequence of bool [:(TS (DTConOSA X)), the carrier of S:] holds @ (nt,x) = { [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st

( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st

( dom w3 = dom x & ( for y being Nat st y in dom x holds

[(x2 . y),(w3 /. y)] in x . y ) ) ) } ;

for S being OrderSortedSign

for X being V2() ManySortedSet of S

for nt being Symbol of (DTConOSA X)

for x being FinSequence of bool [:(TS (DTConOSA X)), the carrier of S:] holds @ (nt,x) = { [((Den (o2,(ParsedTermsOSA X))) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args (o2,(ParsedTermsOSA X)), s3 is Element of S : ( ex o1 being OperSymbol of S st

( nt = [o1, the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st

( dom w3 = dom x & ( for y being Nat st y in dom x holds

[(x2 . y),(w3 /. y)] in x . y ) ) ) } ;

:: a bit technical, to create the PTCongruence

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) st

( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b_{1} . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b_{1} . (nt -tree ts) = @ (nt,(b_{1} * ts)) ) )

for b_{1}, b_{2} being Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) st ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b_{1} . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b_{1} . (nt -tree ts) = @ (nt,(b_{1} * ts)) ) & ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b_{2} . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b_{2} . (nt -tree ts) = @ (nt,(b_{2} * ts)) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func PTClasses X -> Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) means :Def21: :: OSAFREE:def 21

( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

it . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

it . (nt -tree ts) = @ (nt,(it * ts)) ) );

existence ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

it . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

it . (nt -tree ts) = @ (nt,(it * ts)) ) );

ex b

( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b

proof end;

uniqueness for b

b

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b

b

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b

b

proof end;

:: deftheorem Def21 defines PTClasses OSAFREE:def 21 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) holds

( b_{3} = PTClasses X iff ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b_{3} . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b_{3} . (nt -tree ts) = @ (nt,(b_{3} * ts)) ) ) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

b

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b

theorem Th19: :: OSAFREE:19

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X) holds

( ( for s being Element of S holds

( t in the Sorts of (ParsedTermsOSA X) . s iff [t,s] in (PTClasses X) . t ) ) & ( for s being Element of S

for y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds

[t,s] in (PTClasses X) . y ) )

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X) holds

( ( for s being Element of S holds

( t in the Sorts of (ParsedTermsOSA X) . s iff [t,s] in (PTClasses X) . t ) ) & ( for s being Element of S

for y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds

[t,s] in (PTClasses X) . y ) )

proof end;

:: switched to have easier prooving

theorem Th20: :: OSAFREE:20

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X)

for s being Element of S st ex y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds

[t,s] in (PTClasses X) . t

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X)

for s being Element of S st ex y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds

[t,s] in (PTClasses X) . t

proof end;

theorem Th21: :: OSAFREE:21

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for x, y being Element of TS (DTConOSA X)

for s1, s2 being Element of S st s1 <= s2 & x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds

( [y,s1] in (PTClasses X) . x iff [y,s2] in (PTClasses X) . x )

for X being V2() ManySortedSet of S

for x, y being Element of TS (DTConOSA X)

for s1, s2 being Element of S st s1 <= s2 & x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds

( [y,s1] in (PTClasses X) . x iff [y,s2] in (PTClasses X) . x )

proof end;

theorem Th22: :: OSAFREE:22

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for x, y, z being Element of TS (DTConOSA X)

for s being Element of S st [y,s] in (PTClasses X) . x & [z,s] in (PTClasses X) . y holds

[x,s] in (PTClasses X) . z

for X being V2() ManySortedSet of S

for x, y, z being Element of TS (DTConOSA X)

for s being Element of S st [y,s] in (PTClasses X) . x & [z,s] in (PTClasses X) . y holds

[x,s] in (PTClasses X) . z

proof end;

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X st

for i being set st i in the carrier of S holds

b_{1} . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y }

for b_{1}, b_{2} being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X st ( for i being set st i in the carrier of S holds

b_{1} . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) & ( for i being set st i in the carrier of S holds

b_{2} . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func PTCongruence X -> MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X means :Def22: :: OSAFREE:def 22

for i being set st i in the carrier of S holds

it . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ;

existence for i being set st i in the carrier of S holds

it . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } ;

ex b

for i being set st i in the carrier of S holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def22 defines PTCongruence OSAFREE:def 22 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X holds

( b_{3} = PTCongruence X iff for i being set st i in the carrier of S holds

b_{3} . i = { [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y } );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

b

theorem Th23: :: OSAFREE:23

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for x, y, s being object st [x,s] in (PTClasses X) . y holds

( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )

for X being V2() ManySortedSet of S

for x, y, s being object st [x,s] in (PTClasses X) . y holds

( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )

proof end;

theorem Th24: :: OSAFREE:24

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for C being Component of S

for x, y being object holds

( [x,y] in CompClass ((PTCongruence X),C) iff ex s1 being Element of S st

( s1 in C & [x,s1] in (PTClasses X) . y ) )

for X being V2() ManySortedSet of S

for C being Component of S

for x, y being object holds

( [x,y] in CompClass ((PTCongruence X),C) iff ex s1 being Element of S st

( s1 in C & [x,s1] in (PTClasses X) . y ) )

proof end;

theorem Th25: :: OSAFREE:25

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s holds OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x)

for X being V2() ManySortedSet of S

for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s holds OSClass ((PTCongruence X),x) = proj1 ((PTClasses X) . x)

proof end;

:: more explicit description of PTCongruence

theorem Th26: :: OSAFREE:26

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for R being ManySortedRelation of (ParsedTermsOSA X) holds

( R = PTCongruence X iff ( ( for s1, s2 being Element of S

for x being object st x in X . s1 holds

( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in R . s2 ) & ( for y being object st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds

( s1 <= s2 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S

for x1 being Element of Args (o1,(ParsedTermsOSA X))

for x2 being Element of Args (o2,(ParsedTermsOSA X))

for s3 being Element of S holds

( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in R . s3 iff ( o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of the carrier of S * st

( dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds

[(x1 . y),(x2 . y)] in R . (w3 /. y) ) ) ) ) ) ) )

for X being V2() ManySortedSet of S

for R being ManySortedRelation of (ParsedTermsOSA X) holds

( R = PTCongruence X iff ( ( for s1, s2 being Element of S

for x being object st x in X . s1 holds

( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in R . s2 ) & ( for y being object st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds

( s1 <= s2 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S

for x1 being Element of Args (o1,(ParsedTermsOSA X))

for x2 being Element of Args (o2,(ParsedTermsOSA X))

for s3 being Element of S holds

( [((Den (o1,(ParsedTermsOSA X))) . x1),((Den (o2,(ParsedTermsOSA X))) . x2)] in R . s3 iff ( o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of the carrier of S * st

( dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds

[(x1 . y),(x2 . y)] in R . (w3 /. y) ) ) ) ) ) ) )

proof end;

:: the minimality for regular oss is done later

theorem Th27: :: OSAFREE:27

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds PTCongruence X is monotone

for X being V2() ManySortedSet of S holds PTCongruence X is monotone

proof end;

:: MSCongruence-like is ensured by the OSALG_4 cluster

registration

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

coherence

PTCongruence X is monotone by Th27;

end;
let X be V2() ManySortedSet of S;

coherence

PTCongruence X is monotone by Th27;

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let s be Element of S;

ex b_{1} being Subset of ( the Sorts of (ParsedTermsOSA X) . s) st

for x being object holds

( x in b_{1} iff ex a being object st

( a in X . s & x = root-tree [a,s] ) )

for b_{1}, b_{2} being Subset of ( the Sorts of (ParsedTermsOSA X) . s) st ( for x being object holds

( x in b_{1} iff ex a being object st

( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being object holds

( x in b_{2} iff ex a being object st

( a in X . s & x = root-tree [a,s] ) ) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

let s be Element of S;

func PTVars (s,X) -> Subset of ( the Sorts of (ParsedTermsOSA X) . s) means :Def23: :: OSAFREE:def 23

for x being object holds

( x in it iff ex a being object st

( a in X . s & x = root-tree [a,s] ) );

existence for x being object holds

( x in it iff ex a being object st

( a in X . s & x = root-tree [a,s] ) );

ex b

for x being object holds

( x in b

( a in X . s & x = root-tree [a,s] ) )

proof end;

uniqueness for b

( x in b

( a in X . s & x = root-tree [a,s] ) ) ) & ( for x being object holds

( x in b

( a in X . s & x = root-tree [a,s] ) ) ) holds

b

proof end;

:: deftheorem Def23 defines PTVars OSAFREE:def 23 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for b_{4} being Subset of ( the Sorts of (ParsedTermsOSA X) . s) holds

( b_{4} = PTVars (s,X) iff for x being object holds

( x in b_{4} iff ex a being object st

( a in X . s & x = root-tree [a,s] ) ) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for b

( b

( x in b

( a in X . s & x = root-tree [a,s] ) ) );

registration

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let s be Element of S;

coherence

not PTVars (s,X) is empty

end;
let X be V2() ManySortedSet of S;

let s be Element of S;

coherence

not PTVars (s,X) is empty

proof end;

theorem Th28: :: OSAFREE:28

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S holds PTVars (s,X) = { (root-tree t) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }

for X being V2() ManySortedSet of S

for s being Element of S holds PTVars (s,X) = { (root-tree t) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }

proof end;

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being MSSubset of (ParsedTermsOSA X) st

for s being Element of S holds b_{1} . s = PTVars (s,X)

for b_{1}, b_{2} being MSSubset of (ParsedTermsOSA X) st ( for s being Element of S holds b_{1} . s = PTVars (s,X) ) & ( for s being Element of S holds b_{2} . s = PTVars (s,X) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func PTVars X -> MSSubset of (ParsedTermsOSA X) means :Def24: :: OSAFREE:def 24

for s being Element of S holds it . s = PTVars (s,X);

existence for s being Element of S holds it . s = PTVars (s,X);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def24 defines PTVars OSAFREE:def 24 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being MSSubset of (ParsedTermsOSA X) holds

( b_{3} = PTVars X iff for s being Element of S holds b_{3} . s = PTVars (s,X) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

theorem :: OSAFREE:29

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds PTVars X is V2()

for X being V2() ManySortedSet of S holds PTVars X is V2()

proof end;

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let s be Element of S;

ex b_{1} being Subset of ( the Sorts of (FreeOSA X) . s) st

for x being object holds

( x in b_{1} iff ex a being object st

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) )

for b_{1}, b_{2} being Subset of ( the Sorts of (FreeOSA X) . s) st ( for x being object holds

( x in b_{1} iff ex a being object st

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) & ( for x being object holds

( x in b_{2} iff ex a being object st

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

let s be Element of S;

func OSFreeGen (s,X) -> Subset of ( the Sorts of (FreeOSA X) . s) means :Def25: :: OSAFREE:def 25

for x being object holds

( x in it iff ex a being object st

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) );

existence for x being object holds

( x in it iff ex a being object st

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) );

ex b

for x being object holds

( x in b

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) )

proof end;

uniqueness for b

( x in b

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) & ( for x being object holds

( x in b

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) holds

b

proof end;

:: deftheorem Def25 defines OSFreeGen OSAFREE:def 25 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for b_{4} being Subset of ( the Sorts of (FreeOSA X) . s) holds

( b_{4} = OSFreeGen (s,X) iff for x being object holds

( x in b_{4} iff ex a being object st

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for b

( b

( x in b

( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) );

registration

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let s be Element of S;

coherence

not OSFreeGen (s,X) is empty

end;
let X be V2() ManySortedSet of S;

let s be Element of S;

coherence

not OSFreeGen (s,X) is empty

proof end;

theorem Th30: :: OSAFREE:30

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S holds OSFreeGen (s,X) = { (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }

for X being V2() ManySortedSet of S

for s being Element of S holds OSFreeGen (s,X) = { (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }

proof end;

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being OSGeneratorSet of FreeOSA X st

for s being Element of S holds b_{1} . s = OSFreeGen (s,X)

for b_{1}, b_{2} being OSGeneratorSet of FreeOSA X st ( for s being Element of S holds b_{1} . s = OSFreeGen (s,X) ) & ( for s being Element of S holds b_{2} . s = OSFreeGen (s,X) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func OSFreeGen X -> OSGeneratorSet of FreeOSA X means :Def26: :: OSAFREE:def 26

for s being Element of S holds it . s = OSFreeGen (s,X);

existence for s being Element of S holds it . s = OSFreeGen (s,X);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def26 defines OSFreeGen OSAFREE:def 26 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being OSGeneratorSet of FreeOSA X holds

( b_{3} = OSFreeGen X iff for s being Element of S holds b_{3} . s = OSFreeGen (s,X) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

theorem Th31: :: OSAFREE:31

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds OSFreeGen X is V2()

for X being V2() ManySortedSet of S holds OSFreeGen X is V2()

proof end;

registration

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

coherence

OSFreeGen X is non-empty by Th31;

end;
let X be V2() ManySortedSet of S;

coherence

OSFreeGen X is non-empty by Th31;

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let R be OSCongruence of ParsedTermsOSA X;

let t be Element of TS (DTConOSA X);

ex b_{1} being Element of OSClass (R,(LeastSort t)) st

for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

b_{1} = OSClass (R,x)

for b_{1}, b_{2} being Element of OSClass (R,(LeastSort t)) st ( for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

b_{1} = OSClass (R,x) ) & ( for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

b_{2} = OSClass (R,x) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

let R be OSCongruence of ParsedTermsOSA X;

let t be Element of TS (DTConOSA X);

func OSClass (R,t) -> Element of OSClass (R,(LeastSort t)) means :Def27: :: OSAFREE:def 27

for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

it = OSClass (R,x);

existence for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

it = OSClass (R,x);

ex b

for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

b

proof end;

uniqueness for b

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

b

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

b

b

proof end;

:: deftheorem Def27 defines OSClass OSAFREE:def 27 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for R being OSCongruence of ParsedTermsOSA X

for t being Element of TS (DTConOSA X)

for b_{5} being Element of OSClass (R,(LeastSort t)) holds

( b_{5} = OSClass (R,t) iff for s being Element of S

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

b_{5} = OSClass (R,x) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for R being OSCongruence of ParsedTermsOSA X

for t being Element of TS (DTConOSA X)

for b

( b

for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds

b

theorem Th32: :: OSAFREE:32

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for R being OSCongruence of ParsedTermsOSA X

for t being Element of TS (DTConOSA X) holds t in OSClass (R,t)

for X being V2() ManySortedSet of S

for R being OSCongruence of ParsedTermsOSA X

for t being Element of TS (DTConOSA X) holds t in OSClass (R,t)

proof end;

theorem Th33: :: OSAFREE:33

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for t being Element of TS (DTConOSA X)

for x, x1 being set st x in X . s & t = root-tree [x,s] holds

( x1 in OSClass ((PTCongruence X),t) iff x1 = t )

for X being V2() ManySortedSet of S

for s being Element of S

for t being Element of TS (DTConOSA X)

for x, x1 being set st x in X . s & t = root-tree [x,s] holds

( x1 in OSClass ((PTCongruence X),t) iff x1 = t )

proof end;

theorem Th34: :: OSAFREE:34

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for R being OSCongruence of ParsedTermsOSA X

for t1, t2 being Element of TS (DTConOSA X) holds

( t2 in OSClass (R,t1) iff OSClass (R,t1) = OSClass (R,t2) )

for X being V2() ManySortedSet of S

for R being OSCongruence of ParsedTermsOSA X

for t1, t2 being Element of TS (DTConOSA X) holds

( t2 in OSClass (R,t1) iff OSClass (R,t1) = OSClass (R,t2) )

proof end;

theorem Th35: :: OSAFREE:35

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for R1, R2 being OSCongruence of ParsedTermsOSA X

for t being Element of TS (DTConOSA X) st R1 c= R2 holds

OSClass (R1,t) c= OSClass (R2,t)

for X being V2() ManySortedSet of S

for R1, R2 being OSCongruence of ParsedTermsOSA X

for t being Element of TS (DTConOSA X) st R1 c= R2 holds

OSClass (R1,t) c= OSClass (R2,t)

proof end;

theorem Th36: :: OSAFREE:36

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for t being Element of TS (DTConOSA X)

for x, x1 being set st x in X . s & t = root-tree [x,s] holds

( x1 in OSClass ((LCongruence X),t) iff x1 = t )

for X being V2() ManySortedSet of S

for s being Element of S

for t being Element of TS (DTConOSA X)

for x, x1 being set st x in X . s & t = root-tree [x,s] holds

( x1 in OSClass ((LCongruence X),t) iff x1 = t )

proof end;

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let A be V2() ManySortedSet of the carrier of S;

let F be ManySortedFunction of PTVars X,A;

let t be Symbol of (DTConOSA X);

assume A1: t in Terminals (DTConOSA X) ;

ex b_{1} being Element of Union A st

for f being Function st f = F . (t `2) holds

b_{1} = f . (root-tree t)

for b_{1}, b_{2} being Element of Union A st ( for f being Function st f = F . (t `2) holds

b_{1} = f . (root-tree t) ) & ( for f being Function st f = F . (t `2) holds

b_{2} = f . (root-tree t) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

let A be V2() ManySortedSet of the carrier of S;

let F be ManySortedFunction of PTVars X,A;

let t be Symbol of (DTConOSA X);

assume A1: t in Terminals (DTConOSA X) ;

func pi (F,A,t) -> Element of Union A means :Def28: :: OSAFREE:def 28

for f being Function st f = F . (t `2) holds

it = f . (root-tree t);

existence for f being Function st f = F . (t `2) holds

it = f . (root-tree t);

ex b

for f being Function st f = F . (t `2) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def28 defines pi OSAFREE:def 28 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for A being V2() ManySortedSet of the carrier of S

for F being ManySortedFunction of PTVars X,A

for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

for b_{6} being Element of Union A holds

( b_{6} = pi (F,A,t) iff for f being Function st f = F . (t `2) holds

b_{6} = f . (root-tree t) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for A being V2() ManySortedSet of the carrier of S

for F being ManySortedFunction of PTVars X,A

for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

for b

( b

b

theorem Th37: :: OSAFREE:37

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for U1 being non-empty monotone OSAlgebra of S

for f being ManySortedFunction of PTVars X, the Sorts of U1 ex h being ManySortedFunction of (ParsedTermsOSA X),U1 st

( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = f )

for X being V2() ManySortedSet of S

for U1 being non-empty monotone OSAlgebra of S

for f being ManySortedFunction of PTVars X, the Sorts of U1 ex h being ManySortedFunction of (ParsedTermsOSA X),U1 st

( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = f )

proof end;

:: NH stanbds for NatHom

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

let s be Element of S;

ex b_{1} being Function of (OSFreeGen (s,X)),(PTVars (s,X)) st

for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds

b_{1} . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t

for b_{1}, b_{2} being Function of (OSFreeGen (s,X)),(PTVars (s,X)) st ( for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds

b_{1} . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t ) & ( for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds

b_{2} . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

let s be Element of S;

func NHReverse (s,X) -> Function of (OSFreeGen (s,X)),(PTVars (s,X)) means :: OSAFREE:def 29

for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds

it . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t;

existence for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds

it . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t;

ex b

for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem defines NHReverse OSAFREE:def 29 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for b_{4} being Function of (OSFreeGen (s,X)),(PTVars (s,X)) holds

( b_{4} = NHReverse (s,X) iff for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds

b_{4} . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for s being Element of S

for b

( b

b

definition

let S be locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being ManySortedFunction of OSFreeGen X, PTVars X st

for s being Element of S holds b_{1} . s = NHReverse (s,X)

for b_{1}, b_{2} being ManySortedFunction of OSFreeGen X, PTVars X st ( for s being Element of S holds b_{1} . s = NHReverse (s,X) ) & ( for s being Element of S holds b_{2} . s = NHReverse (s,X) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func NHReverse X -> ManySortedFunction of OSFreeGen X, PTVars X means :: OSAFREE:def 30

for s being Element of S holds it . s = NHReverse (s,X);

existence for s being Element of S holds it . s = NHReverse (s,X);

ex b

for s being Element of S holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem defines NHReverse OSAFREE:def 30 :

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being ManySortedFunction of OSFreeGen X, PTVars X holds

( b_{3} = NHReverse X iff for s being Element of S holds b_{3} . s = NHReverse (s,X) );

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

theorem Th38: :: OSAFREE:38

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds OSFreeGen X is osfree

for X being V2() ManySortedSet of S holds OSFreeGen X is osfree

proof end;

theorem Th39: :: OSAFREE:39

for S being locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds FreeOSA X is osfree

for X being V2() ManySortedSet of S holds FreeOSA X is osfree

proof end;

registration

let S be locally_directed OrderSortedSign;

existence

ex b_{1} being non-empty monotone OSAlgebra of S st

( b_{1} is osfree & b_{1} is strict )

end;
existence

ex b

( b

proof end;

:: PTMin ... minimality of PTCongruence on regular signatures

:: minimal terms

:: minimal terms

definition

let S be monotone regular locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) st

( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b_{1} . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b_{1} . (nt -tree ts) = pi ((@ (X,nt)),(b_{1} * ts)) ) )

for b_{1}, b_{2} being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) st ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b_{1} . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b_{1} . (nt -tree ts) = pi ((@ (X,nt)),(b_{1} * ts)) ) & ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b_{2} . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b_{2} . (nt -tree ts) = pi ((@ (X,nt)),(b_{2} * ts)) ) holds

b_{1} = b_{2}

end;
let X be V2() ManySortedSet of S;

func PTMin X -> Function of (TS (DTConOSA X)),(TS (DTConOSA X)) means :Def31: :: OSAFREE:def 31

( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

it . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

it . (nt -tree ts) = pi ((@ (X,nt)),(it * ts)) ) );

existence ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

it . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

it . (nt -tree ts) = pi ((@ (X,nt)),(it * ts)) ) );

ex b

( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b

proof end;

uniqueness for b

b

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b

b

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b

b

proof end;

:: deftheorem Def31 defines PTMin OSAFREE:def 31 :

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) holds

( b_{3} = PTMin X iff ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds

b_{3} . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b_{3} . (nt -tree ts) = pi ((@ (X,nt)),(b_{3} * ts)) ) ) );

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

b

for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds

b

theorem Th40: :: OSAFREE:40

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X) holds

( (PTMin X) . t in OSClass ((PTCongruence X),t) & LeastSort ((PTMin X) . t) <= LeastSort t & ( for s being Element of S

for x being set st x in X . s & t = root-tree [x,s] holds

(PTMin X) . t = t ) & ( for o being OperSymbol of S

for ts being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots ts & t = (OSSym (o,X)) -tree ts holds

( LeastSorts ((PTMin X) * ts) <= the_arity_of o & OSSym (o,X) ==> roots ((PTMin X) * ts) & OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X) ==> roots ((PTMin X) * ts) & (PTMin X) . t = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X)) -tree ((PTMin X) * ts) ) ) )

for X being V2() ManySortedSet of S

for t being Element of TS (DTConOSA X) holds

( (PTMin X) . t in OSClass ((PTCongruence X),t) & LeastSort ((PTMin X) . t) <= LeastSort t & ( for s being Element of S

for x being set st x in X . s & t = root-tree [x,s] holds

(PTMin X) . t = t ) & ( for o being OperSymbol of S

for ts being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots ts & t = (OSSym (o,X)) -tree ts holds

( LeastSorts ((PTMin X) * ts) <= the_arity_of o & OSSym (o,X) ==> roots ((PTMin X) * ts) & OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X) ==> roots ((PTMin X) * ts) & (PTMin X) . t = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X)) -tree ((PTMin X) * ts) ) ) )

proof end;

theorem Th41: :: OSAFREE:41

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for t, t1 being Element of TS (DTConOSA X) st t1 in OSClass ((PTCongruence X),t) holds

(PTMin X) . t1 = (PTMin X) . t

for X being V2() ManySortedSet of S

for t, t1 being Element of TS (DTConOSA X) st t1 in OSClass ((PTCongruence X),t) holds

(PTMin X) . t1 = (PTMin X) . t

proof end;

theorem Th42: :: OSAFREE:42

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for t1, t2 being Element of TS (DTConOSA X) holds

( t2 in OSClass ((PTCongruence X),t1) iff (PTMin X) . t2 = (PTMin X) . t1 )

for X being V2() ManySortedSet of S

for t1, t2 being Element of TS (DTConOSA X) holds

( t2 in OSClass ((PTCongruence X),t1) iff (PTMin X) . t2 = (PTMin X) . t1 )

proof end;

theorem Th43: :: OSAFREE:43

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for t1 being Element of TS (DTConOSA X) holds (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1

for X being V2() ManySortedSet of S

for t1 being Element of TS (DTConOSA X) holds (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1

proof end;

theorem Th44: :: OSAFREE:44

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X

for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)

for X being V2() ManySortedSet of S

for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X

for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)

proof end;

theorem Th45: :: OSAFREE:45

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X holds PTCongruence X c= R

for X being V2() ManySortedSet of S

for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X holds PTCongruence X c= R

proof end;

:: minimality of PTCongruence

theorem :: OSAFREE:46

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds LCongruence X = PTCongruence X

for X being V2() ManySortedSet of S holds LCongruence X = PTCongruence X

proof end;

:: I would prefer attribute "minimal", but non-clusterable

definition

let S be monotone regular locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

ex b_{1} being Element of TS (DTConOSA X) st (PTMin X) . b_{1} = b_{1}

end;
let X be V2() ManySortedSet of S;

mode MinTerm of S,X -> Element of TS (DTConOSA X) means :Def32: :: OSAFREE:def 32

(PTMin X) . it = it;

existence (PTMin X) . it = it;

ex b

proof end;

:: deftheorem Def32 defines MinTerm OSAFREE:def 32 :

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b_{3} being Element of TS (DTConOSA X) holds

( b_{3} is MinTerm of S,X iff (PTMin X) . b_{3} = b_{3} );

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for b

( b

definition

let S be monotone regular locally_directed OrderSortedSign;

let X be V2() ManySortedSet of S;

correctness

coherence

rng (PTMin X) is Subset of (TS (DTConOSA X));

by RELAT_1:def 19;

end;
let X be V2() ManySortedSet of S;

correctness

coherence

rng (PTMin X) is Subset of (TS (DTConOSA X));

by RELAT_1:def 19;

:: deftheorem defines MinTerms OSAFREE:def 33 :

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds MinTerms X = rng (PTMin X);

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S holds MinTerms X = rng (PTMin X);

theorem :: OSAFREE:47

for S being monotone regular locally_directed OrderSortedSign

for X being V2() ManySortedSet of S

for x being set holds

( x is MinTerm of S,X iff x in MinTerms X )

for X being V2() ManySortedSet of S

for x being set holds

( x is MinTerm of S,X iff x in MinTerms X )

proof end;

:: changing to MSSubset and its OSCl, to make free algebras easier

:: no good way how to retypeOSCL into OSSubset now?