let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite realistic COM-Struct of N
for i being Instruction of S holds card (Macro i) = 2
let S be non empty stored-program IC-Ins-separated definite realistic COM-Struct of N; :: thesis: for i being Instruction of S holds card (Macro i) = 2
let i be Instruction of S; :: thesis: card (Macro i) = 2
thus card (Macro i) = len <%i,(halt S)%> by AFINSQ_1:80
.= 2 by AFINSQ_1:42 ; :: thesis: verum