thus
(f,a) := b is parahalting
(f,a) := b is keeping_0 proof
set Ma =
Macro ((f,a) := b);
let s be
State of
SCM+FSA;
EXTPRO_1:def 10,
SCMFSA6B:def 3,
SCMFSA6C:def 1 ( not Initialize (Macro ((f,a) := b)) c= s or for b1 being set holds
( not ProgramPart (Initialize (Macro ((f,a) := b))) c= b1 or b1 halts_on s ) )
assume A67:
Initialize (Macro ((f,a) := b)) c= s
;
for b1 being set holds
( not ProgramPart (Initialize (Macro ((f,a) := b))) c= b1 or b1 halts_on s )
let P be the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
( not ProgramPart (Initialize (Macro ((f,a) := b))) c= P or P halts_on s )
assume A68:
ProgramPart (Initialize (Macro ((f,a) := b))) c= P
;
P halts_on s
A69:
Macro ((f,a) := b) c= P
by A68, COMPOS_1:144;
take
1
;
EXTPRO_1:def 7 ( IC (Comput (P,s,1)) in proj1 P & CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA )
A70:
dom P = NAT
by PARTFUN1:def 4;
thus
IC (Comput (P,s,1)) in dom P
by A70;
CurInstr (P,(Comput (P,s,1))) = halt SCM+FSA
dom (Start-At (0,SCM+FSA)) = {(IC )}
by FUNCOP_1:19;
then A71:
IC in dom (Start-At (0,SCM+FSA))
by TARSKI:def 1;
Start-At (
0,
SCM+FSA)
c= Initialize (Macro ((f,a) := b))
by FUNCT_4:26;
then
Start-At (
0,
SCM+FSA)
c= s
by A67, XBOOLE_1:1;
then A72:
IC s =
(Start-At (0,SCM+FSA)) . (IC )
by A71, GRFUNC_1:8
.=
0
by FUNCOP_1:87
;
then A73:
IC (Exec (((f,a) := b),s)) =
succ 0
by SCMFSA_2:99
.=
0 + 1
;
A74:
1
in dom (Macro ((f,a) := b))
by COMPOS_1:147;
A75:
0 in dom (Macro ((f,a) := b))
by COMPOS_1:147;
A76:
P . 0 =
(Macro ((f,a) := b)) . 0
by A69, A75, GRFUNC_1:8
.=
(
f,
a)
:= b
by COMPOS_1:148
;
A77:
P . 1 =
(Macro ((f,a) := b)) . 1
by A69, A74, GRFUNC_1:8
.=
halt SCM+FSA
by COMPOS_1:148
;
Comput (
P,
s,
(0 + 1)) =
Following (
P,
(Comput (P,s,0)))
by EXTPRO_1:4
.=
Following (
P,
s)
by EXTPRO_1:3
.=
Exec (
((f,a) := b),
s)
by A72, A70, PARTFUN1:def 8, A76
;
hence
CurInstr (
P,
(Comput (P,s,1)))
= halt SCM+FSA
by A73, A70, PARTFUN1:def 8, A77;
verum
end;
thus
(f,a) := b is keeping_0
verumproof
set Ma =
Macro ((f,a) := b);
let s be
State of
SCM+FSA;
SCMFSA6B:def 4,
SCMFSA6C:def 2 ( not Initialize (Macro ((f,a) := b)) c= s or for b1 being set holds
( not Macro ((f,a) := b) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) ) )
assume A78:
Initialize (Macro ((f,a) := b)) c= s
;
for b1 being set holds
( not Macro ((f,a) := b) c= b1 or for b2 being Element of NAT holds (Comput (b1,s,b2)) . (intloc 0) = s . (intloc 0) )
let P be the
Instructions of
SCM+FSA -valued ManySortedSet of
NAT ;
( not Macro ((f,a) := b) c= P or for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0) )
assume A79:
Macro ((f,a) := b) c= P
;
for b1 being Element of NAT holds (Comput (P,s,b1)) . (intloc 0) = s . (intloc 0)
let k be
Element of
NAT ;
(Comput (P,s,k)) . (intloc 0) = s . (intloc 0)
dom (Start-At (0,SCM+FSA)) = {(IC )}
by FUNCOP_1:19;
then A80:
IC in dom (Start-At (0,SCM+FSA))
by TARSKI:def 1;
Start-At (
0,
SCM+FSA)
c= Initialize (Macro ((f,a) := b))
by FUNCT_4:26;
then
Start-At (
0,
SCM+FSA)
c= s
by A78, XBOOLE_1:1;
then A81:
IC s =
(Start-At (0,SCM+FSA)) . (IC )
by A80, GRFUNC_1:8
.=
0
by FUNCOP_1:87
;
0 in dom (Macro ((f,a) := b))
by COMPOS_1:147;
then A82:
(Macro ((f,a) := b)) . 0 = P . 0
by A79, GRFUNC_1:8;
A83:
P /. (IC s) = P . (IC s)
by PBOOLE:158;
A84:
Comput (
P,
s,
(0 + 1)) =
Following (
P,
(Comput (P,s,0)))
by EXTPRO_1:4
.=
Following (
P,
s)
by EXTPRO_1:3
.=
Exec (
((f,a) := b),
s)
by A81, A82, A83, COMPOS_1:148
;
1
in dom (Macro ((f,a) := b))
by COMPOS_1:147;
then
(Macro ((f,a) := b)) . 1
= P . 1
by A79, GRFUNC_1:8;
then A85:
P . 1
= halt SCM+FSA
by COMPOS_1:148;
IC (Exec (((f,a) := b),s)) =
succ 0
by A81, SCMFSA_2:99
.=
0 + 1
;
then A86:
CurInstr (
P,
(Comput (P,s,1)))
= halt SCM+FSA
by A85, A84, PBOOLE:158;
end;