deffunc H1( Symbol of F1(), FinSequence, FinSequence of F2()) -> Element of F2() = F6($1,($2 . 1),($2 . 2),($3 . 1),($3 . 2));
A3:
now 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;
assume A4:
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 A5:
(
roots ts = <*(root-label tl),(root-label tr)*> &
tl = ts . 1 &
tr = ts . 2 &
nt -tree ts = nt -tree tl,
tr &
tl in rng ts &
tr in rng ts )
by Th12;
A6:
(
root-label tl = (roots ts) . 1 &
root-label tr = (roots ts) . 2 )
by A5, FINSEQ_1:61;
set x =
F3()
* ts;
reconsider xl =
F3()
. tl as
Element of
F2() ;
reconsider xr =
F3()
. tr as
Element of
F2() ;
A7:
(
nt is
NonTerminal of
F1() &
dom ts = {1,2} & 1
in dom ts & 2
in dom ts )
by A4, Th12;
then
(
(F3() * ts) . 1
= xl &
(F3() * ts) . 2
= xr )
by A5, FUNCT_1:23;
hence
F3()
. (nt -tree ts) = H1(
nt,
roots ts,
F3()
* ts)
by A1, A4, A5, A6, A7;
:: thesis: verum end;
A8:
now 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;
assume A9:
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 A10:
(
roots ts = <*(root-label tl),(root-label tr)*> &
tl = ts . 1 &
tr = ts . 2 &
nt -tree ts = nt -tree tl,
tr &
tl in rng ts &
tr in rng ts )
by Th12;
A11:
(
root-label tl = (roots ts) . 1 &
root-label tr = (roots ts) . 2 )
by A10, FINSEQ_1:61;
set x =
F4()
* ts;
reconsider xl =
F4()
. tl as
Element of
F2() ;
reconsider xr =
F4()
. tr as
Element of
F2() ;
A12:
(
nt is
NonTerminal of
F1() &
dom ts = {1,2} & 1
in dom ts & 2
in dom ts )
by A9, Th12;
then
(
(F4() * ts) . 1
= xl &
(F4() * ts) . 2
= xr )
by A10, FUNCT_1:23;
hence
F4()
. (nt -tree ts) = H1(
nt,
roots ts,
F4()
* ts)
by A2, A9, A10, A11, A12;
:: thesis: verum end;
thus
F3() = F4()
from DTCONSTR:sch 9(A3, A8); :: thesis: verum