let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty IC-Ins-separated AMI-Struct of N
for i being Element of the Instructions of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds
JUMP i is empty
let S be non empty IC-Ins-separated AMI-Struct of N; :: thesis: for i being Element of the Instructions of S st ( for l being Element of NAT holds NIC (i,l) = {l} ) holds
JUMP i is empty
let i be Element of the Instructions of S; :: thesis: ( ( for l being Element of NAT holds NIC (i,l) = {l} ) implies JUMP i is empty )
set p = 0 ;
set q = 1;
set X = { (NIC (i,l)) where l is Element of NAT : verum } ;
reconsider p = 0 , q = 1 as Element of NAT ;
assume A1: for l being Element of NAT holds NIC (i,l) = {l} ; :: thesis: JUMP i is empty
assume not JUMP i is empty ; :: thesis: contradiction
then consider x being set such that
A2: x in meet { (NIC (i,l)) where l is Element of NAT : verum } by XBOOLE_0:def 1;
NIC (i,p) = {p} by A1;
then {p} in { (NIC (i,l)) where l is Element of NAT : verum } ;
then A3: x in {p} by A2, SETFAM_1:def 1;
NIC (i,q) = {q} by A1;
then {q} in { (NIC (i,l)) where l is Element of NAT : verum } ;
then x in {q} by A2, SETFAM_1:def 1;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum