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

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

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

defpred S_{1}[ DecoratedTree] means S variables_in $1 c= X;

A1: for o being OperSymbol of S

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

S_{1}[t] ) holds

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

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

hence for t being Term of S,X holds S variables_in t c= X ; :: thesis: verum

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

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

defpred S

A1: for o being OperSymbol of S

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

S

S

proof

A7:
for s being SortSymbol of S
let o be OperSymbol of S; :: thesis: for p being ArgumentSeq of Sym (o,X) st ( for t being Term of S,X 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); :: thesis: ( ( for t being Term of S,X st t in rng p holds

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

assume A2: for t being Term of S,X st t in rng p holds

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

set q = [o, the carrier of S] -tree p;

thus S variables_in ([o, the carrier of S] -tree p) c= X :: thesis: verum

end;S

S

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

S

assume A2: for t being Term of S,X st t in rng p holds

S variables_in t c= X ; :: thesis: S

set q = [o, the carrier of S] -tree p;

thus S variables_in ([o, the carrier of S] -tree p) c= X :: thesis: verum

proof

let s9 be object ; :: according to PBOOLE:def 2 :: thesis: ( not s9 in the carrier of S or (S variables_in ([o, the carrier of S] -tree p)) . s9 c= X . s9 )

assume s9 in the carrier of S ; :: thesis: (S variables_in ([o, the carrier of S] -tree p)) . s9 c= X . s9

then reconsider z = s9 as SortSymbol of S ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (S variables_in ([o, the carrier of S] -tree p)) . s9 or x in X . s9 )

assume x in (S variables_in ([o, the carrier of S] -tree p)) . s9 ; :: thesis: x in X . s9

then consider t being DecoratedTree such that

A3: t in rng p and

A4: x in (S variables_in t) . z by Th11;

consider i being object such that

A5: i in dom p and

A6: t = p . i by A3, FUNCT_1:def 3;

reconsider i = i as Nat by A5;

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

S variables_in t c= X by A2, A3, A6;

then (S variables_in t) . z c= X . z ;

hence x in X . s9 by A4, A6; :: thesis: verum

end;assume s9 in the carrier of S ; :: thesis: (S variables_in ([o, the carrier of S] -tree p)) . s9 c= X . s9

then reconsider z = s9 as SortSymbol of S ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (S variables_in ([o, the carrier of S] -tree p)) . s9 or x in X . s9 )

assume x in (S variables_in ([o, the carrier of S] -tree p)) . s9 ; :: thesis: x in X . s9

then consider t being DecoratedTree such that

A3: t in rng p and

A4: x in (S variables_in t) . z by Th11;

consider i being object such that

A5: i in dom p and

A6: t = p . i by A3, FUNCT_1:def 3;

reconsider i = i as Nat by A5;

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

S variables_in t c= X by A2, A3, A6;

then (S variables_in t) . z c= X . z ;

hence x in X . s9 by A4, A6; :: thesis: verum

for v being Element of X . s holds S

proof

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

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

thus S variables_in (root-tree [v,s]) c= X :: thesis: verum

end;let v be Element of X . s; :: thesis: S

thus S variables_in (root-tree [v,s]) c= X :: thesis: verum

proof

let s9 be object ; :: according to PBOOLE:def 2 :: thesis: ( not s9 in the carrier of S or (S variables_in (root-tree [v,s])) . s9 c= X . s9 )

assume s9 in the carrier of S ; :: thesis: (S variables_in (root-tree [v,s])) . s9 c= X . s9

then reconsider z = s9 as SortSymbol of S ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (S variables_in (root-tree [v,s])) . s9 or x in X . s9 )

assume A8: x in (S variables_in (root-tree [v,s])) . s9 ; :: thesis: x in X . s9

then A9: ( s <> z implies x in {} ) by Th10;

( s = z implies x in {v} ) by A8, Th10;

hence x in X . s9 by A9; :: thesis: verum

end;assume s9 in the carrier of S ; :: thesis: (S variables_in (root-tree [v,s])) . s9 c= X . s9

then reconsider z = s9 as SortSymbol of S ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (S variables_in (root-tree [v,s])) . s9 or x in X . s9 )

assume A8: x in (S variables_in (root-tree [v,s])) . s9 ; :: thesis: x in X . s9

then A9: ( s <> z implies x in {} ) by Th10;

( s = z implies x in {v} ) by A8, Th10;

hence x in X . s9 by A9; :: thesis: verum

hence for t being Term of S,X holds S variables_in t c= X ; :: thesis: verum