let R be non trivial good Ring; for a being Data-Location of R
for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
let a be Data-Location of R; for il, i1 being Element of NAT holds NIC ((a =0_goto i1),il) = {i1,(succ il)}
let il, i1 be Element of NAT ; NIC ((a =0_goto i1),il) = {i1,(succ il)}
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: ObjectKind a =
(SCM-OK R) . a9
by SCMRING2:def 1
.=
the carrier of R
by AMI_3:27, SCMRING1:4
;
reconsider il1 = il as Element of ObjectKind (IC ) by MEMSTR_0:def 3;
thus
NIC ((a =0_goto i1),il) c= {i1,(succ il)}
by Th61; XBOOLE_0:def 10 {i1,(succ il)} c= NIC ((a =0_goto i1),il)
reconsider u = the State of (SCM R) +* ((IC ),il1) as Element of product the Object-Kind 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 set ; TARSKI:def 3 ( not x in {i1,(succ il)} or x in NIC ((a =0_goto i1),il) )
A3:
IC <> a
by Th3;
xx:
IC in dom the State of (SCM R)
by MEMSTR_0:2;
assume A4:
x in {i1,(succ il)}
; x in NIC ((a =0_goto i1),il)
per cases
( x = i1 or x = succ il )
by A4, TARSKI:def 2;
suppose A5:
x = i1
;
x in NIC ((a =0_goto i1),il)reconsider 0R =
0. R as
Element of
ObjectKind a by A1;
reconsider v =
u +* (a .--> 0R) as
Element of
product the
Object-Kind of
(SCM R) by CARD_3:107;
A9:
dom (a .--> 0R) = {a}
by FUNCOP_1:13;
then
not
IC in dom (a .--> 0R)
by A3, TARSKI:def 1;
then A10:
IC v =
IC u
by FUNCT_4:11
.=
il
by xx, FUNCT_7:31
;
A12:
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 B12:
P . il = a =0_goto i1
by FUNCT_7:31;
a in dom (a .--> 0R)
by A9, 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 A10, A12, B12, SCMRING2:16;
hence
x in NIC (
(a =0_goto i1),
il)
by A5, A10, A12, B12;
verum end; suppose A13:
x = succ il
;
x in NIC ((a =0_goto i1),il)consider e being
Element of
R such that A14:
e <> 0. R
by STRUCT_0:def 18;
reconsider E =
e as
Element of
ObjectKind a by A1;
reconsider v =
u +* (a .--> E) as
Element of
product the
Object-Kind of
(SCM R) by CARD_3:107;
A18:
dom (a .--> E) = {a}
by FUNCOP_1:13;
then
not
IC in dom (a .--> E)
by A3, TARSKI:def 1;
then A19:
IC v =
IC u
by FUNCT_4:11
.=
il
by xx, FUNCT_7:31
;
A21:
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 B21:
P . il = a =0_goto i1
by FUNCT_7:31;
a in dom (a .--> E)
by A18, TARSKI:def 1;
then v . a =
(a .--> E) . a
by FUNCT_4:13
.=
E
by FUNCOP_1:72
;
then
IC (Following (P,v)) = succ il
by A14, A19, A21, B21, SCMRING2:16;
hence
x in NIC (
(a =0_goto i1),
il)
by A13, A19, A21, B21;
verum end;