theorem Th46: :: COMPOS_2:47

for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3, i4 being No-StopCode Instruction of S holds (((i1 ';' i2) ';' i3) ';' i4) . 1 = IncAddr (i2,1)