let R be Ring; for a being Data-Location of R
for il, i1 being Nat holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )
let a be Data-Location of R; for il, i1 being Nat holds
( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )
let il, i1 be Nat; ( i1 in NIC ((a =0_goto i1),il) & NIC ((a =0_goto i1),il) c= {i1,(il + 1)} )
set t = the State of (SCM R);
set Q = the Instruction-Sequence of (SCM R);
set I = a =0_goto i1;
reconsider a9 = a as Element of Data-Locations by SCMRING2:1;
A1:
il in NAT
by ORDINAL1:def 12;
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6, A1;
Values a =
((SCM-VAL R) * SCM-OK) . a9
by SCMRING2:24
.=
the carrier of R
by AMI_3:27, SCMRING1:4
;
then reconsider 0R = 0. R as Element of Values a ;
reconsider u = the State of (SCM R) +* ((IC ),il1) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
reconsider P = the Instruction-Sequence of (SCM R) +* (il,(a =0_goto i1)) as Instruction-Sequence of (SCM R) ;
reconsider v = u +* (a .--> 0R) as Element of product (the_Values_of (SCM R)) by CARD_3:107;
A2:
IC in dom the State of (SCM R)
by MEMSTR_0:2;
IC <> a
by Th2;
then
not IC in dom (a .--> 0R)
by TARSKI:def 1;
then A4: IC v =
IC u
by FUNCT_4:11
.=
il
by A2, FUNCT_7:31
;
A5:
P /. il = P . il
by PBOOLE:143, A1;
il in NAT
by ORDINAL1:def 12;
then
il in dom the Instruction-Sequence of (SCM R)
by PARTFUN1:def 2;
then A6:
P . il = a =0_goto i1
by FUNCT_7:31;
a in dom (a .--> 0R)
by TARSKI:def 1;
then v . a =
(a .--> 0R) . a
by FUNCT_4:13
.=
0. R
by FUNCOP_1:72
;
then
IC (Following (P,v)) = i1
by A4, A6, A5, SCMRING2:16;
hence
i1 in NIC ((a =0_goto i1),il)
by A4, A6, A5; NIC ((a =0_goto i1),il) c= {i1,(il + 1)}
let x be object ; TARSKI:def 3 ( not x in NIC ((a =0_goto i1),il) or x in {i1,(il + 1)} )
assume
x in NIC ((a =0_goto i1),il)
; x in {i1,(il + 1)}
then consider s being Element of product (the_Values_of (SCM R)) such that
A7:
( x = IC (Exec ((a =0_goto i1),s)) & IC s = il )
;