consider f being Function of (TS SCM-AE ),(Funcs NAT ,(the Instructions of SCM * )) such that
A1: ( ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM * ) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = H₁(t,n) ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,(the Instructions of SCM * ) st
( g = f . (nt -tree t1,t2) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = H₂(nt,f1,f2,n) ) ) ) ) from BINTREE1:sch 5();
reconsider IT = (f . term) . aux as Element of the Instructions of SCM * ;
take IT ; :: thesis: ex f being Function of (TS SCM-AE ),(Funcs NAT ,(the Instructions of SCM * )) st
( IT = (f . term) . aux & ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM * ) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,(the Instructions of SCM * ) st
( g = f . (nt -tree t1,t2) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) )
take f ; :: thesis: ( IT = (f . term) . aux & ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM * ) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,(the Instructions of SCM * ) st
( g = f . (nt -tree t1,t2) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) )
thus ( IT = (f . term) . aux & ( for t being Terminal of SCM-AE ex g being Function of NAT ,(the Instructions of SCM * ) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = <*((dl. n) := (@ t))*> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being Function of NAT ,(the Instructions of SCM * ) st
( g = f . (nt -tree t1,t2) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) ) ) ) ) by A1; :: thesis: verum