defpred S_{1}[ set , set , set , set ] means for a being Element of F_{2}()

for ntv being Function of F_{2}(),F_{3}() st ntv = $4 holds

ntv . a = F_{7}($1,$2,$3,a);

defpred S_{2}[ set , set ] means for tv being Function of F_{2}(),F_{3}() st tv = $2 holds

for a being Element of F_{2}() holds tv . a = F_{6}($1,a);

reconsider FAB = Funcs (F_{2}(),F_{3}()) as non empty set ;

reconsider f29 = F_{5}() as Function of (TS F_{1}()),FAB ;

_{1}()),FAB such that

A5: for e being Element of Terminals F_{1}() holds S_{2}[e,TV . e]
from FUNCT_2:sch 3(A3);

deffunc H_{1}( Terminal of F_{1}()) -> Element of FAB = TV . $1;

_{1}()),FAB,FAB:],FAB such that

A8: for x being Element of NonTerminals F_{1}()

for y, z being Element of FAB holds S_{1}[x,y,z,NTV . [x,y,z]]
from MULTOP_1:sch 1(A6);

deffunc H_{2}( NonTerminal of F_{1}(), set , set , Element of FAB, Element of FAB) -> Element of FAB = NTV . [$1,$4,$5];

_{4}() as Function of (TS F_{1}()),FAB ;

hence F_{4}() = F_{5}()
; :: thesis: verum

for ntv being Function of F

ntv . a = F

defpred S

for a being Element of F

reconsider FAB = Funcs (F

reconsider f29 = F

A3: now :: thesis: for x being Element of Terminals F_{1}() ex y being Element of FAB st S_{2}[x,y]

consider TV being Function of (Terminals Flet x be Element of Terminals F_{1}(); :: thesis: ex y being Element of FAB st S_{2}[x,y]

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

consider y being Function of F_{2}(),F_{3}() such that

A4: for a being Element of F_{2}() holds y . a = H_{1}(a)
from FUNCT_2:sch 4();

( F_{2}() = dom y & rng y c= F_{3}() )
by FUNCT_2:def 1;

then reconsider y = y as Element of FAB by FUNCT_2:def 2;

take y = y; :: thesis: S_{2}[x,y]

thus S_{2}[x,y]
by A4; :: thesis: verum

end;deffunc H

consider y being Function of F

A4: for a being Element of F

( F

then reconsider y = y as Element of FAB by FUNCT_2:def 2;

take y = y; :: thesis: S

thus S

A5: for e being Element of Terminals F

deffunc H

A6: now :: thesis: for x being Element of NonTerminals F_{1}()

for y, z being Element of FAB ex fab being Element of FAB st S_{1}[x,y,z,fab]

consider NTV being Function of [:(NonTerminals Ffor y, z being Element of FAB ex fab being Element of FAB st S

let x be Element of NonTerminals F_{1}(); :: thesis: for y, z being Element of FAB ex fab being Element of FAB st S_{1}[x,y,z,fab]

let y, z be Element of FAB; :: thesis: ex fab being Element of FAB st S_{1}[x,y,z,fab]

deffunc H_{2}( Element of F_{2}()) -> Element of F_{3}() = F_{7}(x,y,z,$1);

consider fab being Function of F_{2}(),F_{3}() such that

A7: for a being Element of F_{2}() holds fab . a = H_{2}(a)
from FUNCT_2:sch 4();

( F_{2}() = dom fab & rng fab c= F_{3}() )
by FUNCT_2:def 1;

then reconsider fab = fab as Element of FAB by FUNCT_2:def 2;

take fab = fab; :: thesis: S_{1}[x,y,z,fab]

thus S_{1}[x,y,z,fab]
by A7; :: thesis: verum

end;let y, z be Element of FAB; :: thesis: ex fab being Element of FAB st S

deffunc H

consider fab being Function of F

A7: for a being Element of F

( F

then reconsider fab = fab as Element of FAB by FUNCT_2:def 2;

take fab = fab; :: thesis: S

thus S

A8: for x being Element of NonTerminals F

for y, z being Element of FAB holds S

deffunc H

A9: now :: thesis: ( ( for t being Terminal of F_{1}() holds f29 . (root-tree t) = H_{1}(t) ) & ( for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() 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)) = H_{2}(nt,rtl,rtr,xl,xr) ) )_{1}(); :: thesis: for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() 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)) = H_{2}(nt,rtl,rtr,xl,xr)

let tl, tr be Element of TS F_{1}(); :: thesis: for rtl, rtr being Symbol of F_{1}() 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)) = H_{2}(nt,rtl,rtr,xl,xr)

