let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N
for F being pre-Macro of S holds (Stop S) ';' F = F
let S be non empty stored-program IC-Ins-separated definite standard-ins halting standard homogeneous regular J/A-independent AMI-Struct of N; :: thesis: for F being pre-Macro of S holds (Stop S) ';' F = F
let F be pre-Macro of S; :: thesis: (Stop S) ';' F = F
set k = (card (Stop S)) -' 1;
A1: (card (Stop S)) -' 1 = 0 by Lm6;
hence (Stop S) ';' F = (CutLastLoc (Stop S)) +* (Shift F,((card (Stop S)) -' 1)) by Th38
.= (CutLastLoc (Stop S)) +* F by A1, VALUED_1:29
.= F by FUNCT_4:21 ;
:: thesis: verum