:: OSAFREE semantic presentation

definition
let c1 be OrderSortedSign;
let c2 be OSAlgebra of c1;
mode OSGeneratorSet of c2 -> MSSubset of a2 means :Def1: :: OSAFREE:def 1
for b1 being OSSubset of a2 st b1 = OSCl a3 holds
the Sorts of (GenOSAlg b1) = the Sorts of a2;
existence
ex b1 being MSSubset of c2 st
for b2 being OSSubset of c2 st b2 = OSCl b1 holds
the Sorts of (GenOSAlg b2) = the Sorts of c2
proof end;
end;

:: deftheorem Def1 defines OSGeneratorSet OSAFREE:def 1 :
for b1 being OrderSortedSign
for b2 being OSAlgebra of b1
for b3 being MSSubset of b2 holds
( b3 is OSGeneratorSet of b2 iff for b4 being OSSubset of b2 st b4 = OSCl b3 holds
the Sorts of (GenOSAlg b4) = the Sorts of b2 );

theorem Th1: :: OSAFREE:1
for b1 being OrderSortedSign
for b2 being strict non-empty OSAlgebra of b1
for b3 being MSSubset of b2 holds
( b3 is OSGeneratorSet of b2 iff for b4 being OSSubset of b2 st b4 = OSCl b3 holds
GenOSAlg b4 = b2 )
proof end;

definition
let c1 be OrderSortedSign;
let c2 be monotone OSAlgebra of c1;
let c3 be OSGeneratorSet of c2;
attr a3 is osfree means :: OSAFREE:def 2
for b1 being non-empty monotone OSAlgebra of a1
for b2 being ManySortedFunction of a3,the Sorts of b1 ex b3 being ManySortedFunction of a2,b1 st
( b3 is_homomorphism a2,b1 & b3 is order-sorted & b3 || a3 = b2 );
end;

:: deftheorem Def2 defines osfree OSAFREE:def 2 :
for b1 being OrderSortedSign
for b2 being monotone OSAlgebra of b1
for b3 being OSGeneratorSet of b2 holds
( b3 is osfree iff for b4 being non-empty monotone OSAlgebra of b1
for b5 being ManySortedFunction of b3,the Sorts of b4 ex b6 being ManySortedFunction of b2,b4 st
( b6 is_homomorphism b2,b4 & b6 is order-sorted & b6 || b3 = b5 ) );

definition
let c1 be OrderSortedSign;
let c2 be monotone OSAlgebra of c1;
attr a2 is osfree means :: OSAFREE:def 3
ex b1 being OSGeneratorSet of a2 st b1 is osfree;
end;

:: deftheorem Def3 defines osfree OSAFREE:def 3 :
for b1 being OrderSortedSign
for b2 being monotone OSAlgebra of b1 holds
( b2 is osfree iff ex b3 being OSGeneratorSet of b2 st b3 is osfree );

