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