consider f being Function of (TS SCM-AE),NAT such that
A1: ( ( for t being Terminal of SCM-AE holds f . (root-tree t) = H₂(t) ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = H₃(nt,rtl,rtr,xl,xr) ) ) from BINTREE1:sch 3();
reconsider fterm = f . term as Element of NAT ;
take fterm ; :: thesis: ex f being Function of (TS SCM-AE),NAT st
( fterm = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) )
take f ; :: thesis: ( fterm = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) )
thus ( fterm = f . term & ( for t being Terminal of SCM-AE holds f . (root-tree t) = d". t ) & ( for nt being NonTerminal of SCM-AE
for tl, tr being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> holds
for xl, xr being Element of NAT st xl = f . tl & xr = f . tr holds
f . (nt -tree (tl,tr)) = max (xl,xr) ) ) by A1; :: thesis: verum