let R be good Ring; :: thesis: for i being Instruction of (SCM R) st ( for l being Element of NAT holds NIC i,l = {(succ l)} ) 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 = {(succ l)} ) implies JUMP i is empty )
assume A1: for l being Element of NAT holds NIC i,l = {(succ l)} ; :: thesis: JUMP i is empty
set X = { (NIC i,f) where f is Element of NAT : verum } ;
reconsider p = 1, q = 2 as Element of NAT ;
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;
NIC i,p = {(succ p)} by A1;
then {(succ p)} in { (NIC i,f) where f is Element of NAT : verum } ;
then x in {(succ p)} by A2, SETFAM_1:def 1;
then A3: x = succ p by TARSKI:def 1;
NIC i,q = {(succ q)} by A1;
then {(succ q)} in { (NIC i,f) where f is Element of NAT : verum } ;
then x in {(succ q)} by A2, SETFAM_1:def 1;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum