let loc be Nat; not SCM-goto loc is halting
set f = the Object-Kind of SCM;
set s = the SCM-State;
assume A1:
SCM-goto loc is halting
; contradiction
reconsider a3 = loc as Element of NAT by ORDINAL1:def 12;
reconsider V = SCM-goto loc as Element of SCM-Instr ;
set t = the SCM-State +* (NAT .--> (succ a3));
A2:
dom the SCM-State = the carrier of SCM
by PARTFUN1:def 2;
A3:
dom (NAT .--> (succ a3)) = {NAT}
by FUNCOP_1:13;
then
NAT in dom (NAT .--> (succ a3))
by TARSKI:def 1;
then A4: ( the SCM-State +* (NAT .--> (succ a3))) . NAT =
(NAT .--> (succ a3)) . NAT
by FUNCT_4:13
.=
succ a3
by FUNCOP_1:72
;
A5:
for x being set st x in dom the Object-Kind of SCM holds
( the SCM-State +* (NAT .--> (succ a3))) . x in the Object-Kind of SCM . x
A8:
{NAT} c= SCM-Memory
by AMI_2:22, ZFMISC_1:31;
A9: dom ( the SCM-State +* (NAT .--> (succ a3))) =
(dom the SCM-State) \/ (dom (NAT .--> (succ a3)))
by FUNCT_4:def 1
.=
SCM-Memory \/ (dom (NAT .--> (succ a3)))
by A2
.=
SCM-Memory \/ {NAT}
by FUNCOP_1:13
.=
SCM-Memory
by A8, XBOOLE_1:12
;
dom the Object-Kind of SCM = SCM-Memory
by FUNCT_2:def 1;
then reconsider t = the SCM-State +* (NAT .--> (succ a3)) as State of SCM by A9, A5, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
reconsider w = t as SCM-State by CARD_3:107;
dom (NAT .--> loc) = {NAT}
by FUNCOP_1:13;
then
NAT in dom (NAT .--> loc)
by TARSKI:def 1;
then A10: (w +* (NAT .--> loc)) . NAT =
(NAT .--> loc) . NAT
by FUNCT_4:13
.=
loc
by FUNCOP_1:72
;
6 is Element of Segm 9
by NAT_1:44;
then w +* (NAT .--> loc) =
SCM-Chg (w,(V jump_address))
by AMI_2:18
.=
SCM-Exec-Res (V,w)
by AMI_2:def 13
.=
Exec ((SCM-goto loc),t)
by AMI_2:def 14
.=
t
by A1, EXTPRO_1:def 3
;
hence
contradiction
by A4, A10; verum