let i1, il be Element of NAT ; NIC ((goto i1),il) = {i1}
now let x be
set ;
( x in {i1} iff x in { (IC (Exec ((goto i1),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il } )A1:
now reconsider il1 =
il as
Element of
ObjectKind (IC ) by COMPOS_1:def 6;
reconsider n =
il1 as
Element of
NAT ;
reconsider I =
goto i1 as
Element of the
Object-Kind of
SCM+FSA . il by COMPOS_1:def 8;
set t = the
State of
SCM+FSA;
set Q = the the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
assume A2:
x = i1
;
x in { (IC (Exec ((goto i1),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il } 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 ;
IC in dom the
State of
SCM+FSA
by COMPOS_1:9;
then A3:
IC u = n
by FUNCT_7:33;
A4:
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 B4:
P . n = I
by FUNCT_7:33;
then
IC (Following (P,u)) = i1
by A3, SCMFSA_2:95, A4;
hence
x in { (IC (Exec ((goto i1),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il }
by A2, A3, B4, A4;
verum end; hence
(
x in {i1} iff
x in { (IC (Exec ((goto i1),s))) where s is Element of product the Object-Kind of SCM+FSA : IC s = il } )
by A1, TARSKI:def 1;
verum end;
hence
NIC ((goto i1),il) = {i1}
by TARSKI:2; verum