definition
let c1 be OrderSortedSign;
let c2 be ManySortedSet of c1;
func OSREL c2 -> Relation of [:the OperSymbols of a1,{the carrier of a1}:] \/ (Union (coprod a2)),([:the OperSymbols of a1,{the carrier of a1}:] \/ (Union (coprod a2))) * means :Def4: :: OSAFREE:def 4
for b1 being Element of [:the OperSymbols of a1,{the carrier of a1}:] \/ (Union (coprod a2))
for b2 being Element of ([:the OperSymbols of a1,{the carrier of a1}:] \/ (Union (coprod a2))) * holds
( [b1,b2] in a3 iff ( b1 in [:the OperSymbols of a1,{the carrier of a1}:] & ( for b3 being OperSymbol of a1 st [b3,the carrier of a1] = b1 holds
( len b2 = len (the_arity_of b3) & ( for b4 being set st b4 in dom b2 holds
( ( b2 . b4 in [:the OperSymbols of a1,{the carrier of a1}:] implies for b5 being OperSymbol of a1 st [b5,the carrier of a1] = b2 . b4 holds
the_result_sort_of b5 <= (the_arity_of b3) /. b4 ) & ( b2 . b4 in Union (coprod a2) implies ex b5 being Element of a1 st
( b5 <= (the_arity_of b3) /. b4 & b2 . b4 in coprod b5,a2 ) ) ) ) ) ) ) );
existence
ex b1 being Relation of [:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2)),([:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))) * st
for b2 being Element of [:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))
for b3 being Element of ([:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))) * holds
( [b2,b3] in b1 iff ( b2 in [:the OperSymbols of c1,{the carrier of c1}:] & ( for b4 being OperSymbol of c1 st [b4,the carrier of c1] = b2 holds
( len b3 = len (the_arity_of b4) & ( for b5 being set st b5 in dom b3 holds
( ( b3 . b5 in [:the OperSymbols of c1,{the carrier of c1}:] implies for b6 being OperSymbol of c1 st [b6,the carrier of c1] = b3 . b5 holds
the_result_sort_of b6 <= (the_arity_of b4) /. b5 ) & ( b3 . b5 in Union (coprod c2) implies ex b6 being Element of c1 st
( b6 <= (the_arity_of b4) /. b5 & b3 . b5 in coprod b6,c2 ) ) ) ) ) ) ) )
proof end;
uniqueness
for b1, b2 being Relation of [:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2)),([:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))) * st ( for b3 being Element of [:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))
for b4 being Element of ([:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))) * holds
( [b3,b4] in b1 iff ( b3 in [:the OperSymbols of c1,{the carrier of c1}:] & ( for b5 being OperSymbol of c1 st [b5,the carrier of c1] = b3 holds
( len b4 = len (the_arity_of b5) & ( for b6 being set st b6 in dom b4 holds
( ( b4 . b6 in [:the OperSymbols of c1,{the carrier of c1}:] implies for b7 being OperSymbol of c1 st [b7,the carrier of c1] = b4 . b6 holds
the_result_sort_of b7 <= (the_arity_of b5) /. b6 ) & ( b4 . b6 in Union (coprod c2) implies ex b7 being Element of c1 st
( b7 <= (the_arity_of b5) /. b6 & b4 . b6 in coprod b7,c2 ) ) ) ) ) ) ) ) ) & ( for b3 being Element of [:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))
for b4 being Element of ([:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))) * holds
( [b3,b4] in b2 iff ( b3 in [:the OperSymbols of c1,{the carrier of c1}:] & ( for b5 being OperSymbol of c1 st [b5,the carrier of c1] = b3 holds
( len b4 = len (the_arity_of b5) & ( for b6 being set st b6 in dom b4 holds
( ( b4 . b6 in [:the OperSymbols of c1,{the carrier of c1}:] implies for b7 being OperSymbol of c1 st [b7,the carrier of c1] = b4 . b6 holds
the_result_sort_of b7 <= (the_arity_of b5) /. b6 ) & ( b4 . b6 in Union (coprod c2) implies ex b7 being Element of c1 st
( b7 <= (the_arity_of b5) /. b6 & b4 . b6 in coprod b7,c2 ) ) ) ) ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines OSREL OSAFREE:def 4 :
for b1 being OrderSortedSign
for b2 being ManySortedSet of b1
for b3 being Relation of [:the OperSymbols of b1,{the carrier of b1}:] \/ (Union (coprod b2)),([:the OperSymbols of b1,{the carrier of b1}:] \/ (Union (coprod b2))) * holds
( b3 = OSREL b2 iff for b4 being Element of [:the OperSymbols of b1,{the carrier of b1}:] \/ (Union (coprod b2))
for b5 being Element of ([:the OperSymbols of b1,{the carrier of b1}:] \/ (Union (coprod b2))) * holds
( [b4,b5] in b3 iff ( b4 in [:the OperSymbols of b1,{the carrier of b1}:] & ( for b6 being OperSymbol of b1 st [b6,the carrier of b1] = b4 holds
( len b5 = len (the_arity_of b6) & ( for b7 being set st b7 in dom b5 holds
( ( b5 . b7 in [:the OperSymbols of b1,{the carrier of b1}:] implies for b8 being OperSymbol of b1 st [b8,the carrier of b1] = b5 . b7 holds
the_result_sort_of b8 <= (the_arity_of b6) /. b7 ) & ( b5 . b7 in Union (coprod b2) implies ex b8 being Element of b1 st
( b8 <= (the_arity_of b6) /. b7 & b5 . b7 in coprod b8,b2 ) ) ) ) ) ) ) ) );

theorem Th2: :: OSAFREE:2
for b1 being OrderSortedSign
for b2 being ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being Element of ([:the OperSymbols of b1,{the carrier of b1}:] \/ (Union (coprod b2))) * holds
( [[b3,the carrier of b1],b4] in OSREL b2 iff ( len b4 = len (the_arity_of b3) & ( for b5 being set st b5 in dom b4 holds
( ( b4 . b5 in [:the OperSymbols of b1,{the carrier of b1}:] implies for b6 being OperSymbol of b1 st [b6,the carrier of b1] = b4 . b5 holds
the_result_sort_of b6 <= (the_arity_of b3) /. b5 ) & ( b4 . b5 in Union (coprod b2) implies ex b6 being Element of b1 st
( b6 <= (the_arity_of b3) /. b5 & b4 . b5 in coprod b6,b2 ) ) ) ) ) )
proof end;

definition
let c1 be OrderSortedSign;
let c2 be ManySortedSet of c1;
func DTConOSA c2 -> DTConstrStr equals :: OSAFREE:def 5
 DTConstrStr(# ([:the OperSymbols of a1,{the carrier of a1}:] \/ (Union (coprod a2))),(OSREL a2) #);
correctness
coherence
DTConstrStr(# ([:the OperSymbols of c1,{the carrier of c1}:] \/ (Union (coprod c2))),(OSREL c2) #) is DTConstrStr ;
;
end;

:: deftheorem Def5 defines DTConOSA OSAFREE:def 5 :
for b1 being OrderSortedSign
for b2 being ManySortedSet of b1 holds DTConOSA b2 = DTConstrStr(# ([:the OperSymbols of b1,{the carrier of b1}:] \/ (Union (coprod b2))),(OSREL b2) #);

registration
let c1 be OrderSortedSign;
let c2 be ManySortedSet of c1;
cluster DTConOSA a2 -> non empty strict ;
coherence
( DTConOSA c2 is strict & not DTConOSA c2 is empty ) ;
end;

theorem Th3: :: OSAFREE:3
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds
( NonTerminals (DTConOSA b2) = [:the OperSymbols of b1,{the carrier of b1}:] & Terminals (DTConOSA b2) = Union (coprod b2) )
proof end;

registration
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
cluster DTConOSA a2 -> non empty strict with_terminals with_nonterminals with_useful_nonterminals ;
coherence
( DTConOSA c2 is with_terminals & DTConOSA c2 is with_nonterminals & DTConOSA c2 is with_useful_nonterminals )
proof end;
end;

theorem Th4: :: OSAFREE:4
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being set holds
( b3 in Terminals (DTConOSA b2) iff ex b4 being Element of b1ex b5 being set st
( b5 in b2 . b4 & b3 = [b5,b4] ) )
proof end;

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be OperSymbol of c1;
func OSSym c3,c2 -> Symbol of (DTConOSA a2) equals :: OSAFREE:def 6
[a3,the carrier of a1];
coherence
[c3,the carrier of c1] is Symbol of (DTConOSA c2)
proof end;
end;

:: deftheorem Def6 defines OSSym OSAFREE:def 6 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1 holds OSSym b3,b2 = [b3,the carrier of b1];

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of c1;
func ParsedTerms c2,c3 -> Subset of (TS (DTConOSA a2)) equals :: OSAFREE:def 7
{ b1 where B is Element of TS (DTConOSA a2) : ( ex b1 being Element of a1ex b2 being set st
( b2 <= a3 & b3 in a2 . b2 & b1 = root-tree [b3,b2] ) or ex b1 being OperSymbol of a1 st
( [b2,the carrier of a1] = b1 . {} & the_result_sort_of b2 <= a3 ) ) } ;
coherence
{ b1 where B is Element of TS (DTConOSA c2) : ( ex b1 being Element of c1ex b2 being set st
( b2 <= c3 & b3 in c2 . b2 & b1 = root-tree [b3,b2] ) or ex b1 being OperSymbol of c1 st
( [b2,the carrier of c1] = b1 . {} & the_result_sort_of b2 <= c3 ) ) } is Subset of (TS (DTConOSA c2))
proof end;
end;

:: deftheorem Def7 defines ParsedTerms OSAFREE:def 7 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1 holds ParsedTerms b2,b3 = { b4 where B is Element of TS (DTConOSA b2) : ( ex b1 being Element of b1ex b2 being set st
( b5 <= b3 & b6 in b2 . b5 & b4 = root-tree [b6,b5] ) or ex b1 being OperSymbol of b1 st
( [b5,the carrier of b1] = b4 . {} & the_result_sort_of b5 <= b3 ) ) } ;

registration
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of c1;
cluster ParsedTerms a2,a3 -> non empty ;
coherence
not ParsedTerms c2,c3 is empty
proof end;
end;

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func ParsedTerms c2 -> OrderSortedSet of a1 means :Def8: :: OSAFREE:def 8
for b1 being Element of a1 holds a3 . b1 = ParsedTerms a2,b1;
existence
ex b1 being OrderSortedSet of c1 st
for b2 being Element of c1 holds b1 . b2 = ParsedTerms c2,b2
proof end;
uniqueness
for b1, b2 being OrderSortedSet of c1 st ( for b3 being Element of c1 holds b1 . b3 = ParsedTerms c2,b3 ) & ( for b3 being Element of c1 holds b2 . b3 = ParsedTerms c2,b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def8 defines ParsedTerms OSAFREE:def 8 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OrderSortedSet of b1 holds
( b3 = ParsedTerms b2 iff for b4 being Element of b1 holds b3 . b4 = ParsedTerms b2,b4 );

registration
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
cluster ParsedTerms a2 -> V3 ;
coherence
ParsedTerms c2 is non-empty
proof end;
end;

theorem Th5: :: OSAFREE:5
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being set st b4 in (((ParsedTerms b2) # ) * the Arity of b1) . b3 holds
b4 is FinSequence of TS (DTConOSA b2)
proof end;

theorem Th6: :: OSAFREE:6
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being FinSequence of TS (DTConOSA b2) holds
( b4 in (((ParsedTerms b2) # ) * the Arity of b1) . b3 iff ( dom b4 = dom (the_arity_of b3) & ( for b5 being Nat st b5 in dom b4 holds
b4 . b5 in ParsedTerms b2,((the_arity_of b3) /. b5) ) ) )
proof end;

theorem Th7: :: OSAFREE:7
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being FinSequence of TS (DTConOSA b2) holds
( OSSym b3,b2 ==> roots b4 iff b4 in (((ParsedTerms b2) # ) * the Arity of b1) . b3 )
proof end;

theorem Th8: :: OSAFREE:8
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds union (rng (ParsedTerms b2)) = TS (DTConOSA b2)
proof end;

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be OperSymbol of c1;
func PTDenOp c3,c2 -> Function of (((ParsedTerms a2) # ) * the Arity of a1) . a3,((ParsedTerms a2) * the ResultSort of a1) . a3 means :Def9: :: OSAFREE:def 9
for b1 being FinSequence of TS (DTConOSA a2) st OSSym a3,a2 ==> roots b1 holds
a4 . b1 = (OSSym a3,a2) -tree b1;
existence
ex b1 being Function of (((ParsedTerms c2) # ) * the Arity of c1) . c3,((ParsedTerms c2) * the ResultSort of c1) . c3 st
for b2 being FinSequence of TS (DTConOSA c2) st OSSym c3,c2 ==> roots b2 holds
b1 . b2 = (OSSym c3,c2) -tree b2
proof end;
uniqueness
for b1, b2 being Function of (((ParsedTerms c2) # ) * the Arity of c1) . c3,((ParsedTerms c2) * the ResultSort of c1) . c3 st ( for b3 being FinSequence of TS (DTConOSA c2) st OSSym c3,c2 ==> roots b3 holds
b1 . b3 = (OSSym c3,c2) -tree b3 ) & ( for b3 being FinSequence of TS (DTConOSA c2) st OSSym c3,c2 ==> roots b3 holds
b2 . b3 = (OSSym c3,c2) -tree b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines PTDenOp OSAFREE:def 9 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being Function of (((ParsedTerms b2) # ) * the Arity of b1) . b3,((ParsedTerms b2) * the ResultSort of b1) . b3 holds
( b4 = PTDenOp b3,b2 iff for b5 being FinSequence of TS (DTConOSA b2) st OSSym b3,b2 ==> roots b5 holds
b4 . b5 = (OSSym b3,b2) -tree b5 );

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func PTOper c2 -> ManySortedFunction of ((ParsedTerms a2) # ) * the Arity of a1,(ParsedTerms a2) * the ResultSort of a1 means :Def10: :: OSAFREE:def 10
for b1 being OperSymbol of a1 holds a3 . b1 = PTDenOp b1,a2;
existence
ex b1 being ManySortedFunction of ((ParsedTerms c2) # ) * the Arity of c1,(ParsedTerms c2) * the ResultSort of c1 st
for b2 being OperSymbol of c1 holds b1 . b2 = PTDenOp b2,c2
proof end;
uniqueness
for b1, b2 being ManySortedFunction of ((ParsedTerms c2) # ) * the Arity of c1,(ParsedTerms c2) * the ResultSort of c1 st ( for b3 being OperSymbol of c1 holds b1 . b3 = PTDenOp b3,c2 ) & ( for b3 being OperSymbol of c1 holds b2 . b3 = PTDenOp b3,c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines PTOper OSAFREE:def 10 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being ManySortedFunction of ((ParsedTerms b2) # ) * the Arity of b1,(ParsedTerms b2) * the ResultSort of b1 holds
( b3 = PTOper b2 iff for b4 being OperSymbol of b1 holds b3 . b4 = PTDenOp b4,b2 );

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func ParsedTermsOSA c2 -> OSAlgebra of a1 equals :: OSAFREE:def 11
 MSAlgebra(# (ParsedTerms a2),(PTOper a2) #);
coherence
MSAlgebra(# (ParsedTerms c2),(PTOper c2) #) is OSAlgebra of c1 by OSALG_1:17;
end;

:: deftheorem Def11 defines ParsedTermsOSA OSAFREE:def 11 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds ParsedTermsOSA b2 = MSAlgebra(# (ParsedTerms b2),(PTOper b2) #);

registration
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
cluster ParsedTermsOSA a2 -> strict non-empty ;
coherence
( ParsedTermsOSA c2 is strict & ParsedTermsOSA c2 is non-empty ) by MSUALG_1:def 8;
end;

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be OperSymbol of c1;
redefine func OSSym as OSSym c3,c2 -> NonTerminal of (DTConOSA a2);
coherence
OSSym c3,c2 is NonTerminal of (DTConOSA c2)
proof end;
end;

theorem Th9: :: OSAFREE:9
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1 holds the Sorts of (ParsedTermsOSA b2) . b3 = { b4 where B is Element of TS (DTConOSA b2) : ( ex b1 being Element of b1ex b2 being set st
( b5 <= b3 & b6 in b2 . b5 & b4 = root-tree [b6,b5] ) or ex b1 being OperSymbol of b1 st
( [b5,the carrier of b1] = b4 . {} & the_result_sort_of b5 <= b3 ) ) }
proof end;

theorem Th10: :: OSAFREE:10
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3, b4 being Element of b1
for b5 being set st b5 in b2 . b3 holds
( root-tree [b5,b3] is Element of TS (DTConOSA b2) & ( for b6 being set holds [b6,the carrier of b1] <> (root-tree [b5,b3]) . {} ) & ( root-tree [b5,b3] in the Sorts of (ParsedTermsOSA b2) . b4 implies b3 <= b4 ) & ( b3 <= b4 implies root-tree [b5,b3] in the Sorts of (ParsedTermsOSA b2) . b4 ) )
proof end;

theorem Th11: :: OSAFREE:11
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of TS (DTConOSA b2)
for b4 being OperSymbol of b1 st b3 . {} = [b4,the carrier of b1] holds
( ex b5 being SubtreeSeq of OSSym b4,b2 st
( b3 = (OSSym b4,b2) -tree b5 & OSSym b4,b2 ==> roots b5 & b5 in Args b4,(ParsedTermsOSA b2) & b3 = (Den b4,(ParsedTermsOSA b2)) . b5 ) & ( for b5 being Element of b1
for b6 being set holds b3 <> root-tree [b6,b5] ) & ( for b5 being Element of b1 holds
( b3 in the Sorts of (ParsedTermsOSA b2) . b5 iff the_result_sort_of b4 <= b5 ) ) )
proof end;

theorem Th12: :: OSAFREE:12
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Symbol of (DTConOSA b2)
for b4 being FinSequence of TS (DTConOSA b2) st b3 ==> roots b4 holds
( b3 in NonTerminals (DTConOSA b2) & b3 -tree b4 in TS (DTConOSA b2) & ex b5 being OperSymbol of b1 st
( b3 = [b5,the carrier of b1] & b4 in Args b5,(ParsedTermsOSA b2) & b3 -tree b4 = (Den b5,(ParsedTermsOSA b2)) . b4 & ( for b6 being Element of b1 holds
( b3 -tree b4 in the Sorts of (ParsedTermsOSA b2) . b6 iff the_result_sort_of b5 <= b6 ) ) ) )
proof end;

theorem Th13: :: OSAFREE:13
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being FinSequence holds
( b4 in Args b3,(ParsedTermsOSA b2) iff ( b4 is FinSequence of TS (DTConOSA b2) & OSSym b3,b2 ==> roots b4 ) )
proof end;

theorem Th14: :: OSAFREE:14
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of TS (DTConOSA b2) ex b4 being SortSymbol of b1 st
( b3 in the Sorts of (ParsedTermsOSA b2) . b4 & ( for b5 being Element of b1 st b3 in the Sorts of (ParsedTermsOSA b2) . b5 holds
b4 <= b5 ) )
proof end;

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of TS (DTConOSA c2);
func LeastSort c3 -> SortSymbol of a1 means :Def12: :: OSAFREE:def 12
( a3 in the Sorts of (ParsedTermsOSA a2) . a4 & ( for b1 being Element of a1 st a3 in the Sorts of (ParsedTermsOSA a2) . b1 holds
a4 <= b1 ) );
existence
ex b1 being SortSymbol of c1 st
( c3 in the Sorts of (ParsedTermsOSA c2) . b1 & ( for b2 being Element of c1 st c3 in the Sorts of (ParsedTermsOSA c2) . b2 holds
b1 <= b2 ) ) by Th14;
uniqueness
for b1, b2 being SortSymbol of c1 st c3 in the Sorts of (ParsedTermsOSA c2) . b1 & ( for b3 being Element of c1 st c3 in the Sorts of (ParsedTermsOSA c2) . b3 holds
b1 <= b3 ) & c3 in the Sorts of (ParsedTermsOSA c2) . b2 & ( for b3 being Element of c1 st c3 in the Sorts of (ParsedTermsOSA c2) . b3 holds
b2 <= b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines LeastSort OSAFREE:def 12 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of TS (DTConOSA b2)
for b4 being SortSymbol of b1 holds
( b4 = LeastSort b3 iff ( b3 in the Sorts of (ParsedTermsOSA b2) . b4 & ( for b5 being Element of b1 st b3 in the Sorts of (ParsedTermsOSA b2) . b5 holds
b4 <= b5 ) ) );

definition
let c1 be non empty non void ManySortedSign ;
let c2 be non-empty MSAlgebra of c1;
mode Element of a2 is Element of Union the Sorts of a2;
end;

theorem Th15: :: OSAFREE:15
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being set holds
( b3 is Element of (ParsedTermsOSA b2) iff b3 is Element of TS (DTConOSA b2) )
proof end;

theorem Th16: :: OSAFREE:16
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1
for b4 being set st b4 in the Sorts of (ParsedTermsOSA b2) . b3 holds
b4 is Element of TS (DTConOSA b2)
proof end;

theorem Th17: :: OSAFREE:17
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1
for b4 being set st b4 in b2 . b3 holds
for b5 being Element of TS (DTConOSA b2) st b5 = root-tree [b4,b3] holds
LeastSort b5 = b3
proof end;

theorem Th18: :: OSAFREE:18
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being Element of Args b3,(ParsedTermsOSA b2)
for b5 being Element of TS (DTConOSA b2) st b5 = (Den b3,(ParsedTermsOSA b2)) . b4 holds
LeastSort b5 = the_result_sort_of b3
proof end;

registration
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be OperSymbol of c1;
cluster Args a3,(ParsedTermsOSA a2) -> non empty ;
coherence
not Args c3,(ParsedTermsOSA c2) is empty ;
end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be FinSequence of TS (DTConOSA c2);
canceled;
func LeastSorts c3 -> Element of the carrier of a1 * means :Def14: :: OSAFREE:def 14
( dom a4 = dom a3 & ( for b1 being Nat st b1 in dom a3 holds
ex b2 being Element of TS (DTConOSA a2) st
( b2 = a3 . b1 & a4 . b1 = LeastSort b2 ) ) );
existence
ex b1 being Element of the carrier of c1 * st
( dom b1 = dom c3 & ( for b2 being Nat st b2 in dom c3 holds
ex b3 being Element of TS (DTConOSA c2) st
( b3 = c3 . b2 & b1 . b2 = LeastSort b3 ) ) )
proof end;
uniqueness
for b1, b2 being Element of the carrier of c1 * st dom b1 = dom c3 & ( for b3 being Nat st b3 in dom c3 holds
ex b4 being Element of TS (DTConOSA c2) st
( b4 = c3 . b3 & b1 . b3 = LeastSort b4 ) ) & dom b2 = dom c3 & ( for b3 being Nat st b3 in dom c3 holds
ex b4 being Element of TS (DTConOSA c2) st
( b4 = c3 . b3 & b2 . b3 = LeastSort b4 ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def13 OSAFREE:def 13 :
canceled;

:: deftheorem Def14 defines LeastSorts OSAFREE:def 14 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being FinSequence of TS (DTConOSA b2)
for b4 being Element of the carrier of b1 * holds
( b4 = LeastSorts b3 iff ( dom b4 = dom b3 & ( for b5 being Nat st b5 in dom b3 holds
ex b6 being Element of TS (DTConOSA b2) st
( b6 = b3 . b5 & b4 . b5 = LeastSort b6 ) ) ) );

theorem Th19: :: OSAFREE:19
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being FinSequence of TS (DTConOSA b2) holds
( LeastSorts b4 <= the_arity_of b3 iff b4 in Args b3,(ParsedTermsOSA b2) )
proof end;

registration
cluster monotone regular locally_directed OverloadedRSSign ;
existence
ex b1 being monotone OrderSortedSign st
( b1 is locally_directed & b1 is regular )
proof end;
end;

definition
let c1 be monotone regular locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be OperSymbol of c1;
let c4 be FinSequence of TS (DTConOSA c2);
assume E25: OSSym (LBound c3,(LeastSorts c4)),c2 ==> roots c4 ;
func pi c3,c4 -> Element of TS (DTConOSA a2) equals :Def15: :: OSAFREE:def 15
(OSSym (LBound a3,(LeastSorts a4)),a2) -tree a4;
correctness
coherence
(OSSym (LBound c3,(LeastSorts c4)),c2) -tree c4 is Element of TS (DTConOSA c2);
by E25, Th12;
end;

:: deftheorem Def15 defines pi OSAFREE:def 15 :
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OperSymbol of b1
for b4 being FinSequence of TS (DTConOSA b2) st OSSym (LBound b3,(LeastSorts b4)),b2 ==> roots b4 holds
pi b3,b4 = (OSSym (LBound b3,(LeastSorts b4)),b2) -tree b4;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Symbol of (DTConOSA c2);
assume E26: ex b1 being FinSequence st c3 ==> b1 ;
func @ c2,c3 -> OperSymbol of a1 means :Def16: :: OSAFREE:def 16
[a4,the carrier of a1] = a3;
existence
ex b1 being OperSymbol of c1 st [b1,the carrier of c1] = c3
proof end;
uniqueness
for b1, b2 being OperSymbol of c1 st [b1,the carrier of c1] = c3 & [b2,the carrier of c1] = c3 holds
b1 = b2 by ZFMISC_1:33;
end;

:: deftheorem Def16 defines @ OSAFREE:def 16 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Symbol of (DTConOSA b2) st ex b4 being FinSequence st b3 ==> b4 holds
for b4 being OperSymbol of b1 holds
( b4 = @ b2,b3 iff [b4,the carrier of b1] = b3 );

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Symbol of (DTConOSA c2);
assume E27: c3 in Terminals (DTConOSA c2) ;
func pi c3 -> Element of TS (DTConOSA a2) equals :Def17: :: OSAFREE:def 17
 root-tree a3;
correctness
coherence
root-tree c3 is Element of TS (DTConOSA c2);
by E27, DTCONSTR:def 4;
end;

:: deftheorem Def17 defines pi OSAFREE:def 17 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Symbol of (DTConOSA b2) st b3 in Terminals (DTConOSA b2) holds
pi b3 = root-tree b3;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func LCongruence c2 -> monotone OSCongruence of ParsedTermsOSA a2 means :Def18: :: OSAFREE:def 18
for b1 being monotone OSCongruence of ParsedTermsOSA a2 holds a3 c= b1;
existence
ex b1 being monotone OSCongruence of ParsedTermsOSA c2 st
for b2 being monotone OSCongruence of ParsedTermsOSA c2 holds b1 c= b2
proof end;
uniqueness
for b1, b2 being monotone OSCongruence of ParsedTermsOSA c2 st ( for b3 being monotone OSCongruence of ParsedTermsOSA c2 holds b1 c= b3 ) & ( for b3 being monotone OSCongruence of ParsedTermsOSA c2 holds b2 c= b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines LCongruence OSAFREE:def 18 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being monotone OSCongruence of ParsedTermsOSA b2 holds
( b3 = LCongruence b2 iff for b4 being monotone OSCongruence of ParsedTermsOSA b2 holds b3 c= b4 );

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func FreeOSA c2 -> strict non-empty monotone OSAlgebra of a1 equals :: OSAFREE:def 19
 QuotOSAlg (ParsedTermsOSA a2),(LCongruence a2);
correctness
coherence
QuotOSAlg (ParsedTermsOSA c2),(LCongruence c2) is strict non-empty monotone OSAlgebra of c1;
;
end;

:: deftheorem Def19 defines FreeOSA OSAFREE:def 19 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds FreeOSA b2 = QuotOSAlg (ParsedTermsOSA b2),(LCongruence b2);

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Symbol of (DTConOSA c2);
func @ c3 -> Subset of [:(TS (DTConOSA a2)),the carrier of a1:] equals :: OSAFREE:def 20
{ [(root-tree a3),b1] where B is Element of a1 : ex b1 being Element of a1ex b2 being set st
( b3 in a2 . b2 & a3 = [b3,b2] & b2 <= b1 ) } ;
correctness
coherence
{ [(root-tree c3),b1] where B is Element of c1 : ex b1 being Element of c1ex b2 being set st
( b3 in c2 . b2 & c3 = [b3,b2] & b2 <= b1 ) } is Subset of [:(TS (DTConOSA c2)),the carrier of c1:];
proof end;
end;

:: deftheorem Def20 defines @ OSAFREE:def 20 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Symbol of (DTConOSA b2) holds @ b3 = { [(root-tree b3),b4] where B is Element of b1 : ex b1 being Element of b1ex b2 being set st
( b6 in b2 . b5 & b3 = [b6,b5] & b5 <= b4 ) } ;

definition
let c1 be OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Symbol of (DTConOSA c2);
let c4 be FinSequence of bool [:(TS (DTConOSA c2)),the carrier of c1:];
func @ c3,c4 -> Subset of [:(TS (DTConOSA a2)),the carrier of a1:] equals :: OSAFREE:def 21
{ [((Den b1,(ParsedTermsOSA a2)) . b2),b3] where B is OperSymbol of a1, B is Element of Args b1,(ParsedTermsOSA a2), B is Element of a1 : ( ex b1 being OperSymbol of a1 st
( a3 = [b4,the carrier of a1] & b4 ~= b1 & len (the_arity_of b4) = len (the_arity_of b1) & the_result_sort_of b4 <= b3 & the_result_sort_of b1 <= b3 ) & ex b1 being Element of the carrier of a1 * st
( dom b4 = dom a4 & ( for b2 being Nat st b5 in dom a4 holds
[(b2 . b5),(b4 /. b5)] in a4 . b5 ) ) ) } ;
correctness
coherence
{ [((Den b1,(ParsedTermsOSA c2)) . b2),b3] where B is OperSymbol of c1, B is Element of Args b1,(ParsedTermsOSA c2), B is Element of c1 : ( ex b1 being OperSymbol of c1 st
( c3 = [b4,the carrier of c1] & b4 ~= b1 & len (the_arity_of b4) = len (the_arity_of b1) & the_result_sort_of b4 <= b3 & the_result_sort_of b1 <= b3 ) & ex b1 being Element of the carrier of c1 * st
( dom b4 = dom c4 & ( for b2 being Nat st b5 in dom c4 holds
[(b2 . b5),(b4 /. b5)] in c4 . b5 ) ) ) } is Subset of [:(TS (DTConOSA c2)),the carrier of c1:];
proof end;
end;

:: deftheorem Def21 defines @ OSAFREE:def 21 :
for b1 being OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Symbol of (DTConOSA b2)
for b4 being FinSequence of bool [:(TS (DTConOSA b2)),the carrier of b1:] holds @ b3,b4 = { [((Den b5,(ParsedTermsOSA b2)) . b6),b7] where B is OperSymbol of b1, B is Element of Args b5,(ParsedTermsOSA b2), B is Element of b1 : ( ex b1 being OperSymbol of b1 st
( b3 = [b8,the carrier of b1] & b8 ~= b5 & len (the_arity_of b8) = len (the_arity_of b5) & the_result_sort_of b8 <= b7 & the_result_sort_of b5 <= b7 ) & ex b1 being Element of the carrier of b1 * st
( dom b8 = dom b4 & ( for b2 being Nat st b9 in dom b4 holds
[(b6 . b9),(b8 /. b9)] in b4 . b9 ) ) ) } ;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func PTClasses c2 -> Function of TS (DTConOSA a2), bool [:(TS (DTConOSA a2)),the carrier of a1:] means :Def22: :: OSAFREE:def 22
( ( for b1 being Symbol of (DTConOSA a2) st b1 in Terminals (DTConOSA a2) holds
a3 . (root-tree b1) = @ b1 ) & ( for b1 being Symbol of (DTConOSA a2)
for b2 being FinSequence of TS (DTConOSA a2) st b1 ==> roots b2 holds
a3 . (b1 -tree b2) = @ b1,(a3 * b2) ) );
existence
ex b1 being Function of TS (DTConOSA c2), bool [:(TS (DTConOSA c2)),the carrier of c1:] st
( ( for b2 being Symbol of (DTConOSA c2) st b2 in Terminals (DTConOSA c2) holds
b1 . (root-tree b2) = @ b2 ) & ( for b2 being Symbol of (DTConOSA c2)
for b3 being FinSequence of TS (DTConOSA c2) st b2 ==> roots b3 holds
b1 . (b2 -tree b3) = @ b2,(b1 * b3) ) )
proof end;
uniqueness
for b1, b2 being Function of TS (DTConOSA c2), bool [:(TS (DTConOSA c2)),the carrier of c1:] st ( for b3 being Symbol of (DTConOSA c2) st b3 in Terminals (DTConOSA c2) holds
b1 . (root-tree b3) = @ b3 ) & ( for b3 being Symbol of (DTConOSA c2)
for b4 being FinSequence of TS (DTConOSA c2) st b3 ==> roots b4 holds
b1 . (b3 -tree b4) = @ b3,(b1 * b4) ) & ( for b3 being Symbol of (DTConOSA c2) st b3 in Terminals (DTConOSA c2) holds
b2 . (root-tree b3) = @ b3 ) & ( for b3 being Symbol of (DTConOSA c2)
for b4 being FinSequence of TS (DTConOSA c2) st b3 ==> roots b4 holds
b2 . (b3 -tree b4) = @ b3,(b2 * b4) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def22 defines PTClasses OSAFREE:def 22 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Function of TS (DTConOSA b2), bool [:(TS (DTConOSA b2)),the carrier of b1:] holds
( b3 = PTClasses b2 iff ( ( for b4 being Symbol of (DTConOSA b2) st b4 in Terminals (DTConOSA b2) holds
b3 . (root-tree b4) = @ b4 ) & ( for b4 being Symbol of (DTConOSA b2)
for b5 being FinSequence of TS (DTConOSA b2) st b4 ==> roots b5 holds
b3 . (b4 -tree b5) = @ b4,(b3 * b5) ) ) );

theorem Th20: :: OSAFREE:20
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of TS (DTConOSA b2) holds
( ( for b4 being Element of b1 holds
( b3 in the Sorts of (ParsedTermsOSA b2) . b4 iff [b3,b4] in (PTClasses b2) . b3 ) ) & ( for b4 being Element of b1
for b5 being Element of TS (DTConOSA b2) st [b5,b4] in (PTClasses b2) . b3 holds
[b3,b4] in (PTClasses b2) . b5 ) )
proof end;

theorem Th21: :: OSAFREE:21
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of TS (DTConOSA b2)
for b4 being Element of b1 st ex b5 being Element of TS (DTConOSA b2) st [b5,b4] in (PTClasses b2) . b3 holds
[b3,b4] in (PTClasses b2) . b3
proof end;

theorem Th22: :: OSAFREE:22
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3, b4 being Element of TS (DTConOSA b2)
for b5, b6 being Element of b1 st b5 <= b6 & b3 in the Sorts of (ParsedTermsOSA b2) . b5 & b4 in the Sorts of (ParsedTermsOSA b2) . b5 holds
( [b4,b5] in (PTClasses b2) . b3 iff [b4,b6] in (PTClasses b2) . b3 )
proof end;

theorem Th23: :: OSAFREE:23
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3, b4, b5 being Element of TS (DTConOSA b2)
for b6 being Element of b1 st [b4,b6] in (PTClasses b2) . b3 & [b5,b6] in (PTClasses b2) . b4 holds
[b3,b6] in (PTClasses b2) . b5
proof end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func PTCongruence c2 -> MSEquivalence-like OrderSortedRelation of ParsedTermsOSA a2 means :Def23: :: OSAFREE:def 23
for b1 being set st b1 in the carrier of a1 holds
a3 . b1 = { [b2,b3] where B is Element of TS (DTConOSA a2), B is Element of TS (DTConOSA a2) : [b2,b1] in (PTClasses a2) . b3 } ;
existence
ex b1 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA c2 st
for b2 being set st b2 in the carrier of c1 holds
b1 . b2 = { [b3,b4] where B is Element of TS (DTConOSA c2), B is Element of TS (DTConOSA c2) : [b3,b2] in (PTClasses c2) . b4 }
proof end;
uniqueness
for b1, b2 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA c2 st ( for b3 being set st b3 in the carrier of c1 holds
b1 . b3 = { [b4,b5] where B is Element of TS (DTConOSA c2), B is Element of TS (DTConOSA c2) : [b4,b3] in (PTClasses c2) . b5 } ) & ( for b3 being set st b3 in the carrier of c1 holds
b2 . b3 = { [b4,b5] where B is Element of TS (DTConOSA c2), B is Element of TS (DTConOSA c2) : [b4,b3] in (PTClasses c2) . b5 } ) holds
b1 = b2
proof end;
end;

:: deftheorem Def23 defines PTCongruence OSAFREE:def 23 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being MSEquivalence-like OrderSortedRelation of ParsedTermsOSA b2 holds
( b3 = PTCongruence b2 iff for b4 being set st b4 in the carrier of b1 holds
b3 . b4 = { [b5,b6] where B is Element of TS (DTConOSA b2), B is Element of TS (DTConOSA b2) : [b5,b4] in (PTClasses b2) . b6 } );

theorem Th24: :: OSAFREE:24
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3, b4, b5 being set st [b3,b5] in (PTClasses b2) . b4 holds
( b3 in TS (DTConOSA b2) & b4 in TS (DTConOSA b2) & b5 in the carrier of b1 )
proof end;

theorem Th25: :: OSAFREE:25
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Component of b1
for b4, b5 being set holds
( [b4,b5] in CompClass (PTCongruence b2),b3 iff ex b6 being Element of b1 st
( b6 in b3 & [b4,b6] in (PTClasses b2) . b5 ) )
proof end;

theorem Th26: :: OSAFREE:26
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1
for b4 being Element of the Sorts of (ParsedTermsOSA b2) . b3 holds OSClass (PTCongruence b2),b4 = proj1 ((PTClasses b2) . b4)
proof end;

theorem Th27: :: OSAFREE:27
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being ManySortedRelation of (ParsedTermsOSA b2) holds
( b3 = PTCongruence b2 iff ( ( for b4, b5 being Element of b1
for b6 being set st b6 in b2 . b4 holds
( ( b4 <= b5 implies [(root-tree [b6,b4]),(root-tree [b6,b4])] in b3 . b5 ) & ( for b7 being set st ( [(root-tree [b6,b4]),b7] in b3 . b5 or [b7,(root-tree [b6,b4])] in b3 . b5 ) holds
( b4 <= b5 & b7 = root-tree [b6,b4] ) ) ) ) & ( for b4, b5 being OperSymbol of b1
for b6 being Element of Args b4,(ParsedTermsOSA b2)
for b7 being Element of Args b5,(ParsedTermsOSA b2)
for b8 being Element of b1 holds
( [((Den b4,(ParsedTermsOSA b2)) . b6),((Den b5,(ParsedTermsOSA b2)) . b7)] in b3 . b8 iff ( b4 ~= b5 & len (the_arity_of b4) = len (the_arity_of b5) & the_result_sort_of b4 <= b8 & the_result_sort_of b5 <= b8 & ex b9 being Element of the carrier of b1 * st
( dom b9 = dom b6 & ( for b10 being Nat st b10 in dom b9 holds
[(b6 . b10),(b7 . b10)] in b3 . (b9 /. b10) ) ) ) ) ) ) )
proof end;

theorem Th28: :: OSAFREE:28
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds PTCongruence b2 is monotone
proof end;

registration
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
cluster PTCongruence a2 -> MSEquivalence-like monotone ;
coherence
PTCongruence c2 is monotone by Th28;
end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of c1;
func PTVars c3,c2 -> Subset of (the Sorts of (ParsedTermsOSA a2) . a3) means :Def24: :: OSAFREE:def 24
for b1 being set holds
( b1 in a4 iff ex b2 being set st
( b2 in a2 . a3 & b1 = root-tree [b2,a3] ) );
existence
ex b1 being Subset of (the Sorts of (ParsedTermsOSA c2) . c3) st
for b2 being set holds
( b2 in b1 iff ex b3 being set st
( b3 in c2 . c3 & b2 = root-tree [b3,c3] ) )
proof end;
uniqueness
for b1, b2 being Subset of (the Sorts of (ParsedTermsOSA c2) . c3) st ( for b3 being set holds
( b3 in b1 iff ex b4 being set st
( b4 in c2 . c3 & b3 = root-tree [b4,c3] ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being set st
( b4 in c2 . c3 & b3 = root-tree [b4,c3] ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines PTVars OSAFREE:def 24 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1
for b4 being Subset of (the Sorts of (ParsedTermsOSA b2) . b3) holds
( b4 = PTVars b3,b2 iff for b5 being set holds
( b5 in b4 iff ex b6 being set st
( b6 in b2 . b3 & b5 = root-tree [b6,b3] ) ) );

registration
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of c1;
cluster PTVars a3,a2 -> non empty ;
coherence
not PTVars c3,c2 is empty
proof end;
end;

theorem Th29: :: OSAFREE:29
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1 holds PTVars b3,b2 = { (root-tree b4) where B is Symbol of (DTConOSA b2) : ( b4 in Terminals (DTConOSA b2) & b4 `2 = b3 ) }
proof end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func PTVars c2 -> MSSubset of (ParsedTermsOSA a2) means :Def25: :: OSAFREE:def 25
for b1 being Element of a1 holds a3 . b1 = PTVars b1,a2;
existence
ex b1 being MSSubset of (ParsedTermsOSA c2) st
for b2 being Element of c1 holds b1 . b2 = PTVars b2,c2
proof end;
uniqueness
for b1, b2 being MSSubset of (ParsedTermsOSA c2) st ( for b3 being Element of c1 holds b1 . b3 = PTVars b3,c2 ) & ( for b3 being Element of c1 holds b2 . b3 = PTVars b3,c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines PTVars OSAFREE:def 25 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being MSSubset of (ParsedTermsOSA b2) holds
( b3 = PTVars b2 iff for b4 being Element of b1 holds b3 . b4 = PTVars b4,b2 );

theorem Th30: :: OSAFREE:30
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds PTVars b2 is non-empty
proof end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of c1;
func OSFreeGen c3,c2 -> Subset of (the Sorts of (FreeOSA a2) . a3) means :Def26: :: OSAFREE:def 26
for b1 being set holds
( b1 in a4 iff ex b2 being set st
( b2 in a2 . a3 & b1 = ((OSNat_Hom (ParsedTermsOSA a2),(LCongruence a2)) . a3) . (root-tree [b2,a3]) ) );
existence
ex b1 being Subset of (the Sorts of (FreeOSA c2) . c3) st
for b2 being set holds
( b2 in b1 iff ex b3 being set st
( b3 in c2 . c3 & b2 = ((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree [b3,c3]) ) )
proof end;
uniqueness
for b1, b2 being Subset of (the Sorts of (FreeOSA c2) . c3) st ( for b3 being set holds
( b3 in b1 iff ex b4 being set st
( b4 in c2 . c3 & b3 = ((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree [b4,c3]) ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being set st
( b4 in c2 . c3 & b3 = ((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree [b4,c3]) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def26 defines OSFreeGen OSAFREE:def 26 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1
for b4 being Subset of (the Sorts of (FreeOSA b2) . b3) holds
( b4 = OSFreeGen b3,b2 iff for b5 being set holds
( b5 in b4 iff ex b6 being set st
( b6 in b2 . b3 & b5 = ((OSNat_Hom (ParsedTermsOSA b2),(LCongruence b2)) . b3) . (root-tree [b6,b3]) ) ) );

registration
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of c1;
cluster OSFreeGen a3,a2 -> non empty ;
coherence
not OSFreeGen c3,c2 is empty
proof end;
end;

theorem Th31: :: OSAFREE:31
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1 holds OSFreeGen b3,b2 = { (((OSNat_Hom (ParsedTermsOSA b2),(LCongruence b2)) . b3) . (root-tree b4)) where B is Symbol of (DTConOSA b2) : ( b4 in Terminals (DTConOSA b2) & b4 `2 = b3 ) }
proof end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func OSFreeGen c2 -> OSGeneratorSet of FreeOSA a2 means :Def27: :: OSAFREE:def 27
for b1 being Element of a1 holds a3 . b1 = OSFreeGen b1,a2;
existence
ex b1 being OSGeneratorSet of FreeOSA c2 st
for b2 being Element of c1 holds b1 . b2 = OSFreeGen b2,c2
proof end;
uniqueness
for b1, b2 being OSGeneratorSet of FreeOSA c2 st ( for b3 being Element of c1 holds b1 . b3 = OSFreeGen b3,c2 ) & ( for b3 being Element of c1 holds b2 . b3 = OSFreeGen b3,c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def27 defines OSFreeGen OSAFREE:def 27 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OSGeneratorSet of FreeOSA b2 holds
( b3 = OSFreeGen b2 iff for b4 being Element of b1 holds b3 . b4 = OSFreeGen b4,b2 );

theorem Th32: :: OSAFREE:32
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds OSFreeGen b2 is non-empty
proof end;

registration
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
cluster OSFreeGen a2 -> V3 ;
coherence
OSFreeGen c2 is non-empty by Th32;
end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be OSCongruence of ParsedTermsOSA c2;
let c4 be Element of TS (DTConOSA c2);
func OSClass c3,c4 -> Element of OSClass a3,(LeastSort a4) means :Def28: :: OSAFREE:def 28
for b1 being Element of a1
for b2 being Element of the Sorts of (ParsedTermsOSA a2) . b1 st a4 = b2 holds
a5 = OSClass a3,b2;
existence
ex b1 being Element of OSClass c3,(LeastSort c4) st
for b2 being Element of c1
for b3 being Element of the Sorts of (ParsedTermsOSA c2) . b2 st c4 = b3 holds
b1 = OSClass c3,b3
proof end;
uniqueness
for b1, b2 being Element of OSClass c3,(LeastSort c4) st ( for b3 being Element of c1
for b4 being Element of the Sorts of (ParsedTermsOSA c2) . b3 st c4 = b4 holds
b1 = OSClass c3,b4 ) & ( for b3 being Element of c1
for b4 being Element of the Sorts of (ParsedTermsOSA c2) . b3 st c4 = b4 holds
b2 = OSClass c3,b4 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def28 defines OSClass OSAFREE:def 28 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OSCongruence of ParsedTermsOSA b2
for b4 being Element of TS (DTConOSA b2)
for b5 being Element of OSClass b3,(LeastSort b4) holds
( b5 = OSClass b3,b4 iff for b6 being Element of b1
for b7 being Element of the Sorts of (ParsedTermsOSA b2) . b6 st b4 = b7 holds
b5 = OSClass b3,b7 );

theorem Th33: :: OSAFREE:33
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OSCongruence of ParsedTermsOSA b2
for b4 being Element of TS (DTConOSA b2) holds b4 in OSClass b3,b4
proof end;

theorem Th34: :: OSAFREE:34
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1
for b4 being Element of TS (DTConOSA b2)
for b5, b6 being set st b5 in b2 . b3 & b4 = root-tree [b5,b3] holds
( b6 in OSClass (PTCongruence b2),b4 iff b6 = b4 )
proof end;

theorem Th35: :: OSAFREE:35
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being OSCongruence of ParsedTermsOSA b2
for b4, b5 being Element of TS (DTConOSA b2) holds
( b5 in OSClass b3,b4 iff OSClass b3,b4 = OSClass b3,b5 )
proof end;

theorem Th36: :: OSAFREE:36
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3, b4 being OSCongruence of ParsedTermsOSA b2
for b5 being Element of TS (DTConOSA b2) st b3 c= b4 holds
OSClass b3,b5 c= OSClass b4,b5
proof end;

theorem Th37: :: OSAFREE:37
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1
for b4 being Element of TS (DTConOSA b2)
for b5, b6 being set st b5 in b2 . b3 & b4 = root-tree [b5,b3] holds
( b6 in OSClass (LCongruence b2),b4 iff b6 = b4 )
proof end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be V3 ManySortedSet of the carrier of c1;
let c4 be ManySortedFunction of PTVars c2,c3;
let c5 be Symbol of (DTConOSA c2);
assume E53: c5 in Terminals (DTConOSA c2) ;
func pi c4,c3,c5 -> Element of Union a3 means :Def29: :: OSAFREE:def 29
for b1 being Function st b1 = a4 . (a5 `2 ) holds
a6 = b1 . (root-tree a5);
existence
ex b1 being Element of Union c3 st
for b2 being Function st b2 = c4 . (c5 `2 ) holds
b1 = b2 . (root-tree c5)
proof end;
uniqueness
for b1, b2 being Element of Union c3 st ( for b3 being Function st b3 = c4 . (c5 `2 ) holds
b1 = b3 . (root-tree c5) ) & ( for b3 being Function st b3 = c4 . (c5 `2 ) holds
b2 = b3 . (root-tree c5) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def29 defines pi OSAFREE:def 29 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being V3 ManySortedSet of the carrier of b1
for b4 being ManySortedFunction of PTVars b2,b3
for b5 being Symbol of (DTConOSA b2) st b5 in Terminals (DTConOSA b2) holds
for b6 being Element of Union b3 holds
( b6 = pi b4,b3,b5 iff for b7 being Function st b7 = b4 . (b5 `2 ) holds
b6 = b7 . (root-tree b5) );

theorem Th38: :: OSAFREE:38
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being non-empty monotone OSAlgebra of b1
for b4 being ManySortedFunction of PTVars b2,the Sorts of b3 ex b5 being ManySortedFunction of (ParsedTermsOSA b2),b3 st
( b5 is_homomorphism ParsedTermsOSA b2,b3 & b5 is order-sorted & b5 || (PTVars b2) = b4 )
proof end;

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
let c3 be Element of c1;
func NHReverse c3,c2 -> Function of OSFreeGen a3,a2, PTVars a3,a2 means :: OSAFREE:def 30
for b1 being Symbol of (DTConOSA a2) st ((OSNat_Hom (ParsedTermsOSA a2),(LCongruence a2)) . a3) . (root-tree b1) in OSFreeGen a3,a2 holds
a4 . (((OSNat_Hom (ParsedTermsOSA a2),(LCongruence a2)) . a3) . (root-tree b1)) = root-tree b1;
existence
ex b1 being Function of OSFreeGen c3,c2, PTVars c3,c2 st
for b2 being Symbol of (DTConOSA c2) st ((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree b2) in OSFreeGen c3,c2 holds
b1 . (((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree b2)) = root-tree b2
proof end;
uniqueness
for b1, b2 being Function of OSFreeGen c3,c2, PTVars c3,c2 st ( for b3 being Symbol of (DTConOSA c2) st ((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree b3) in OSFreeGen c3,c2 holds
b1 . (((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree b3)) = root-tree b3 ) & ( for b3 being Symbol of (DTConOSA c2) st ((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree b3) in OSFreeGen c3,c2 holds
b2 . (((OSNat_Hom (ParsedTermsOSA c2),(LCongruence c2)) . c3) . (root-tree b3)) = root-tree b3 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def30 defines NHReverse OSAFREE:def 30 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of b1
for b4 being Function of OSFreeGen b3,b2, PTVars b3,b2 holds
( b4 = NHReverse b3,b2 iff for b5 being Symbol of (DTConOSA b2) st ((OSNat_Hom (ParsedTermsOSA b2),(LCongruence b2)) . b3) . (root-tree b5) in OSFreeGen b3,b2 holds
b4 . (((OSNat_Hom (ParsedTermsOSA b2),(LCongruence b2)) . b3) . (root-tree b5)) = root-tree b5 );

definition
let c1 be locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func NHReverse c2 -> ManySortedFunction of OSFreeGen a2, PTVars a2 means :: OSAFREE:def 31
for b1 being Element of a1 holds a3 . b1 = NHReverse b1,a2;
existence
ex b1 being ManySortedFunction of OSFreeGen c2, PTVars c2 st
for b2 being Element of c1 holds b1 . b2 = NHReverse b2,c2
proof end;
uniqueness
for b1, b2 being ManySortedFunction of OSFreeGen c2, PTVars c2 st ( for b3 being Element of c1 holds b1 . b3 = NHReverse b3,c2 ) & ( for b3 being Element of c1 holds b2 . b3 = NHReverse b3,c2 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def31 defines NHReverse OSAFREE:def 31 :
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being ManySortedFunction of OSFreeGen b2, PTVars b2 holds
( b3 = NHReverse b2 iff for b4 being Element of b1 holds b3 . b4 = NHReverse b4,b2 );

theorem Th39: :: OSAFREE:39
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds OSFreeGen b2 is osfree
proof end;

theorem Th40: :: OSAFREE:40
for b1 being locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds FreeOSA b2 is osfree
proof end;

registration
let c1 be locally_directed OrderSortedSign;
cluster strict non-empty monotone osfree MSAlgebra of a1;
existence
ex b1 being non-empty monotone OSAlgebra of c1 st
( b1 is osfree & b1 is strict )
proof end;
end;

definition
let c1 be monotone regular locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func PTMin c2 -> Function of TS (DTConOSA a2), TS (DTConOSA a2) means :Def32: :: OSAFREE:def 32
( ( for b1 being Symbol of (DTConOSA a2) st b1 in Terminals (DTConOSA a2) holds
a3 . (root-tree b1) = pi b1 ) & ( for b1 being Symbol of (DTConOSA a2)
for b2 being FinSequence of TS (DTConOSA a2) st b1 ==> roots b2 holds
a3 . (b1 -tree b2) = pi (@ a2,b1),(a3 * b2) ) );
existence
ex b1 being Function of TS (DTConOSA c2), TS (DTConOSA c2) st
( ( for b2 being Symbol of (DTConOSA c2) st b2 in Terminals (DTConOSA c2) holds
b1 . (root-tree b2) = pi b2 ) & ( for b2 being Symbol of (DTConOSA c2)
for b3 being FinSequence of TS (DTConOSA c2) st b2 ==> roots b3 holds
b1 . (b2 -tree b3) = pi (@ c2,b2),(b1 * b3) ) )
proof end;
uniqueness
for b1, b2 being Function of TS (DTConOSA c2), TS (DTConOSA c2) st ( for b3 being Symbol of (DTConOSA c2) st b3 in Terminals (DTConOSA c2) holds
b1 . (root-tree b3) = pi b3 ) & ( for b3 being Symbol of (DTConOSA c2)
for b4 being FinSequence of TS (DTConOSA c2) st b3 ==> roots b4 holds
b1 . (b3 -tree b4) = pi (@ c2,b3),(b1 * b4) ) & ( for b3 being Symbol of (DTConOSA c2) st b3 in Terminals (DTConOSA c2) holds
b2 . (root-tree b3) = pi b3 ) & ( for b3 being Symbol of (DTConOSA c2)
for b4 being FinSequence of TS (DTConOSA c2) st b3 ==> roots b4 holds
b2 . (b3 -tree b4) = pi (@ c2,b3),(b2 * b4) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def32 defines PTMin OSAFREE:def 32 :
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Function of TS (DTConOSA b2), TS (DTConOSA b2) holds
( b3 = PTMin b2 iff ( ( for b4 being Symbol of (DTConOSA b2) st b4 in Terminals (DTConOSA b2) holds
b3 . (root-tree b4) = pi b4 ) & ( for b4 being Symbol of (DTConOSA b2)
for b5 being FinSequence of TS (DTConOSA b2) st b4 ==> roots b5 holds
b3 . (b4 -tree b5) = pi (@ b2,b4),(b3 * b5) ) ) );

theorem Th41: :: OSAFREE:41
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of TS (DTConOSA b2) holds
( (PTMin b2) . b3 in OSClass (PTCongruence b2),b3 & LeastSort ((PTMin b2) . b3) <= LeastSort b3 & ( for b4 being Element of b1
for b5 being set st b5 in b2 . b4 & b3 = root-tree [b5,b4] holds
(PTMin b2) . b3 = b3 ) & ( for b4 being OperSymbol of b1
for b5 being FinSequence of TS (DTConOSA b2) st OSSym b4,b2 ==> roots b5 & b3 = (OSSym b4,b2) -tree b5 holds
( LeastSorts ((PTMin b2) * b5) <= the_arity_of b4 & OSSym b4,b2 ==> roots ((PTMin b2) * b5) & OSSym (LBound b4,(LeastSorts ((PTMin b2) * b5))),b2 ==> roots ((PTMin b2) * b5) & (PTMin b2) . b3 = (OSSym (LBound b4,(LeastSorts ((PTMin b2) * b5))),b2) -tree ((PTMin b2) * b5) ) ) )
proof end;

theorem Th42: :: OSAFREE:42
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3, b4 being Element of TS (DTConOSA b2) st b4 in OSClass (PTCongruence b2),b3 holds
(PTMin b2) . b4 = (PTMin b2) . b3
proof end;

theorem Th43: :: OSAFREE:43
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3, b4 being Element of TS (DTConOSA b2) holds
( b4 in OSClass (PTCongruence b2),b3 iff (PTMin b2) . b4 = (PTMin b2) . b3 )
proof end;

theorem Th44: :: OSAFREE:44
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of TS (DTConOSA b2) holds (PTMin b2) . ((PTMin b2) . b3) = (PTMin b2) . b3
proof end;

theorem Th45: :: OSAFREE:45
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA b2
for b4 being Element of TS (DTConOSA b2) holds [b4,((PTMin b2) . b4)] in b3 . (LeastSort b4)
proof end;

theorem Th46: :: OSAFREE:46
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA b2 holds PTCongruence b2 c= b3
proof end;

theorem Th47: :: OSAFREE:47
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds LCongruence b2 = PTCongruence b2
proof end;

definition
let c1 be monotone regular locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
mode MinTerm of c1,c2 -> Element of TS (DTConOSA a2) means :Def33: :: OSAFREE:def 33
(PTMin a2) . a3 = a3;
existence
ex b1 being Element of TS (DTConOSA c2) st (PTMin c2) . b1 = b1
proof end;
end;

:: deftheorem Def33 defines MinTerm OSAFREE:def 33 :
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being Element of TS (DTConOSA b2) holds
( b3 is MinTerm of b1,b2 iff (PTMin b2) . b3 = b3 );

definition
let c1 be monotone regular locally_directed OrderSortedSign;
let c2 be V3 ManySortedSet of c1;
func MinTerms c2 -> Subset of (TS (DTConOSA a2)) equals :: OSAFREE:def 34
 rng (PTMin a2);
correctness
coherence
rng (PTMin c2) is Subset of (TS (DTConOSA c2));
by RELSET_1:12;
end;

:: deftheorem Def34 defines MinTerms OSAFREE:def 34 :
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1 holds MinTerms b2 = rng (PTMin b2);

theorem Th48: :: OSAFREE:48
for b1 being monotone regular locally_directed OrderSortedSign
for b2 being V3 ManySortedSet of b1
for b3 being set holds
( b3 is MinTerm of b1,b2 iff b3 in MinTerms b2 )
proof end;