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

for I being Instruction of S st ( for f being Element of NAT holds NIC (I,f) = {(f + 1)} ) holds

JUMP I is empty

let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; :: thesis: for I being Instruction of S st ( for f being Element of NAT holds NIC (I,f) = {(f + 1)} ) holds

JUMP I is empty

let I be Instruction of S; :: thesis: ( ( for f being Element of NAT holds NIC (I,f) = {(f + 1)} ) implies JUMP I is empty )

assume A1: for f being Element of NAT holds NIC (I,f) = {(f + 1)} ; :: 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 Nat : verum } ;

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

then consider x being object such that

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

A3: NIC (I,p) = {(p + 1)} by A1;

A4: NIC (I,q) = {(q + 1)} by A1;

A5: {(succ p)} in { (NIC (I,f)) where f is Nat : verum } by A3;

A6: {(succ q)} in { (NIC (I,f)) where f is Nat : verum } by A4;

A7: x in {(succ p)} by A2, A5, SETFAM_1:def 1;

A8: x in {(succ q)} by A2, A6, SETFAM_1:def 1;

x = succ p by A7, TARSKI:def 1;

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

for I being Instruction of S st ( for f being Element of NAT holds NIC (I,f) = {(f + 1)} ) holds

JUMP I is empty

let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N; :: thesis: for I being Instruction of S st ( for f being Element of NAT holds NIC (I,f) = {(f + 1)} ) holds

JUMP I is empty

let I be Instruction of S; :: thesis: ( ( for f being Element of NAT holds NIC (I,f) = {(f + 1)} ) implies JUMP I is empty )

assume A1: for f being Element of NAT holds NIC (I,f) = {(f + 1)} ; :: 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 Nat : verum } ;

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

then consider x being object such that

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

A3: NIC (I,p) = {(p + 1)} by A1;

A4: NIC (I,q) = {(q + 1)} by A1;

A5: {(succ p)} in { (NIC (I,f)) where f is Nat : verum } by A3;

A6: {(succ q)} in { (NIC (I,f)) where f is Nat : verum } by A4;

A7: x in {(succ p)} by A2, A5, SETFAM_1:def 1;

A8: x in {(succ q)} by A2, A6, SETFAM_1:def 1;

x = succ p by A7, TARSKI:def 1;

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