let a be Data-Location ; :: thesis: for il being Instruction-Location of SCM
for k being natural number holds NIC (a >0_goto k),il = {k,(Next )}
let il be Instruction-Location of SCM ; :: thesis: for k being natural number holds NIC (a >0_goto k),il = {k,(Next )}
let k be natural number ; :: thesis: NIC (a >0_goto k),il = {k,(Next )}
consider t being State of ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {k,(Next )} c= NIC (a >0_goto k),il

let x be set ; :: thesis: ( x in NIC (a >0_goto k),il implies b₁ in {k,(Next )} )
assume x in NIC (a >0_goto k),il ; :: thesis: b₁ in {k,(Next )}
then consider s being State of such that
A1: ( x = IC (Following s) & IC s = il & s . il = a >0_goto k ) ;

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

suppose s . a > 0 ; :: thesis: b₁ in {k,(Next )}

then x = k by A1, AMI_3:15;
hence x in {k,(Next )} by TARSKI:def 2; :: thesis: verum

end;

suppose s . a <= 0 ; :: thesis: b₁ in {k,(Next )}

then x = Next by A1, AMI_3:15;
hence x in {k,(Next )} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {k,(Next )} or x in NIC (a >0_goto k),il )
reconsider I = a >0_goto k as Element of ObjectKind il by AMI_1:def 14;
A2: IC SCM <> a by AMI_5:20;
il in NAT by AMI_1:def 4;
then reconsider il1 = il as Element of ObjectKind (IC SCM ) by AMI_1:def 11;
set u = t +* ((IC SCM ),il --> il1,I);
il in NAT by AMI_1:def 4;
then A3: a <> il by Th1;
assume A4: x in {k,(Next )} ; :: thesis: x in NIC (a >0_goto k),il

per cases ( x = k or x = Next ) by A4, TARSKI:def 2;

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

set v = (t +* ((IC SCM ),il --> il1,I)) +* (a .--> 1);
A6: dom (a .--> 1) = {a} by FUNCOP_1:19;
then not IC SCM in dom (a .--> 1) by A2, TARSKI:def 1;
then A7: IC ((t +* ((IC SCM ),il --> il1,I)) +* (a .--> 1)) = IC (t +* ((IC SCM ),il --> il1,I)) by FUNCT_4:12
.= il1 by AMI_1:129 ;
not il in dom (a .--> 1) by A3, A6, TARSKI:def 1;
then A8: ((t +* ((IC SCM ),il --> il1,I)) +* (a .--> 1)) . il = (t +* ((IC SCM ),il --> il1,I)) . il by FUNCT_4:12
.= I by AMI_1:129 ;
a in dom (a .--> 1) by A6, TARSKI:def 1;
then ((t +* ((IC SCM ),il --> il1,I)) +* (a .--> 1)) . a = (a .--> 1) . a by FUNCT_4:14
.= 1 by FUNCOP_1:87 ;
then IC (Following ((t +* ((IC SCM ),il --> il1,I)) +* (a .--> 1))) = k by A7, A8, AMI_3:15;
hence x in NIC (a >0_goto k),il by A5, A7, A8; :: thesis: verum

end;

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

set v = (t +* ((IC SCM ),il --> il1,I)) +* (a .--> 0 );
A10: dom (a .--> 0 ) = {a} by FUNCOP_1:19;
then not IC SCM in dom (a .--> 0 ) by A2, TARSKI:def 1;
then A11: IC ((t +* ((IC SCM ),il --> il1,I)) +* (a .--> 0 )) = IC (t +* ((IC SCM ),il --> il1,I)) by FUNCT_4:12
.= il1 by AMI_1:129 ;
not il in dom (a .--> 0 ) by A3, A10, TARSKI:def 1;
then A12: ((t +* ((IC SCM ),il --> il1,I)) +* (a .--> 0 )) . il = (t +* ((IC SCM ),il --> il1,I)) . il by FUNCT_4:12
.= I by AMI_1:129 ;
a in dom (a .--> 0 ) by A10, TARSKI:def 1;
then ((t +* ((IC SCM ),il --> il1,I)) +* (a .--> 0 )) . a = (a .--> 0 ) . a by FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
then IC (Following ((t +* ((IC SCM ),il --> il1,I)) +* (a .--> 0 ))) = Next by A11, A12, AMI_3:15;
hence x in NIC (a >0_goto k),il by A9, A11, A12; :: thesis: verum

end;

end;