let i be Element of SCM+FSA-Instr ; :: thesis: InsCode i <= 12
( not not InsCode i = 0 & ... & not InsCode i = 8 or not not InsCode i = 9 & ... & not InsCode i = 12 ) by Th7;
hence InsCode i <= 12 ; :: thesis: verum