let i be Instruction of SCMPDS; ( ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) implies JUMP i is empty )
set p = 1;
set q = 2;
assume A1:
for l being Element of NAT holds NIC (i,l) = {(l + 1)}
; 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
; 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; verum