set X = F2();
set G = DTConMSA F2();
A3:
for s being Symbol of (DTConMSA F2()) st s in Terminals (DTConMSA F2()) holds
P1[ root-tree s]
A4:
for nt being Symbol of (DTConMSA F2())
for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof
let nt be
Symbol of
(DTConMSA F2());
:: thesis: for ts being FinSequence of TS (DTConMSA F2()) st nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]let ts be
FinSequence of
TS (DTConMSA F2());
:: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of st t in rng ts holds
P1[t] ) implies P1[nt -tree ts] )
assume that A5:
nt ==> roots ts
and A6:
for
t being
DecoratedTree of st
t in rng ts holds
P1[
t]
;
:: thesis: P1[nt -tree ts]
(
nt in { s where s is Symbol of (DTConMSA F2()) : ex n being FinSequence st s ==> n } &
NonTerminals (DTConMSA F2()) = { s where s is Symbol of (DTConMSA F2()) : ex n being FinSequence st s ==> n } )
by A5, LANG1:def 3;
then reconsider sy =
nt as
NonTerminal of
(DTConMSA F2()) ;
sy in [:the carrier' of F1(),{the carrier of F1()}:]
by Lm5;
then consider o being
OperSymbol of
F1(),
x2 being
Element of
{the carrier of F1()} such that A7:
sy = [o,x2]
by DOMAIN_1:9;
A8:
x2 = the
carrier of
F1()
by TARSKI:def 1;
reconsider p =
ts as
FinSequence of
F1()
-Terms F2() ;
[o,the carrier of F1()] = Sym o,
F2()
by MSAFREE:def 11;
then
ts is
SubtreeSeq of
Sym o,
F2()
by A5, A7, A8, DTCONSTR:def 9;
then reconsider p =
p as
ArgumentSeq of
Sym o,
F2()
by Def2;
for
t being
Term of
F1(),
F2() st
t in rng p holds
P1[
t]
by A6;
hence
P1[
nt -tree ts]
by A2, A7, A8;
:: thesis: verum
end;
for t being DecoratedTree of st t in TS (DTConMSA F2()) holds
P1[t]
from DTCONSTR:sch 7(A3, A4);
hence
for t being Term of F1(),F2() holds P1[t]
; :: thesis: verum