let R be good Ring; for i1, il being Element of NAT holds NIC ((goto (i1,R)),il) = {i1}
let i1, il be Element of NAT ; NIC ((goto (i1,R)),il) = {i1}
now let x be
set ;
( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il } )A1:
now reconsider il1 =
il as
Element of
ObjectKind (IC ) by COMPOS_1:def 6;
reconsider I =
goto (
i1,
R) as
Element of the
Object-Kind of
(SCM R) . il by COMPOS_1:def 8;
set t = the
State of
(SCM R);
set Q = the the
Instructions of
(SCM R) -valued ManySortedSet of
NAT ;
assume A2:
x = i1
;
x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il } reconsider u = the
State of
(SCM R) +* (
(IC ),
il1) as
Element of
product the
Object-Kind of
(SCM R) by PBOOLE:155;
reconsider P = the the
Instructions of
(SCM R) -valued ManySortedSet of
NAT +* (
il,
I) as the
Instructions of
(SCM R) -valued ManySortedSet of
NAT ;
A3:
P /. il = P . il
by PBOOLE:158;
IC in dom the
State of
(SCM R)
by COMPOS_1:9;
then A4:
IC u = il
by FUNCT_7:33;
il in NAT
;
then
il in dom the the
Instructions of
(SCM R) -valued ManySortedSet of
NAT
by PARTFUN1:def 4;
then B4:
P . il = I
by FUNCT_7:33;
then
IC (Following (P,u)) = i1
by A4, A3, SCMRING2:17;
hence
x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il }
by A2, A3, A4, B4;
verum end; hence
(
x in {i1} iff
x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product the Object-Kind of (SCM R) : IC s = il } )
by A1, TARSKI:def 1;
verum end;
hence
NIC ((goto (i1,R)),il) = {i1}
by TARSKI:2; verum