let s be State of SCM+FSA; for P being Instruction-Sequence of SCM+FSA
for i being sequential Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
let P be Instruction-Sequence of SCM+FSA; for i being sequential Instruction of SCM+FSA holds Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
let i be sequential Instruction of SCM+FSA; Exec (i,(Initialized s)) = IExec ((Macro i),P,s)
set Mi = Macro i;
set sI = s +* (Initialize ((intloc 0) .--> 1));
set pI = P +* (Macro i);
A1:
Macro i c= P +* (Macro i)
by FUNCT_4:25;
set Is = Initialized s;
set IC1 = IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1));
reconsider Mi = Macro i as parahalting Program of SCM+FSA ;
IC (s +* (Initialize ((intloc 0) .--> 1))) = 0
by MEMSTR_0:def 11;
then
IC (s +* (Initialize ((intloc 0) .--> 1))) in dom Mi
by AFINSQ_1:65;
then A2:
IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) in dom Mi
by A1, AMISTD_1:21;
A3:
1 in dom Mi
by COMPOS_1:60;
A4:
0 in dom Mi
by COMPOS_1:60;
A5:
Mi . 0 = i
by COMPOS_1:58;
A6:
IC (s +* (Initialize ((intloc 0) .--> 1))) = 0
by MEMSTR_0:def 11;
A7: Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),(0 + 1)) =
Following ((P +* Mi),(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0)))
by EXTPRO_1:3
.=
Exec (((P +* (Macro i)) . 0),(s +* (Initialize ((intloc 0) .--> 1))))
by A6, PBOOLE:143
.=
Exec (i,(s +* (Initialize ((intloc 0) .--> 1))))
by A5, A1, A4, GRFUNC_1:2
;
per cases
( IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 0 or IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 1 )
by A2, COMPOS_1:60;
suppose A8:
IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 0
;
Exec (i,(Initialized s)) = IExec ((Macro i),P,s)then A9:
CurInstr (
(P +* Mi),
(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) =
(P +* Mi) . 0
by PBOOLE:143
.=
i
by A5, A4, FUNCT_4:13
;
IC (s +* (Initialize ((intloc 0) .--> 1))) = 0
by A6;
then A10:
InsCode i in {0,6,7,8}
by A7, A8, SCMFSA6A:3;
hereby verum
per cases
( InsCode i = 0 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 )
by A10, ENUMSET1:def 2;
suppose A12:
(
InsCode i = 6 or
InsCode i = 7 or
InsCode i = 8 )
;
Exec (i,(Initialized s)) = IExec ((Macro i),P,s)A15:
Following (
(P +* Mi),
(s +* (Initialize ((intloc 0) .--> 1)))) =
Following (
(P +* Mi),
(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),0)))
.=
Exec (
i,
(s +* (Initialize ((intloc 0) .--> 1))))
by A7, EXTPRO_1:3
;
A16:
InsCode (halt SCM+FSA) = 0
by COMPOS_1:70;
for
n being
Nat holds
CurInstr (
(P +* Mi),
(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),n)))
<> halt SCM+FSA
by A9, A12, A13, A14, A7, A8, A6, A15, A16, AMISTD_2:11, SCMFSA_2:104;
then A17:
not
P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1))
;
Mi c= P +* Mi
by FUNCT_4:25;
hence
Exec (
i,
(Initialized s))
= IExec (
(Macro i),
P,
s)
by A17, AMISTD_1:def 11;
verum end; end;
end; end; suppose A18:
IC (Comput ((P +* (Macro i)),(s +* (Initialize ((intloc 0) .--> 1))),1)) = 1
;
Exec (i,(Initialized s)) = IExec ((Macro i),P,s)A19:
Mi . 1
= halt SCM+FSA
by COMPOS_1:59;
A20:
CurInstr (
(P +* Mi),
(Comput ((P +* Mi),(s +* (Initialize ((intloc 0) .--> 1))),1))) =
(P +* Mi) . 1
by A18, PBOOLE:143
.=
halt SCM+FSA
by A19, A1, A3, GRFUNC_1:2
;
then
P +* Mi halts_on s +* (Initialize ((intloc 0) .--> 1))
by EXTPRO_1:29;
hence
Exec (
i,
(Initialized s))
= IExec (
(Macro i),
P,
s)
by A7, A20, EXTPRO_1:def 9;
verum end; end;