:: Free Order Sorted Universal Algebra
:: by Josef Urban
::
:: Received September 19, 2002
:: Copyright (c) 2002-2012 Association of Mizar Users


begin

:: REVISE: should rather be attribute
:: changing to MSSubset and its OSCl, to make free algebras easier
:: no good way how to retypeOSCL into OSSubset now?
definition
let S be OrderSortedSign;
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
 ex b1 being MSSubset of U0 st
for O being OSSubset of U0 st O = OSCl b1 holds
the Sorts of (GenOSAlg O) = the Sorts of U0
proofend;
end;

:: deftheorem Def1 defines OSGeneratorSet OSAFREE:def_1_:_
 for S being OrderSortedSign
for U0 being OSAlgebra of S
for b3 being MSSubset of U0 holds
( b3 is OSGeneratorSet of U0 iff for O being OSSubset of U0 st O = OSCl b3 holds
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 )
proofend;

:: 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
definition
let S be OrderSortedSign;
let U0 be monotone OSAlgebra of S;
let IT be OSGeneratorSet of U0;
attrIT 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 );
end;

:: 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 ) );

definition
let S be OrderSortedSign;
let IT be monotone OSAlgebra of S;
attrIT is osfree  means :: OSAFREE:def 3
 ex G being OSGeneratorSet of IT st G is osfree ;
end;

:: 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 );

begin

::
:: Construction of Free Order Sorted Algebras for Given Signature
::
definition
let S be OrderSortedSign;
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 ) &amp; ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x &amp; b . x in coprod (i,X) ) ) ) ) ) ) ) );
existence
 ex b1 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 b1 iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( 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 ) &amp; ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x &amp; b . x in coprod (i,X) ) ) ) ) ) ) ) )
proofend;
uniqueness
 for b1, b2 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 b1 iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( 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 ) &amp; ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x &amp; b . x in coprod (i,X) ) ) ) ) ) ) ) ) ) &amp; ( 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 b2 iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( 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 ) &amp; ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x &amp; b . x in coprod (i,X) ) ) ) ) ) ) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines OSREL OSAFREE:def_4_:_
 for S being OrderSortedSign
for X being ManySortedSet of S
for b3 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
( b3 = 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 b3 iff ( a in [: the carrier' of S,{ the carrier of S}:] &amp; ( for o being OperSymbol of S st [o, the carrier of S] = a holds
( len b = len (the_arity_of o) &amp; ( 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 ) &amp; ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x &amp; 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) &amp; ( 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 ) &amp; ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x &amp; b . x in coprod (i,X) ) ) ) ) ) )
proofend;

definition
let S be OrderSortedSign;
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
coherence
DTConstrStr(# ([: the carrier' of S,{ the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #) is DTConstrStr ;
;
end;

:: 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) #);

registration
let S be OrderSortedSign;
let X be ManySortedSet of S;
cluster DTConOSA X ->  non empty strict ;
coherence
 ( DTConOSA X is strict &amp; not DTConOSA X is empty ) ;
end;

theorem Th3: :: OSAFREE:3
for S being OrderSortedSign
for X being V16() ManySortedSet of S holds
( NonTerminals (DTConOSA X) = [: the carrier' of S,{ the carrier of S}:] &amp; Terminals (DTConOSA X) = Union (coprod X) )
proofend;

registration
let S be OrderSortedSign;
let X be V16() ManySortedSet of S;
cluster DTConOSA X ->  with_terminals with_nonterminals with_useful_nonterminals ;
coherence
 ( DTConOSA X is with_terminals &amp; DTConOSA X is with_nonterminals &amp; DTConOSA X is with_useful_nonterminals )
proofend;
end;

theorem Th4: :: OSAFREE:4
for S being OrderSortedSign
for X being V16() 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 &amp; t = [x,s] ) )
proofend;

:: have to rename
definition
let S be OrderSortedSign;
let X be V16() ManySortedSet of S;
let o be OperSymbol of S;
func OSSym (o,X) ->  Symbol of (DTConOSA X) equals :: OSAFREE:def 6
[o, the carrier of S];
coherence
 [o, the carrier of S] is Symbol of (DTConOSA X)
proofend;
end;

:: deftheorem  defines OSSym OSAFREE:def_6_:_
 for S being OrderSortedSign
for X being V16() 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 V16() 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 set st
( s1 <= s &amp; x in X . s1 &amp; a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} &amp; 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 set st
( s1 <= s &amp; x in X . s1 &amp; a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} &amp; the_result_sort_of o <= s ) )  }  is Subset of (TS (DTConOSA X))
proofend;
end;

