let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i, j, k being No-StopCode Instruction of S holds ((i ';' j) ';' k) . 1 = IncAddr (j,1)
let i, j, k be No-StopCode Instruction of S; :: thesis: ((i ';' j) ';' k) . 1 = IncAddr (j,1)
LastLoc (i ';' j) = 2 by Th30;
hence ((i ';' j) ';' k) . 1 = (i ';' j) . 1 by Th23, Th28
.= IncAddr (j,1) by Th44 ;
:: thesis: verum