let loc be Nat; not SCM-goto loc is halting
set f = the Object-Kind of SCM ;
consider s being SCM-State;
assume A1:
SCM-goto loc is halting
; contradiction
reconsider a3 = loc as Element of NAT by ORDINAL1:def 13;
reconsider V = SCM-goto loc as Element of SCM-Instr ;
set t = s +* (NAT .--> (succ a3));
A2:
dom s = the carrier of SCM
by PARTFUN1:def 4;
A3:
dom (NAT .--> (succ a3)) = {NAT }
by FUNCOP_1:19;
then
NAT in dom (NAT .--> (succ a3))
by TARSKI:def 1;
then A4: (s +* (NAT .--> (succ a3))) . NAT =
(NAT .--> (succ a3)) . NAT
by FUNCT_4:14
.=
succ a3
by FUNCOP_1:87
;
A5:
for x being set st x in dom the Object-Kind of SCM holds
(s +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x
A8:
{NAT } c= SCM-Memory
by AMI_2:30, ZFMISC_1:37;
A9: dom (s +* (NAT .--> (succ a3))) =
(dom s) \/ (dom (NAT .--> (succ a3)))
by FUNCT_4:def 1
.=
SCM-Memory \/ (dom (NAT .--> (succ a3)))
by A2
.=
SCM-Memory \/ {NAT }
by FUNCOP_1:19
.=
SCM-Memory
by A8, XBOOLE_1:12
;
dom the Object-Kind of SCM = SCM-Memory
by FUNCT_2:def 1;
then reconsider t = s +* (NAT .--> (succ a3)) as State of SCM by A9, A5, FUNCT_1:def 20, PARTFUN1:def 4, RELAT_1:def 18;
reconsider w = t as SCM-State by PBOOLE:155;
dom (NAT .--> loc) = {NAT }
by FUNCOP_1:19;
then
NAT in dom (NAT .--> loc)
by TARSKI:def 1;
then A10: (w +* (NAT .--> loc)) . NAT =
(NAT .--> loc) . NAT
by FUNCT_4:14
.=
loc
by FUNCOP_1:87
;
6 is Element of Segm 9
by NAT_1:45;
then w +* (NAT .--> loc) =
SCM-Chg w,(V jump_address )
by AMI_2:24
.=
SCM-Exec-Res V,w
by AMI_2:def 16
.=
Exec (SCM-goto loc),t
by AMI_2:def 17
.=
t
by A1, AMI_1:def 8
;
hence
contradiction
by A4, A10; verum