let s be State of SCMPDS ; :: thesis: for I, J being shiftable Program of SCMPDS
for n being Element of NAT holds (I ';' (Goto n)) ';' J is shiftable
let I, J be shiftable Program of SCMPDS ; :: thesis: for n being Element of NAT holds (I ';' (Goto n)) ';' J is shiftable
let n be Element of NAT ; :: thesis: (I ';' (Goto n)) ';' J is shiftable
(I ';' (Goto n)) ';' J = (I ';' (Load (goto n))) ';' J by SCMPDS_6:def 1;
hence (I ';' (Goto n)) ';' J is shiftable ; :: thesis: verum