let S be non empty non void ManySortedSign ; :: thesis: for X being ManySortedSet of the carrier of S

for t being Term of S,(X (\/) ( the carrier of S --> {0}))

for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds

t in the Sorts of (Free (S,X)) . s

let X be ManySortedSet of the carrier of S; :: thesis: for t being Term of S,(X (\/) ( the carrier of S --> {0}))

for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds

t in the Sorts of (Free (S,X)) . s

set Y = X (\/) ( the carrier of S --> {0});

set T = the Sorts of (Free (S,X));

defpred S_{1}[ set ] means for s being SortSymbol of S st $1 in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds

$1 in the Sorts of (Free (S,X)) . s;

A1: ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) by Def1;

then reconsider TT = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by MSUALG_2:def 9;

_{1}[t]
from MSATERM:sch 1(A13, A2); :: thesis: verum

for t being Term of S,(X (\/) ( the carrier of S --> {0}))

for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds

t in the Sorts of (Free (S,X)) . s

let X be ManySortedSet of the carrier of S; :: thesis: for t being Term of S,(X (\/) ( the carrier of S --> {0}))

for s being SortSymbol of S st t in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s holds

t in the Sorts of (Free (S,X)) . s

set Y = X (\/) ( the carrier of S --> {0});

set T = the Sorts of (Free (S,X));

defpred S

$1 in the Sorts of (Free (S,X)) . s;

A1: ex A being MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) st

( Free (S,X) = GenMSAlg A & A = (Reverse (X (\/) ( the carrier of S --> {0}))) "" X ) by Def1;

then reconsider TT = the Sorts of (Free (S,X)) as MSSubset of (FreeMSA (X (\/) ( the carrier of S --> {0}))) by MSUALG_2:def 9;

A2: now :: thesis: for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) st ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds

S_{1}[t] ) holds

S_{1}[[o, the carrier of S] -tree p]

A12:
S -Terms (X,(X (\/) ( the carrier of S --> {0}))) c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0})))
by PBOOLE:def 18;for p being ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) st ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds

S

S

let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) st ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds

S_{1}[t] ) holds

S_{1}[[o, the carrier of S] -tree p]

let p be ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))); :: thesis: ( ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds

S_{1}[t] ) implies S_{1}[[o, the carrier of S] -tree p] )

assume A3: for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds

S_{1}[t]
; :: thesis: S_{1}[[o, the carrier of S] -tree p]

thus S_{1}[[o, the carrier of S] -tree p]
:: thesis: verum

end;S

S

let p be ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))); :: thesis: ( ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds

S

assume A3: for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds

S

thus S

proof

let s be SortSymbol of S; :: thesis: ( [o, the carrier of S] -tree p in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s implies [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s )

assume A4: [o, the carrier of S] -tree p in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s

A5: Sym (o,(X (\/) ( the carrier of S --> {0}))) = [o, the carrier of S] by MSAFREE:def 9;

the_sort_of ((Sym (o,(X (\/) ( the carrier of S --> {0})))) -tree p) = the_result_sort_of o by MSATERM:20;

then A6: s = the_result_sort_of o by A4, A5, Th17;

then A7: rng p c= Union (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) by A4, A5, Th19;

A8: rng p c= Union TT

hence [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s by A5, A6, A8, Th20; :: thesis: verum

end;assume A4: [o, the carrier of S] -tree p in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s

A5: Sym (o,(X (\/) ( the carrier of S --> {0}))) = [o, the carrier of S] by MSAFREE:def 9;

the_sort_of ((Sym (o,(X (\/) ( the carrier of S --> {0})))) -tree p) = the_result_sort_of o by MSATERM:20;

then A6: s = the_result_sort_of o by A4, A5, Th17;

then A7: rng p c= Union (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) by A4, A5, Th19;

A8: rng p c= Union TT

proof

TT is opers_closed
by A1, MSUALG_2:def 9;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng p or x in Union TT )

assume A9: x in rng p ; :: thesis: x in Union TT

then consider y being object such that

A10: y in dom (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) and

A11: x in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y by A7, CARD_5:2;

reconsider y = y as SortSymbol of S by A10;

(S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y = (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y ;

then reconsider x = x as Term of S,(X (\/) ( the carrier of S --> {0})) by A11, Th16;

( dom the Sorts of (Free (S,X)) = the carrier of S & x in the Sorts of (Free (S,X)) . y ) by A3, A9, A11, PARTFUN1:def 2;

hence x in Union TT by CARD_5:2; :: thesis: verum

end;assume A9: x in rng p ; :: thesis: x in Union TT

then consider y being object such that

A10: y in dom (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) and

A11: x in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y by A7, CARD_5:2;

reconsider y = y as SortSymbol of S by A10;

(S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y = (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . y ;

then reconsider x = x as Term of S,(X (\/) ( the carrier of S --> {0})) by A11, Th16;

( dom the Sorts of (Free (S,X)) = the carrier of S & x in the Sorts of (Free (S,X)) . y ) by A3, A9, A11, PARTFUN1:def 2;

hence x in Union TT by CARD_5:2; :: thesis: verum

hence [o, the carrier of S] -tree p in the Sorts of (Free (S,X)) . s by A5, A6, A8, Th20; :: thesis: verum

A13: now :: thesis: for s1 being SortSymbol of S

for v being Element of (X (\/) ( the carrier of S --> {0})) . s1 holds S_{1}[ root-tree [v,s1]]

thus
for t being Term of S,(X (\/) ( the carrier of S --> {0})) holds Sfor v being Element of (X (\/) ( the carrier of S --> {0})) . s1 holds S

let s1 be SortSymbol of S; :: thesis: for v being Element of (X (\/) ( the carrier of S --> {0})) . s1 holds S_{1}[ root-tree [v,s1]]

let v be Element of (X (\/) ( the carrier of S --> {0})) . s1; :: thesis: S_{1}[ root-tree [v,s1]]

thus S_{1}[ root-tree [v,s1]]
:: thesis: verum

end;let v be Element of (X (\/) ( the carrier of S --> {0})) . s1; :: thesis: S

thus S

proof

reconsider t = root-tree [v,s1] as Term of S,(X (\/) ( the carrier of S --> {0})) by MSATERM:4;

let s be SortSymbol of S; :: thesis: ( root-tree [v,s1] in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s implies root-tree [v,s1] in the Sorts of (Free (S,X)) . s )

assume A14: root-tree [v,s1] in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: root-tree [v,s1] in the Sorts of (Free (S,X)) . s

(S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) . s by A12;

then A15: the_sort_of t = s by A14, Th7;

A16: the_sort_of t = s1 by MSATERM:14;

then v in X . s by A14, A15, Th18;

hence root-tree [v,s1] in the Sorts of (Free (S,X)) . s by A15, A16, Th4; :: thesis: verum

end;let s be SortSymbol of S; :: thesis: ( root-tree [v,s1] in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s implies root-tree [v,s1] in the Sorts of (Free (S,X)) . s )

assume A14: root-tree [v,s1] in (S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s ; :: thesis: root-tree [v,s1] in the Sorts of (Free (S,X)) . s

(S -Terms (X,(X (\/) ( the carrier of S --> {0})))) . s c= the Sorts of (FreeMSA (X (\/) ( the carrier of S --> {0}))) . s by A12;

then A15: the_sort_of t = s by A14, Th7;

A16: the_sort_of t = s1 by MSATERM:14;

then v in X . s by A14, A15, Th18;

hence root-tree [v,s1] in the Sorts of (Free (S,X)) . s by A15, A16, Th4; :: thesis: verum