A3:
for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F_{1}() st t in rng ts holds

P_{1}[t] ) holds

P_{1}[nt -tree ts]
_{1}() st s in Terminals F_{1}() holds

P_{1}[ root-tree s]
by A1;

for t being DecoratedTree of the carrier of F_{1}() st t in TS F_{1}() holds

P_{1}[t]
from DTCONSTR:sch 7(A10, A3);

hence for t being Element of TS F_{1}() holds P_{1}[t]
; :: thesis: verum

for ts being FinSequence of TS F

P

P

proof

A10:
for s being Symbol of F
let nt be Symbol of F_{1}(); :: thesis: for ts being FinSequence of TS F_{1}() st nt ==> roots ts & ( for t being DecoratedTree of the carrier of F_{1}() st t in rng ts holds

P_{1}[t] ) holds

P_{1}[nt -tree ts]

let ts be FinSequence of TS F_{1}(); :: thesis: ( nt ==> roots ts & ( for t being DecoratedTree of the carrier of F_{1}() st t in rng ts holds

P_{1}[t] ) implies P_{1}[nt -tree ts] )

assume that

A4: nt ==> roots ts and

A5: for t being DecoratedTree of the carrier of F_{1}() st t in rng ts holds

P_{1}[t]
; :: thesis: P_{1}[nt -tree ts]

A6: nt is NonTerminal of F_{1}()
by A4, Th10;

consider tl, tr being Element of TS F_{1}() 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, Th10;

( P_{1}[tl] & P_{1}[tr] )
by A5, A9;

hence P_{1}[nt -tree ts]
by A2, A4, A6, A7, A8; :: thesis: verum

end;P

P

let ts be FinSequence of TS F

P

assume that

A4: nt ==> roots ts and

A5: for t being DecoratedTree of the carrier of F

P

A6: nt is NonTerminal of F

consider tl, tr being Element of TS F

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, Th10;

( P

hence P

P

for t being DecoratedTree of the carrier of F

P

hence for t being Element of TS F