let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for i1, i2, i3, i4, i5 being No-StopCode Instruction of S holds ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 = IncAddr (i4,3)
let i1, i2, i3, i4, i5 be No-StopCode Instruction of S; :: thesis: ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 = IncAddr (i4,3)
B: LastLoc (((i1 ';' i2) ';' i3) ';' i4) = 4 by Th33;
thus ((((i1 ';' i2) ';' i3) ';' i4) ';' i5) . 3 = (((i1 ';' i2) ';' i3) ';' i4) . 3 by Th23, B, Th28
.= IncAddr (i4,3) by Th55 ; :: thesis: verum