let S be non void Signature; :: thesis: for X, Y being V8() ManySortedSet of the carrier of S

for t being Term of S,Y st variables_in t c= X holds

t is Term of S,X

let X, Y be V8() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,Y st variables_in t c= X holds

t is Term of S,X

defpred S_{1}[ DecoratedTree] means ( Y variables_in $1 c= X implies $1 is Term of S,X );

let t be Term of S,Y; :: thesis: ( variables_in t c= X implies t is Term of S,X )

A1: for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,Y) st ( for t being Term of S,Y st t in rng p holds

S_{1}[t] ) holds

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

then A8: Y variables_in t c= X by Th15;

A9: for s being SortSymbol of S

for x being Element of Y . s holds S_{1}[ root-tree [x,s]]
_{1}[t]
from MSATERM:sch 1(A9, A1);

hence t is Term of S,X by A8; :: thesis: verum

for t being Term of S,Y st variables_in t c= X holds

t is Term of S,X

let X, Y be V8() ManySortedSet of the carrier of S; :: thesis: for t being Term of S,Y st variables_in t c= X holds

t is Term of S,X

defpred S

let t be Term of S,Y; :: thesis: ( variables_in t c= X implies t is Term of S,X )

A1: for o being OperSymbol of S

for p being ArgumentSeq of Sym (o,Y) st ( for t being Term of S,Y st t in rng p holds

S

S

proof

assume
variables_in t c= X
; :: thesis: t is Term of S,X
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,Y) st ( for t being Term of S,Y 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,Y); :: thesis: ( ( for t being Term of S,Y st t in rng p holds

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

assume that

A2: for t being Term of S,Y st t in rng p & Y variables_in t c= X holds

t is Term of S,X and

A3: Y variables_in ([o, the carrier of S] -tree p) c= X ; :: thesis: [o, the carrier of S] -tree p is Term of S,X

then reconsider p = p as ArgumentSeq of Sym (o,X) by A4, MSATERM:24;

(Sym (o,X)) -tree p is Term of S,X ;

hence [o, the carrier of S] -tree p is Term of S,X by MSAFREE:def 9; :: thesis: verum

end;S

S

let p be ArgumentSeq of Sym (o,Y); :: thesis: ( ( for t being Term of S,Y st t in rng p holds

S

assume that

A2: for t being Term of S,Y st t in rng p & Y variables_in t c= X holds

t is Term of S,X and

A3: Y variables_in ([o, the carrier of S] -tree p) c= X ; :: thesis: [o, the carrier of S] -tree p is Term of S,X

A4: now :: thesis: for i being Nat st i in dom p holds

ex t9 being Term of S,X st

( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )

len p = len (the_arity_of o)
by MSATERM:22;ex t9 being Term of S,X st

( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )

let i be Nat; :: thesis: ( i in dom p implies ex t9 being Term of S,X st

( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) )

assume A5: i in dom p ; :: thesis: ex t9 being Term of S,X st

( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )

then reconsider t = p . i as Term of S,Y by MSATERM:22;

A6: t in rng p by A5, FUNCT_1:def 3;

Y variables_in t c= X

take t9 = t9; :: thesis: ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )

thus t9 = p . i ; :: thesis: the_sort_of t9 = (the_arity_of o) . i

the_sort_of t = (the_arity_of o) . i by A5, MSATERM:23;

hence the_sort_of t9 = (the_arity_of o) . i by Th29; :: thesis: verum

end;( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i ) )

assume A5: i in dom p ; :: thesis: ex t9 being Term of S,X st

( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )

then reconsider t = p . i as Term of S,Y by MSATERM:22;

A6: t in rng p by A5, FUNCT_1:def 3;

Y variables_in t c= X

proof

then reconsider t9 = t as Term of S,X by A2, A6;
let y be object ; :: according to PBOOLE:def 2 :: thesis: ( not y in the carrier of S or (Y variables_in t) . y c= X . y )

assume y in the carrier of S ; :: thesis: (Y variables_in t) . y c= X . y

then reconsider s = y as SortSymbol of S ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Y variables_in t) . y or x in X . y )

assume x in (Y variables_in t) . y ; :: thesis: x in X . y

then A7: x in (Y variables_in ([o, the carrier of S] -tree p)) . s by A6, Th13;

(Y variables_in ([o, the carrier of S] -tree p)) . s c= X . s by A3;

hence x in X . y by A7; :: thesis: verum

end;assume y in the carrier of S ; :: thesis: (Y variables_in t) . y c= X . y

then reconsider s = y as SortSymbol of S ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Y variables_in t) . y or x in X . y )

assume x in (Y variables_in t) . y ; :: thesis: x in X . y

then A7: x in (Y variables_in ([o, the carrier of S] -tree p)) . s by A6, Th13;

(Y variables_in ([o, the carrier of S] -tree p)) . s c= X . s by A3;

hence x in X . y by A7; :: thesis: verum

take t9 = t9; :: thesis: ( t9 = p . i & the_sort_of t9 = (the_arity_of o) . i )

thus t9 = p . i ; :: thesis: the_sort_of t9 = (the_arity_of o) . i

the_sort_of t = (the_arity_of o) . i by A5, MSATERM:23;

hence the_sort_of t9 = (the_arity_of o) . i by Th29; :: thesis: verum

then reconsider p = p as ArgumentSeq of Sym (o,X) by A4, MSATERM:24;

(Sym (o,X)) -tree p is Term of S,X ;

hence [o, the carrier of S] -tree p is Term of S,X by MSAFREE:def 9; :: thesis: verum

then A8: Y variables_in t c= X by Th15;

A9: for s being SortSymbol of S

for x being Element of Y . s holds S

proof

for t being Term of S,Y holds S
let s be SortSymbol of S; :: thesis: for x being Element of Y . s holds S_{1}[ root-tree [x,s]]

let x be Element of Y . s; :: thesis: S_{1}[ root-tree [x,s]]

assume Y variables_in (root-tree [x,s]) c= X ; :: thesis: root-tree [x,s] is Term of S,X

then A10: (Y variables_in (root-tree [x,s])) . s c= X . s ;

(Y variables_in (root-tree [x,s])) . s = {x} by Th12;

then x in X . s by A10, ZFMISC_1:31;

hence root-tree [x,s] is Term of S,X by MSATERM:4; :: thesis: verum

end;let x be Element of Y . s; :: thesis: S

assume Y variables_in (root-tree [x,s]) c= X ; :: thesis: root-tree [x,s] is Term of S,X

then A10: (Y variables_in (root-tree [x,s])) . s c= X . s ;

(Y variables_in (root-tree [x,s])) . s = {x} by Th12;

then x in X . s by A10, ZFMISC_1:31;

hence root-tree [x,s] is Term of S,X by MSATERM:4; :: thesis: verum

hence t is Term of S,X by A8; :: thesis: verum