theorem Th44: :: COMPOS_2:45
for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S holds (i ';' j) . 1 = IncAddr (j,1)