let it1, it2 be Element of NAT ; :: thesis: ( ex f being Function of (TS SCM-AE),NAT st
( it1 = 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) ) ) & ex f being Function of (TS SCM-AE),NAT st
( it2 = 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) ) ) implies it1 = it2 )
given f1 being Function of (TS SCM-AE),NAT such that A2: it1 = f1 . term and
A3: ( ( for t being Terminal of SCM-AE holds f1 . (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 = f1 . tl & xr = f1 . tr holds
f1 . (nt -tree (tl,tr)) = H₃(nt,rtl,rtr,xl,xr) ) ) ; :: thesis: ( for f being Function of (TS SCM-AE),NAT holds
( not it2 = f . term or ex t being Terminal of SCM-AE st not f . (root-tree t) = d". t or ex nt being NonTerminal of SCM-AE ex tl, tr being bin-term ex rtl, rtr being Symbol of SCM-AE st
( rtl = root-label tl & rtr = root-label tr & nt ==> <*rtl,rtr*> & ex xl, xr being Element of NAT st
( xl = f . tl & xr = f . tr & not f . (nt -tree (tl,tr)) = max (xl,xr) ) ) ) or it1 = it2 )
given f2 being Function of (TS SCM-AE),NAT such that A4: it2 = f2 . term and
A5: ( ( for t being Terminal of SCM-AE holds f2 . (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 = f2 . tl & xr = f2 . tr holds
f2 . (nt -tree (tl,tr)) = H₃(nt,rtl,rtr,xl,xr) ) ) ; :: thesis: it1 = it2
f1 = f2 from BINTREE1:sch 4(A3, A5);
hence it1 = it2 by A2, A4; :: thesis: verum