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