let R be non trivial Ring; for a being Data-Location of R
for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}
let a be Data-Location of R; for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(il + 1)}
let il, i1 be Element of NAT ; NIC ((a =0_goto i1),il) = {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: Values a =
((SCM-VAL R) * SCM-OK) . a9
by SCMRING2:24
.=
the carrier of R
by AMI_3:27, SCMRING1:4
;
reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6;
thus
NIC ((a =0_goto i1),il) c= {i1,(il + 1)}
by Th31; XBOOLE_0:def 10 {i1,(il + 1)} c= NIC ((a =0_goto i1),il)
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) ;
let x be object ; TARSKI:def 3 ( not x in {i1,(il + 1)} or x in NIC ((a =0_goto i1),il) )
A2:
IC <> a
by Th2;
A3:
IC in dom the State of (SCM R)
by MEMSTR_0:2;
assume A4:
x in {i1,(il + 1)}
; x in NIC ((a =0_goto i1),il)
per cases
( x = i1 or x = il + 1 )
by A4, TARSKI:def 2;
suppose A5:
x = i1
;
x in NIC ((a =0_goto i1),il)reconsider 0R =
0. R as
Element of
Values a by A1;
reconsider v =
u +* (a .--> 0R) as
Element of
product (the_Values_of (SCM R)) by CARD_3:107;
not
IC in dom (a .--> 0R)
by A2, TARSKI:def 1;
then A7:
IC v =
IC u
by FUNCT_4:11
.=
il
by A3, FUNCT_7:31
;
A8:
P /. il = P . il
by PBOOLE:143;
il in NAT
;
then
il in dom the
Instruction-Sequence of
(SCM R)
by PARTFUN1:def 2;
then A9:
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 A7, A8, A9, SCMRING2:16;
hence
x in NIC (
(a =0_goto i1),
il)
by A5, A7, A8, A9;
verum end; suppose A10:
x = il + 1
;
x in NIC ((a =0_goto i1),il)consider e being
Element of
R such that A11:
e <> 0. R
by STRUCT_0:def 18;
reconsider E =
e as
Element of
Values a by A1;
reconsider v =
u +* (a .--> E) as
Element of
product (the_Values_of (SCM R)) by CARD_3:107;
not
IC in dom (a .--> E)
by A2, TARSKI:def 1;
then A13:
IC v =
IC u
by FUNCT_4:11
.=
il
by A3, FUNCT_7:31
;
A14:
P /. il = P . il
by PBOOLE:143;
il in NAT
;
then
il in dom the
Instruction-Sequence of
(SCM R)
by PARTFUN1:def 2;
then A15:
P . il = a =0_goto i1
by FUNCT_7:31;
a in dom (a .--> E)
by TARSKI:def 1;
then v . a =
(a .--> E) . a
by FUNCT_4:13
.=
E
by FUNCOP_1:72
;
then
IC (Following (P,v)) = il + 1
by A11, A13, A14, A15, SCMRING2:16;
hence
x in NIC (
(a =0_goto i1),
il)
by A10, A13, A14, A15;
verum end;