thus
(f,a) := b is keeping_0
verumproof
set Ma =
Macro ((f,a) := b);
let s be
0 -started State of
SCM+FSA;
SCMFSA6B:def 4,
SCMFSA6C:def 1 for b1 being set holds
( not Macro ((f,a) := b) c= b1 or for b2 being set holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
A1:
Start-At (
0,
SCM+FSA)
c= s
by MEMSTR_0:29;
let P be
Instruction-Sequence of
SCM+FSA;
( not Macro ((f,a) := b) c= P or for b1 being set holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A2:
Macro ((f,a) := b) c= P
;
for b1 being set holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be
Nat;
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
A3:
IC in dom (Start-At (0,SCM+FSA))
by TARSKI:def 1;
A4:
IC s =
(Start-At (0,SCM+FSA)) . (IC )
by A3, A1, GRFUNC_1:2
.=
0
by FUNCOP_1:72
;
0 in dom (Macro ((f,a) := b))
by COMPOS_1:60;
then A5:
(Macro ((f,a) := b)) . 0 = P . 0
by A2, GRFUNC_1:2;
A6:
P /. (IC s) = P . (IC s)
by PBOOLE:143;
A7:
Comput (
P,
s,
(0 + 1)) =
Following (
P,
(Comput (P,s,0)))
by EXTPRO_1:3
.=
Exec (
((f,a) := b),
s)
by A4, A5, A6, COMPOS_1:58
;
1
in dom (Macro ((f,a) := b))
by COMPOS_1:60;
then
(Macro ((f,a) := b)) . 1
= P . 1
by A2, GRFUNC_1:2;
then A8:
P . 1
= halt SCM+FSA
by COMPOS_1:59;
IC (Exec (((f,a) := b),s)) = 0 + 1
by A4, SCMFSA_2:73;
then A9:
CurInstr (
P,
(Comput (P,s,1)))
= halt SCM+FSA
by A8, A7, PBOOLE:143;
end;