let R be good Ring; :: thesis: for il being Instruction-Location of SCM R holds NIC (halt (SCM R)),il = {il}
let il be Instruction-Location of SCM R; :: thesis: NIC (halt (SCM R)),il = {il}
now let x be
set ;
:: thesis: ( x in {il} iff x in { (IC (Following s)) where s is State of (SCM R) : ( IC s = il & s . il = halt (SCM R) ) } )A1:
now assume A2:
x = il
;
:: thesis: x in { (IC (Following s)) where s is State of (SCM R) : ( IC s = il & s . il = halt (SCM R) ) } consider t being
State of
(SCM R);
il in NAT
by AMI_1:def 4;
then reconsider il1 =
il as
Element of
ObjectKind (IC (SCM R)) by AMI_1:def 11;
reconsider I =
halt (SCM R) as
Element of
ObjectKind il by AMI_1:def 14;
set u =
t +* ((IC (SCM R)),il --> il1,I);
A3:
dom ((IC (SCM R)),il --> il1,I) = {(IC (SCM R)),il}
by FUNCT_4:65;
then A4:
IC (SCM R) in dom ((IC (SCM R)),il --> il1,I)
by TARSKI:def 2;
A5:
IC (SCM R) <> il
by AMI_1:48;
il in dom ((IC (SCM R)),il --> il1,I)
by A3, TARSKI:def 2;
then A6:
(t +* ((IC (SCM R)),il --> il1,I)) . il =
((IC (SCM R)),il --> il1,I) . il
by FUNCT_4:14
.=
halt (SCM R)
by FUNCT_4:66
;
A7:
IC (t +* ((IC (SCM R)),il --> il1,I)) =
((IC (SCM R)),il --> il1,I) . (IC (SCM R))
by A4, FUNCT_4:14
.=
il
by A5, FUNCT_4:66
;
then IC (Following (t +* ((IC (SCM R)),il --> il1,I))) =
(t +* ((IC (SCM R)),il --> il1,I)) . (IC (SCM R))
by A6, AMI_1:def 8
.=
((IC (SCM R)),il --> il1,I) . (IC (SCM R))
by A4, FUNCT_4:14
.=
il
by A5, FUNCT_4:66
;
hence
x in { (IC (Following s)) where s is State of (SCM R) : ( IC s = il & s . il = halt (SCM R) ) }
by A2, A6, A7;
:: thesis: verum end; hence
(
x in {il} iff
x in { (IC (Following s)) where s is State of (SCM R) : ( IC s = il & s . il = halt (SCM R) ) } )
by A1, TARSKI:def 1;
:: thesis: verum end;
hence
NIC (halt (SCM R)),il = {il}
by TARSKI:2; :: thesis: verum