let R be Ring; :: thesis: for a being Data-Location of R
for il, i1 being Nat holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )
let a be Data-Location of R; :: thesis: for il, i1 being Nat holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )
let il, i1 be Nat; :: thesis: ( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {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: il in NAT by ORDINAL1:def 12;
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6, A1;
Values a = ((SCM-VAL R) * SCM-OK) . a9 by SCMRING2:24
.= the carrier of R by AMI_3:27, SCMRING1:4 ;
then reconsider 0R = 0. R as Element of Values a ;
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) ;
reconsider v = u +* (a .--> 0R) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
A2: IC in dom the State of (SCM R) by MEMSTR_0:2;
IC <> a by Th2;
then not IC in dom (a .--> 0R) by TARSKI:def 1;
then A4: IC v = IC u by FUNCT_4:11
.= il by A2, FUNCT_7:31 ;
A5: P /. il = P . il by PBOOLE:143, A1;
il in NAT by ORDINAL1:def 12;
then il in dom the Instruction-Sequence of (SCM R) by PARTFUN1:def 2;
then A6: 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 A4, A6, A5, SCMRING2:16;
hence i1 in NIC ((a =0_goto i1),il) by A4, A6, A5; :: thesis: NIC ((a =0_goto i1),il) c= {i1,(il + 1)}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC ((a =0_goto i1),il) or x in {i1,(il + 1)} )
assume x in NIC ((a =0_goto i1),il) ; :: thesis: x in {i1,(il + 1)}
then consider s being Element of product (the_Values_of (SCM R)) such that
A7: ( x = IC (Exec ((a =0_goto i1),s)) & IC s = il ) ;

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

suppose s . a = 0. R ; :: thesis: x in {i1,(il + 1)}

then x = i1 by A7, SCMRING2:16;
hence x in {i1,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;

suppose s . a <> 0. R ; :: thesis: x in {i1,(il + 1)}

then x = il + 1 by A7, SCMRING2:16;
hence x in {i1,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;

end;