let S be with_non_trivial_Instructions COM-Struct ; :: thesis: for j being No-StopCode Instruction of S

for I being MacroInstruction of S holds card (I ';' j) = (card I) + 1

let j be No-StopCode Instruction of S; :: thesis: for I being MacroInstruction of S holds card (I ';' j) = (card I) + 1

let I be MacroInstruction of S; :: thesis: card (I ';' j) = (card I) + 1

thus card (I ';' j) = ((card I) + (card (Macro j))) - 1 by COMPOS_1:20

.= (2 + (card I)) - 1 by COMPOS_1:56

.= (card I) + 1 ; :: thesis: verum

for I being MacroInstruction of S holds card (I ';' j) = (card I) + 1

let j be No-StopCode Instruction of S; :: thesis: for I being MacroInstruction of S holds card (I ';' j) = (card I) + 1

let I be MacroInstruction of S; :: thesis: card (I ';' j) = (card I) + 1

thus card (I ';' j) = ((card I) + (card (Macro j))) - 1 by COMPOS_1:20

.= (2 + (card I)) - 1 by COMPOS_1:56

.= (card I) + 1 ; :: thesis: verum