let R be good Ring; :: thesis: for a being Data-Location of R
for i1, il being Instruction-Location of SCM R holds
( i1 in NIC (a =0_goto i1),il & NIC (a =0_goto i1),il c= {i1,(Next il)} )
let a be Data-Location of R; :: thesis: for i1, il being Instruction-Location of SCM R holds
( i1 in NIC (a =0_goto i1),il & NIC (a =0_goto i1),il c= {i1,(Next il)} )
let i1, il be Instruction-Location of SCM R; :: thesis: ( i1 in NIC (a =0_goto i1),il & NIC (a =0_goto i1),il c= {i1,(Next il)} )
consider t being State of (SCM R);
il in NAT by AMI_1:def 4;
then reconsider il1 = il as Element of ObjectKind (IC (SCM R)) by AMI_1:def 11;
reconsider I = a =0_goto i1 as Element of ObjectKind il by AMI_1:def 14;
set u = t +* ((IC (SCM R)),il --> il1,I);
reconsider a' = a as Element of SCM-Data-Loc by SCMRING2:1;
ObjectKind a = (SCM-OK R) . a' by SCMRING2:def 1
.= the carrier of R by SCMRING1:5 ;
then reconsider 0R = 0. R as Element of ObjectKind a ;
set v = (t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R);
A1: dom ((IC (SCM R)),il --> il1,I) = {(IC (SCM R)),il} by FUNCT_4:65;
A2: dom (a .--> 0R) = {a} by FUNCOP_1:19;
A3: IC (SCM R) in dom ((IC (SCM R)),il --> il1,I) by A1, TARSKI:def 2;
A4: IC (SCM R) <> il by AMI_1:48;
IC (SCM R) <> a by Th3;
then not IC (SCM R) in dom (a .--> 0R) by A2, TARSKI:def 1;
then A5: IC ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R)) = (t +* ((IC (SCM R)),il --> il1,I)) . (IC (SCM R)) by FUNCT_4:12
.= ((IC (SCM R)),il --> il1,I) . (IC (SCM R)) by A3, FUNCT_4:14
.= il by A4, FUNCT_4:66 ;
A6: il in dom ((IC (SCM R)),il --> il1,I) by A1, TARSKI:def 2;
il in NAT by AMI_1:def 4;
then a <> il by Th2;
then not il in dom (a .--> 0R) by A2, TARSKI:def 1;
then A7: ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R)) . il = (t +* ((IC (SCM R)),il --> il1,I)) . il by FUNCT_4:12
.= ((IC (SCM R)),il --> il1,I) . il by A6, FUNCT_4:14
.= I by FUNCT_4:66 ;
a in dom (a .--> 0R) by A2, TARSKI:def 1;
then ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R)) . a = (a .--> 0R) . a by FUNCT_4:14
.= 0. R by FUNCOP_1:87 ;
then IC (Following ((t +* ((IC (SCM R)),il --> il1,I)) +* (a .--> 0R))) = i1 by A5, A7, SCMRING2:18;
hence i1 in NIC (a =0_goto i1),il by A5, A7; :: thesis: NIC (a =0_goto i1),il c= {i1,(Next il)}
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC (a =0_goto i1),il or x in {i1,(Next il)} )
assume x in NIC (a =0_goto i1),il ; :: thesis: x in {i1,(Next il)}
then consider s being State of (SCM R) such that
A8: ( x = IC (Following s) & IC s = il & s . il = a =0_goto i1 ) ;

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

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

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

end;

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

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

end;

end;