let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for i being Instruction of S
for l being Element of NAT holds JUMP i c= NIC (i,l)
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of N; :: thesis: for i being Instruction of S
for l being Element of NAT holds JUMP i c= NIC (i,l)
let i be Instruction of S; :: thesis: for l being Element of NAT holds JUMP i c= NIC (i,l)
let l be Element of NAT ; :: thesis: JUMP i c= NIC (i,l)
set X = { (NIC (i,k)) where k is Element of NAT : verum } ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in JUMP i or x in NIC (i,l) )
A1: NIC (i,l) in { (NIC (i,k)) where k is Element of NAT : verum } ;
assume x in JUMP i ; :: thesis: x in NIC (i,l)
hence x in NIC (i,l) by A1, SETFAM_1:def 1; :: thesis: verum