let a be Data-Location; :: thesis: for il, k being Nat holds NIC ((a =0_goto k),il) = {k,(il + 1)}

let il, k be Nat; :: thesis: NIC ((a =0_goto k),il) = {k,(il + 1)}

set t = the State of SCM;

set Q = the Instruction-Sequence of SCM;

set I = a =0_goto k;

A2: IC <> a by AMI_5:2;

reconsider n = il as Element of NAT by ORDINAL1:def 12;

reconsider il1 = n as Element of Values (IC ) by MEMSTR_0:def 6;

reconsider u = the State of SCM +* ((IC ),il1) as Element of product (the_Values_of SCM) by CARD_3:107;

reconsider P = the Instruction-Sequence of SCM +* (il,(a =0_goto k)) as Instruction-Sequence of SCM ;

assume A3: x in {k,(il + 1)} ; :: thesis: x in NIC ((a =0_goto k),il)

let il, k be Nat; :: thesis: NIC ((a =0_goto k),il) = {k,(il + 1)}

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,(il + 1)} c= NIC ((a =0_goto k),il)

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {k,(il + 1)} or x in NIC ((a =0_goto k),il) )let x be object ; :: thesis: ( x in NIC ((a =0_goto k),il) implies b_{1} in {k,(il + 1)} )

assume x in NIC ((a =0_goto k),il) ; :: thesis: b_{1} in {k,(il + 1)}

then consider s being Element of product (the_Values_of SCM) such that

A1: ( x = IC (Exec ((a =0_goto k),s)) & IC s = il ) ;

end;assume x in NIC ((a =0_goto k),il) ; :: thesis: b

then consider s being Element of product (the_Values_of SCM) such that

A1: ( x = IC (Exec ((a =0_goto k),s)) & IC s = il ) ;

set I = a =0_goto k;

A2: IC <> a by AMI_5:2;

reconsider n = il as Element of NAT by ORDINAL1:def 12;

reconsider il1 = n as Element of Values (IC ) by MEMSTR_0:def 6;

reconsider u = the State of SCM +* ((IC ),il1) as Element of product (the_Values_of SCM) by CARD_3:107;

reconsider P = the Instruction-Sequence of SCM +* (il,(a =0_goto k)) as Instruction-Sequence of SCM ;

assume A3: x in {k,(il + 1)} ; :: thesis: x in NIC ((a =0_goto k),il)

per cases
( x = k or x = il + 1 )
by A3, TARSKI:def 2;

end;

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

reconsider v = u +* (a .--> 0) as Element of product (the_Values_of SCM) by CARD_3:107;

A5: IC in dom the State of SCM by MEMSTR_0:2;

not IC in dom (a .--> 0) by A2, TARSKI:def 1;

then A7: IC v = IC u by FUNCT_4:11

.= n by A5, FUNCT_7:31 ;

reconsider il = il as Element of NAT by ORDINAL1:def 12;

A8: 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 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, A8, AMI_3:8;

hence x in NIC ((a =0_goto k),il) by A4, A7, A9, A8; :: thesis: verum

end;A5: IC in dom the State of SCM by MEMSTR_0:2;

not IC in dom (a .--> 0) by A2, TARSKI:def 1;

then A7: IC v = IC u by FUNCT_4:11

.= n by A5, FUNCT_7:31 ;

reconsider il = il as Element of NAT by ORDINAL1:def 12;

A8: 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 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, A8, AMI_3:8;

hence x in NIC ((a =0_goto k),il) by A4, A7, A9, A8; :: thesis: verum

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

reconsider v = u +* (a .--> 1) as Element of product (the_Values_of SCM) by CARD_3:107;

A11: IC in dom the State of SCM by MEMSTR_0:2;

not IC in dom (a .--> 1) by A2, TARSKI:def 1;

then A13: IC v = IC u by FUNCT_4:11

.= n by A11, FUNCT_7:31 ;

reconsider il = il as Element of NAT by ORDINAL1:def 12;

A14: P /. il = P . il by PBOOLE:143;

il in NAT ;

then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;

then A15: P . il = a =0_goto k by FUNCT_7:31;

a in dom (a .--> 1) by TARSKI:def 1;

then v . a = (a .--> 1) . a by FUNCT_4:13

.= 1 by FUNCOP_1:72 ;

then IC (Following (P,v)) = il + 1 by A13, A15, A14, AMI_3:8;

hence x in NIC ((a =0_goto k),il) by A10, A13, A15, A14; :: thesis: verum

end;A11: IC in dom the State of SCM by MEMSTR_0:2;

not IC in dom (a .--> 1) by A2, TARSKI:def 1;

then A13: IC v = IC u by FUNCT_4:11

.= n by A11, FUNCT_7:31 ;

reconsider il = il as Element of NAT by ORDINAL1:def 12;

A14: P /. il = P . il by PBOOLE:143;

il in NAT ;

then il in dom the Instruction-Sequence of SCM by PARTFUN1:def 2;

then A15: P . il = a =0_goto k by FUNCT_7:31;

a in dom (a .--> 1) by TARSKI:def 1;

then v . a = (a .--> 1) . a by FUNCT_4:13

.= 1 by FUNCOP_1:72 ;

then IC (Following (P,v)) = il + 1 by A13, A15, A14, AMI_3:8;

hence x in NIC ((a =0_goto k),il) by A10, A13, A15, A14; :: thesis: verum