let ins be Instruction of SCM+FSA ; :: thesis: ( InsCode ins = 8 implies ex lb being Element of NAT ex da being Int-Location st ins = da >0_goto lb )
assume A1: InsCode ins = 8 ; :: thesis: ex lb being Element of NAT ex da being Int-Location st ins = da >0_goto lb
then reconsider I = ins as Instruction of SCM by Th34;
consider La being Element of NAT , A being Data-Location such that
A2: I = A >0_goto La by A1, AMI_5:54;
A in SCM-Data-Loc by AMI_3:def 2;
then reconsider da = A as Int-Location by Def4;
reconsider loc = La as Element of NAT ;
take loc ; :: thesis: ex da being Int-Location st ins = da >0_goto loc
take da ; :: thesis: ins = da >0_goto loc
thus ins = da >0_goto loc by A2, Def18; :: thesis: verum