let il be Element of NAT ; NIC (halt SCM ),il = {il}
now let x be
set ;
( x in {il} iff x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = halt SCM ) } )A1:
now reconsider il1 =
il as
Element of
ObjectKind (IC SCM ) by COMPOS_1:def 6;
reconsider I =
halt SCM as
Element of the
Object-Kind of
SCM . il by COMPOS_1:def 8;
consider t being
State of
SCM ;
assume A2:
x = il
;
x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = halt SCM ) } reconsider p =
(IC SCM ),
il --> il1,
I as
PartState of
SCM by COMPOS_1:37;
reconsider u =
t +* p as
Element of
product the
Object-Kind of
SCM by PBOOLE:155;
reconsider n =
il as
Element of
NAT ;
dom ((IC SCM ),il --> il1,I) = {(IC SCM ),il}
by FUNCT_4:65;
then A3:
IC SCM in dom ((IC SCM ),il --> il1,I)
by TARSKI:def 2;
X:
(ProgramPart u) /. il = u . il
by COMPOS_1:38;
A4:
(
u . n = halt SCM &
IC u = n )
by AMI_1:129;
then IC (Following (ProgramPart u),u) =
u . (IC SCM )
by X, AMI_1:def 8
.=
((IC SCM ),il --> il1,I) . (IC SCM )
by A3, FUNCT_4:14
.=
il
by COMPOS_1:3, FUNCT_4:66
;
hence
x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = halt SCM ) }
by A2, A4, X;
verum end; hence
(
x in {il} iff
x in { (IC (Following (ProgramPart s),s)) where s is Element of product the Object-Kind of SCM : ( IC s = il & (ProgramPart s) /. il = halt SCM ) } )
by A1, TARSKI:def 1;
verum end;
hence
NIC (halt SCM ),il = {il}
by TARSKI:2; verum