deffunc H_{1}( Symbol of F_{1}(), FinSequence, FinSequence of F_{2}()) -> Element of F_{2}() = F_{6}($1,($2 . 1),($2 . 2),($3 . 1),($3 . 2));

_{3}() = F_{4}()
from DTCONSTR:sch 9(A12, A3); :: thesis: verum

A3: now :: thesis: ( ( for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

F_{4}() . (root-tree t) = F_{5}(t) ) & ( for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

F_{4}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{4}() * ts) ) )

F

for ts being FinSequence of TS F

F

thus
for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

F_{4}() . (root-tree t) = F_{5}(t)
by A2; :: thesis: for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

F_{4}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{4}() * ts)

let nt be Symbol of F_{1}(); :: thesis: for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

F_{4}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{4}() * ts)

let ts be FinSequence of TS F_{1}(); :: thesis: ( nt ==> roots ts implies F_{4}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{4}() * ts) )

set rts = roots ts;

set x = F_{4}() * ts;

assume A4: nt ==> roots ts ; :: thesis: F_{4}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{4}() * ts)

then consider tl, tr being Element of TS F_{1}() such that

A5: roots ts = <*(root-label tl),(root-label tr)*> and

A6: tl = ts . 1 and

A7: tr = ts . 2 and

A8: nt -tree ts = nt -tree (tl,tr) and

tl in rng ts and

tr in rng ts by Th10;

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

reconsider xr = F_{4}() . tr as Element of F_{2}() ;

2 in dom ts by A4, Th10;

then A10: (F_{4}() * ts) . 2 = xr
by A7, FUNCT_1:13;

reconsider xl = F_{4}() . tl as Element of F_{2}() ;

1 in dom ts by A4, Th10;

then A11: (F_{4}() * ts) . 1 = xl
by A6, FUNCT_1:13;

( root-label tl = (roots ts) . 1 & root-label tr = (roots ts) . 2 ) by A5, FINSEQ_1:44;

hence F_{4}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{4}() * ts)
by A2, A4, A5, A8, A9, A11, A10; :: thesis: verum

end;F

for ts being FinSequence of TS F

F

let nt be Symbol of F

F

let ts be FinSequence of TS F

set rts = roots ts;

set x = F

assume A4: nt ==> roots ts ; :: thesis: F

then consider tl, tr being Element of TS F

A5: roots ts = <*(root-label tl),(root-label tr)*> and

A6: tl = ts . 1 and

A7: tr = ts . 2 and

A8: nt -tree ts = nt -tree (tl,tr) and

tl in rng ts and

tr in rng ts by Th10;

A9: nt is NonTerminal of F

reconsider xr = F

2 in dom ts by A4, Th10;

then A10: (F

reconsider xl = F

1 in dom ts by A4, Th10;

then A11: (F

( root-label tl = (roots ts) . 1 & root-label tr = (roots ts) . 2 ) by A5, FINSEQ_1:44;

hence F

A12: now :: thesis: ( ( for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

F_{3}() . (root-tree t) = F_{5}(t) ) & ( for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

F_{3}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{3}() * ts) ) )

thus
FF

for ts being FinSequence of TS F

F

thus
for t being Symbol of F_{1}() st t in Terminals F_{1}() holds

F_{3}() . (root-tree t) = F_{5}(t)
by A1; :: thesis: for nt being Symbol of F_{1}()

for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

F_{3}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{3}() * ts)

let nt be Symbol of F_{1}(); :: thesis: for ts being FinSequence of TS F_{1}() st nt ==> roots ts holds

F_{3}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{3}() * ts)

let ts be FinSequence of TS F_{1}(); :: thesis: ( nt ==> roots ts implies F_{3}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{3}() * ts) )

set rts = roots ts;

set x = F_{3}() * ts;

assume A13: nt ==> roots ts ; :: thesis: F_{3}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{3}() * ts)

then consider tl, tr being Element of TS F_{1}() such that

A14: roots ts = <*(root-label tl),(root-label tr)*> and

A15: tl = ts . 1 and

A16: tr = ts . 2 and

A17: nt -tree ts = nt -tree (tl,tr) and

tl in rng ts and

tr in rng ts by Th10;

A18: nt is NonTerminal of F_{1}()
by A13, Th10;

reconsider xr = F_{3}() . tr as Element of F_{2}() ;

2 in dom ts by A13, Th10;

then A19: (F_{3}() * ts) . 2 = xr
by A16, FUNCT_1:13;

reconsider xl = F_{3}() . tl as Element of F_{2}() ;

1 in dom ts by A13, Th10;

then A20: (F_{3}() * ts) . 1 = xl
by A15, FUNCT_1:13;

( root-label tl = (roots ts) . 1 & root-label tr = (roots ts) . 2 ) by A14, FINSEQ_1:44;

hence F_{3}() . (nt -tree ts) = H_{1}(nt, roots ts,F_{3}() * ts)
by A1, A13, A14, A17, A18, A20, A19; :: thesis: verum

end;F

for ts being FinSequence of TS F

F

let nt be Symbol of F

F

let ts be FinSequence of TS F

set rts = roots ts;

set x = F

assume A13: nt ==> roots ts ; :: thesis: F

then consider tl, tr being Element of TS F

A14: roots ts = <*(root-label tl),(root-label tr)*> and

A15: tl = ts . 1 and

A16: tr = ts . 2 and

A17: nt -tree ts = nt -tree (tl,tr) and

tl in rng ts and

tr in rng ts by Th10;

A18: nt is NonTerminal of F

reconsider xr = F

2 in dom ts by A13, Th10;

then A19: (F

reconsider xl = F

1 in dom ts by A13, Th10;

then A20: (F

( root-label tl = (roots ts) . 1 & root-label tr = (roots ts) . 2 ) by A14, FINSEQ_1:44;

hence F