let R be Ring; for il, i1 being Nat holds NIC ((goto (i1,R)),il) = {i1}
let il, i1 be Nat; NIC ((goto (i1,R)),il) = {i1}
now for x being object holds
( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )let x be
object ;
( x in {i1} iff x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )A1:
il in NAT
by ORDINAL1:def 12;
A2:
now ( x = i1 implies x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )reconsider il1 =
il as
Element of
Values (IC ) by MEMSTR_0:def 6, A1;
set I =
goto (
i1,
R);
set t = the
State of
(SCM R);
set Q = the
Instruction-Sequence of
(SCM R);
assume A3:
x = i1
;
x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } reconsider u = the
State of
(SCM R) +* (
(IC ),
il1) as
Element of
product (the_Values_of (SCM R)) by CARD_3:107;
reconsider P = the
Instruction-Sequence of
(SCM R) +* (
il,
(goto (i1,R))) as
Instruction-Sequence of
(SCM R) ;
A4:
P /. il = P . il
by PBOOLE:143, A1;
IC in dom the
State of
(SCM R)
by MEMSTR_0:2;
then A5:
IC u = il
by FUNCT_7:31;
il in NAT
by ORDINAL1:def 12;
then
il in dom the
Instruction-Sequence of
(SCM R)
by PARTFUN1:def 2;
then A6:
P . il = goto (
i1,
R)
by FUNCT_7:31;
then
IC (Following (P,u)) = i1
by A5, A4, SCMRING2:15;
hence
x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il }
by A3, A4, A5, A6;
verum end; hence
(
x in {i1} iff
x in { (IC (Exec ((goto (i1,R)),s))) where s is Element of product (the_Values_of (SCM R)) : IC s = il } )
by A2, TARSKI:def 1;
verum end;
hence
NIC ((goto (i1,R)),il) = {i1}
by TARSKI:2; verum