deffunc H1( Symbol of F1(), FinSequence, FinSequence of F2()) -> Element of F2() = F6($1,($2 . 1),($2 . 2),($3 . 1),($3 . 2));
A3:
now ( ( 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;
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();
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();
( 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
;
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;
(
root-label tl = (roots ts) . 1 &
root-label tr = (roots ts) . 2 )
by A5, FINSEQ_1:44;
hence
F4()
. (nt -tree ts) = H1(
nt,
roots ts,
F4()
* ts)
by A2, A4, A5, A8, A9, A11, A10;
verum end;
A12:
now ( ( 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;
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();
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();
( 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
;
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;
(
root-label tl = (roots ts) . 1 &
root-label tr = (roots ts) . 2 )
by A14, FINSEQ_1:44;
hence
F3()
. (nt -tree ts) = H1(
nt,
roots ts,
F3()
* ts)
by A1, A13, A14, A17, A18, A20, A19;
verum end;
thus
F3() = F4()
from DTCONSTR:sch 9(A12, A3); verum