let S be with_non_trivial_Instructions COM-Struct ; for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 = IncAddr (i2,1)
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 = IncAddr (i2,1)
LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4
by Th32;
hence ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 1 =
(((i1 ';' i2) ';' i3) ';' i4) . 1
by Th23, Th28
.=
IncAddr (i2,1)
by Th46
;
verum