let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i1, i2, i3 being No-StopCode Instruction of S holds ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2)
let i1, i2, i3 be No-StopCode Instruction of S; :: thesis: ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2)
LastLoc (i1 ';' i2) = 2 by Th30;
hence ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2) by Th49; :: thesis: verum