let R be non trivial Ring; :: thesis: for a being Data-Location of R

for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}

let a be Data-Location of R; :: thesis: for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}

let il, i1 be Element of NAT ; :: thesis: NIC ((a =0_goto i1),il) = {i1,(il + 1)}

set t = the State of (SCM R);

set Q = the Instruction-Sequence of (SCM R);

set I = a =0_goto i1;

reconsider a9 = a as Element of Data-Locations by SCMRING2:1;

A1: Values a = ((SCM-VAL R) * SCM-OK) . a9 by SCMRING2:24

.= the carrier of R by AMI_3:27, SCMRING1:4 ;

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

thus NIC ((a =0_goto i1),il) c= {i1,(il + 1)} by Th31; :: according to XBOOLE_0:def 10 :: thesis: {i1,(il + 1)} c= NIC ((a =0_goto i1),il)

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

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

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

A2: IC <> a by Th2;

A3: IC in dom the State of (SCM R) by MEMSTR_0:2;

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

for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}

let a be Data-Location of R; :: thesis: for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}

let il, i1 be Element of NAT ; :: thesis: NIC ((a =0_goto i1),il) = {i1,(il + 1)}

set t = the State of (SCM R);

set Q = the Instruction-Sequence of (SCM R);

set I = a =0_goto i1;

reconsider a9 = a as Element of Data-Locations by SCMRING2:1;

A1: Values a = ((SCM-VAL R) * SCM-OK) . a9 by SCMRING2:24

.= the carrier of R by AMI_3:27, SCMRING1:4 ;

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

thus NIC ((a =0_goto i1),il) c= {i1,(il + 1)} by Th31; :: according to XBOOLE_0:def 10 :: thesis: {i1,(il + 1)} c= NIC ((a =0_goto i1),il)

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

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

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

A2: IC <> a by Th2;

A3: IC in dom the State of (SCM R) by MEMSTR_0:2;

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

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

end;

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

reconsider 0R = 0. R as Element of Values a by A1;

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

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

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

.= il by A3, FUNCT_7:31 ;

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

il in NAT ;

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

then A9: P . il = a =0_goto i1 by FUNCT_7:31;

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

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

.= 0. R by FUNCOP_1:72 ;

then IC (Following (P,v)) = i1 by A7, A8, A9, SCMRING2:16;

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

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

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

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

.= il by A3, FUNCT_7:31 ;

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

il in NAT ;

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

then A9: P . il = a =0_goto i1 by FUNCT_7:31;

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

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

.= 0. R by FUNCOP_1:72 ;

then IC (Following (P,v)) = i1 by A7, A8, A9, SCMRING2:16;

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

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

consider e being Element of R such that

A11: e <> 0. R by STRUCT_0:def 18;

reconsider E = e as Element of Values a by A1;

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

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

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

.= il by A3, FUNCT_7:31 ;

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

il in NAT ;

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

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

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

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

.= E by FUNCOP_1:72 ;

then IC (Following (P,v)) = il + 1 by A11, A13, A14, A15, SCMRING2:16;

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

end;A11: e <> 0. R by STRUCT_0:def 18;

reconsider E = e as Element of Values a by A1;

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

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

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

.= il by A3, FUNCT_7:31 ;

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

il in NAT ;

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

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

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

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

.= E by FUNCOP_1:72 ;

then IC (Following (P,v)) = il + 1 by A11, A13, A14, A15, SCMRING2:16;

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