defpred S1[ set , set , set , set ] means for a being Element of F2()
for ntv being Function of F2(),F3() st ntv = $4 holds
ntv . a = F7($1,$2,$3,a);
defpred S2[ set , set ] means for tv being Function of F2(),F3() st tv = $2 holds
for a being Element of F2() holds tv . a = F6($1,a);
reconsider FAB = Funcs (F2(),F3()) as non empty set ;
reconsider f29 = F5() as Function of (TS F1()),FAB ;
consider TV being Function of (Terminals F1()),FAB such that
A5:
for e being Element of Terminals F1() holds S2[e,TV . e]
from FUNCT_2:sch 3(A3);
deffunc H1( Terminal of F1()) -> Element of FAB = TV . $1;
A6:
now for x being Element of NonTerminals F1()
for y, z being Element of FAB ex fab being Element of FAB st S1[x,y,z,fab]let x be
Element of
NonTerminals F1();
for y, z being Element of FAB ex fab being Element of FAB st S1[x,y,z,fab]let y,
z be
Element of
FAB;
ex fab being Element of FAB st S1[x,y,z,fab]deffunc H2(
Element of
F2())
-> Element of
F3() =
F7(
x,
y,
z,$1);
consider fab being
Function of
F2(),
F3()
such that A7:
for
a being
Element of
F2() holds
fab . a = H2(
a)
from FUNCT_2:sch 4();
(
F2()
= dom fab &
rng fab c= F3() )
by FUNCT_2:def 1;
then reconsider fab =
fab as
Element of
FAB by FUNCT_2:def 2;
take fab =
fab;
S1[x,y,z,fab]thus
S1[
x,
y,
z,
fab]
by A7;
verum end;
consider NTV being Function of [:(NonTerminals F1()),FAB,FAB:],FAB such that
A8:
for x being Element of NonTerminals F1()
for y, z being Element of FAB holds S1[x,y,z,NTV . [x,y,z]]
from MULTOP_1:sch 1(A6);
deffunc H2( NonTerminal of F1(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [$1,$4,$5];
A9:
now ( ( for t being Terminal of F1() holds f29 . (root-tree t) = H1(t) ) & ( for nt being NonTerminal of F1()
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) )let nt be
NonTerminal of
F1();
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)let tl,
tr be
Element of
TS F1();
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)let rtl,
rtr be
Symbol of
F1();
( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) )assume
(
rtl = root-label tl &
rtr = root-label tr &
nt ==> <*rtl,rtr*> )
;
for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)then consider g,
ff1,
ff2 being
Function of
F2(),
F3()
such that A15:
g = F5()
. (nt -tree (tl,tr))
and A16:
(
ff1 = F5()
. tl &
ff2 = F5()
. tr & ( for
a being
Element of
F2() holds
g . a = F7(
nt,
ff1,
ff2,
a) ) )
by A2;
let xl,
xr be
Element of
FAB;
( xl = f29 . tl & xr = f29 . tr implies f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) )consider ntvnt being
Function such that A17:
ntvnt = NTV . [nt,xl,xr]
and A18:
(
dom ntvnt = F2() &
rng ntvnt c= F3() )
by FUNCT_2:def 2;
reconsider ntvnt =
ntvnt as
Function of
F2(),
F3()
by A18, FUNCT_2:def 1, RELSET_1:4;
assume A19:
(
xl = f29 . tl &
xr = f29 . tr )
;
f29 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)hence
f29 . (nt -tree (tl,tr)) = H2(
nt,
rtl,
rtr,
xl,
xr)
by A15, A17, FUNCT_1:2;
verum end;
reconsider f19 = F4() as Function of (TS F1()),FAB ;
A20:
now ( ( for t being Terminal of F1() holds f19 . (root-tree t) = H1(t) ) & ( for nt being NonTerminal of F1()
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) ) )let nt be
NonTerminal of
F1();
for tl, tr being Element of TS F1()
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)let tl,
tr be
Element of
TS F1();
for rtl, rtr being Symbol of F1() st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)let rtl,
rtr be
Symbol of
F1();
( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> implies for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) )assume
(
rtl = root-label tl &
rtr = root-label tr &
nt ==> <*rtl,rtr*> )
;
for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)then consider g,
ff1,
ff2 being
Function of
F2(),
F3()
such that A26:
g = F4()
. (nt -tree (tl,tr))
and A27:
(
ff1 = F4()
. tl &
ff2 = F4()
. tr & ( for
a being
Element of
F2() holds
g . a = F7(
nt,
ff1,
ff2,
a) ) )
by A1;
let xl,
xr be
Element of
FAB;
( xl = f19 . tl & xr = f19 . tr implies f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr) )consider ntvnt being
Function such that A28:
ntvnt = NTV . [nt,xl,xr]
and A29:
(
dom ntvnt = F2() &
rng ntvnt c= F3() )
by FUNCT_2:def 2;
reconsider ntvnt =
ntvnt as
Function of
F2(),
F3()
by A29, FUNCT_2:def 1, RELSET_1:4;
assume A30:
(
xl = f19 . tl &
xr = f19 . tr )
;
f19 . (nt -tree (tl,tr)) = H2(nt,rtl,rtr,xl,xr)hence
f19 . (nt -tree (tl,tr)) = H2(
nt,
rtl,
rtr,
xl,
xr)
by A26, A28, FUNCT_1:2;
verum end;
f19 = f29
from BINTREE1:sch 4(A20, A9);
hence
F4() = F5()
; verum