let nt be NonTerminal of SCM-AE ; :: thesis: for t1, t2 being bin-term
for n being Element of NAT
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
SCM-Compile (nt -tree t1,t2),n = ((SCM-Compile t1,n) ^ (SCM-Compile t2,(n + 1))) ^ (Selfwork nt,n)
let t1, t2 be bin-term; :: thesis: for n being Element of NAT
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
SCM-Compile (nt -tree t1,t2),n = ((SCM-Compile t1,n) ^ (SCM-Compile t2,(n + 1))) ^ (Selfwork nt,n)
let n be Element of NAT ; :: thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
SCM-Compile (nt -tree t1,t2),n = ((SCM-Compile t1,n) ^ (SCM-Compile t2,(n + 1))) ^ (Selfwork nt,n)
let rtl, rtr be Symbol of SCM-AE ; :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies SCM-Compile (nt -tree t1,t2),n = ((SCM-Compile t1,n) ^ (SCM-Compile t2,(n + 1))) ^ (Selfwork nt,n) )
assume Z: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: SCM-Compile (nt -tree t1,t2),n = ((SCM-Compile t1,n) ^ (SCM-Compile t2,(n + 1))) ^ (Selfwork nt,n)
consider g, f1, f2 being Function of NAT ,(the Instructions of SCM ^omega ) such that
W4: g = SCM-Compile . (nt -tree t1,t2) and
W5: f1 = SCM-Compile . t1 and
W6: f2 = SCM-Compile . t2 and
W7: for n being Element of NAT holds g . n = ((f1 . n) ^ (f2 . (n + 1))) ^ (Selfwork nt,n) by Z, Def11k;
thus SCM-Compile (nt -tree t1,t2),n = ((SCM-Compile t1,n) ^ (SCM-Compile t2,(n + 1))) ^ (Selfwork nt,n) by W5, W6, W7, W4; :: thesis: verum