let i1, il be Element of NAT ; :: thesis: for a being Int-Location holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
let a be Int-Location ; :: thesis: NIC ((a =0_goto i1),il) = {i1,(succ il)}
set t = the State of SCM+FSA;
set Q = the the Instructions of SCM+FSA -valued ManySortedSet of NAT ;

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {i1,(succ 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,(succ il)} )
assume x in NIC ((a =0_goto i1),il) ; :: thesis: b₁ in {i1,(succ il)}
then consider s being Element of product the Object-Kind 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,(succ il)}

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

end;

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

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

end;

end;

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {i1,(succ il)} or x in NIC ((a =0_goto i1),il) )
reconsider I = a =0_goto i1 as Element of the Object-Kind of SCM+FSA . il by COMPOS_1:def 8;
A3: IC <> a by SCMFSA_2:81;
reconsider il1 = il as Element of ObjectKind (IC ) by COMPOS_1:def 6;
reconsider u = the State of SCM+FSA +* ((IC ),il1) as Element of product the Object-Kind of SCM+FSA by PBOOLE:155;
reconsider P = the the Instructions of SCM+FSA -valued ManySortedSet of NAT +* (il,I) as the Instructions of SCM+FSA -valued ManySortedSet of NAT ;
reconsider n = il as Element of NAT ;
assume A5: x in {i1,(succ il)} ; :: thesis: x in NIC ((a =0_goto i1),il)

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

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

reconsider v = u +* (a .--> 0) as Element of product the Object-Kind of SCM+FSA by PBOOLE:155;
xx: IC in dom the State of SCM+FSA by COMPOS_1:9;
A7: dom (a .--> 0) = {a} by FUNCOP_1:19;
then not IC in dom (a .--> 0) by A3, TARSKI:def 1;
then A8: IC v = IC u by FUNCT_4:12
.= n by FUNCT_7:33, xx ;
B10: P /. il = P . il by PBOOLE:158;
il in NAT ;
then il in dom the the Instructions of SCM+FSA -valued ManySortedSet of NAT by PARTFUN1:def 4;
then A10: P . il = I by FUNCT_7:33;
a in dom (a .--> 0) by A7, TARSKI:def 1;
then v . a = (a .--> 0) . a by FUNCT_4:14
.= 0 by FUNCOP_1:87 ;
then IC (Following (P,v)) = i1 by A8, A10, SCMFSA_2:96, B10;
hence x in NIC ((a =0_goto i1),il) by A6, A8, A10, B10; :: thesis: verum

end;

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

reconsider v = u +* (a .--> 1) as Element of product the Object-Kind of SCM+FSA by PBOOLE:155;
xx: IC in dom the State of SCM+FSA by COMPOS_1:9;
A12: dom (a .--> 1) = {a} by FUNCOP_1:19;
then not IC in dom (a .--> 1) by A3, TARSKI:def 1;
then A13: IC v = IC u by FUNCT_4:12
.= n by FUNCT_7:33, xx ;
B15: P /. il = P . il by PBOOLE:158;
il in NAT ;
then il in dom the the Instructions of SCM+FSA -valued ManySortedSet of NAT by PARTFUN1:def 4;
then A15: P . il = I by FUNCT_7:33;
a in dom (a .--> 1) by A12, TARSKI:def 1;
then v . a = (a .--> 1) . a by FUNCT_4:14
.= 1 by FUNCOP_1:87 ;
then IC (Following (P,v)) = succ il by A13, A15, SCMFSA_2:96, B15;
hence x in NIC ((a =0_goto i1),il) by A11, A13, A15, B15; :: thesis: verum

end;

end;