let N be non empty with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of S st ( for f being Element of NAT holds NIC I,f = {(NextLoc f,S)} ) holds
JUMP I is empty
let S be non empty stored-program IC-Ins-separated definite standard AMI-Struct of N; :: thesis: for I being Instruction of S st ( for f being Element of NAT holds NIC I,f = {(NextLoc f,S)} ) holds
JUMP I is empty
let I be Instruction of S; :: thesis: ( ( for f being Element of NAT holds NIC I,f = {(NextLoc f,S)} ) implies JUMP I is empty )
assume A1: for f being Element of NAT holds NIC I,f = {(NextLoc f,S)} ; :: thesis: JUMP I is empty
set p = 1;
set q = 2;
reconsider p = 1, q = 2 as Element of NAT ;
set X = { (NIC I,f) where f is Element of NAT : verum } ;
assume not JUMP I is empty ; :: thesis: contradiction
then consider x being set such that
A2: x in meet { (NIC I,f) where f is Element of NAT : verum } by XBOOLE_0:def 1;
A3: NIC I,p = {(NextLoc p,S)} by A1;
A4: NIC I,q = {(NextLoc q,S)} by A1;
A5: {(NextLoc p,S)} in { (NIC I,f) where f is Element of NAT : verum } by A3;
A6: {(NextLoc q,S)} in { (NIC I,f) where f is Element of NAT : verum } by A4;
A7: x in {(NextLoc p,S)} by A2, A5, SETFAM_1:def 1;
A8: x in {(NextLoc q,S)} by A2, A6, SETFAM_1:def 1;
A9: x = NextLoc p,S by A7, TARSKI:def 1;
x = NextLoc q,S by A8, TARSKI:def 1;
hence contradiction by A9, AMISTD_1:36; :: thesis: verum