:: deftheorem  defines ParsedTerms OSAFREE:def_7_:_
 for S being OrderSortedSign
for X being V16() 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 set st
( s1 <= s &amp; x in X . s1 &amp; a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} &amp; the_result_sort_of o <= s ) )  }  ;

registration
let S be OrderSortedSign;
let X be V16() ManySortedSet of S;
let s be Element of S;
cluster ParsedTerms (X,s) ->  non empty ;
coherence
 not ParsedTerms (X,s) is empty
proofend;
end;

definition
let S be OrderSortedSign;
let X be V16() 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
 ex b1 being OrderSortedSet of S st
for s being Element of S holds b1 . s = ParsedTerms (X,s)
proofend;
uniqueness
 for b1, b2 being OrderSortedSet of S st ( for s being Element of S holds b1 . s = ParsedTerms (X,s) ) &amp; ( for s being Element of S holds b2 . s = ParsedTerms (X,s) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines ParsedTerms OSAFREE:def_8_:_
 for S being OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being OrderSortedSet of S holds
( b3 = ParsedTerms X iff for s being Element of S holds b3 . s = ParsedTerms (X,s) );

registration
let S be OrderSortedSign;
let X be V16() ManySortedSet of S;
cluster ParsedTerms X -> V16() ;
coherence
 ParsedTerms X is non-empty
proofend;
end;

theorem Th5: :: OSAFREE:5
for S being OrderSortedSign
for X being V16() 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)
proofend;

theorem Th6: :: OSAFREE:6
for S being OrderSortedSign
for X being V16() 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) &amp; ( for n being Nat st n in dom p holds
p . n in ParsedTerms (X,((the_arity_of o) /. n)) ) ) )
proofend;

theorem Th7: :: OSAFREE:7
for S being OrderSortedSign
for X being V16() 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 )
proofend;

theorem Th8: :: OSAFREE:8
for S being OrderSortedSign
for X being V16() ManySortedSet of S holds union (rng (ParsedTerms X)) = TS (DTConOSA X)
proofend;

definition
let S be OrderSortedSign;
let X be V16() 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
 ex b1 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
b1 . p = (OSSym (o,X)) -tree p
proofend;
uniqueness
 for b1, b2 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
b1 . p = (OSSym (o,X)) -tree p ) &amp; ( for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
b2 . p = (OSSym (o,X)) -tree p ) holds
b1 = b2
proofend;
end;

:: deftheorem Def9 defines PTDenOp OSAFREE:def_9_:_
 for S being OrderSortedSign
for X being V16() ManySortedSet of S
for o being OperSymbol of S
for b4 being Function of ((((ParsedTerms X) #) * the Arity of S) . o),(((ParsedTerms X) * the ResultSort of S) . o) holds
( b4 = PTDenOp (o,X) iff for p being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots p holds
b4 . p = (OSSym (o,X)) -tree p );

definition
let S be OrderSortedSign;
let X be V16() 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
 ex b1 being ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S st
for o being OperSymbol of S holds b1 . o = PTDenOp (o,X)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S st ( for o being OperSymbol of S holds b1 . o = PTDenOp (o,X) ) &amp; ( for o being OperSymbol of S holds b2 . o = PTDenOp (o,X) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def10 defines PTOper OSAFREE:def_10_:_
 for S being OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being ManySortedFunction of ((ParsedTerms X) #) * the Arity of S,(ParsedTerms X) * the ResultSort of S holds
( b3 = PTOper X iff for o being OperSymbol of S holds b3 . o = PTDenOp (o,X) );

definition
let S be OrderSortedSign;
let X be V16() ManySortedSet of S;
func ParsedTermsOSA X ->  OSAlgebra of S equals :: OSAFREE:def 11
 MSAlgebra(# (ParsedTerms X),(PTOper X) #);
coherence
 MSAlgebra(# (ParsedTerms X),(PTOper X) #) is OSAlgebra of S by OSALG_1:17;
end;

:: deftheorem  defines ParsedTermsOSA OSAFREE:def_11_:_
 for S being OrderSortedSign
for X being V16() ManySortedSet of S holds ParsedTermsOSA X = MSAlgebra(# (ParsedTerms X),(PTOper X) #);

registration
let S be OrderSortedSign;
let X be V16() ManySortedSet of S;
cluster ParsedTermsOSA X ->  strict non-empty ;
coherence
 ( ParsedTermsOSA X is strict &amp; ParsedTermsOSA X is non-empty ) by MSUALG_1:def_3;
end;

definition
let S be OrderSortedSign;
let X be V16() 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)
proofend;
end;

theorem Th9: :: OSAFREE:9
for S being OrderSortedSign
for X being V16() 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 set st
( s1 <= s &amp; x in X . s1 &amp; a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o, the carrier of S] = a . {} &amp; the_result_sort_of o <= s ) )  }
proofend;

theorem Th10: :: OSAFREE:10
for S being OrderSortedSign
for X being V16() 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) &amp; ( for z being set holds [z, the carrier of S] <> (root-tree [x,s]) . {} ) &amp; ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) &amp; ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
proofend;

theorem Th11: :: OSAFREE:11
for S being OrderSortedSign
for X being V16() 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 &amp; OSSym (o,X) ==> roots p &amp; p in Args (o,(ParsedTermsOSA X)) &amp; t = (Den (o,(ParsedTermsOSA X))) . p ) &amp; ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) &amp; ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )
proofend;

