let S be with_non_trivial_Instructions COM-Struct ; for i1, i2, i3, i4, i5, i6 being No-StopCode Instruction of S holds (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 5 = IncAddr (i6,5)
let i1, i2, i3, i4, i5, i6 be No-StopCode Instruction of S; (((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 5 = IncAddr (i6,5)
LastLoc ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) = 5
by Th33;
hence
(((((i1 ';' i2) ';' i3) ';' i4) ';' i5) ';' i6) . 5 = IncAddr (i6,5)
by Th49; verum