let R be good Ring; :: thesis: for a being Data-Location of R
for i1, il being Element of NAT holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(succ il)} )
let a be Data-Location of R; :: thesis: for i1, il being Element of NAT holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(succ il)} )
let i1, il be Element of NAT ; :: thesis: ( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(succ il)} )
consider t being State of (SCM R);
reconsider I = a =0_goto i1 as Element of the Object-Kind of (SCM R) . il by COMPOS_1:def 8;
reconsider a9 = a as Element of Data-Locations SCM by SCMRING2:1;
reconsider il1 = il as Element of ObjectKind (IC (SCM R)) by COMPOS_1:def 6;
ObjectKind a = (SCM-OK R) . a9 by SCMRING2:def 1
.= the carrier of R by AMI_3:72, SCMRING1:5 ;
then reconsider 0R = 0. R as Element of ObjectKind a ;
reconsider p = ((IC (SCM R)),il) --> (il1,I) as PartState of (SCM R) by COMPOS_1:37;
reconsider u = t +* p as State of (SCM R) ;
reconsider v = u +* (a .--> 0R) as Element of product the Object-Kind of (SCM R) by PBOOLE:155;
A1: dom (a .--> 0R) = {a} by FUNCOP_1:19;
A2: dom (((IC (SCM R)),il) --> (il1,I)) = {(IC (SCM R)),il} by FUNCT_4:65;
then A3: IC (SCM R) in dom (((IC (SCM R)),il) --> (il1,I)) by TARSKI:def 2;
IC (SCM R) <> a by Th3;
then not IC (SCM R) in dom (a .--> 0R) by A1, TARSKI:def 1;
then A4: IC v = u . (IC (SCM R)) by FUNCT_4:12
.= (((IC (SCM R)),il) --> (il1,I)) . (IC (SCM R)) by A3, FUNCT_4:14
.= il by COMPOS_1:3, FUNCT_4:66 ;
A5: il in dom (((IC (SCM R)),il) --> (il1,I)) by A2, TARSKI:def 2;
a <> il by Th2;
then u: not il in dom (a .--> 0R) by A1, TARSKI:def 1;
A6: (ProgramPart v) /. il = v . il by COMPOS_1:38
.= u . il by u, FUNCT_4:12
.= (((IC (SCM R)),il) --> (il1,I)) . il by A5, FUNCT_4:14
.= I by FUNCT_4:66 ;
a in dom (a .--> 0R) by A1, TARSKI:def 1;
then v . a = (a .--> 0R) . a by FUNCT_4:14
.= 0. R by FUNCOP_1:87 ;
then IC (Following ((ProgramPart v),v)) = i1 by A4, A6, SCMRING2:18;
hence i1 in NIC ((a =0_goto i1),il) by A4, A6; :: thesis: NIC ((a =0_goto i1),il) c= {i1,(succ il)}
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC ((a =0_goto i1),il) or x in {i1,(succ il)} )
assume x in NIC ((a =0_goto i1),il) ; :: thesis: x in {i1,(succ il)}
then consider s being Element of product the Object-Kind 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,(succ il)}

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

end;

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

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

end;

end;