let a be Data-Location; for loc being Nat holds not a >0_goto loc is halting
let loc be Nat; not a >0_goto loc is halting
set f = the_Values_of SCM;
set s = the SCM-State;
reconsider V = a >0_goto loc as Element of SCM-Instr ;
reconsider a3 = loc as Nat ;
set t = the SCM-State +* (NAT .--> (a3 + 1));
A1:
{NAT} c= SCM-Memory
by AMI_2:22, ZFMISC_1:31;
A2:
dom the SCM-State = the carrier of SCM
by AMI_2:28;
A3: dom ( the SCM-State +* (NAT .--> (a3 + 1))) =
(dom the SCM-State) \/ (dom (NAT .--> (a3 + 1)))
by FUNCT_4:def 1
.=
SCM-Memory \/ (dom (NAT .--> (a3 + 1)))
by A2
.=
SCM-Memory \/ {NAT}
.=
SCM-Memory
by A1, XBOOLE_1:12
;
A4:
8 is Element of Segm 9
by NAT_1:44;
NAT in dom (NAT .--> (a3 + 1))
by TARSKI:def 1;
then A6: ( the SCM-State +* (NAT .--> (a3 + 1))) . NAT =
(NAT .--> (a3 + 1)) . NAT
by FUNCT_4:13
.=
a3 + 1
by FUNCOP_1:72
;
A7:
for x being object st x in dom (the_Values_of SCM) holds
( the SCM-State +* (NAT .--> (a3 + 1))) . x in (the_Values_of SCM) . x
dom (the_Values_of SCM) = SCM-Memory
by AMI_2:27;
then reconsider t = the SCM-State +* (NAT .--> (a3 + 1)) as State of SCM by A3, A7, FUNCT_1:def 14, PARTFUN1:def 2, RELAT_1:def 18;
reconsider w = t as SCM-State by CARD_3:107;
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
;
assume A11:
a >0_goto loc is halting
; contradiction
A12:
a is Element of SCM-Data-Loc
by AMI_2:def 16;
per cases
( w . (V cond_address) <= 0 or w . (V cond_address) > 0 )
;
suppose
w . (V cond_address) > 0
;
contradictionthen
IFGT (
(w . (V cond_address)),
0,
(V cjump_address),
((IC w) + 1))
= V cjump_address
by XXREAL_0:def 11;
then w +* (NAT .--> loc) =
SCM-Chg (
w,
(IFGT ((w . (V cond_address)),0,(V cjump_address),((IC w) + 1))))
by A4, A12, SCM_INST:7
.=
SCM-Exec-Res (
V,
w)
by A12, AMI_2:def 14
.=
Exec (
(a >0_goto loc),
t)
by AMI_2:def 15
.=
t
by A11
;
hence
contradiction
by A6, A10;
verum end; end;