let i1, il be Instruction-Location of SCM+FSA ; :: thesis: for a being Int-Location holds NIC (a >0_goto i1),il = {i1,(Next il)}
let a be Int-Location ; :: thesis: NIC (a >0_goto i1),il = {i1,(Next il)}
consider t being State of ;

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

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

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

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

then x = i1 by A1, A2, A3, SCMFSA_2:97;
hence x in {i1,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

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

then x = Next il by A1, A2, A3, SCMFSA_2:97;
hence x in {i1,(Next il)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

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

per cases ( x = i1 or x = Next il ) by A6, TARSKI:def 2;

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

set v = (t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 1);
A8: dom (a .--> 1) = {a} by FUNCOP_1:19;
then not IC SCM+FSA in dom (a .--> 1) by A4, TARSKI:def 1;
then A9: IC ((t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 1)) = IC (t +* ((IC SCM+FSA ),il --> il1,I)) by FUNCT_4:12
.= il by AMI_1:129 ;
not il in dom (a .--> 1) by A5, A8, TARSKI:def 1;
then A10: ((t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 1)) . il = (t +* ((IC SCM+FSA ),il --> il1,I)) . il by FUNCT_4:12
.= I by AMI_1:129 ;
a in dom (a .--> 1) by A8, TARSKI:def 1;
then ((t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 1)) . a = (a .--> 1) . a by FUNCT_4:14
.= 1 by FUNCOP_1:87 ;
then IC (Following ((t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 1))) = i1 by A9, A10, SCMFSA_2:97;
hence x in NIC (a >0_goto i1),il by A7, A9, A10; :: thesis: verum

end;

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

set v = (t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 0 );
A12: dom (a .--> 0 ) = {a} by FUNCOP_1:19;
then not IC SCM+FSA in dom (a .--> 0 ) by A4, TARSKI:def 1;
then A13: IC ((t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 0 )) = IC (t +* ((IC SCM+FSA ),il --> il1,I)) by FUNCT_4:12
.= il by AMI_1:129 ;
not il in dom (a .--> 0 ) by A5, A12, TARSKI:def 1;
then A14: ((t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 0 )) . il = (t +* ((IC SCM+FSA ),il --> il1,I)) . il by FUNCT_4:12
.= I by AMI_1:129 ;
a in dom (a .--> 0 ) by A12, TARSKI:def 1;
then ((t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 0 )) . a = (a .--> 0 ) . a by FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
then IC (Following ((t +* ((IC SCM+FSA ),il --> il1,I)) +* (a .--> 0 ))) = Next il by A13, A14, SCMFSA_2:97;
hence x in NIC (a >0_goto i1),il by A11, A13, A14; :: thesis: verum

end;

end;