:: OSAFREE semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

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
proof end;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let S be OrderSortedSign;
let U0 be monotone OSAlgebra of S;
let IT be OSGeneratorSet of U0;
attr IT is osfree means :: OSAFREE:def 2
for U1 being non-empty monotone OSAlgebra of S
for f being ManySortedFunction of IT,the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 & h is order-sorted & h || IT = f );
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;
attr IT 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 );

definition
let S be OrderSortedSign;
let X be ManySortedSet of S;
func OSREL X -> Relation of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X)),([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * means :Def4: :: OSAFREE:def 4
for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in it iff ( a in [:the OperSymbols 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 OperSymbols of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,X ) ) ) ) ) ) ) );
existence
ex b1 being Relation of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X)),([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * st
for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [:the OperSymbols 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 OperSymbols of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,X ) ) ) ) ) ) ) )
proof end;
uniqueness
for b1, b2 being Relation of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X)),([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * st ( for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b1 iff ( a in [:the OperSymbols 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 OperSymbols of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,X ) ) ) ) ) ) ) ) ) & ( for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b2 iff ( a in [:the OperSymbols 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 OperSymbols of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,X ) ) ) ) ) ) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines OSREL OSAFREE:def 4 :
for S being OrderSortedSign
for X being ManySortedSet of S
for b3 being Relation of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X)),([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( b3 = OSREL X iff for a being Element of [:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [a,b] in b3 iff ( a in [:the OperSymbols 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 OperSymbols of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,X ) ) ) ) ) ) ) ) );

theorem Th2: :: OSAFREE:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being ManySortedSet of S
for o being OperSymbol of S
for b being Element of ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))) * holds
( [[o,the carrier of S],b] in OSREL X iff ( len b = len (the_arity_of o) & ( for x being set st x in dom b holds
( ( b . x in [:the OperSymbols of S,{the carrier of S}:] implies for o1 being OperSymbol of S st [o1,the carrier of S] = b . x holds
the_result_sort_of o1 <= (the_arity_of o) /. x ) & ( b . x in Union (coprod X) implies ex i being Element of S st
( i <= (the_arity_of o) /. x & b . x in coprod i,X ) ) ) ) ) )
proof end;

definition
let S be OrderSortedSign;
let X be ManySortedSet of S;
func DTConOSA X -> DTConstrStr equals :: OSAFREE:def 5
DTConstrStr(# ([:the OperSymbols of S,{the carrier of S}:] \/ (Union (coprod X))),(OSREL X) #);
correctness
coherence
DTConstrStr(# ([:the OperSymbols 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 OperSymbols 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 & not DTConOSA X is empty )
;
end;

theorem Th3: :: OSAFREE:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S holds
( NonTerminals (DTConOSA X) = [:the OperSymbols of S,{the carrier of S}:] & Terminals (DTConOSA X) = Union (coprod X) )
proof end;

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

theorem Th4: :: OSAFREE:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for t being set holds
( t in Terminals (DTConOSA X) iff ex s being Element of S ex x being set st
( x in X . s & t = [x,s] ) )
proof end;

definition
let S be OrderSortedSign;
let X be V3 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)
proof end;
end;

:: deftheorem defines OSSym OSAFREE:def 6 :
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for o being OperSymbol of S holds OSSym o,X = [o,the carrier of S];

definition
let S be OrderSortedSign;
let X be V3 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 & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) )
}
;
coherence
{ a where a is Element of TS (DTConOSA X) : ( ex s1 being Element of S ex x being set st
( s1 <= s & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) )
}
is Subset of (TS (DTConOSA X))
proof end;
end;

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

registration
let S be OrderSortedSign;
let X be V3 ManySortedSet of S;
let s be Element of S;
cluster ParsedTerms X,s -> non empty ;
coherence
not ParsedTerms X,s is empty
proof end;
end;

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

:: deftheorem Def8 defines ParsedTerms OSAFREE:def 8 :
for S being OrderSortedSign
for X being V3 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 V3 ManySortedSet of S;
cluster ParsedTerms X -> V3 ;
coherence
ParsedTerms X is non-empty
proof end;
end;

