let ins be Instruction of SCM+FSA; :: thesis: ( InsCode ins = 8 implies ex lb being Nat ex da being Int-Location st ins = da >0_goto lb )
assume A1: InsCode ins = 8 ; :: thesis: ex lb being Nat ex da being Int-Location st ins = da >0_goto lb
then reconsider I = ins as Instruction of SCM by Th8;
consider La being Nat, A being Data-Location such that
A2: I = A >0_goto La by A1, AMI_5:15;
A3: Int-Locations = SCM+FSA-Data-Loc ;
A in SCM-Data-Loc by AMI_2:def 16;
then reconsider da = A as Int-Location by A3;
take La ; :: thesis: ex da being Int-Location st ins = da >0_goto La
take da ; :: thesis: ins = da >0_goto La
thus ins = da >0_goto La by A2, Def13; :: thesis: verum