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 A1: ( 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 sequence of ( the InstructionsF of SCM ^omega) such that

A2: g = SCM-Compile . (nt -tree (t1,t2)) and

A3: f1 = SCM-Compile . t1 and

A4: f2 = SCM-Compile . t2 and

A5: for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) by A1, Def11;

g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) by A5;

hence SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n)) by A3, A4, A2; :: thesis: verum

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 A1: ( 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 sequence of ( the InstructionsF of SCM ^omega) such that

A2: g = SCM-Compile . (nt -tree (t1,t2)) and

A3: f1 = SCM-Compile . t1 and

A4: f2 = SCM-Compile . t2 and

A5: for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) by A1, Def11;

g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) by A5;

hence SCM-Compile ((nt -tree (t1,t2)),n) = ((SCM-Compile (t1,n)) ^ (SCM-Compile (t2,(n + 1)))) ^ (Selfwork (nt,n)) by A3, A4, A2; :: thesis: verum