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