theorem Th36: :: COMPOS_2:37

for S being with_non_trivial_Instructions COM-Struct
for i, j being No-StopCode Instruction of S
for K being MacroInstruction of S holds ((i ';' j) ';' K) . 0 = i