let rtl, rtr be Symbol of F_{1}(); :: thesis: ( 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)) = H_{2}(nt,rtl,rtr,xl,xr) )

assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds

f29 . (nt -tree (tl,tr)) = H_{2}(nt,rtl,rtr,xl,xr)

then consider g, ff1, ff2 being Function of F_{2}(),F_{3}() such that

A15: g = F_{5}() . (nt -tree (tl,tr))
and

A16: ( ff1 = F_{5}() . tl & ff2 = F_{5}() . tr & ( for a being Element of F_{2}() holds g . a = F_{7}(nt,ff1,ff2,a) ) )
by A2;

let xl, xr be Element of FAB; :: thesis: ( xl = f29 . tl & xr = f29 . tr implies f29 . (nt -tree (tl,tr)) = H_{2}(nt,rtl,rtr,xl,xr) )

consider ntvnt being Function such that

A17: ntvnt = NTV . [nt,xl,xr] and

A18: ( dom ntvnt = F_{2}() & rng ntvnt c= F_{3}() )
by FUNCT_2:def 2;

reconsider ntvnt = ntvnt as Function of F_{2}(),F_{3}() by A18, FUNCT_2:def 1, RELSET_1:4;

assume A19: ( xl = f29 . tl & xr = f29 . tr ) ; :: thesis: f29 . (nt -tree (tl,tr)) = H_{2}(nt,rtl,rtr,xl,xr)

_{2}(nt,rtl,rtr,xl,xr)
by A15, A17, FUNCT_1:2; :: thesis: verum

end;

reconsider f19 = Ffor tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds

f29 . (nt -tree (tl,tr)) = H

hereby :: thesis: for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() 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)) = H_{2}(nt,rtl,rtr,xl,xr)

let nt be NonTerminal of Ffor tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds

f29 . (nt -tree (tl,tr)) = H

let t be Terminal of F_{1}(); :: thesis: f29 . (root-tree t) = H_{1}(t)

consider TVt being Function such that

A10: TV . t = TVt and

A11: dom TVt = F_{2}()
and

A12: rng TVt c= F_{3}()
by FUNCT_2:def 2;

reconsider TVt = TVt as Function of F_{2}(),F_{3}() by A11, A12, FUNCT_2:def 1, RELSET_1:4;

consider g being Function of F_{2}(),F_{3}() such that

A13: g = F_{5}() . (root-tree t)
and

A14: for a being Element of F_{2}() holds g . a = F_{6}(t,a)
by A2;

_{1}(t)
by A13, A10, FUNCT_1:2; :: thesis: verum

end;consider TVt being Function such that

A10: TV . t = TVt and

A11: dom TVt = F

A12: rng TVt c= F

reconsider TVt = TVt as Function of F

consider g being Function of F

A13: g = F

A14: for a being Element of F

now :: thesis: ( F_{2}() = dom g & F_{2}() = dom TVt & ( for x being object st x in F_{2}() holds

g . x = TVt . x ) )

hence
f29 . (root-tree t) = Hg . x = TVt . x ) )

thus
F_{2}() = dom g
by FUNCT_2:def 1; :: thesis: ( F_{2}() = dom TVt & ( for x being object st x in F_{2}() holds

g . x = TVt . x ) )

thus F_{2}() = dom TVt
by A11; :: thesis: for x being object st x in F_{2}() holds

g . x = TVt . x

let x be object ; :: thesis: ( x in F_{2}() implies g . x = TVt . x )

assume x in F_{2}()
; :: thesis: g . x = TVt . x

then reconsider xx = x as Element of F_{2}() ;

g . xx = F_{6}(t,xx)
by A14

.= TVt . xx by A5, A10 ;

hence g . x = TVt . x ; :: thesis: verum

end;g . x = TVt . x ) )

thus F

g . x = TVt . x