theorem Th12: :: OSAFREE:12
for S being OrderSortedSign
for X being V16() 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) &amp; nt -tree ts in TS (DTConOSA X) &amp; ex o being OperSymbol of S st
( nt = [o, the carrier of S] &amp; ts in Args (o,(ParsedTermsOSA X)) &amp; nt -tree ts = (Den (o,(ParsedTermsOSA X))) . ts &amp; ( for s1 being Element of S holds
( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) ) )
proofend;

:: Element of Args is FinSequence (if clusters MSUALG_9)
theorem Th13: :: OSAFREE:13
for S being OrderSortedSign
for X being V16() 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) &amp; OSSym (o,X) ==> roots x ) )
proofend;

:: 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)
definition
let S be OrderSortedSign;
let X be V16() 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 &amp; ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
it <= s1 ) );
existence
 ex b1 being SortSymbol of S st
( t in the Sorts of (ParsedTermsOSA X) . b1 &amp; ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b1 <= s1 ) )
proofend;
uniqueness
 for b1, b2 being SortSymbol of S st t in the Sorts of (ParsedTermsOSA X) . b1 &amp; ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b1 <= s1 ) &amp; t in the Sorts of (ParsedTermsOSA X) . b2 &amp; ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b2 <= s1 ) holds
b1 = b2
proofend;
end;

:: deftheorem Def12 defines LeastSort OSAFREE:def_12_:_
 for S being OrderSortedSign
for X being V16() ManySortedSet of S
for t being Element of TS (DTConOSA X)
for b4 being SortSymbol of S holds
( b4 = LeastSort t iff ( t in the Sorts of (ParsedTermsOSA X) . b4 &amp; ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b4 <= s1 ) ) );

:: 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)
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;

theorem Th14: :: OSAFREE:14
for S being OrderSortedSign
for X being V16() ManySortedSet of S
for x being set holds
( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) )
proofend;

theorem Th15: :: OSAFREE:15
for S being OrderSortedSign
for X being V16() 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)
proofend;

theorem :: OSAFREE:16
for S being OrderSortedSign
for X being V16() 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
proofend;

theorem Th17: :: OSAFREE:17
for S being OrderSortedSign
for X being V16() 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
proofend;

:: WHY is this necessary??? bug?
registration
let S be OrderSortedSign;
let X be V16() ManySortedSet of S;
let o2 be OperSymbol of S;
cluster Args (o2,(ParsedTermsOSA X)) ->  non empty ;
coherence
 not Args (o2,(ParsedTermsOSA X)) is empty ;
end;

:: REVISE: was probably needed for casting, but try if
:: LeastSort * x does the work and if so, remove this
definition
let S be locally_directed OrderSortedSign;
let X be V16() 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 &amp; ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y &amp; it . y = LeastSort t ) ) );
existence
 ex b1 being Element of the carrier of S * st
( dom b1 = dom x &amp; ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y &amp; b1 . y = LeastSort t ) ) )
proofend;
uniqueness
 for b1, b2 being Element of the carrier of S * st dom b1 = dom x &amp; ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y &amp; b1 . y = LeastSort t ) ) &amp; dom b2 = dom x &amp; ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y &amp; b2 . y = LeastSort t ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def13 defines LeastSorts OSAFREE:def_13_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for x being FinSequence of TS (DTConOSA X)
