theorem Th50: :: COMPOS_2:51
for S being with_non_trivial_Instructions COM-Struct
for i1, i2, i3 being No-StopCode Instruction of S holds ((i1 ';' i2) ';' i3) . 2 = IncAddr (i3,2)