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);
reconsider I = a =0_goto i1 as Element of the Object-Kind of (SCM R) . il by COMPOS_1:def 8;
reconsider a9 = a as Element of Data-Locations SCM by SCMRING2:1;
A1: ObjectKind a =
(SCM-OK R) . a9
by SCMRING2:def 1
.=
the carrier of R
by AMI_3:72, SCMRING1:5
;
A2:
a <> il
by Th2;
reconsider il1 = il as Element of ObjectKind (IC ) by COMPOS_1:def 6;
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 p = ((IC ),il) --> (il1,I) as PartState of (SCM R) by COMPOS_1:37;
reconsider u = the State of (SCM R) +* p as State 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;
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 PBOOLE:155;
A6:
dom (((IC ),il) --> (il1,I)) = {(IC ),il}
by FUNCT_4:65;
then A7:
IC in dom (((IC ),il) --> (il1,I))
by TARSKI:def 2;
A8:
il in dom (((IC ),il) --> (il1,I))
by A6, TARSKI:def 2;
A9:
dom (a .--> 0R) = {a}
by FUNCOP_1:19;
then
not
IC in dom (a .--> 0R)
by A3, TARSKI:def 1;
then A10:
IC v =
u . (IC )
by FUNCT_4:12
.=
(((IC ),il) --> (il1,I)) . (IC )
by A7, FUNCT_4:14
.=
il
by COMPOS_1:3, FUNCT_4:66
;
A11:
not
il in dom (a .--> 0R)
by A2, A9, TARSKI:def 1;
A12:
(ProgramPart v) /. il =
v . il
by COMPOS_1:38
.=
u . il
by A11, FUNCT_4:12
.=
(((IC ),il) --> (il1,I)) . il
by A8, FUNCT_4:14
.=
I
by FUNCT_4:66
;
a in dom (a .--> 0R)
by A9, TARSKI:def 1;
then v . a =
(a .--> 0R) . a
by FUNCT_4:14
.=
0. R
by FUNCOP_1:87
;
then
IC (Following ((ProgramPart v),v)) = i1
by A10, A12, SCMRING2:18;
hence
x in NIC (
(a =0_goto i1),
il)
by A5, A10, A12;
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 19;
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 PBOOLE:155;
A15:
dom (((IC ),il) --> (il1,I)) = {(IC ),il}
by FUNCT_4:65;
then A16:
IC in dom (((IC ),il) --> (il1,I))
by TARSKI:def 2;
A17:
il in dom (((IC ),il) --> (il1,I))
by A15, TARSKI:def 2;
A18:
dom (a .--> E) = {a}
by FUNCOP_1:19;
then
not
IC in dom (a .--> E)
by A3, TARSKI:def 1;
then A19:
IC v =
u . (IC )
by FUNCT_4:12
.=
(((IC ),il) --> (il1,I)) . (IC )
by A16, FUNCT_4:14
.=
il
by COMPOS_1:3, FUNCT_4:66
;
A20:
not
il in dom (a .--> E)
by A2, A18, TARSKI:def 1;
A21:
(ProgramPart v) /. il =
v . il
by COMPOS_1:38
.=
u . il
by A20, FUNCT_4:12
.=
(((IC ),il) --> (il1,I)) . il
by A17, FUNCT_4:14
.=
I
by FUNCT_4:66
;
a in dom (a .--> E)
by A18, TARSKI:def 1;
then v . a =
(a .--> E) . a
by FUNCT_4:14
.=
E
by FUNCOP_1:87
;
then
IC (Following ((ProgramPart v),v)) = succ il
by A14, A19, A21, SCMRING2:18;
hence
x in NIC (
(a =0_goto i1),
il)
by A13, A19, A21;
verum end;