let S be non empty non void ManySortedSign ; for V being V2() ManySortedSet of the carrier of S
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 V2() ManySortedSet of the carrier of S; 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; 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; ( ( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding ) iff a is ArgumentSeq of Sym (o,V) )
A1:
[o, the carrier of S] = Sym (o,V)
by MSAFREE:def 9;
A2:
S -Terms V = TS (DTConMSA V)
;
hereby ( 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
;
( 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
;
a is ArgumentSeq of Sym (o,V)then
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
and A5:
Sym (
o,
V)
==> roots p
by A1, DTCONSTR:10;
a = p
by A3, A4, TREES_4:15;
then
a is
SubtreeSeq of
Sym (
o,
V)
by A5, DTCONSTR:def 6;
hence
a is
ArgumentSeq of
Sym (
o,
V)
by A2, Def2;
verum
end;
assume
a is ArgumentSeq of Sym (o,V)
; ( [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 6;
hence
( [o, the carrier of S] -tree a in S -Terms V & a is DTree-yielding )
by A1, DTCONSTR:def 1; verum