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