let R be Ring; for a being Data-Location of R
for i1 being Nat holds not a =0_goto i1 is halting
let a be Data-Location of R; for i1 being Nat holds not a =0_goto i1 is halting
let i1 be Nat; not a =0_goto i1 is halting
reconsider i5 = i1 as Element of NAT by ORDINAL1:def 12;
set s = the SCM-State of R;
set t = the SCM-State of R +* (NAT .--> (i1 + 1));
set f = the_Values_of (SCM R);
reconsider V = a =0_goto i1 as Element of SCM-Instr R by Def1;
A1:
{NAT} c= SCM-Memory
by AMI_2:22, ZFMISC_1:31;
A2: dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) =
(dom the SCM-State of R) \/ (dom (NAT .--> (i1 + 1)))
by FUNCT_4:def 1
.=
SCM-Memory \/ (dom (NAT .--> (i1 + 1)))
by SCMRING1:19
.=
SCM-Memory \/ {NAT}
.=
SCM-Memory
by A1, XBOOLE_1:12
;
A3:
the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK
by Lm1;
NAT in dom (NAT .--> (i1 + 1))
by TARSKI:def 1;
then A5: ( the SCM-State of R +* (NAT .--> (i1 + 1))) . NAT =
(NAT .--> (i1 + 1)) . NAT
by FUNCT_4:13
.=
i5 + 1
by FUNCOP_1:72
;
A6: dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) =
the carrier of (SCM R)
by A2, Def1
.=
dom (the_Values_of (SCM R))
by PARTFUN1:def 2
;
A7:
for x being object st x in dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) holds
( the SCM-State of R +* (NAT .--> (i1 + 1))) . x in (the_Values_of (SCM R)) . x
dom ( the SCM-State of R +* (NAT .--> (i1 + 1))) = the carrier of (SCM R)
by A2, Def1;
then reconsider t = the SCM-State of R +* (NAT .--> (i1 + 1)) as PartState of (SCM R) by A7, FUNCT_1:def 14, RELAT_1:def 18;
dom t = the carrier of (SCM R)
by A2, Def1;
then reconsider t = t as State of (SCM R) by PARTFUN1:def 2;
A10:
the_Values_of (SCM R) = (SCM-VAL R) * SCM-OK
by Lm1;
reconsider w = t as SCM-State of R by A10, CARD_3:107;
NAT in dom (NAT .--> i1)
by TARSKI:def 1;
then A11: (w +* (NAT .--> i1)) . NAT =
(NAT .--> i1) . NAT
by FUNCT_4:13
.=
i1
by FUNCOP_1:72
;
A12:
7 is Element of Segm 8
by NAT_1:44;
A13:
a is Element of Data-Locations
by Th1;
assume A14:
a =0_goto i1 is halting
; contradiction
A15:
i1 in NAT
by ORDINAL1:def 12;
per cases
( w . (V cond_address) <> 0. R or w . (V cond_address) = 0. R )
;
suppose A19:
w . (V cond_address) = 0. R
;
contradictionw +* (NAT .--> i1) =
SCM-Chg (
w,
i5)
.=
SCM-Chg (
w,
(V cjump_address))
by A12, A13, AMI_3:27, SCMRINGI:3
.=
SCM-Chg (
w,
(IFEQ ((w . (V cond_address)),(0. R),(V cjump_address),((IC w) + 1))))
by A19, FUNCOP_1:def 8
.=
SCM-Exec-Res (
V,
w)
by A13, AMI_3:27, SCMRING1:def 14, A15
.=
Exec (
(a =0_goto i1),
t)
by Th10
.=
t
by A14
;
hence
contradiction
by A5, A11;
verum end; end;