let N be with_zero set ; :: thesis: for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N

for i being Element of the InstructionsF of S st ( for l being Nat holds NIC (i,l) = {l} ) holds

JUMP i is empty

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for i being Element of the InstructionsF of S st ( for l being Nat holds NIC (i,l) = {l} ) holds

JUMP i is empty

let i be Element of the InstructionsF of S; :: thesis: ( ( for l being 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 Nat : verum } ;

reconsider p = 0 , q = 1 as Nat ;

assume A1: for l being Nat holds NIC (i,l) = {l} ; :: thesis: JUMP i is empty

assume not JUMP i is empty ; :: thesis: contradiction

then consider x being object such that

A2: x in meet { (NIC (i,l)) where l is Nat : verum } ;

NIC (i,p) = {p} by A1;

then {p} in { (NIC (i,l)) where l is 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 Nat : verum } ;

then x in {q} by A2, SETFAM_1:def 1;

hence contradiction by A3, TARSKI:def 1; :: thesis: verum

for i being Element of the InstructionsF of S st ( for l being Nat holds NIC (i,l) = {l} ) holds

JUMP i is empty

let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; :: thesis: for i being Element of the InstructionsF of S st ( for l being Nat holds NIC (i,l) = {l} ) holds

JUMP i is empty

let i be Element of the InstructionsF of S; :: thesis: ( ( for l being 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 Nat : verum } ;

reconsider p = 0 , q = 1 as Nat ;

assume A1: for l being Nat holds NIC (i,l) = {l} ; :: thesis: JUMP i is empty

assume not JUMP i is empty ; :: thesis: contradiction

then consider x being object such that

A2: x in meet { (NIC (i,l)) where l is Nat : verum } ;

NIC (i,p) = {p} by A1;

then {p} in { (NIC (i,l)) where l is 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 Nat : verum } ;

then x in {q} by A2, SETFAM_1:def 1;

hence contradiction by A3, TARSKI:def 1; :: thesis: verum