let R be Ring; :: thesis: for i being Instruction of (SCM R) st ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) holds

JUMP i is empty

set p = 1;

set q = 2;

let i be Instruction of (SCM R); :: thesis: ( ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) implies JUMP i is empty )

assume A1: for l being Element of NAT holds NIC (i,l) = {(l + 1)} ; :: thesis: JUMP i is empty

set X = { (NIC (i,f)) where f is Nat : verum } ;

reconsider p = 1, q = 2 as Element of NAT ;

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 } ;

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

then {(p + 1)} in { (NIC (i,f)) where f is Nat : verum } ;

then x in {(p + 1)} by A2, SETFAM_1:def 1;

then A3: x = p + 1 by TARSKI:def 1;

NIC (i,q) = {(q + 1)} by A1;

then {(q + 1)} in { (NIC (i,f)) where f is Nat : verum } ;

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

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

JUMP i is empty

set p = 1;

set q = 2;

let i be Instruction of (SCM R); :: thesis: ( ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) implies JUMP i is empty )

assume A1: for l being Element of NAT holds NIC (i,l) = {(l + 1)} ; :: thesis: JUMP i is empty

set X = { (NIC (i,f)) where f is Nat : verum } ;

reconsider p = 1, q = 2 as Element of NAT ;

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 } ;

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

then {(p + 1)} in { (NIC (i,f)) where f is Nat : verum } ;

then x in {(p + 1)} by A2, SETFAM_1:def 1;

then A3: x = p + 1 by TARSKI:def 1;

NIC (i,q) = {(q + 1)} by A1;

then {(q + 1)} in { (NIC (i,f)) where f is Nat : verum } ;

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

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