for b4 being Element of the carrier of S * holds
( b4 = LeastSorts x iff ( dom b4 = dom x &amp; ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y &amp; b4 . y = LeastSort t ) ) ) );

:: all these should be generalized to any leastsorted osa
theorem Th18: :: OSAFREE:18
for S being locally_directed OrderSortedSign
for X being V16() 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)) )
proofend;

registration
cluster non empty non void V60() reflexive transitive antisymmetric order-sorted discernable monotone regular locally_directed for OverloadedRSSign ;
existence
 ex b1 being monotone OrderSortedSign st
( b1 is locally_directed &amp; b1 is regular )
proofend;
end;

:: just casting funcs necessary for the usage of schemes
definition
let S be monotone regular locally_directed OrderSortedSign;
let X be V16() 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
coherence
(OSSym ((LBound (o,(LeastSorts x))),X)) -tree x is Element of TS (DTConOSA X);
by A1, Th12;
end;

:: deftheorem Def14 defines pi OSAFREE:def_14_:_
 for S being monotone regular locally_directed OrderSortedSign
for X being V16() 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 V16() ManySortedSet of S;
let t be Symbol of (DTConOSA X);
assume A1: ex p being FinSequence st t ==> p ;
func @ (X,t) ->  OperSymbol of S means :Def15: :: OSAFREE:def 15
[it, the carrier of S] = t;
existence
 ex b1 being OperSymbol of S st [b1, the carrier of S] = t
proofend;
uniqueness
 for b1, b2 being OperSymbol of S st [b1, the carrier of S] = t &amp; [b2, the carrier of S] = t holds
b1 = b2 by XTUPLE_0:1;
end;

:: deftheorem Def15 defines @ OSAFREE:def_15_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for t being Symbol of (DTConOSA X) st ex p being FinSequence st t ==> p holds
for b4 being OperSymbol of S holds
( b4 = @ (X,t) iff [b4, the carrier of S] = t );

definition
let S be OrderSortedSign;
let X be V16() ManySortedSet of S;
let t be Symbol of (DTConOSA X);
assume A1: t in Terminals (DTConOSA X) ;
func pi t ->  Element of TS (DTConOSA X) equals :Def16: :: OSAFREE:def 16
 root-tree t;
correctness
coherence
root-tree t is Element of TS (DTConOSA X);
by A1, DTCONSTR:def_1;
end;

:: deftheorem Def16 defines pi OSAFREE:def_16_:_
 for S being OrderSortedSign
for X being V16() 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 V16() 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
 ex b1 being monotone OSCongruence of ParsedTermsOSA X st
for R being monotone OSCongruence of ParsedTermsOSA X holds b1 c= R
proofend;
uniqueness
 for b1, b2 being monotone OSCongruence of ParsedTermsOSA X st ( for R being monotone OSCongruence of ParsedTermsOSA X holds b1 c= R ) &amp; ( for R being monotone OSCongruence of ParsedTermsOSA X holds b2 c= R ) holds
b1 = b2
proofend;
end;

:: deftheorem Def17 defines LCongruence OSAFREE:def_17_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being monotone OSCongruence of ParsedTermsOSA X holds
( b3 = LCongruence X iff for R being monotone OSCongruence of ParsedTermsOSA X holds b3 c= R );

definition
let S be locally_directed OrderSortedSign;
let X be V16() ManySortedSet of S;
func FreeOSA X ->  strict non-empty monotone OSAlgebra of S equals :: OSAFREE:def 18
 QuotOSAlg ((ParsedTermsOSA X),(LCongruence X));
correctness
coherence
QuotOSAlg ((ParsedTermsOSA X),(LCongruence X)) is strict non-empty monotone OSAlgebra of S;
;
end;

:: deftheorem  defines FreeOSA OSAFREE:def_18_:_
 for S being locally_directed OrderSortedSign
for X being V16() 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
definition
let S be OrderSortedSign;
let X be V16() 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 &amp; t = [x,s] &amp; s <= s1 )  }  ;
correctness
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 &amp; t = [x,s] &amp; s <= s1 )  }  is Subset of [:(TS (DTConOSA X)), the carrier of S:];
proofend;
end;

:: deftheorem  defines @ OSAFREE:def_19_:_
 for S being OrderSortedSign
for X being V16() 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 &amp; t = [x,s] &amp; s <= s1 )  }  ;

