let il, i1 be Nat; :: thesis: for a being Int-Location holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}
let a be Int-Location; :: thesis: NIC ((a =0_goto i1),il) = {i1,(il + 1)}
set t = the State of SCM+FSA;
set Q = the Instruction-Sequence of SCM+FSA;

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

let x be object ; :: thesis: ( x in NIC ((a =0_goto i1),il) implies b₁ in {i1,(il + 1)} )
assume x in NIC ((a =0_goto i1),il) ; :: thesis: b₁ in {i1,(il + 1)}
then consider s being Element of product (the_Values_of SCM+FSA) such that
A1: x = IC (Exec ((a =0_goto i1),s)) and
A2: IC s = il ;

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

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

then x = i1 by A1, SCMFSA_2:70;
hence x in {i1,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;

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

then x = il + 1 by A1, A2, SCMFSA_2:70;
hence x in {i1,(il + 1)} by TARSKI:def 2; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {i1,(il + 1)} or x in NIC ((a =0_goto i1),il) )
set I = a =0_goto i1;
A3: IC <> a by SCMFSA_2:56;
il in NAT by ORDINAL1:def 12;
then reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6;
reconsider u = the State of SCM+FSA +* ((IC ),il1) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM+FSA +* (il,(a =0_goto i1)) as Instruction-Sequence of SCM+FSA ;
reconsider n = il as Nat ;
assume A4: x in {i1,(il + 1)} ; :: thesis: x in NIC ((a =0_goto i1),il)

per cases ( x = i1 or x = il + 1 ) by A4, TARSKI:def 2;

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

reconsider v = u +* (a .--> 0) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
A6: IC in dom the State of SCM+FSA by MEMSTR_0:2;
not IC in dom (a .--> 0) by A3, TARSKI:def 1;
then A8: IC v = IC u by FUNCT_4:11
.= n by A6, FUNCT_7:31 ;
il in NAT by ORDINAL1:def 12;
then A9: P /. il = P . il by PBOOLE:143;
il in NAT by ORDINAL1:def 12;
then il in dom the Instruction-Sequence of SCM+FSA by PARTFUN1:def 2;
then A10: P . il = a =0_goto i1 by FUNCT_7:31;
a in dom (a .--> 0) by TARSKI:def 1;
then v . a = (a .--> 0) . a by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
then IC (Following (P,v)) = i1 by A8, A10, A9, SCMFSA_2:70;
hence x in NIC ((a =0_goto i1),il) by A5, A8, A10, A9; :: thesis: verum

end;

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

reconsider v = u +* (a .--> 1) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
A12: IC in dom the State of SCM+FSA by MEMSTR_0:2;
not IC in dom (a .--> 1) by A3, TARSKI:def 1;
then A14: IC v = IC u by FUNCT_4:11
.= n by A12, FUNCT_7:31 ;
il in NAT by ORDINAL1:def 12;
then A15: P /. il = P . il by PBOOLE:143;
il in NAT by ORDINAL1:def 12;
then il in dom the Instruction-Sequence of SCM+FSA by PARTFUN1:def 2;
then A16: P . il = a =0_goto i1 by FUNCT_7:31;
a in dom (a .--> 1) by TARSKI:def 1;
then v . a = (a .--> 1) . a by FUNCT_4:13
.= 1 by FUNCOP_1:72 ;
then IC (Following (P,v)) = il + 1 by A14, A16, A15, SCMFSA_2:70;
hence x in NIC ((a =0_goto i1),il) by A11, A14, A16, A15; :: thesis: verum

end;

end;