let S be non void Signature; :: thesis: for X being V6() ManySortedSet of
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 V6() ManySortedSet of ; :: thesis: 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); :: thesis: ( 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 t' = t as Term of S,(X \/ (the carrier of S --> {0 })) by MSAFREE3:9;
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;
:: thesis: 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;
:: thesis: S1[ root-tree [v,s]]
set t =
root-tree [v,s];
assume B1:
root-tree [v,s] is
Element of
(Free S,X)
;
:: thesis: ( 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:47;
then
(root-tree [v,s]) . {} in rng (root-tree [v,s])
by FUNCT_1:12;
then
[v,s] in rng (root-tree [v,s])
by TREES_4:3;
then
v in X . s
by B1, MSAFREE3:36;
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 })) ) )
;
:: thesis: verum
end;
A2:
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;
:: 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
S1[t] ) holds
S1[[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
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]
;
:: thesis: 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)
;
:: thesis: ( 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
set such that B4:
(
s in dom the
Sorts of
(Free S,X) &
[o,the carrier of S] -tree p in the
Sorts of
(Free S,X) . s )
by CARD_5:10;
reconsider s =
s as
Element of
S by B4, PARTFUN1:def 4;
B5:
(
[o,the carrier of S] -tree p = (Sym o,(X \/ (the carrier of S --> {0 }))) -tree p & the
Sorts of
(Free S,X) = S -Terms X,
(X \/ (the carrier of S --> {0 })) &
the_sort_of ((Sym o,(X \/ (the carrier of S --> {0 }))) -tree p) = the_result_sort_of o )
by MSAFREE3:25, MSATERM:20;
then
s = the_result_sort_of o
by B4, MSAFREE3:18;
then
rng p c= Union (S -Terms X,(X \/ (the carrier of S --> {0 })))
by B4, B5, MSAFREE3:20;
then
(
p is
FinSequence of
(Free S,X) &
len (the_arity_of o) = len p )
by B5, FINSEQ_1:def 4, 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 })) ) )
;
:: thesis: verum
end;
for t being Term of S,(X \/ (the carrier of S --> {0 })) holds S1[t]
from MSATERM:sch 1(A1, A2);
then
S1[t']
;
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 })) ) )
; :: thesis: verum