definition
let S be OrderSortedSign;
let X be V16() 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] &amp; o1 ~= o2 &amp; len (the_arity_of o1) = len (the_arity_of o2) &amp; the_result_sort_of o1 <= s3 &amp; the_result_sort_of o2 <= s3 ) &amp; ex w3 being Element of the carrier of S * st
( dom w3 = dom x &amp; ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) )  }  ;
correctness
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] &amp; o1 ~= o2 &amp; len (the_arity_of o1) = len (the_arity_of o2) &amp; the_result_sort_of o1 <= s3 &amp; the_result_sort_of o2 <= s3 ) &amp; ex w3 being Element of the carrier of S * st
( dom w3 = dom x &amp; ( 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:];
proofend;
end;

:: deftheorem  defines @ OSAFREE:def_20_:_
 for S being OrderSortedSign
for X being V16() 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] &amp; o1 ~= o2 &amp; len (the_arity_of o1) = len (the_arity_of o2) &amp; the_result_sort_of o1 <= s3 &amp; the_result_sort_of o2 <= s3 ) &amp; ex w3 being Element of the carrier of S * st
( dom w3 = dom x &amp; ( 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 V16() 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 ) &amp; ( 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
 ex b1 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
b1 . (root-tree t) = @ t ) &amp; ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b1 . (nt -tree ts) = @ (nt,(b1 * ts)) ) )
proofend;
uniqueness
 for b1, b2 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
b1 . (root-tree t) = @ t ) &amp; ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b1 . (nt -tree ts) = @ (nt,(b1 * ts)) ) &amp; ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b2 . (root-tree t) = @ t ) &amp; ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b2 . (nt -tree ts) = @ (nt,(b2 * ts)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def21 defines PTClasses OSAFREE:def_21_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) holds
( b3 = PTClasses X iff ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b3 . (root-tree t) = @ t ) &amp; ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b3 . (nt -tree ts) = @ (nt,(b3 * ts)) ) ) );

theorem Th19: :: OSAFREE:19
for S being locally_directed OrderSortedSign
for X being V16() 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 ) ) &amp; ( 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 ) )
proofend;

:: switched to have easier prooving
theorem Th20: :: OSAFREE:20
for S being locally_directed OrderSortedSign
for X being V16() 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
proofend;

theorem Th21: :: OSAFREE:21
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for x, y being Element of TS (DTConOSA X)
for s1, s2 being Element of S st s1 <= s2 &amp; x in the Sorts of (ParsedTermsOSA X) . s1 &amp; y in the Sorts of (ParsedTermsOSA X) . s1 holds
( [y,s1] in (PTClasses X) . x iff [y,s2] in (PTClasses X) . x )
proofend;

theorem Th22: :: OSAFREE:22
for S being locally_directed OrderSortedSign
for X being V16() 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 &amp; [z,s] in (PTClasses X) . y holds
[x,s] in (PTClasses X) . z
proofend;

definition
let S be locally_directed OrderSortedSign;
let X be V16() 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
 ex b1 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X st
for i being set st i in the carrier of S holds
b1 . i =  {  [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y  }
proofend;
uniqueness
 for b1, b2 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X st ( for i being set st i in the carrier of S holds
b1 . i =  {  [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y  }  ) &amp; ( for i being set st i in the carrier of S holds
b2 . i =  {  [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y  }  ) holds
b1 = b2
proofend;
end;

:: deftheorem Def22 defines PTCongruence OSAFREE:def_22_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X holds
( b3 = PTCongruence X iff for i being set st i in the carrier of S holds
b3 . i =  {  [x,y] where x, y is Element of TS (DTConOSA X) : [x,i] in (PTClasses X) . y  }  );

theorem Th23: :: OSAFREE:23
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for x, y, s being set st [x,s] in (PTClasses X) . y holds
( x in TS (DTConOSA X) &amp; y in TS (DTConOSA X) &amp; s in the carrier of S )
proofend;

theorem Th24: :: OSAFREE:24
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for C being Component of S
for x, y being set holds
( [x,y] in CompClass ((PTCongruence X),C) iff ex s1 being Element of S st
( s1 in C &amp; [x,s1] in (PTClasses X) . y ) )
proofend;

theorem Th25: :: OSAFREE:25
for S being locally_directed OrderSortedSign
for X being V16() 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)
proofend;

:: more explicit description of PTCongruence
theorem Th26: :: OSAFREE:26
for S being locally_directed OrderSortedSign
for X being V16() 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 set st x in X . s1 holds
( ( s1 <= s2 implies [(root-tree [x,s1]),(root-tree [x,s1])] in R . s2 ) &amp; ( for y being set st ( [(root-tree [x,s1]),y] in R . s2 or [y,(root-tree [x,s1])] in R . s2 ) holds
( s1 <= s2 &amp; y = root-tree [x,s1] ) ) ) ) &amp; ( 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 &amp; len (the_arity_of o1) = len (the_arity_of o2) &amp; the_result_sort_of o1 <= s3 &amp; the_result_sort_of o2 <= s3 &amp; ex w3 being Element of the carrier of S * st
( dom w3 = dom x1 &amp; ( for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in R . (w3 /. y) ) ) ) ) ) ) )
proofend;