theorem Th5: :: OSAFREE:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for o being OperSymbol of S
for x being set st x in (((ParsedTerms X) # ) * the Arity of S) . o holds
x is FinSequence of TS (DTConOSA X)
proof end;

theorem Th6: :: OSAFREE:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConOSA X) holds
( p in (((ParsedTerms X) # ) * the Arity of S) . o iff ( dom p = dom (the_arity_of o) & ( for n being Nat st n in dom p holds
p . n in ParsedTerms X,((the_arity_of o) /. n) ) ) )
proof end;

theorem Th7: :: OSAFREE:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for o being OperSymbol of S
for p being FinSequence of TS (DTConOSA X) holds
( OSSym o,X ==> roots p iff p in (((ParsedTerms X) # ) * the Arity of S) . o )
proof end;

theorem Th8: :: OSAFREE:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S holds union (rng (ParsedTerms X)) = TS (DTConOSA X)
proof end;

definition
let S be OrderSortedSign;
let X be V3 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
proof end;
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 ) & ( 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
proof end;
end;

:: deftheorem Def9 defines PTDenOp OSAFREE:def 9 :
for S being OrderSortedSign
for X being V3 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 V3 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
proof end;
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 ) & ( for o being OperSymbol of S holds b2 . o = PTDenOp o,X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def10 defines PTOper OSAFREE:def 10 :
for S being OrderSortedSign
for X being V3 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 V3 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 V3 ManySortedSet of S holds ParsedTermsOSA X = MSAlgebra(# (ParsedTerms X),(PTOper X) #);

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

definition
let S be OrderSortedSign;
let X be V3 ManySortedSet of S;
let o be OperSymbol of S;
:: original: OSSym
redefine func OSSym o,X -> NonTerminal of (DTConOSA X);
coherence
OSSym o,X is NonTerminal of (DTConOSA X)
proof end;
end;

theorem Th9: :: OSAFREE:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 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 & x in X . s1 & a = root-tree [x,s1] ) or ex o being OperSymbol of S st
( [o,the carrier of S] = a . {} & the_result_sort_of o <= s ) )
}
proof end;

theorem Th10: :: OSAFREE:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for s, s1 being Element of S
for x being set st x in X . s holds
( root-tree [x,s] is Element of TS (DTConOSA X) & ( for z being set holds [z,the carrier of S] <> (root-tree [x,s]) . {} ) & ( root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 implies s <= s1 ) & ( s <= s1 implies root-tree [x,s] in the Sorts of (ParsedTermsOSA X) . s1 ) )
proof end;

theorem Th11: :: OSAFREE:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for t being Element of TS (DTConOSA X)
for o being OperSymbol of S st t . {} = [o,the carrier of S] holds
( ex p being SubtreeSeq of OSSym o,X st
( t = (OSSym o,X) -tree p & OSSym o,X ==> roots p & p in Args o,(ParsedTermsOSA X) & t = (Den o,(ParsedTermsOSA X)) . p ) & ( for s2 being Element of S
for x being set holds t <> root-tree [x,s2] ) & ( for s1 being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) )
proof end;

theorem Th12: :: OSAFREE:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
( nt in NonTerminals (DTConOSA X) & nt -tree ts in TS (DTConOSA X) & ex o being OperSymbol of S st
( nt = [o,the carrier of S] & ts in Args o,(ParsedTermsOSA X) & nt -tree ts = (Den o,(ParsedTermsOSA X)) . ts & ( for s1 being Element of S holds
( nt -tree ts in the Sorts of (ParsedTermsOSA X) . s1 iff the_result_sort_of o <= s1 ) ) ) )
proof end;

theorem Th13: :: OSAFREE:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for o being OperSymbol of S
for x being FinSequence holds
( x in Args o,(ParsedTermsOSA X) iff ( x is FinSequence of TS (DTConOSA X) & OSSym o,X ==> roots x ) )
proof end;

theorem Th14: :: OSAFREE:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for t being Element of TS (DTConOSA X) ex s being SortSymbol of S st
( t in the Sorts of (ParsedTermsOSA X) . s & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
s <= s1 ) )
proof end;

definition
let S be OrderSortedSign;
let X be V3 ManySortedSet of S;
let t be Element of TS (DTConOSA X);
func LeastSort t -> SortSymbol of S means :Def12: :: OSAFREE:def 12
( t in the Sorts of (ParsedTermsOSA X) . it & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
it <= s1 ) );
existence
ex b1 being SortSymbol of S st
( t in the Sorts of (ParsedTermsOSA X) . b1 & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b1 <= s1 ) )
by Th14;
uniqueness
for b1, b2 being SortSymbol of S st t in the Sorts of (ParsedTermsOSA X) . b1 & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b1 <= s1 ) & t in the Sorts of (ParsedTermsOSA X) . b2 & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b2 <= s1 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def12 defines LeastSort OSAFREE:def 12 :
for S being OrderSortedSign
for X being V3 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 & ( for s1 being Element of S st t in the Sorts of (ParsedTermsOSA X) . s1 holds
b4 <= s1 ) ) );

