let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for i being Element of the Instructions of S st not IL is trivial & ( for l being Instruction-Location of S holds NIC i,l = {l} ) holds
JUMP i is empty
let IL be non empty set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for i being Element of the Instructions of S st not IL is trivial & ( for l being Instruction-Location of S holds NIC i,l = {l} ) holds
JUMP i is empty
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N; :: thesis: for i being Element of the Instructions of S st not IL is trivial & ( for l being Instruction-Location of S holds NIC i,l = {l} ) holds
JUMP i is empty
let i be Element of the Instructions of S; :: thesis: ( not IL is trivial & ( for l being Instruction-Location of S holds NIC i,l = {l} ) implies JUMP i is empty )
given p, q being Element of IL such that A1: p <> q ; :: according to YELLOW_8:def 1 :: thesis: ( ex l being Instruction-Location of S st not NIC i,l = {l} or JUMP i is empty )
set X = { (NIC i,l) where l is Instruction-Location of S : verum } ;
reconsider p = p, q = q as Instruction-Location of S by AMI_1:def 4;
assume A2: for l being Instruction-Location of S 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
A3: x in meet { (NIC i,l) where l is Instruction-Location of S : verum } by XBOOLE_0:def 1;
NIC i,p = {p} by A2;
then {p} in { (NIC i,l) where l is Instruction-Location of S : verum } ;
then x in {p} by A3, SETFAM_1:def 1;
then A4: x = p by TARSKI:def 1;
NIC i,q = {q} by A2;
then {q} in { (NIC i,l) where l is Instruction-Location of S : verum } ;
then x in {q} by A3, SETFAM_1:def 1;
hence contradiction by A1, A4, TARSKI:def 1; :: thesis: verum