let il, i1 be Nat; for a being Int-Location holds NIC ((a >0_goto i1),il) = {i1,(il + 1)}
let a be Int-Location; NIC ((a >0_goto i1),il) = {i1,(il + 1)}
set t = the State of SCM+FSA;
set Q = the Instruction-Sequence of SCM+FSA;
let x be object ; TARSKI:def 3 ( not x in {i1,(il + 1)} or x in NIC ((a >0_goto i1),il) )
set I = a >0_goto i1;
A3:
IC <> a
by SCMFSA_2:56;
il in NAT
by ORDINAL1:def 12;
then reconsider il1 = il as Element of Values (IC ) by MEMSTR_0:def 6;
reconsider n = il as Nat ;
reconsider u = the State of SCM+FSA +* ((IC ),il1) as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
reconsider P = the Instruction-Sequence of SCM+FSA +* (il,(a >0_goto i1)) as Instruction-Sequence of SCM+FSA ;
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 v =
u +* (a .--> 1) as
Element of
product (the_Values_of SCM+FSA) by CARD_3:107;
A6:
IC in dom the
State of
SCM+FSA
by MEMSTR_0:2;
not
IC in dom (a .--> 1)
by A3, TARSKI:def 1;
then A8:
IC v =
IC u
by FUNCT_4:11
.=
n
by A6, FUNCT_7:31
;
il in NAT
by ORDINAL1:def 12;
then A9:
P /. il = P . il
by PBOOLE:143;
il in NAT
by ORDINAL1:def 12;
then
il in dom the
Instruction-Sequence of
SCM+FSA
by PARTFUN1:def 2;
then A10:
P . il = a >0_goto i1
by FUNCT_7:31;
a in dom (a .--> 1)
by TARSKI:def 1;
then v . a =
(a .--> 1) . a
by FUNCT_4:13
.=
1
by FUNCOP_1:72
;
then
IC (Following (P,v)) = i1
by A8, A10, A9, SCMFSA_2:71;
hence
x in NIC (
(a >0_goto i1),
il)
by A5, A8, A10, A9;
verum end; suppose A11:
x = il + 1
;
x in NIC ((a >0_goto i1),il)reconsider v =
u +* (a .--> 0) as
Element of
product (the_Values_of SCM+FSA) by CARD_3:107;
A12:
IC in dom the
State of
SCM+FSA
by MEMSTR_0:2;
not
IC in dom (a .--> 0)
by A3, TARSKI:def 1;
then A14:
IC v =
IC u
by FUNCT_4:11
.=
n
by A12, FUNCT_7:31
;
il in NAT
by ORDINAL1:def 12;
then A15:
P /. il = P . il
by PBOOLE:143;
il in NAT
by ORDINAL1:def 12;
then
il in dom the
Instruction-Sequence of
SCM+FSA
by PARTFUN1:def 2;
then A16:
P . il = a >0_goto i1
by FUNCT_7:31;
a in dom (a .--> 0)
by TARSKI:def 1;
then v . a =
(a .--> 0) . a
by FUNCT_4:13
.=
0
by FUNCOP_1:72
;
then
IC (Following (P,v)) = il + 1
by A14, A16, A15, SCMFSA_2:71;
hence
x in NIC (
(a >0_goto i1),
il)
by A11, A14, A16, A15;
verum end; end;