definition
let S be non empty non void ManySortedSign ;
let A be non-empty MSAlgebra of S;
mode Element of A is Element of Union the Sorts of A;
end;

theorem Th15: :: OSAFREE:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for x being set holds
( x is Element of (ParsedTermsOSA X) iff x is Element of TS (DTConOSA X) )
proof end;

theorem Th16: :: OSAFREE:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for s being Element of S
for x being set st x in the Sorts of (ParsedTermsOSA X) . s holds
x is Element of TS (DTConOSA X)
proof end;

theorem :: OSAFREE:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for s being Element of S
for x being set st x in X . s holds
for t being Element of TS (DTConOSA X) st t = root-tree [x,s] holds
LeastSort t = s
proof end;

theorem Th18: :: OSAFREE:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for o being OperSymbol of S
for x being Element of Args o,(ParsedTermsOSA X)
for t being Element of TS (DTConOSA X) st t = (Den o,(ParsedTermsOSA X)) . x holds
LeastSort t = the_result_sort_of o
proof end;

registration
let S be OrderSortedSign;
let X be V3 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;

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
let x be FinSequence of TS (DTConOSA X);
canceled;
func LeastSorts x -> Element of the carrier of S * means :Def14: :: OSAFREE:def 14
( dom it = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & it . y = LeastSort t ) ) );
existence
ex b1 being Element of the carrier of S * st
( dom b1 = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & b1 . y = LeastSort t ) ) )
proof end;
uniqueness
for b1, b2 being Element of the carrier of S * st dom b1 = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & b1 . y = LeastSort t ) ) & dom b2 = dom x & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & b2 . y = LeastSort t ) ) holds
b1 = b2
proof end;
end;

:: deftheorem OSAFREE:def 13 :
canceled;

:: deftheorem Def14 defines LeastSorts OSAFREE:def 14 :
for S being locally_directed OrderSortedSign
for X being V3 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 & ( for y being Nat st y in dom x holds
ex t being Element of TS (DTConOSA X) st
( t = x . y & b4 . y = LeastSort t ) ) ) );

theorem Th19: :: OSAFREE:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for o being OperSymbol of S
for x being FinSequence of TS (DTConOSA X) holds
( LeastSorts x <= the_arity_of o iff x in Args o,(ParsedTermsOSA X) )
proof end;

registration
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 S be monotone regular locally_directed OrderSortedSign;
let X be V3 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 :Def15: :: OSAFREE:def 15
(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 Def15 defines pi OSAFREE:def 15 :
for S being monotone regular locally_directed OrderSortedSign
for X being V3 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 V3 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 :Def16: :: OSAFREE:def 16
[it,the carrier of S] = t;
existence
ex b1 being OperSymbol of S st [b1,the carrier of S] = t
proof end;
uniqueness
for b1, b2 being OperSymbol of S st [b1,the carrier of S] = t & [b2,the carrier of S] = t holds
b1 = b2
by ZFMISC_1:33;
end;

:: deftheorem Def16 defines @ OSAFREE:def 16 :
for S being locally_directed OrderSortedSign
for X being V3 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 V3 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 :Def17: :: OSAFREE:def 17
root-tree t;
correctness
coherence
root-tree t is Element of TS (DTConOSA X)
;
by A1, DTCONSTR:def 4;
end;

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

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
func LCongruence X -> monotone OSCongruence of ParsedTermsOSA X means :Def18: :: OSAFREE:def 18
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
proof end;
uniqueness
for b1, b2 being monotone OSCongruence of ParsedTermsOSA X st ( for R being monotone OSCongruence of ParsedTermsOSA X holds b1 c= R ) & ( for R being monotone OSCongruence of ParsedTermsOSA X holds b2 c= R ) holds
b1 = b2
proof end;
end;

:: deftheorem Def18 defines LCongruence OSAFREE:def 18 :
for S being locally_directed OrderSortedSign
for X being V3 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 V3 ManySortedSet of S;
func FreeOSA X -> strict non-empty monotone OSAlgebra of S equals :: OSAFREE:def 19
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 19 :
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S holds FreeOSA X = QuotOSAlg (ParsedTermsOSA X),(LCongruence X);

definition
let S be OrderSortedSign;
let X be V3 ManySortedSet of S;
let t be Symbol of (DTConOSA X);
func @ t -> Subset of [:(TS (DTConOSA X)),the carrier of S:] equals :: OSAFREE:def 20
{ [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 )
}
;
correctness
coherence
{ [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 )
}
is Subset of [:(TS (DTConOSA X)),the carrier of S:]
;
proof end;
end;

:: deftheorem defines @ OSAFREE:def 20 :
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for t being Symbol of (DTConOSA X) holds @ t = { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 )
}
;

definition
let S be OrderSortedSign;
let X be V3 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 21
{ [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) )
}
;
correctness
coherence
{ [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) )
}
is Subset of [:(TS (DTConOSA X)),the carrier of S:]
;
proof end;
end;

:: deftheorem defines @ OSAFREE:def 21 :
for S being OrderSortedSign
for X being V3 ManySortedSet of S
for nt being Symbol of (DTConOSA X)
for x being FinSequence of bool [:(TS (DTConOSA X)),the carrier of S:] holds @ nt,x = { [((Den o2,(ParsedTermsOSA X)) . x2),s3] where o2 is OperSymbol of S, x2 is Element of Args o2,(ParsedTermsOSA X), s3 is Element of S : ( ex o1 being OperSymbol of S st
( nt = [o1,the carrier of S] & o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 ) & ex w3 being Element of the carrier of S * st
( dom w3 = dom x & ( for y being Nat st y in dom x holds
[(x2 . y),(w3 /. y)] in x . y ) ) )
}
;

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
func PTClasses X -> Function of TS (DTConOSA X), bool [:(TS (DTConOSA X)),the carrier of S:] means :Def22: :: OSAFREE:def 22
( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
it . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
it . (nt -tree ts) = @ nt,(it * ts) ) );
existence
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 ) & ( 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) ) )
proof end;
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 ) & ( 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) ) & ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b2 . (root-tree t) = @ t ) & ( 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
proof end;
end;

:: deftheorem Def22 defines PTClasses OSAFREE:def 22 :
for S being locally_directed OrderSortedSign
for X being V3 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 ) & ( 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 Th20: :: OSAFREE:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for t being Element of TS (DTConOSA X) holds
( ( for s being Element of S holds
( t in the Sorts of (ParsedTermsOSA X) . s iff [t,s] in (PTClasses X) . t ) ) & ( for s being Element of S
for y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . y ) )
proof end;

theorem Th21: :: OSAFREE:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for t being Element of TS (DTConOSA X)
for s being Element of S st ex y being Element of TS (DTConOSA X) st [y,s] in (PTClasses X) . t holds
[t,s] in (PTClasses X) . t
proof end;

theorem Th22: :: OSAFREE:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for x, y being Element of TS (DTConOSA X)
for s1, s2 being Element of S st s1 <= s2 & x in the Sorts of (ParsedTermsOSA X) . s1 & y in the Sorts of (ParsedTermsOSA X) . s1 holds
( [y,s1] in (PTClasses X) . x iff [y,s2] in (PTClasses X) . x )
proof end;

theorem Th23: :: OSAFREE:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for x, y, z being Element of TS (DTConOSA X)
for s being Element of S st [y,s] in (PTClasses X) . x & [z,s] in (PTClasses X) . y holds
[x,s] in (PTClasses X) . z
proof end;

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
func PTCongruence X -> MSEquivalence-like OrderSortedRelation of ParsedTermsOSA X means :Def23: :: OSAFREE:def 23
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 }
proof end;
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 } ) & ( 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
proof end;
end;

:: deftheorem Def23 defines PTCongruence OSAFREE:def 23 :
for S being locally_directed OrderSortedSign
for X being V3 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 Th24: :: OSAFREE:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for x, y, s being set st [x,s] in (PTClasses X) . y holds
( x in TS (DTConOSA X) & y in TS (DTConOSA X) & s in the carrier of S )
proof end;

theorem Th25: :: OSAFREE:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 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 & [x,s1] in (PTClasses X) . y ) )
proof end;

