let lb be Instruction-Location of SCM+FSA ; :: thesis: for a being Int-Location holds InsCode (a >0_goto lb) = 8
let a be Int-Location ; :: thesis: InsCode (a >0_goto lb) = 8
ex A being Data-Location ex La being Instruction-Location of SCM st
( a = A & lb = La & a >0_goto lb = A >0_goto La ) by Def18;
hence InsCode (a >0_goto lb) = 8 by MCART_1:7; :: thesis: verum