let S be non empty non void ManySortedSign ; :: thesis: for V being V5() ManySortedSet of
for o being OperSymbol of S
for a being FinSequence holds
( ( [o,the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym o,V )
let V be V5() ManySortedSet of ; :: thesis: for o being OperSymbol of S
for a being FinSequence holds
( ( [o,the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym o,V )
let o be OperSymbol of S; :: thesis: for a being FinSequence holds
( ( [o,the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym o,V )
let a be FinSequence; :: thesis: ( ( [o,the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym o,V )
A1:
S -Terms V = TS (DTConMSA V)
;
A2:
[o,the carrier of S] = Sym o,V
by MSAFREE:def 11;
hereby :: thesis: ( a is ArgumentSeq of Sym o,V implies ( [o,the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) )
assume
[o,the carrier of S] -tree a in S -Terms V
;
:: thesis: ( a is DTree-yielding implies a is ArgumentSeq of Sym o,V )then reconsider t =
[o,the carrier of S] -tree a as
Element of
TS (DTConMSA V) ;
assume A3:
a is
DTree-yielding
;
:: thesis: a is ArgumentSeq of Sym o,Vthen
t . {} = [o,the carrier of S]
by TREES_4:def 4;
then consider p being
FinSequence of
TS (DTConMSA V) such that A4:
(
t = (Sym o,V) -tree p &
Sym o,
V ==> roots p )
by A2, DTCONSTR:10;
a = p
by A3, A4, TREES_4:15;
then
a is
SubtreeSeq of
Sym o,
V
by A4, DTCONSTR:def 9;
hence
a is
ArgumentSeq of
Sym o,
V
by A1, Def2;
:: thesis: verum
end;
assume
a is ArgumentSeq of Sym o,V
; :: thesis: ( [o,the carrier of S] -tree a in S -Terms V & a is DTree-yielding )
then reconsider a = a as ArgumentSeq of Sym o,V ;
reconsider p = a as FinSequence of TS (DTConMSA V) by Def1;
p is SubtreeSeq of Sym o,V
by Def2;
then
Sym o,V ==> roots p
by DTCONSTR:def 9;
hence
( [o,the carrier of S] -tree a in S -Terms V & a is DTree-yielding )
by A2, DTCONSTR:def 4; :: thesis: verum