theorem Th26: :: OSAFREE:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for s being Element of S
for x being Element of the Sorts of (ParsedTermsOSA X) . s holds OSClass (PTCongruence X),x = proj1 ((PTClasses X) . x)
proof end;

theorem Th27: :: OSAFREE:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 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 ) & ( 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 & y = root-tree [x,s1] ) ) ) ) & ( for o1, o2 being OperSymbol of S
for x1 being Element of Args o1,(ParsedTermsOSA X)
for x2 being Element of Args o2,(ParsedTermsOSA X)
for s3 being Element of S holds
( [((Den o1,(ParsedTermsOSA X)) . x1),((Den o2,(ParsedTermsOSA X)) . x2)] in R . s3 iff ( o1 ~= o2 & len (the_arity_of o1) = len (the_arity_of o2) & the_result_sort_of o1 <= s3 & the_result_sort_of o2 <= s3 & ex w3 being Element of the carrier of S * st
( dom w3 = dom x1 & ( for y being Nat st y in dom w3 holds
[(x1 . y),(x2 . y)] in R . (w3 /. y) ) ) ) ) ) ) )
proof end;

theorem Th28: :: OSAFREE:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S holds PTCongruence X is monotone
proof end;

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

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
let s be Element of S;
func PTVars s,X -> Subset of (the Sorts of (ParsedTermsOSA X) . s) means :Def24: :: OSAFREE:def 24
for x being set holds
( x in it iff ex a being set st
( a in X . s & 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 & x = root-tree [a,s] ) )
proof end;
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 & x = root-tree [a,s] ) ) ) & ( for x being set holds
( x in b2 iff ex a being set st
( a in X . s & x = root-tree [a,s] ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def24 defines PTVars OSAFREE:def 24 :
for S being locally_directed OrderSortedSign
for X being V3 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 & x = root-tree [a,s] ) ) );

registration
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
let s be Element of S;
cluster PTVars s,X -> non empty ;
coherence
not PTVars s,X is empty
proof end;
end;