:: the minimality for regular oss is done later
theorem Th27: :: OSAFREE:27
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds PTCongruence X is monotone
proofend;

:: MSCongruence-like is ensured by the OSALG_4 cluster
registration
let S be locally_directed OrderSortedSign;
let X be V16() ManySortedSet of S;
cluster PTCongruence X ->  MSEquivalence-like monotone ;
coherence
 PTCongruence X is monotone by Th27;
end;

definition
let S be locally_directed OrderSortedSign;
let X be V16() 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 set holds
( x in it iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) );
existence
 ex b1 being Subset of ( the Sorts of (ParsedTermsOSA X) . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) )
proofend;
uniqueness
 for b1, b2 being Subset of ( the Sorts of (ParsedTermsOSA X) . s) st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) ) ) &amp; ( for x being set holds
( x in b2 iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def23 defines PTVars OSAFREE:def_23_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for s being Element of S
for b4 being Subset of ( the Sorts of (ParsedTermsOSA X) . s) holds
( b4 = PTVars (s,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . s &amp; x = root-tree [a,s] ) ) );

registration
let S be locally_directed OrderSortedSign;
let X be V16() ManySortedSet of S;
let s be Element of S;
cluster PTVars (s,X) ->  non empty ;
coherence
 not PTVars (s,X) is empty
proofend;
end;

theorem Th28: :: OSAFREE:28
for S being locally_directed OrderSortedSign
for X being V16() 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) &amp; t `2 = s )  }
proofend;

definition
let S be locally_directed OrderSortedSign;
let X be V16() 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
 ex b1 being MSSubset of (ParsedTermsOSA X) st
for s being Element of S holds b1 . s = PTVars (s,X)
proofend;
uniqueness
 for b1, b2 being MSSubset of (ParsedTermsOSA X) st ( for s being Element of S holds b1 . s = PTVars (s,X) ) &amp; ( for s being Element of S holds b2 . s = PTVars (s,X) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def24 defines PTVars OSAFREE:def_24_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being MSSubset of (ParsedTermsOSA X) holds
( b3 = PTVars X iff for s being Element of S holds b3 . s = PTVars (s,X) );

theorem :: OSAFREE:29
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds PTVars X is V16()
proofend;

definition
let S be locally_directed OrderSortedSign;
let X be V16() 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 set holds
( x in it iff ex a being set st
( a in X . s &amp; x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) );
existence
 ex b1 being Subset of ( the Sorts of (FreeOSA X) . s) st
for x being set holds
( x in b1 iff ex a being set st
( a in X . s &amp; x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) )
proofend;
uniqueness
 for b1, b2 being Subset of ( the Sorts of (FreeOSA X) . s) st ( for x being set holds
( x in b1 iff ex a being set st
( a in X . s &amp; x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) &amp; ( for x being set holds
( x in b2 iff ex a being set st
( a in X . s &amp; x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def25 defines OSFreeGen OSAFREE:def_25_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for s being Element of S
for b4 being Subset of ( the Sorts of (FreeOSA X) . s) holds
( b4 = OSFreeGen (s,X) iff for x being set holds
( x in b4 iff ex a being set st
( a in X . s &amp; x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) );

registration
let S be locally_directed OrderSortedSign;
let X be V16() ManySortedSet of S;
let s be Element of S;
cluster OSFreeGen (s,X) ->  non empty ;
coherence
 not OSFreeGen (s,X) is empty
proofend;
end;

theorem Th30: :: OSAFREE:30
for S being locally_directed OrderSortedSign
for X being V16() 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) &amp; t `2 = s )  }
proofend;

definition
let S be locally_directed OrderSortedSign;
let X be V16() 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
 ex b1 being OSGeneratorSet of FreeOSA X st