let x be object ; :: thesis: ( x in F

assume x in F

then reconsider xx = x as Element of F

g . xx = F

.= TVt . xx by A5, A10 ;

hence g . x = TVt . x ; :: thesis: verum

for rtl, rtr being Symbol of F

for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds

f29 . (nt -tree (tl,tr)) = H

let tl, tr be Element of TS F

for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds

f29 . (nt -tree (tl,tr)) = H

let rtl, rtr be Symbol of F

f29 . (nt -tree (tl,tr)) = H

assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of FAB st xl = f29 . tl & xr = f29 . tr holds

f29 . (nt -tree (tl,tr)) = H

then consider g, ff1, ff2 being Function of F

A15: g = F

A16: ( ff1 = F

let xl, xr be Element of FAB; :: thesis: ( xl = f29 . tl & xr = f29 . tr implies f29 . (nt -tree (tl,tr)) = H

consider ntvnt being Function such that

A17: ntvnt = NTV . [nt,xl,xr] and

A18: ( dom ntvnt = F

reconsider ntvnt = ntvnt as Function of F

assume A19: ( xl = f29 . tl & xr = f29 . tr ) ; :: thesis: f29 . (nt -tree (tl,tr)) = H

now :: thesis: ( F_{2}() = dom g & F_{2}() = dom ntvnt & ( for x being object st x in F_{2}() holds

g . x = ntvnt . x ) )

hence
f29 . (nt -tree (tl,tr)) = Hg . x = ntvnt . x ) )

thus
F_{2}() = dom g
by FUNCT_2:def 1; :: thesis: ( F_{2}() = dom ntvnt & ( for x being object st x in F_{2}() holds

g . x = ntvnt . x ) )

thus F_{2}() = dom ntvnt
by FUNCT_2:def 1; :: thesis: for x being object st x in F_{2}() holds

g . x = ntvnt . x

let x be object ; :: thesis: ( x in F_{2}() implies g . x = ntvnt . x )

assume x in F_{2}()
; :: thesis: g . x = ntvnt . x

then reconsider xx = x as Element of F_{2}() ;

g . xx = F_{7}(nt,xl,xr,xx)
by A19, A16

.= ntvnt . xx by A8, A17 ;

hence g . x = ntvnt . x ; :: thesis: verum

end;g . x = ntvnt . x ) )

thus F

g . x = ntvnt . x

let x be object ; :: thesis: ( x in F

assume x in F

then reconsider xx = x as Element of F

g . xx = F

.= ntvnt . xx by A8, A17 ;

hence g . x = ntvnt . x ; :: thesis: verum

A20: now :: thesis: ( ( for t being Terminal of F_{1}() holds f19 . (root-tree t) = H_{1}(t) ) & ( for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() 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)) = H_{2}(nt,rtl,rtr,xl,xr) ) )_{1}(); :: thesis: for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() 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)) = H_{2}(nt,rtl,rtr,xl,xr)

let tl, tr be Element of TS F_{1}(); :: thesis: for rtl, rtr being Symbol of F_{1}() 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)) = H_{2}(nt,rtl,rtr,xl,xr)

let rtl, rtr be Symbol of F_{1}(); :: thesis: ( 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)) = H_{2}(nt,rtl,rtr,xl,xr) )

assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds

f19 . (nt -tree (tl,tr)) = H_{2}(nt,rtl,rtr,xl,xr)

then consider g, ff1, ff2 being Function of F_{2}(),F_{3}() such that

A26: g = F_{4}() . (nt -tree (tl,tr))
and

A27: ( ff1 = F_{4}() . tl & ff2 = F_{4}() . tr & ( for a being Element of F_{2}() holds g . a = F_{7}(nt,ff1,ff2,a) ) )
by A1;

let xl, xr be Element of FAB; :: thesis: ( xl = f19 . tl & xr = f19 . tr implies f19 . (nt -tree (tl,tr)) = H_{2}(nt,rtl,rtr,xl,xr) )

consider ntvnt being Function such that

A28: ntvnt = NTV . [nt,xl,xr] and

A29: ( dom ntvnt = F_{2}() & rng ntvnt c= F_{3}() )
by FUNCT_2:def 2;

reconsider ntvnt = ntvnt as Function of F_{2}(),F_{3}() by A29, FUNCT_2:def 1, RELSET_1:4;

assume A30: ( xl = f19 . tl & xr = f19 . tr ) ; :: thesis: f19 . (nt -tree (tl,tr)) = H_{2}(nt,rtl,rtr,xl,xr)

_{2}(nt,rtl,rtr,xl,xr)
by A26, A28, FUNCT_1:2; :: thesis: verum

end;

f19 = f29
from BINTREE1:sch 4(A20, A9);for tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds

f19 . (nt -tree (tl,tr)) = H

hereby :: thesis: for nt being NonTerminal of F_{1}()

for tl, tr being Element of TS F_{1}()

for rtl, rtr being Symbol of F_{1}() 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)) = H_{2}(nt,rtl,rtr,xl,xr)

let nt be NonTerminal of Ffor tl, tr being Element of TS F

for rtl, rtr being Symbol of F

for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds

f19 . (nt -tree (tl,tr)) = H