theorem Th29: :: OSAFREE:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for s being Element of S holds PTVars s,X = { (root-tree t) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }
proof end;

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
func PTVars X -> MSSubset of (ParsedTermsOSA X) means :Def25: :: OSAFREE:def 25
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
proof end;
uniqueness
for b1, b2 being MSSubset of (ParsedTermsOSA X) st ( for s being Element of S holds b1 . s = PTVars s,X ) & ( for s being Element of S holds b2 . s = PTVars s,X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def25 defines PTVars OSAFREE:def 25 :
for S being locally_directed OrderSortedSign
for X being V3 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:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S holds PTVars X is non-empty
proof end;

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
let s be Element of S;
func OSFreeGen s,X -> Subset of (the Sorts of (FreeOSA X) . s) means :Def26: :: OSAFREE:def 26
for x being set holds
( x in it iff ex a being set st
( a in X . s & 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 & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) )
proof end;
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 & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) ) ) & ( for x being set holds
( x in b2 iff ex a being set st
( a in X . s & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def26 defines OSFreeGen OSAFREE:def 26 :
for S being locally_directed OrderSortedSign
for X being V3 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 & x = ((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree [a,s]) ) ) );

registration
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
let s be Element of S;
cluster OSFreeGen s,X -> non empty ;
coherence
not OSFreeGen s,X is empty
proof end;
end;

theorem Th31: :: OSAFREE:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for s being Element of S holds OSFreeGen s,X = { (((OSNat_Hom (ParsedTermsOSA X),(LCongruence X)) . s) . (root-tree t)) where t is Symbol of (DTConOSA X) : ( t in Terminals (DTConOSA X) & t `2 = s ) }
proof end;

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
func OSFreeGen X -> OSGeneratorSet of FreeOSA X means :Def27: :: OSAFREE:def 27
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
proof end;
uniqueness
for b1, b2 being OSGeneratorSet of FreeOSA X st ( for s being Element of S holds b1 . s = OSFreeGen s,X ) & ( for s being Element of S holds b2 . s = OSFreeGen s,X ) holds
b1 = b2
proof end;
end;

:: deftheorem Def27 defines OSFreeGen OSAFREE:def 27 :
for S being locally_directed OrderSortedSign
for X being V3 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 Th32: :: OSAFREE:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S holds OSFreeGen X is non-empty
proof end;

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

definition
let S be locally_directed OrderSortedSign;
let X be V3 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 :Def28: :: OSAFREE:def 28
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
proof end;
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 ) & ( 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
proof end;
end;

:: deftheorem Def28 defines OSClass OSAFREE:def 28 :
for S being locally_directed OrderSortedSign
for X being V3 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 Th33: :: OSAFREE:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for R being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds t in OSClass R,t
proof end;

theorem Th34: :: OSAFREE:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for s being Element of S
for t being Element of TS (DTConOSA X)
for x, x1 being set st x in X . s & t = root-tree [x,s] holds
( x1 in OSClass (PTCongruence X),t iff x1 = t )
proof end;

theorem Th35: :: OSAFREE:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for R being OSCongruence of ParsedTermsOSA X
for t1, t2 being Element of TS (DTConOSA X) holds
( t2 in OSClass R,t1 iff OSClass R,t1 = OSClass R,t2 )
proof end;

theorem Th36: :: OSAFREE:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for R1, R2 being OSCongruence of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) st R1 c= R2 holds
OSClass R1,t c= OSClass R2,t
proof end;

theorem Th37: :: OSAFREE:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for s being Element of S
for t being Element of TS (DTConOSA X)
for x, x1 being set st x in X . s & t = root-tree [x,s] holds
( x1 in OSClass (LCongruence X),t iff x1 = t )
proof end;

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
let A be V3 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 :Def29: :: OSAFREE:def 29
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)
proof end;
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) ) & ( for f being Function st f = F . (t `2 ) holds
b2 = f . (root-tree t) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def29 defines pi OSAFREE:def 29 :
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for A being V3 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 Th38: :: OSAFREE:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for U1 being non-empty monotone OSAlgebra of S
for f being ManySortedFunction of PTVars X,the Sorts of U1 ex h being ManySortedFunction of (ParsedTermsOSA X),U1 st
( h is_homomorphism ParsedTermsOSA X,U1 & h is order-sorted & h || (PTVars X) = f )
proof end;

definition
let S be locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
let s be Element of S;
func NHReverse s,X -> Function of OSFreeGen s,X, PTVars s,X means :: OSAFREE:def 30
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
proof end;
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 ) & ( 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
proof end;
end;

:: deftheorem defines NHReverse OSAFREE:def 30 :
for S being locally_directed OrderSortedSign
for X being V3 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 V3 ManySortedSet of S;
func NHReverse X -> ManySortedFunction of OSFreeGen X, PTVars X means :: OSAFREE:def 31
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
proof end;
uniqueness
for b1, b2 being ManySortedFunction of OSFreeGen X, PTVars X st ( for s being Element of S holds b1 . s = NHReverse s,X ) & ( for s being Element of S holds b2 . s = NHReverse s,X ) holds
b1 = b2
proof end;
end;

:: deftheorem defines NHReverse OSAFREE:def 31 :
for S being locally_directed OrderSortedSign
for X being V3 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 Th39: :: OSAFREE:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S holds OSFreeGen X is osfree
proof end;

theorem Th40: :: OSAFREE:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being locally_directed OrderSortedSign
for X being V3 ManySortedSet of S holds FreeOSA X is osfree
proof end;

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

definition
let S be monotone regular locally_directed OrderSortedSign;
let X be V3 ManySortedSet of S;
func PTMin X -> Function of TS (DTConOSA X), TS (DTConOSA X) means :Def32: :: OSAFREE:def 32
( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
it . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
it . (nt -tree ts) = pi (@ X,nt),(it * ts) ) );
existence
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 ) & ( 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) ) )
proof end;
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 ) & ( 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) ) & ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b2 . (root-tree t) = pi t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b2 . (nt -tree ts) = pi (@ X,nt),(b2 * ts) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def32 defines PTMin OSAFREE:def 32 :
for S being monotone regular locally_directed OrderSortedSign
for X being V3 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 ) & ( 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 Th41: :: OSAFREE:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being monotone regular locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for t being Element of TS (DTConOSA X) holds
( (PTMin X) . t in OSClass (PTCongruence X),t & LeastSort ((PTMin X) . t) <= LeastSort t & ( for s being Element of S
for x being set st x in X . s & t = root-tree [x,s] holds
(PTMin X) . t = t ) & ( for o being OperSymbol of S
for ts being FinSequence of TS (DTConOSA X) st OSSym o,X ==> roots ts & t = (OSSym o,X) -tree ts holds
( LeastSorts ((PTMin X) * ts) <= the_arity_of o & OSSym o,X ==> roots ((PTMin X) * ts) & OSSym (LBound o,(LeastSorts ((PTMin X) * ts))),X ==> roots ((PTMin X) * ts) & (PTMin X) . t = (OSSym (LBound o,(LeastSorts ((PTMin X) * ts))),X) -tree ((PTMin X) * ts) ) ) )
proof end;

theorem Th42: :: OSAFREE:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being monotone regular locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for t, t1 being Element of TS (DTConOSA X) st t1 in OSClass (PTCongruence X),t holds
(PTMin X) . t1 = (PTMin X) . t
proof end;

theorem Th43: :: OSAFREE:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being monotone regular locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for t1, t2 being Element of TS (DTConOSA X) holds
( t2 in OSClass (PTCongruence X),t1 iff (PTMin X) . t2 = (PTMin X) . t1 )
proof end;

theorem Th44: :: OSAFREE:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being monotone regular locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for t1 being Element of TS (DTConOSA X) holds (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1
proof end;

theorem Th45: :: OSAFREE:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being monotone regular locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X
for t being Element of TS (DTConOSA X) holds [t,((PTMin X) . t)] in R . (LeastSort t)
proof end;

theorem Th46: :: OSAFREE:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being monotone regular locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for R being MSEquivalence-like monotone OrderSortedRelation of ParsedTermsOSA X holds PTCongruence X c= R
proof end;

theorem :: OSAFREE:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being monotone regular locally_directed OrderSortedSign
for X being V3 ManySortedSet of S holds LCongruence X = PTCongruence X
proof end;

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

:: deftheorem Def33 defines MinTerm OSAFREE:def 33 :
for S being monotone regular locally_directed OrderSortedSign
for X being V3 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 V3 ManySortedSet of S;
func MinTerms X -> Subset of (TS (DTConOSA X)) equals :: OSAFREE:def 34
rng (PTMin X);
correctness
coherence
rng (PTMin X) is Subset of (TS (DTConOSA X))
;
by RELSET_1:12;
end;

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

theorem :: OSAFREE:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for S being monotone regular locally_directed OrderSortedSign
for X being V3 ManySortedSet of S
for x being set holds
( x is MinTerm of S,X iff x in MinTerms X )
proof end;