deffunc H1( Symbol of F1(), FinSequence, FinSequence of F2()) -> Element of F2() = F6($1,($2 . 1),($2 . 2),($3 . 1),($3 . 2));
A3: now :: thesis: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F4() . (root-tree t) = F5(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) ) )
thus for t being Symbol of F1() st t in Terminals F1() holds
F4() . (root-tree t) = F5(t) by A2; :: thesis: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts)
let nt be Symbol of F1(); :: thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds
F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts)
let ts be FinSequence of TS F1(); :: thesis: ( nt ==> roots ts implies F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) )
set rts = roots ts;
set x = F4() * ts;
assume A4: nt ==> roots ts ; :: thesis: F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts)
then consider tl, tr being Element of TS F1() 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 F1() by A4, Th10;
reconsider xr = F4() . tr as Element of F2() ;
2 in dom ts by A4, Th10;
then A10: (F4() * ts) . 2 = xr by A7, FUNCT_1:13;
reconsider xl = F4() . tl as Element of F2() ;
1 in dom ts by A4, Th10;
then A11: (F4() * ts) . 1 = xl by A6, FUNCT_1:13;
thus F4() . (nt -tree ts) = H1(nt, roots ts,F4() * ts) by A2, A4, A5, A8, A9, A11, A10; :: thesis: verum
end;
A12: now :: thesis: ( ( for t being Symbol of F1() st t in Terminals F1() holds
F3() . (root-tree t) = F5(t) ) & ( for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) ) )
thus for t being Symbol of F1() st t in Terminals F1() holds
F3() . (root-tree t) = F5(t) by A1; :: thesis: for nt being Symbol of F1()
for ts being FinSequence of TS F1() st nt ==> roots ts holds
F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts)
let nt be Symbol of F1(); :: thesis: for ts being FinSequence of TS F1() st nt ==> roots ts holds
F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts)
let ts be FinSequence of TS F1(); :: thesis: ( nt ==> roots ts implies F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) )
set rts = roots ts;
set x = F3() * ts;
assume A13: nt ==> roots ts ; :: thesis: F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts)
then consider tl, tr being Element of TS F1() 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 F1() by A13, Th10;
reconsider xr = F3() . tr as Element of F2() ;
2 in dom ts by A13, Th10;
then A19: (F3() * ts) . 2 = xr by A16, FUNCT_1:13;
reconsider xl = F3() . tl as Element of F2() ;
1 in dom ts by A13, Th10;
then A20: (F3() * ts) . 1 = xl by A15, FUNCT_1:13;
thus F3() . (nt -tree ts) = H1(nt, roots ts,F3() * ts) by A1, A13, A14, A17, A18, A20, A19; :: thesis: verum
end;
thus F3() = F4() from DTCONSTR:sch 9(A12, A3); :: thesis: verum