let t be Terminal of F_{1}(); :: thesis: f19 . (root-tree t) = H_{1}(t)

consider TVt being Function such that

A21: TV . t = TVt and

A22: dom TVt = F_{2}()
and

A23: rng TVt c= F_{3}()
by FUNCT_2:def 2;

reconsider TVt = TVt as Function of F_{2}(),F_{3}() by A22, A23, FUNCT_2:def 1, RELSET_1:4;

consider g being Function of F_{2}(),F_{3}() such that

A24: g = F_{4}() . (root-tree t)
and

A25: for a being Element of F_{2}() holds g . a = F_{6}(t,a)
by A1;

_{1}(t)
by A24, A21, FUNCT_1:2; :: thesis: verum

end;consider TVt being Function such that

A21: TV . t = TVt and

A22: dom TVt = F

A23: rng TVt c= F

reconsider TVt = TVt as Function of F

consider g being Function of F

A24: g = F

A25: for a being Element of F

now :: thesis: ( F_{2}() = dom g & F_{2}() = dom TVt & ( for x being object st x in F_{2}() holds

g . x = TVt . x ) )

hence
f19 . (root-tree t) = Hg . x = TVt . x ) )

thus
F_{2}() = dom g
by FUNCT_2:def 1; :: thesis: ( F_{2}() = dom TVt & ( for x being object st x in F_{2}() holds

g . x = TVt . x ) )

thus F_{2}() = dom TVt
by A22; :: thesis: for x being object st x in F_{2}() holds

g . x = TVt . x

let x be object ; :: thesis: ( x in F_{2}() implies g . x = TVt . x )

assume x in F_{2}()
; :: thesis: g . x = TVt . x

then reconsider xx = x as Element of F_{2}() ;

g . xx = F_{6}(t,xx)
by A25

.= TVt . xx by A5, A21 ;

hence g . x = TVt . x ; :: thesis: verum

end;g . x = TVt . x ) )

thus F

g . x = TVt . x

let x be object ; :: thesis: ( x in F

assume x in F

then reconsider xx = x as Element of F

g . xx = F

.= TVt . xx by A5, A21 ;

hence g . x = TVt . x ; :: thesis: verum

for rtl, rtr being Symbol of F

for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds

f19 . (nt -tree (tl,tr)) = H

let tl, tr be Element of TS F

for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds

f19 . (nt -tree (tl,tr)) = H

let rtl, rtr be Symbol of F

f19 . (nt -tree (tl,tr)) = H

assume ( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> ) ; :: thesis: for xl, xr being Element of FAB st xl = f19 . tl & xr = f19 . tr holds

f19 . (nt -tree (tl,tr)) = H

then consider g, ff1, ff2 being Function of F

A26: g = F

A27: ( ff1 = F

let xl, xr be Element of FAB; :: thesis: ( xl = f19 . tl & xr = f19 . tr implies f19 . (nt -tree (tl,tr)) = H

consider ntvnt being Function such that

A28: ntvnt = NTV . [nt,xl,xr] and

A29: ( dom ntvnt = F

reconsider ntvnt = ntvnt as Function of F

assume A30: ( xl = f19 . tl & xr = f19 . tr ) ; :: thesis: f19 . (nt -tree (tl,tr)) = H

now :: thesis: ( F_{2}() = dom g & F_{2}() = dom ntvnt & ( for x being object st x in F_{2}() holds

g . x = ntvnt . x ) )

hence
f19 . (nt -tree (tl,tr)) = Hg . x = ntvnt . x ) )

thus
F_{2}() = dom g
by FUNCT_2:def 1; :: thesis: ( F_{2}() = dom ntvnt & ( for x being object st x in F_{2}() holds

g . x = ntvnt . x ) )

thus F_{2}() = dom ntvnt
by FUNCT_2:def 1; :: thesis: for x being object st x in F_{2}() holds

g . x = ntvnt . x

let x be object ; :: thesis: ( x in F_{2}() implies g . x = ntvnt . x )

assume x in F_{2}()
; :: thesis: g . x = ntvnt . x

then reconsider xx = x as Element of F_{2}() ;

g . xx = F_{7}(nt,xl,xr,xx)
by A30, A27

.= ntvnt . xx by A8, A28 ;

hence g . x = ntvnt . x ; :: thesis: verum

end;g . x = ntvnt . x ) )

thus F

g . x = ntvnt . x

let x be object ; :: thesis: ( x in F

assume x in F

then reconsider xx = x as Element of F

g . xx = F

.= ntvnt . xx by A8, A28 ;

hence g . x = ntvnt . x ; :: thesis: verum

hence F