let S be non void Signature; for X being V9() ManySortedSet of the carrier of S
for t being Element of (Free (S,X)) holds
( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) )
let X be V9() ManySortedSet of the carrier of S; for t being Element of (Free (S,X)) holds
( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) )
let t be Element of (Free (S,X)); ( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) )
set V = X (\/) ( the carrier of S --> {0});
reconsider t9 = t as Term of S,(X (\/) ( the carrier of S --> {0})) by MSAFREE3:8;
defpred S1[ set ] means ( not $1 is Element of (Free (S,X)) or ex s being SortSymbol of S ex v being set st
( $1 = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( $1 = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) );
A1:
for s being SortSymbol of S
for v being Element of (X (\/) ( the carrier of S --> {0})) . s holds S1[ root-tree [v,s]]
proof
let s be
SortSymbol of
S;
for v being Element of (X (\/) ( the carrier of S --> {0})) . s holds S1[ root-tree [v,s]]let v be
Element of
(X (\/) ( the carrier of S --> {0})) . s;
S1[ root-tree [v,s]]
set t =
root-tree [v,s];
assume A2:
root-tree [v,s] is
Element of
(Free (S,X))
;
( ex s being SortSymbol of S ex v being set st
( root-tree [v,s] = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( root-tree [v,s] = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) )
{} in dom (root-tree [v,s])
by TREES_1:22;
then
(root-tree [v,s]) . {} in rng (root-tree [v,s])
by FUNCT_1:3;
then
[v,s] in rng (root-tree [v,s])
by TREES_4:3;
then
v in X . s
by A2, MSAFREE3:35;
hence
( ex
s being
SortSymbol of
S ex
v being
set st
(
root-tree [v,s] = root-tree [v,s] &
v in X . s ) or ex
o being
OperSymbol of
S ex
p being
FinSequence of
(Free (S,X)) st
(
root-tree [v,s] = [o, the carrier of S] -tree p &
len p = len (the_arity_of o) &
p is
DTree-yielding &
p is
ArgumentSeq of
Sym (
o,
(X (\/) ( the carrier of S --> {0}))) ) )
;
verum
end;
A3:
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
S1[t] ) holds
S1[[o, the carrier of S] -tree p]
proof
let o be
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
S1[t] ) holds
S1[[o, the carrier of S] -tree p]let p be
ArgumentSeq of
Sym (
o,
(X (\/) ( the carrier of S --> {0})));
( ( for t being Term of S,(X (\/) ( the carrier of S --> {0})) st t in rng p holds
S1[t] ) implies S1[[o, the carrier of S] -tree p] )
assume
for
t being
Term of
S,
(X (\/) ( the carrier of S --> {0})) st
t in rng p holds
S1[
t]
;
S1[[o, the carrier of S] -tree p]
set t =
[o, the carrier of S] -tree p;
assume
[o, the carrier of S] -tree p is
Element of
(Free (S,X))
;
( ex s being SortSymbol of S ex v being set st
( [o, the carrier of S] -tree p = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( [o, the carrier of S] -tree p = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) )
then consider s being
object such that A4:
s in dom the
Sorts of
(Free (S,X))
and A5:
[o, the carrier of S] -tree p in the
Sorts of
(Free (S,X)) . s
by CARD_5:2;
reconsider s =
s as
Element of
S by A4;
A6:
the
Sorts of
(Free (S,X)) = S -Terms (
X,
(X (\/) ( the carrier of S --> {0})))
by MSAFREE3:24;
the_sort_of ((Sym (o,(X (\/) ( the carrier of S --> {0})))) -tree p) = the_result_sort_of o
by MSATERM:20;
then
s = the_result_sort_of o
by A5, A6, MSAFREE3:17;
then
rng p c= Union (S -Terms (X,(X (\/) ( the carrier of S --> {0}))))
by A5, A6, MSAFREE3:19;
then A7:
p is
FinSequence of
(Free (S,X))
by A6, FINSEQ_1:def 4;
len (the_arity_of o) = len p
by MSATERM:22;
hence
( ex
s being
SortSymbol of
S ex
v being
set st
(
[o, the carrier of S] -tree p = root-tree [v,s] &
v in X . s ) or ex
o being
OperSymbol of
S ex
p being
FinSequence of
(Free (S,X)) st
(
[o, the carrier of S] -tree p = [o, the carrier of S] -tree p &
len p = len (the_arity_of o) &
p is
DTree-yielding &
p is
ArgumentSeq of
Sym (
o,
(X (\/) ( the carrier of S --> {0}))) ) )
by A7;
verum
end;
for t being Term of S,(X (\/) ( the carrier of S --> {0})) holds S1[t]
from MSATERM:sch 1(A1, A3);
then
S1[t9]
;
hence
( ex s being SortSymbol of S ex v being set st
( t = root-tree [v,s] & v in X . s ) or ex o being OperSymbol of S ex p being FinSequence of (Free (S,X)) st
( t = [o, the carrier of S] -tree p & len p = len (the_arity_of o) & p is DTree-yielding & p is ArgumentSeq of Sym (o,(X (\/) ( the carrier of S --> {0}))) ) )
; verum