let ins be Instruction of SCM+FSA; :: thesis: ( InsCode ins = 7 implies ex lb being Element of NAT ex da being Int-Location st ins = da =0_goto lb )
assume A1: InsCode ins = 7 ; :: 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:14;
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, Def17; :: thesis: verum