let a be Data-Location ; :: thesis: for il being Element of NAT
for k being natural number holds NIC ((a =0_goto k),il) = {k,(succ il)}
let il be Element of NAT ; :: thesis: for k being natural number holds NIC ((a =0_goto k),il) = {k,(succ il)}
let k be natural number ; :: thesis: NIC ((a =0_goto k),il) = {k,(succ il)}
set t = the State of SCM;
set Q = the Instruction-Sequence of SCM;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {k,(succ il)} c= NIC ((a =0_goto k),il)

let x be set ; :: thesis: ( x in NIC ((a =0_goto k),il) implies b₁ in {k,(succ il)} )
assume x in NIC ((a =0_goto k),il) ; :: thesis: b₁ in {k,(succ il)}
then consider s being Element of product the Object-Kind of SCM such that
A1: ( x = IC (Exec ((a =0_goto k),s)) & IC s = il ) ;

per cases ( s . a = 0 or s . a <> 0 ) ;

suppose s . a = 0 ; :: thesis: b₁ in {k,(succ il)}

then x = k by A1, AMI_3:8;
hence x in {k,(succ il)} by TARSKI:def 2; :: thesis: verum

end;

suppose s . a <> 0 ; :: thesis: b₁ in {k,(succ il)}

then x = succ il by A1, AMI_3:8;
hence x in {k,(succ il)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {k,(succ il)} or x in NIC ((a =0_goto k),il) )
set I = a =0_goto k;
A2: IC <> a by AMI_5:2;
reconsider il1 = il as Element of ObjectKind (IC ) by MEMSTR_0:def 3;
reconsider n = il as Element of NAT ;
reconsider u = the State of SCM +* ((IC ),il1) as Element of product the Object-Kind of SCM by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM +* (il,(a =0_goto k)) as Instruction-Sequence of SCM ;
assume A4: x in {k,(succ il)} ; :: thesis: x in NIC ((a =0_goto k),il)

per cases ( x = k or x = succ il ) by A4, TARSKI:def 2;

suppose A5: x = k ; :: thesis: x in NIC ((a =0_goto k),il)

reconsider v = u +* (a .--> 0) as Element of product the Object-Kind of SCM by CARD_3:107;
xx: IC in dom the State of SCM by MEMSTR_0:2;
A6: dom (a .--> 0) = {a} by FUNCOP_1:13;
then not IC in dom (a .--> 0) by A2, TARSKI:def 1;
then A7: IC v = IC u by FUNCT_4:11
.= n by xx, FUNCT_7:31 ;
B9: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;
then A9: P . il = a =0_goto k by FUNCT_7:31;
a in dom (a .--> 0) by A6, TARSKI:def 1;
then v . a = (a .--> 0) . a by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
then IC (Following (P,v)) = k by A7, A9, B9, AMI_3:8;
hence x in NIC ((a =0_goto k),il) by A5, A7, A9, B9; :: thesis: verum

end;

suppose A10: x = succ il ; :: thesis: x in NIC ((a =0_goto k),il)

reconsider v = u +* (a .--> 1) as Element of product the Object-Kind of SCM by CARD_3:107;
xx: IC in dom the State of SCM by MEMSTR_0:2;
A11: dom (a .--> 1) = {a} by FUNCOP_1:13;
then not IC in dom (a .--> 1) by A2, TARSKI:def 1;
then A12: IC v = IC u by FUNCT_4:11
.= n by xx, FUNCT_7:31 ;
B14: P /. il = P . il by PBOOLE:143;
il in NAT ;
then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;
then A14: P . il = a =0_goto k by FUNCT_7:31;
a in dom (a .--> 1) by A11, TARSKI:def 1;
then v . a = (a .--> 1) . a by FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
then IC (Following (P,v)) = succ il by A12, A14, B14, AMI_3:8;
hence x in NIC ((a =0_goto k),il) by A10, A12, A14, B14; :: thesis: verum

end;

end;