for s being Element of S holds b1 . s = OSFreeGen (s,X)
proofend;
uniqueness
 for b1, b2 being OSGeneratorSet of FreeOSA X st ( for s being Element of S holds b1 . s = OSFreeGen (s,X) ) &amp; ( for s being Element of S holds b2 . s = OSFreeGen (s,X) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def26 defines OSFreeGen OSAFREE:def_26_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being OSGeneratorSet of FreeOSA X holds
( b3 = OSFreeGen X iff for s being Element of S holds b3 . s = OSFreeGen (s,X) );

theorem Th31: :: OSAFREE:31
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds OSFreeGen X is V16()
proofend;

registration
let S be locally_directed OrderSortedSign;
let X be V16() ManySortedSet of S;
cluster OSFreeGen X -> V16() ;
coherence
 OSFreeGen X is non-empty by Th31;
end;

definition
let S be locally_directed OrderSortedSign;
let X be V16() 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
 ex b1 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
b1 = OSClass (R,x)
proofend;
uniqueness
 for b1, b2 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
b1 = OSClass (R,x) ) &amp; ( for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s st t = x holds
b2 = OSClass (R,x) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def27 defines OSClass OSAFREE:def_27_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for R being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X)
for b5 being Element of OSClass (R,(LeastSort t)) holds
( b5 = 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
b5 = OSClass (R,x) );

theorem Th32: :: OSAFREE:32
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for R being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds t in OSClass (R,t)
proofend;

theorem Th33: :: OSAFREE:33
for S being locally_directed OrderSortedSign
for X being V16() 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 &amp; t = root-tree [x,s] holds
( x1 in OSClass ((PTCongruence X),t) iff x1 = t )
proofend;

theorem Th34: :: OSAFREE:34
for S being locally_directed OrderSortedSign
for X being V16() 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) )
proofend;

theorem Th35: :: OSAFREE:35
for S being locally_directed OrderSortedSign
for X being V16() 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)
proofend;

theorem Th36: :: OSAFREE:36
for S being locally_directed OrderSortedSign
for X being V16() 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 &amp; t = root-tree [x,s] holds
( x1 in OSClass ((LCongruence X),t) iff x1 = t )
proofend;

definition
let S be locally_directed OrderSortedSign;
let X be V16() ManySortedSet of S;
let A be V16() 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
 ex b1 being Element of Union A st
for f being Function st f = F . (t `2) holds
b1 = f . (root-tree t)
proofend;
uniqueness
 for b1, b2 being Element of Union A st ( for f being Function st f = F . (t `2) holds
b1 = f . (root-tree t) ) &amp; ( for f being Function st f = F . (t `2) holds
b2 = f . (root-tree t) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def28 defines pi OSAFREE:def_28_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for A being V16() 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 b6 being Element of Union A holds
( b6 = pi (F,A,t) iff for f being Function st f = F . (t `2) holds
b6 = f . (root-tree t) );

theorem Th37: :: OSAFREE:37
for S being locally_directed OrderSortedSign
for X being V16() 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 &amp; h is order-sorted &amp; h || (PTVars X) = f )
proofend;

:: NH stanbds for NatHom
definition
let S be locally_directed OrderSortedSign;
let X be V16() 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
 ex b1 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
b1 . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t
proofend;
uniqueness
 for b1, b2 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
b1 . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t ) &amp; ( for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds
b2 . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines NHReverse OSAFREE:def_29_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for s being Element of S
for b4 being Function of (OSFreeGen (s,X)),(PTVars (s,X)) holds
( b4 = 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
b4 . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t );

definition
let S be locally_directed OrderSortedSign;
let X be V16() 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
 ex b1 being ManySortedFunction of OSFreeGen X, PTVars X st
for s being Element of S holds b1 . s = NHReverse (s,X)
proofend;
uniqueness
 for b1, b2 being ManySortedFunction of OSFreeGen X, PTVars X st ( for s being Element of S holds b1 . s = NHReverse (s,X) ) &amp; ( for s being Element of S holds b2 . s = NHReverse (s,X) ) holds
b1 = b2
proofend;
end;

:: deftheorem  defines NHReverse OSAFREE:def_30_:_
 for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being ManySortedFunction of OSFreeGen X, PTVars X holds
( b3 = NHReverse X iff for s being Element of S holds b3 . s = NHReverse (s,X) );

theorem Th38: :: OSAFREE:38
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds OSFreeGen X is osfree
proofend;

theorem Th39: :: OSAFREE:39
for S being locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds FreeOSA X is osfree
proofend;

registration
let S be locally_directed OrderSortedSign;
cluster strict non-empty order-sorted monotone osfree for MSAlgebra over S;
existence
 ex b1 being non-empty monotone OSAlgebra of S st
( b1 is osfree &amp; b1 is strict )
proofend;
end;

begin

:: PTMin ... minimality of PTCongruence on regular signatures
:: minimal terms
definition
let S be monotone regular locally_directed OrderSortedSign;
let X be V16() 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 ) &amp; ( 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
 ex b1 being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) st
( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b1 . (root-tree t) = pi t ) &amp; ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b1 . (nt -tree ts) = pi ((@ (X,nt)),(b1 * ts)) ) )
proofend;
uniqueness
 for b1, b2 being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) st ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b1 . (root-tree t) = pi t ) &amp; ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b1 . (nt -tree ts) = pi ((@ (X,nt)),(b1 * ts)) ) &amp; ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b2 . (root-tree t) = pi t ) &amp; ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b2 . (nt -tree ts) = pi ((@ (X,nt)),(b2 * ts)) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def31 defines PTMin OSAFREE:def_31_:_
 for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) holds
( b3 = PTMin X iff ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b3 . (root-tree t) = pi t ) &amp; ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b3 . (nt -tree ts) = pi ((@ (X,nt)),(b3 * ts)) ) ) );

theorem Th40: :: OSAFREE:40
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for t being Element of TS (DTConOSA X) holds
( (PTMin X) . t in OSClass ((PTCongruence X),t) &amp; LeastSort ((PTMin X) . t) <= LeastSort t &amp; ( for s being Element of S
for x being set st x in X . s &amp; t = root-tree [x,s] holds
(PTMin X) . t = t ) &amp; ( for o being OperSymbol of S
for ts being FinSequence of TS (DTConOSA X) st OSSym (o,X) ==> roots ts &amp; t = (OSSym (o,X)) -tree ts holds
( LeastSorts ((PTMin X) * ts) <= the_arity_of o &amp; OSSym (o,X) ==> roots ((PTMin X) * ts) &amp; OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X) ==> roots ((PTMin X) * ts) &amp; (PTMin X) . t = (OSSym ((LBound (o,(LeastSorts ((PTMin X) * ts)))),X)) -tree ((PTMin X) * ts) ) ) )
proofend;

theorem Th41: :: OSAFREE:41
for S being monotone regular locally_directed OrderSortedSign
for X being V16() 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
proofend;

theorem Th42: :: OSAFREE:42
for S being monotone regular locally_directed OrderSortedSign
for X being V16() 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 )
proofend;

theorem Th43: :: OSAFREE:43
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for t1 being Element of TS (DTConOSA X) holds (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1
proofend;

theorem Th44: :: OSAFREE:44
for S being monotone regular locally_directed OrderSortedSign
for X being V16() 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)
proofend;

theorem Th45: :: OSAFREE:45
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X holds PTCongruence X c= R
proofend;

:: minimality of PTCongruence
theorem :: OSAFREE:46
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds LCongruence X = PTCongruence X
proofend;

:: I would prefer attribute "minimal", but non-clusterable
definition
let S be monotone regular locally_directed OrderSortedSign;
let X be V16() ManySortedSet of S;
mode MinTerm of S,X ->  Element of TS (DTConOSA X) means :Def32: :: OSAFREE:def 32
(PTMin X) . it = it;
existence
 ex b1 being Element of TS (DTConOSA X) st (PTMin X) . b1 = b1
proofend;
end;

:: deftheorem Def32 defines MinTerm OSAFREE:def_32_:_
 for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for b3 being Element of TS (DTConOSA X) holds
( b3 is MinTerm of S,X iff (PTMin X) . b3 = b3 );

definition
let S be monotone regular locally_directed OrderSortedSign;
let X be V16() ManySortedSet of S;
func MinTerms X ->  Subset of (TS (DTConOSA X)) equals :: OSAFREE:def 33
 rng (PTMin X);
correctness
coherence
rng (PTMin X) is Subset of (TS (DTConOSA X));
by RELAT_1:def_19;
end;

:: deftheorem  defines MinTerms OSAFREE:def_33_:_
 for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S holds MinTerms X = rng (PTMin X);

theorem :: OSAFREE:47
for S being monotone regular locally_directed OrderSortedSign
for X being V16() ManySortedSet of S
for x being set holds
( x is MinTerm of S,X iff x in MinTerms X )
proofend;