A3:
for nt being Symbol of
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof
let nt be
Symbol of ;
for ts being FinSequence of TS F1() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]let ts be
FinSequence of
TS F1();
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F1() st t in rng ts holds
P1[t] ) implies P1[nt -tree ts] )
assume that A4:
nt ==> roots ts
and A5:
for
t being
DecoratedTree of the
carrier of
F1() st
t in rng ts holds
P1[
t]
;
P1[nt -tree ts]
A6:
nt is
NonTerminal of
F1()
by A4, Th12;
consider tl,
tr being
Element of
TS F1()
such that A7:
roots ts = <*(root-label tl),(root-label tr)*>
and
tl = ts . 1
and
tr = ts . 2
and A8:
nt -tree ts = nt -tree tl,
tr
and A9:
(
tl in rng ts &
tr in rng ts )
by A4, Th12;
(
P1[
tl] &
P1[
tr] )
by A5, A9;
hence
P1[
nt -tree ts]
by A2, A4, A6, A7, A8;
verum
end;
A10:
for s being Symbol of st s in Terminals F1() holds
P1[ root-tree s]
by A1;
for t being DecoratedTree of the carrier of F1() st t in TS F1() holds
P1[t]
from DTCONSTR:sch 7(A10, A3);
hence
for t being Element of TS F1() holds P1[t]
; verum